diff options
| author | Kathy Gray | 2014-03-20 17:43:22 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-03-20 17:45:57 +0000 |
| commit | 147a734518bbebe34845e1b93fb1042e9915980f (patch) | |
| tree | 93adb7025961dca0b1eab57dfddf3d18be8c8c45 /src/test | |
| parent | 7ffcf38ab6a26f2bd00d94b99ae8b062c6e37f9c (diff) | |
small test changes
Diffstat (limited to 'src/test')
| -rw-r--r-- | src/test/test3.sail | 19 | ||||
| -rw-r--r-- | src/test/vectors.sail | 3 |
2 files changed, 12 insertions, 10 deletions
diff --git a/src/test/test3.sail b/src/test/test3.sail index 778d323a..ac0c1674 100644 --- a/src/test/test3.sail +++ b/src/test/test3.sail @@ -1,7 +1,5 @@ (* a register containing nat numbers *) register nat dummy_reg -(* and one containing a byte *) -register (bit[8]) dummy_reg2 (* a function to read from memory; wmem serves no purpose currently, memory-writing functions are figured out syntactically. *) val extern nat -> nat effect { wmem , rmem } MEM @@ -9,7 +7,7 @@ val extern nat -> nat effect { wmem , rmem } MEM_GPU val extern ( nat * nat ) -> (bit[8]) effect { wmem , rmem } MEM_SIZE val extern nat -> (bit[8]) effect { wmem , rmem } MEM_WORD -(* XXX types are wrong *) +(*(* XXX types are wrong *) val extern forall Type 'a . 'a -> nat effect pure to_num_inc = "to_num_inc" val extern forall Type 'a . 'a -> nat effect pure to_num_dec = "to_num_dec" val extern forall Type 'a . nat -> 'a effect pure to_vec_inc = "to_vec_inc" @@ -21,9 +19,15 @@ function unit ignore(x) = () val extern ( nat * nat ) -> nat effect pure add = "add" val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add" (* infix plus *) +function nat (deinfix * ) ( (nat) x, (nat) y ) = 42*) + +function unit ignore(x) = () function nat (deinfix * ) ( (nat) x, (nat) y ) = 42 +function forall Type 'a . 'a ident x = x + function nat main _ = { + ignore(0b1+ident(0b0)); (* left-hand side function call = memory write *) MEM(0) := 0; (* memory read, thanks to effect { rmem} above *) @@ -56,11 +60,6 @@ function nat main _ = { ignore(MEM_SIZE(0,2)); (* extern calls *) - dummy_reg := 3 + 39; - dummy_reg := add(5, 37); - (* casts and external calls *) - dummy_reg := 0b01 + 0b01; - dummy_reg2 := dummy_reg; (* cast from nat to bit[8] *) - dummy_reg2 := dummy_reg2 + dummy_reg2; (* cast to nat for add call *) - dummy_reg2; (* cast again and return 4 *) + ignore(3 + 39); + (deinfix +)(5, 37); } diff --git a/src/test/vectors.sail b/src/test/vectors.sail index 94132d25..f1af224b 100644 --- a/src/test/vectors.sail +++ b/src/test/vectors.sail @@ -10,6 +10,7 @@ register nat result function forall Type 'a . 'a id ( x ) = x register nat match_success +register nat add_check let (vector<0,3,inc,(register<(bit[10])>)>) gpr_small = [slice_check,slice_check,slice_check] @@ -31,6 +32,8 @@ function bit main _ = { (* id function call - prevents the correct cast currently *) result := gpr_small[1] + id(gpr_small[1]); + add_check := gpr_small[2] + 3; + i := [bitzero, bitzero, bitone, bitzero]; (* literal match *) |