8 files changed, 322 insertions, 166 deletions

diff --git a/test/ocaml/hello_world/hello_world.sail b/test/ocaml/hello_world/hello_world.sail
index d96429f2..bafea2de 100644
--- a/test/ocaml/hello_world/hello_world.sail
+++ b/test/ocaml/hello_world/hello_world.sail
@@ -1,19 +1,18 @@
-
-val unit -> string effect pure hello_world
+val hello_world : unit -> string
 
 function hello_world () = {
-  return "Hello, World!";
+  return("Hello, World!");
   "Unreachable"
 }
 
-val unit -> unit effect {wreg, rreg} main
+val main : unit -> unit effect {wreg, rreg}
 
-register string REG
+register REG : string
 
 function main () = {
-  REG := "Hello, Sail!";
+  REG = "Hello, Sail!";
   print(REG);
-  REG := hello_world ();
+  REG = hello_world();
   print(REG);
-  return ()
+  return(())
 }
diff --git a/test/ocaml/loop/loop.sail b/test/ocaml/loop/loop.sail
index 5ab0e817..3808c19a 100644
--- a/test/ocaml/loop/loop.sail
+++ b/test/ocaml/loop/loop.sail
@@ -1,18 +1,19 @@
+val string_of_int = "string_of_big_int" : int -> string
 
-val extern int -> string effect pure string_of_int = "string_of_big_int"
+val add = "add" : (int, int) -> int
 
-val extern (int, int) -> int effect pure add = "add"
-val extern (int, int) -> bool effect pure lt = "lt_int"
+val lt = "lt_int" : (int, int) -> bool
 
-overload (deinfix +) [add]
-overload (deinfix <) [lt]
+overload operator + = {add}
 
-val unit -> unit effect pure main
+overload operator < = {lt}
+
+val main : unit -> unit
 
 function main () = {
-  (int) x := 0;
+  x : int = 0;
   while x < 100 do {
-    x := x + 1;
+    x = x + 1;
     print(string_of_int(x))
   }
 }
diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail
index fdb9dc43..8c3e9700 100644
--- a/test/ocaml/lsl/lsl.sail
+++ b/test/ocaml/lsl/lsl.sail
@@ -1,31 +1,28 @@
+val zeros : forall ('n : Int), 'n >= 0. atom('n) -> bits('n)
 
-val forall Num 'n, 'n >= 0. [:'n:] -> bit['n] effect pure zeros
+function zeros n = replicate_bits(0b0, 'n)
 
-function zeros n = replicate_bits(0b0, sizeof 'n)
-
-val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> (bit['n], bit) effect pure lslc
+val lslc : forall ('n : Int) ('shift : Int), 'n >= 0.
+  (bits('n), atom('shift)) -> (bits('n), bit) effect {escape}
 
 function lslc (vec, shift) = {
   assert(constraint('shift >= 1), "shift must be positive");
-  (bit['shift + 'n]) extended := vec : zeros(shift);
-  (bit['n]) result := extended[sizeof 'n - 1 .. 0];
-  (bit) c := extended[sizeof 'n];
-  return (result, c)
+  extended : bits('shift + 'n) = vec @ zeros(shift);
+  result : bits('n) = extended[sizeof('n - 1) .. 0];
+  c : bit = extended['n];
+  return((result, c))
 }
 
-val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> bit['n] effect pure lsl
+val lsl : forall ('n : Int) ('shift : Int), 'n >= 0.
+  (bits('n), atom('shift)) -> bits('n) effect {escape}
 
-function lsl (vec, shift) =
-  if shift == 0
-  then vec
-  else let (result, _) = lslc(vec, shift) in result
+function lsl (vec, shift) = if shift == 0 then vec else let (result, _) = lslc(vec, shift) in result
 
-val unit -> unit effect pure main
+val main : unit -> unit effect {escape}
 
 function main () = {
-  print(if lsl(0b0110,1) == 0b1100 then "pass" else "fail");
-  print(if lsl(0b1111,2) == 0b1100 then "pass" else "fail");
-  print(if lsl(0x0F,4) == 0xF0 then "pass" else "fail");
-  let (result, c) = lslc(0xF000,2) in
-  print(if result == 0xC000 & c == bitone then "pass" else "fail")
+  print(if lsl(0b0110, 1) == 0b1100 then "pass" else "fail");
+  print(if lsl(0b1111, 2) == 0b1100 then "pass" else "fail");
+  print(if lsl(0x0F, 4) == 0xF0 then "pass" else "fail");
+  let (result, c) = lslc(0xF000, 2) in print(if (result == 0xC000) & (c == bitone) then "pass" else "fail")
 }
diff --git a/test/ocaml/pattern1/pattern.sail b/test/ocaml/pattern1/pattern.sail
index a2314adc..3c28d46e 100644
--- a/test/ocaml/pattern1/pattern.sail
+++ b/test/ocaml/pattern1/pattern.sail
@@ -1,11 +1,9 @@
-
-val unit -> unit effect pure main
+val main : unit -> unit
 
 function main () = {
-  vec := 0x4F;
-  switch vec {
-    case (0b01 : (bit[2]) x : 0xF) ->
-      if (x == 0b00) then print("pass") else print("x is incorrect")
-    case _ -> print("pattern fail")
+  vec = 0x4F;
+  match vec {
+    0b01 @ x : bits(2) @ 0xF => if x == 0b00 then print("pass") else print("x is incorrect"),
+    _ => print("pattern fail")
   }
 }
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
index cbe1927d..cf9bb2f6 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -1,142 +1,286 @@
-
 default Order dec
 
-val extern (int, int) -> bool effect pure eq_int = "eq_int"
-val extern forall 'n. (bit['n], bit['n]) -> bool effect pure eq_vec = "eq_list"
-val extern (string, string) -> bool effect pure eq_string = "eq_string"
-val (real, real) -> bool effect pure eq_real
+type bits ('n : Int) = vector('n - 1, 'n, dec, bit)
+
+infix 4 ==
+
+val eq_atom = "eq_int" : (atom('n), atom('m)) -> bool
+val lteq_atom = "lteq" : (atom('n), atom('m)) -> bool
+val gteq_atom = "gteq" : (atom('n), atom('m)) -> bool
+val lt_atom = "lt" : (atom('n), atom('m)) -> bool
+val gt_atom = "gt" : (atom('n), atom('m)) -> bool
+
+val eq_int = "eq_int" : (int, int) -> bool
+
+val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool
+
+val eq_string = "eq_string" : (string, string) -> bool
+
+val eq_real = "eq_real" : (real, real) -> bool
+
+val eq_anything = "(fun (x, y) -> x = y)" : forall ('a : Type). ('a, 'a) -> bool
+
+val length = "length" : forall 'n ('a : Type). vector('n - 1, 'n, dec, 'a) -> atom('n)
+
+overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything}
+
+val vector_subrange_A = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+
+val vector_subrange_B = "subrange" : forall ('n : Int) ('m : Int) ('o : Int).
+  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+
+overload vector_subrange = {vector_subrange_A, vector_subrange_B}
+
+val vector_access_A = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
+  (vector('n - 1, 'n, dec, 'a), atom('m)) -> 'a
+
+val vector_access_B = "access" : forall ('n : Int) ('a : Type).
+  (vector('n - 1, 'n, dec, 'a), int) -> 'a
+
+overload vector_access = {vector_access_A, vector_access_B}
+
+val vector_update = "update" : forall 'n ('a : Type).
+  (vector('n - 1, 'n, dec, 'a), int, 'a) -> vector('n - 1, 'n, dec, 'a)
+
+val vector_update_subrange = "update_subrange" : forall 'n 'm 'o.
+  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+val vcons : forall ('n : Int) ('a : Type).
+  ('a, vector('n - 1, 'n, dec, 'a)) -> vector('n, 'n + 1, dec, 'a)
+
+val append = "append" : forall ('n : Int) ('m : Int) ('a : Type).
+  (vector('n - 1, 'n, dec, 'a), vector('m - 1, 'm, dec, 'a)) -> vector('n + 'm - 1, 'n + 'm, dec, 'a)
+
+val not_bool = "not" : bool -> bool
+
+val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
+
+overload ~ = {not_bool, not_vec}
+
+val neq_atom : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+function neq_atom (x, y) = not_bool(eq_atom(x, y))
+
+val neq_int : (int, int) -> bool
+
+function neq_int (x, y) = not_bool(eq_int(x, y))
+
+val neq_vec : forall 'n. (bits('n), bits('n)) -> bool
+
+function neq_vec (x, y) = not_bool(eq_vec(x, y))
+
+val neq_anything : forall ('a : Type). ('a, 'a) -> bool
+
+function neq_anything (x, y) = not_bool(x == y)
+
+overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
+
+val and_bool = "and_bool" : (bool, bool) -> bool
+
+val builtin_and_vec = "and_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+function and_vec (xs, ys) = builtin_and_vec(xs, ys)
+
+overload operator & = {and_bool, and_vec}
+
+val or_bool = "or_bool" : (bool, bool) -> bool
+
+val builtin_or_vec = "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+function or_vec (xs, ys) = builtin_or_vec(xs, ys)
+
+overload operator | = {or_bool, or_vec}
+
+val UInt = "uint" : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+
+val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+
+val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
+
+val __SetSlice_bits = "set_slice" : forall 'n 'm.
+  (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
+
+val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
+
+val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int
+
+val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
+
+val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n)
+
+function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
+
+val __raw_SetSlice_bits : forall 'n 'w.
+  (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n)
+
+val __raw_GetSlice_bits : forall 'n 'w.
+  (atom('n), atom('w), bits('n), int) -> bits('w)
+
+val __ShiftLeft : forall 'm. (bits('m), int) -> bits('m)
+
+val __SignExtendSlice : forall 'm. (bits('m), int, int) -> bits('m)
+
+val __ZeroExtendSlice : forall 'm. (bits('m), int, int) -> bits('m)
+
+val cast cast_unit_vec : bit -> bits(1)
+
+val print = "print_endline" : string -> unit
+
+val putchar = "putchar" : forall ('a : Type). 'a -> unit
+
+val concat_str = "concat_str" : (string, string) -> string
+
+val DecStr : int -> string
+
+val HexStr : int -> string
+
+val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
+
+val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val int_power : (int, int) -> int
+
+val real_power = "real_power" : (real, int) -> real
+
+overload operator ^ = {xor_vec, int_power, real_power}
+
+val add_range = "add" : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
+
+val add_int = "add" : (int, int) -> int
+
+val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n)
+
+val add_real = "add_real" : (real, real) -> real
+
+overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
+
+val sub_range = "sub" : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
+
+val sub_int = "sub" : (int, int) -> int
+
+val sub_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val sub_vec_int = "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n)
+
+val sub_real = "sub_real" : (real, real) -> real
+
+val negate_range = "minus_big_int" : forall 'n. range('n, 'm) -> range(- 'm, - 'n)
+
+val negate_int = "minus_big_int" : int -> int
 
-val extern forall Type 'a. ('a, 'a) -> bool effect pure eq_anything = "(fun (x, y) -> x == y)"
+val negate_real = "Num.minus_num" : real -> real
 
-overload (deinfix ==) [eq_int; eq_vec; eq_string; eq_real; eq_anything]
+overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real}
 
-val extern forall Type 'a, Num 'n. vector<'n - 1, 'n, dec, 'a> -> [:'n:] effect pure length = "length"
+overload negate = {negate_range, negate_int, negate_real}
 
-val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *).
-  (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "subrange"
+val mult_range = "mult" : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p)
 
-(* FIXME: rewriter shouldn't assume this exists *)
-val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *).
-  (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure bitvector_subrange_dec = "subrange"
+val mult_int = "mult" : (int, int) -> int
 
-val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int) -> 'a effect pure vector_access = "access"
+val mult_real = "mult_real" : (real, real) -> real
 
-val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int, 'a) -> vector<'n - 1, 'n, dec, 'a> effect pure vector_update = "update"
+overload operator * = {mult_range, mult_int, mult_real}
 
-val extern forall Num 'n, Num 'm, Num 'o.
-  (bit['n], [:'m:], [:'o:], bit['m - ('o - 1)]) -> bit['n]
-  effect pure vector_update_subrange = "update_subrange"
+val Sqrt = "sqrt_real" : real -> real
 
-val forall Num 'n, Type 'a. ('a, vector<'n - 1, 'n, dec, 'a>) -> vector<'n, 'n + 1, dec, 'a> effect pure vcons
+val gteq_int = "gteq" : (int, int) -> bool
 
-val extern forall Num 'n, Num 'm, Type 'a. (vector<'n - 1, 'n, dec, 'a>, vector<'m - 1, 'm, dec, 'a>) -> vector<('n + 'm) - 1, 'n + 'm, dec, 'a> effect pure append = "append"
+val gteq_real = "gteq_real" : (real, real) -> bool
 
-val extern bool -> bool effect pure not_bool = "not"
-val extern forall 'n. bit['n] -> bit['n] effect pure not_vec = "not_vec"
+overload operator >= = {gteq_atom, gteq_int, gteq_real}
 
-overload ~ [not_bool; not_vec]
+val lteq_int = "lteq" : (int, int) -> bool
 
-val forall Type 'a. ('a, 'a) -> bool effect pure neq_anything
+val lteq_real = "lteq_real" : (real, real) -> bool
 
-function neq_anything (x, y) = not_bool (x == y)
+overload operator <= = {lteq_atom, lteq_int, lteq_real}
 
-overload (deinfix !=) [neq_anything]
+val gt_int = "gt" : (int, int) -> bool
 
-val extern (bool, bool) -> bool effect pure and_bool = "and_bool"
-val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure and_vec = "and_vec"
+val gt_real = "gt_real" : (real, real) -> bool
 
-overload (deinfix &) [and_bool; and_vec]
+overload operator > = {gt_atom, gt_int, gt_real}
 
-val extern (bool, bool) -> bool effect pure or_bool = "or_bool"
-val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure or_vec = "or_vec"
+val lt_int = "lt" : (int, int) -> bool
 
-overload (deinfix |) [or_bool; or_vec]
+val lt_real = "lt_real" : (real, real) -> bool
 
-val extern forall 'n. bit['n] -> [|0:2**'n - 1|] effect pure UInt = "uint"
+overload operator < = {lt_atom, lt_int, lt_real}
 
-val extern forall 'n. bit['n] -> [|- 2**('n - 1):2**('n - 1) - 1|] effect pure SInt = "sint"
+val RoundDown = "round_down" : real -> int
 
-val extern string -> unit effect pure print = "print_endline"
-val extern (string, string) -> string effect pure concat_str = "concat_string"
-val int -> string effect pure DecStr
-val int -> string effect pure HexStr
+val RoundUp = "round_up" : real -> int
 
-val forall 'n. (bit['n], bit['n]) -> bit['n] effect pure xor_vec
-val (int, int) -> int effect pure int_exp
+val abs = "abs_num" : real -> real
 
-overload (deinfix ^) [xor_vec; int_exp]
+val quotient_nat = "quotient" : (nat, nat) -> nat
 
-val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add"
-val extern (int, int) -> int effect pure add_int = "add"
-val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure add_vec = "add_vec"
-val forall 'n. (bit['n], int) -> bit['n] effect pure add_vec_int
+val quotient_real = "quotient_real" : (real, real) -> real
 
-overload (deinfix +) [add_range; add_int; add_vec; add_vec_int]
+val quotient = "quotient" : (int, int) -> int
 
-val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub"
-val extern (int, int) -> int effect pure sub_int = "sub"
-val forall 'n. (bit['n], bit['n]) -> bit['n] effect pure sub_vec
-val forall 'n. (bit['n], int) -> bit ['n] effect pure sub_vec_int
+infixl 7 /
 
-val forall 'n. [|'n:'m|] -> [|-'m:-'n|] effect pure negate_range
-val int -> int effect pure negate_int
+overload operator / = {quotient_nat, quotient, quotient_real}
 
-overload (deinfix -) [sub_range; sub_int; sub_vec; sub_vec_int]
-overload negate [negate_range; negate_int]
+val modulus = "modulus" : (int, int) -> int
 
-val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n * 'o : 'm * 'p|] effect pure mult_range = "mult"
-val extern (int, int) -> int effect pure mult_int = "mult"
+infixl 7 %
 
-overload (deinfix * ) [mult_range; mult_int]
+overload operator % = {modulus}
 
-val (int, int) -> bool effect pure gteq_int
-val (real, real) -> bool effect pure gteq_real
+val Real = "Num.num_of_big_int" : int -> real
 
-overload (deinfix >=) [gteq_int; gteq_real]
+val shl_int = "shl_int" : (int, int) -> int
 
-val (int, int) -> bool effect pure lteq_int
-val (real, real) -> bool effect pure lteq_real
+val shr_int = "shr_int" : (int, int) -> int
 
-overload (deinfix <=) [lteq_int; lteq_real]
+val min_nat = "min_int" : (nat, nat) -> nat
 
-val (int, int) -> bool effect pure gt_int
-val (real, real) -> bool effect pure gt_real
+val min_int = "min_int" : (int, int) -> int
 
-overload (deinfix >) [gt_int; gt_real]
+val max_nat = "max_int" : (nat, nat) -> nat
 
-val (int, int) -> bool effect pure lt_int
-val (real, real) -> bool effect pure lt_real
+val max_int = "max_int" : (int, int) -> int
 
-overload (deinfix <) [lt_int; lt_real]
+overload min = {min_nat, min_int}
 
-val real -> int effect pure RoundDown
-val real -> int effect pure RoundUp
+overload max = {max_nat, max_int}
 
-val extern (int, int) -> int effect pure quotient = "quotient"
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
 
-overload (deinfix quot) [quotient]
+val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)}
 
-val extern (int, int) -> int effect pure modulus = "modulus"
+function ex_nat 'n = n
 
-overload (deinfix mod) [modulus]
+val cast ex_int : int -> {'n, true. atom('n)}
 
-val extern (int, int) -> int effect pure shl_int
-val extern (int, int) -> int effect pure shr_int
+function ex_int 'n = n
 
-val (nat, nat) -> nat effect pure min_nat
-val (int, int) -> int effect pure min_int
-val (nat, nat) -> nat effect pure max_nat
-val (int, int) -> int effect pure max_int
+val ex_range : forall 'n 'm.
+  range('n, 'm) -> {'o, 'n <= 'o & 'o <= 'm. atom('o)}
 
-overload min [min_nat; min_int]
-overload max [max_nat; max_int]
+val coerce_int_nat : int -> nat effect {escape}
 
-val extern forall 'n, 'm. ([:'m:], [:'n:], bit['m], bit['m], bit[8 * 'n]) -> unit effect {wmem} __WriteRAM = "write_ram"
-val extern forall 'n, 'm. ([:'m:], [:'n:], bit['m], bit['m]) -> bit[8 * 'n] effect {rmem} __ReadRAM = "read_ram"
+function coerce_int_nat 'x = {
+  assert(constraint('x >= 0));
+  x
+}
 
-val extern forall 'n, 'm. (bit['n], [:'m:]) -> bit['n * 'm] effect pure replicate_bits
+val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
+  (bits('m), int, atom('n)) -> bits('n)
 
-val extern nat -> exist 'n, 'n >= 0. [:'n:] effect pure ex_nat = "identity"
-val extern int -> exist 'n. [:'n:] effect pure ex_int = "identity"
-val extern forall 'n, 'm. [|'n:'m|] -> exist 'o, 'n <= 'o & 'o <= 'm. [:'o:] effect pure ex_range = "identity"
+val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
 
+val print_int = "print_int" : (string, int) -> unit
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
index 481ff80f..9ed00494 100755
--- a/test/ocaml/run_tests.sh
+++ b/test/ocaml/run_tests.sh
@@ -50,7 +50,7 @@ printf "<testsuites>\n" >> $DIR/tests.xml
 for i in `ls -d */`;
 do
     cd $DIR/$i;
-    if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail` 1> /dev/null;
+    if $SAILDIR/sail -new_parser -o out -ocaml ../prelude.sail `ls *.sail` 1> /dev/null;
     then
 	./out > result;
 	if diff expect result;
@@ -69,4 +69,28 @@ done
 
 finish_suite "Ocaml testing"
 
+cd $DIR
+
+for i in `ls -d */`;
+do
+    cd $DIR/$i;
+    if $SAILDIR/sail -new_parser -o out -ocaml_trace ../prelude.sail `ls *.sail` 1> /dev/null;
+    then
+	./out > result 2> /dev/null;
+	if diff expect result;
+	then
+	    green "built $i" "ok"
+	else
+	    yellow "bad output $i" "fail"
+	fi;
+	rm out;
+	rm result;
+	rm -r _sbuild
+    else
+	red "building $i" "fail"
+    fi
+done
+
+finish_suite "Ocaml trace testing"
+
 printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/ocaml/string_equality/string_equality.sail b/test/ocaml/string_equality/string_equality.sail
index 68629862..568052cd 100644
--- a/test/ocaml/string_equality/string_equality.sail
+++ b/test/ocaml/string_equality/string_equality.sail
@@ -1,10 +1,3 @@
+val main : unit -> unit
 
-val unit -> unit effect pure main
-
-function main () = {
-  if ("test" == "test") then {
-    print("true")
-  } else {
-    print("false")
-  }
-}
+function main () = if "test" == "test" then print("true") else print("false")
diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail
index 8f50e057..a710eb25 100644
--- a/test/ocaml/types/types.sail
+++ b/test/ocaml/types/types.sail
@@ -1,44 +1,44 @@
+enum signal = {Low, High}
 
-typedef signal = enumerate {Low; High}
+enum enum_single = {SingleConstructor}
 
-typedef enum_single = enumerate {SingleConstructor}
+type byte = bits(8)
 
-typedef byte = bit[8]
-typedef b32 = bit[32]
-typedef b64 = bit[64]
+type b32 = bits(32)
 
-register b64 R64
-register b32 R32
-register byte R8
+type b64 = bits(64)
 
-register signal SIGNALREG
+register R64 : b64
 
-typedef TestStruct = const struct {
-  bit[2] field1;
-  byte field2;
-  bool field3
-}
+register R32 : b32
+
+register R8 : byte
 
-register TestStruct SREG
+register SIGNALREG : signal
 
-typedef option = const union forall Type 'a. {
-    None;
-    'a Some
+struct TestStruct = {
+  field1 : bits(2),
+  field2 : byte,
+  field3 : bool
 }
 
-register (option<byte>) OREG
+register SREG : TestStruct
+
+union option ('a : Type) = {None, Some : 'a}
+
+register OREG : option(byte)
 
-val unit -> unit effect {rreg, wreg} main
+val main : unit -> unit effect {rreg, wreg}
 
 function main () = {
-  R8 := 0xFF;
-  SIGNALREG := Low;
+  R8 = 0xFF;
+  SIGNALREG = Low;
   print(if SIGNALREG == Low then "pass" else "fail");
-  SIGNALREG := High;
+  SIGNALREG = High;
   print(if SIGNALREG == High then "pass" else "fail");
-  SREG.field1 := 0b00;
+  SREG.field1 = 0b00;
   print(if SREG.field1 == 0b00 then "pass" else "faiL");
-  SREG.field1 := 0b11;
+  SREG.field1 = 0b11;
   print(if SREG.field1 == 0b11 then "pass" else "faiL");
   print("pass")
 }