summaryrefslogtreecommitdiff
path: root/src/test/test3.sail
diff options
context:
space:
mode:
Diffstat (limited to 'src/test/test3.sail')
-rw-r--r--src/test/test3.sail16
1 files changed, 16 insertions, 0 deletions
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;
+}