blob: 36952bf7ea4b0c607dd5120e64c2f317bf84f8ec (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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;
}
|
