Test read/write reg/mem syntax

2 files changed, 17 insertions, 0 deletions

diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index 58ea2b17..f1956b1e 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -1,6 +1,7 @@
 let tests = [
   "test1", Test1.defs;
   "test2", Test2.defs;
+  "test3", Test3.defs;
 ] ;;
 
 let run_all () = List.iter Run_interp.run tests ;;
diff --git a/src/test/test3.sail b/src/test/test3.sail
new file mode 100644
index 00000000..36952bf7
--- /dev/null
+++ b/src/test/test3.sail
@@ -0,0 +1,16 @@
+(* a register containing nat numbers *)
+register nat reg
+(* a function to read from memory; wmem serves no purpose currently,
+   memory-writing functions are figured out syntactically. *)
+val ( nat -> nat effect { wmem , rmem } ) MEM
+
+function nat main _ = {
+  (* memory read, thanks to effect { rmem} above *)
+  MEM(0);
+  (* left-hand side function call = memory write *)
+  MEM(0) := 1;
+  (* register read, thanks to register declaration *)
+  reg;
+  (* register write, idem *)
+  reg := 1;
+}