diff options
| author | Alasdair Armstrong | 2018-07-30 19:16:34 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-08-01 16:42:33 +0100 |
| commit | 1479ae359fd3afebf9c3dfb6e58a77254e8140ea (patch) | |
| tree | ffcfd96409467a5c41009f68afe1f65a2c7a3d49 /src/test/test3.sail | |
| parent | 0b70a9d7464d6c30534d2f511cb8c9879c76b1e5 (diff) | |
Remove old test directory in src/test
Diffstat (limited to 'src/test/test3.sail')
| -rw-r--r-- | src/test/test3.sail | 57 |
1 files changed, 0 insertions, 57 deletions
diff --git a/src/test/test3.sail b/src/test/test3.sail deleted file mode 100644 index 5e9ba2df..00000000 --- a/src/test/test3.sail +++ /dev/null @@ -1,57 +0,0 @@ -(* a register containing nat numbers *) -register [|0:256|] 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) -> unit effect { wmem } MEMw -val extern nat -> nat effect { rmem } MEMr -val extern (nat,nat) -> unit effect { wmem } MEM_GPUw -val extern nat -> nat effect { rmem} MEM_GPUr -val extern forall Nat 'n . ( nat, [|'n|], bit['n*8]) -> unit effect { wmem } MEM_SIZEw -val extern forall Nat 'n . ( nat, [|'n|]) -> bit['n*8] effect { rmem } MEM_SIZEr -val extern (nat,bit[8]) -> unit effect { wmem } MEM_WORDw -val extern nat -> bit[8] effect { rmem } MEM_WORDr - -function nat (deinfix * ) ( (nat) x, (nat) y ) = 42 - -function nat main _ = { - (* left-hand side function call = memory write *) - MEMw(0) := 0; - ignore(MEMr(0)); - (* register write, idem *) - dummy_reg := 1; - (* register read, thanks to register declaration *) - ignore(dummy_reg); - - - MEM_WORDw(0) := 0b10101010; - (MEM_WORDw(0))[3..4] := 0b10; - (* XXX this one is broken - I don't what it should do, - or even if we should accept it, but the current result - is to eat up one bit, ending up with a 7-bit word. *) - (*(MEM_WORD(0))[4..3] := 0b10;*) (*We reject this as 4 > 3 not <= *) - ignore(MEM_WORDr(0)); - - (* infix call *) - ignore(7 * 9); - - (* Some more checks *) - MEMw(1) := 2; - ignore(MEMr(1)); - MEM_GPUw(0) := 3; - ignore(MEM_GPUr(0)); - MEM_SIZEw(0,1) := 0b11110000; - ignore(MEM_SIZEr(0,1)); - MEM_SIZEw(0,2) := 0b1111000010100000; - ignore(MEM_SIZEr(0,2)); - - (* extern calls *) - dummy_reg := 3 + 39; - (*dummy_reg := (deinfix +)(5, 37);*) - (* casts and external calls *) - dummy_reg := 0b01 + 0b01; - dummy_reg2 := 0b00000001; - dummy_reg2 := dummy_reg2 + dummy_reg2; (* cast to nat for add call *) - dummy_reg2; (* cast again and return 4 *) -} |
