src/test/test3.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

(* a register containing nat numbers *)
register nat dummy_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
val ( nat -> nat effect { wmem , rmem } ) MEM_GPU
val ( ( nat * nat ) -> nat effect { wmem , rmem } ) MEM_SIZE

(* extern functions *)
val extern ( ( nat * nat ) -> nat pure ) add = "add"
val extern ( ( nat * nat ) -> nat pure ) (: + ) = "add_infix"   (* infix plus *)

function nat (: * ) ( < 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 *)
  MEM(0);
  (* register write, idem *)
  dummy_reg := 1;
  (* register read, thanks to register declaration *)
  dummy_reg;

  (* infix call *)
  7 * 9;

  (* Some more checks *)
  MEM(1) := 2;
  MEM(1);
  MEM_GPU(0) := 3;
  MEM_GPU(0);
  MEM_SIZE(0,1) := 4;
  MEM_SIZE(0,1);

  (* extern calls *)
  3 + 39;
  add(5, 37);
}