1 files changed, 31 insertions, 15 deletions

diff --git a/test/mono/set.sail b/test/mono/set.sail
index ecc06137..b7cf4862 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -1,29 +1,45 @@
 default Order dec
-
-(* A function which is merely parametrised by a size does not need to be
-   monomorphised *)
-
-val forall 'n, 'n in {32,64}. [:'n:] -> bit[64] effect pure parametric
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+overload operator == = {eq_int, eq_vec}
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extz(v) = extz_vec(sizeof('m),v)
+val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val exts : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function exts(v) = exts_vec(sizeof('m),v)
+
+/* A function which is merely parametrised by a size does not need to be
+   monomorphised */
+
+val parametric : forall 'n, 'n in {32,64}. atom('n) -> bits(64)
 
 function parametric(n) = {
-  let (bit['n]) x = exts(0x80000000) in
+  let x : bits('n) = exts(0x80000000) in
   extz(x)
 }
 
-(* But if we do a calculation on the size then we'll need to case split *)
+/* But if we do a calculation on the size then we'll need to case split */
 
-val forall 'n, 'n in {16,32}. [:'n:] -> bit[64] effect pure depends
+val depends : forall 'n, 'n in {16,32}. atom('n) -> bits(64)
 
 function depends(n) = {
   let 'm = 2 * n in
-  let (bit['m]) x = exts(0x80000000) in
+  let x : bits('m) = exts(0x80000000) in
   extz(x)
 }
 
-val unit -> bool effect pure run
+val run : unit -> unit effect {escape}
 
-function run () =
-  parametric(32) == 0x0000000080000000 &
-  parametric(64) == 0xffffffff80000000 &
-  depends(16) == 0x0000000080000000 &
-  depends(32) == 0xffffffff80000000
+function run () = {
+  assert(parametric(32) == 0x0000000080000000);
+  assert(parametric(64) == 0xffffffff80000000);
+  assert(depends(16) == 0x0000000080000000);
+  assert(depends(32) == 0xffffffff80000000);
+}