Support separated memory read/write functions.

Also allows register writing functions to be on the left hand side of an assignment in the same way.
The last parameter to a writing function is the value to be written, and should appear on the right hand side of an assignment expression.

1 files changed, 21 insertions, 18 deletions

diff --git a/src/test/test3.sail b/src/test/test3.sail
index e2dbe2f3..98ebb2d6 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -4,44 +4,47 @@ register [|0:256|] dummy_reg
 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
-val extern nat -> nat effect { wmem , rmem }  MEM_GPU
-val extern forall Nat 'n . ( nat, [|'n|] ) -> (bit['n * 8]) effect { wmem , rmem }  MEM_SIZE
-val extern nat -> (bit[8]) effect { wmem , rmem }  MEM_WORD
+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 *)
-  MEM(0) := 0;
-  (* memory read, thanks to effect { rmem} above *)
-  ignore(MEM(0));
+  MEMw(0) := 0;
+  ignore(MEMr(0));
   (* register write, idem *)
   dummy_reg := 1;
   (* register read, thanks to register declaration *)
   ignore(dummy_reg);
 
 
-  MEM_WORD(0) := 0b10101010;
-  (MEM_WORD(0))[3..4] := 0b10;
+  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_WORD(0));
+  ignore(MEM_WORDr(0));
 
   (* infix call *)
   ignore(7 * 9);
 
   (* Some more checks *)
-  MEM(1) := 2;
-  ignore(MEM(1));
-  MEM_GPU(0) := 3;
-  ignore(MEM_GPU(0));
-  MEM_SIZE(0,1) := 0b11110000;
-  ignore(MEM_SIZE(0,1));
-  MEM_SIZE(0,2) := 0b1111000010100000;
-  ignore(MEM_SIZE(0,2));
+  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;