22 files changed, 218 insertions, 105 deletions
diff --git a/test/builtins/run_tests.py b/test/builtins/run_tests.py
index b20d4224..ba13d5b9 100755
--- a/test/builtins/run_tests.py
+++ b/test/builtins/run_tests.py
@@ -86,6 +86,37 @@ def test_lem_builtins(name):
         results.collect(tests)
     return results.finish()
 
+def test_coq_builtins(name):
+    banner('Testing builtins: {}'.format(name))
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
+            basename = os.path.splitext(os.path.basename(filename))[0]
+            tests[filename] = os.fork()
+            if tests[filename] == 0:
+                # Generate Coq from Sail
+                step('sail -no_warn -coq -o {} {}'.format(basename, filename))
+
+                step('mkdir -p _coqbuild_{}'.format(basename))
+                step('mv {}.v _coqbuild_{}'.format(basename, basename))
+                step('mv {}_types.v _coqbuild_{}'.format(basename, basename))
+                step('cp test.v _coqbuild_{}'.format(basename))
+                os.chdir('_coqbuild_{}'.format(basename))
+
+                # TODO: find bbv properly
+                step('coqc -R $SAIL_DIR/../bbv/theories bbv -R $SAIL_DIR/lib/coq Sail {}_types.v'.format(basename))
+                step('coqc -R $SAIL_DIR/../bbv/theories bbv -R $SAIL_DIR/lib/coq Sail {}.v'.format(basename))
+                step('coqtop -R "$SAIL_DIR/../bbv/theories" bbv -R "$SAIL_DIR/lib/coq" Sail -require {}_types -require {} -l test.v -batch | tee /dev/stderr | grep -q OK'.format(basename,basename))
+
+                os.chdir('..')
+                step('rm -r _coqbuild_{}'.format(basename))
+
+                print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
+                sys.exit()
+        results.collect(tests)
+    return results.finish()
+
 xml = '<testsuites>\n'
 
 xml += test_c_builtins('C, No optimisations', '')
@@ -96,6 +127,7 @@ xml += test_ocaml_builtins('OCaml', '')
 
 # Comment this out for most runs because it's really slow
 # xml += test_lem_builtins('Lem to OCaml')
+# xml += test_coq_builtins('Coq')
 
 xml += '</testsuites>\n'
 
diff --git a/test/builtins/test.v b/test/builtins/test.v
new file mode 100644
index 00000000..64c5bf10
--- /dev/null
+++ b/test/builtins/test.v
@@ -0,0 +1,15 @@
+Require Import Sail2_state_monad.
+Require Import Sail2_state_lifting.
+Require Import String.
+Require Import List.
+Import ListNotations.
+
+Goal True.
+let result := eval cbv in (liftState register_accessors (main tt) (init_state tt)) in
+match result with
+  | [(Value tt,_)] => idtac "OK"
+  | [(Ex (Failure ?s),_)] => idtac "Fail:" s
+  | _ => idtac "Fail"
+end.
+exact I.
+Qed.
diff --git a/test/c/assign_rename_bug.sail b/test/c/assign_rename_bug.sail
index 8b74df2a..f9650b85 100644
--- a/test/c/assign_rename_bug.sail
+++ b/test/c/assign_rename_bug.sail
@@ -7,9 +7,8 @@ $include <vector_dec.sail>
 $include <exception_basic.sail>
 
 val sub_vec_int = {
-  ocaml: "sub_vec_int",
-  lem: "sub_vec_int",
-  c: "sub_bits_int"
+  c: "sub_bits_int",
+  _: "sub_vec_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
 overload operator - = {sub_vec_int}
diff --git a/test/c/zero_length_bv.expect b/test/c/zero_length_bv.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/zero_length_bv.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/zero_length_bv.sail b/test/c/zero_length_bv.sail
new file mode 100644
index 00000000..332b8aae
--- /dev/null
+++ b/test/c/zero_length_bv.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let x: bits(0) = [];
+  if x == sail_zeros(0) then {
+    print_endline("ok")
+  };
+  let x: vector(0, dec, string) = [];
+  ()
+}
+\ No newline at end of file
diff --git a/test/coq/pass/while_MM_terminating.sail b/test/coq/pass/while_MM_terminating.sail
new file mode 100644
index 00000000..e3bca7f5
--- /dev/null
+++ b/test/coq/pass/while_MM_terminating.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+register COUNT : int
+
+register INT : bool
+
+function test () -> unit = {
+  COUNT = 0;
+  while not_bool(INT) do {
+    COUNT = COUNT + 1;
+    if COUNT > 5 then
+      INT = true
+  }
+}
+
+termination_measure test while (5 - COUNT)
diff --git a/test/coq/pass/while_MP_terminating.sail b/test/coq/pass/while_MP_terminating.sail
new file mode 100644
index 00000000..d9b71ad9
--- /dev/null
+++ b/test/coq/pass/while_MP_terminating.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+register INT : bool
+
+function test () -> int = {
+  count : int = 0;
+  while not_bool(INT) & count < 5 do count = count + 1;
+  return(count)
+}
+
+termination_measure test while 5 - count
diff --git a/test/coq/pass/while_PM_terminating.sail b/test/coq/pass/while_PM_terminating.sail
new file mode 100644
index 00000000..5129e997
--- /dev/null
+++ b/test/coq/pass/while_PM_terminating.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+register GPR00 : int
+
+function test b : int -> unit = {
+  i : int = 0;
+  while i < 64 do {
+    GPR00 = b + i;
+    i = i + 1;
+  }
+}
+
+termination_measure test while 64 - i
diff --git a/test/coq/pass/while_PP_terminating.sail b/test/coq/pass/while_PP_terminating.sail
new file mode 100644
index 00000000..80840ac9
--- /dev/null
+++ b/test/coq/pass/while_PP_terminating.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+function test n : int -> int = {
+  i : int = 1;
+  j : int = 1;
+  while i < n do {
+    j = i * j;
+    i = i + 1
+  };
+  j
+}
+
+termination_measure test while n - i
diff --git a/test/coq/skip b/test/coq/skip
index 49744fce..259df4b0 100644
--- a/test/coq/skip
+++ b/test/coq/skip
@@ -42,3 +42,10 @@ reg_mod.sail
 reg_ref.sail
 XXXXX Dodgy division/modulo stuff
 Replicate.sail
+XXXXX Non-terminating loops - I've written terminating versions of these
+while_MM.sail
+while_MP.sail
+while_PM.sail
+while_PP.sail
+XXXXX Not yet - haven't decided whether to support register reads in measures
+while_MM_terminating.sail
diff --git a/test/mono/assert2.sail b/test/mono/assert2.sail
index edf92710..90874b68 100644
--- a/test/mono/assert2.sail
+++ b/test/mono/assert2.sail
@@ -1,14 +1,5 @@
-$include <smt.sail>
-$include <flow.sail>
 default Order dec
-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
-overload operator == = {eq_int, eq_vec}
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-overload operator * = {mult_range, mult_int, mult_real}
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-overload operator < = {lt_atom, lt_int}
+$include <prelude.sail>
 
 /* Should find a set constraint below the let */
 
@@ -28,4 +19,4 @@ val run : unit -> unit effect {escape}
 function run () = {
     f(8);
     f(16);
-}
-\ No newline at end of file
+}
diff --git a/test/mono/atomsplit.sail b/test/mono/atomsplit.sail
index 6e5d3e3b..23a1b0fb 100644
--- a/test/mono/atomsplit.sail
+++ b/test/mono/atomsplit.sail
@@ -1,14 +1,5 @@
-$include <smt.sail>
-$include <flow.sail>
 default Order dec
-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
-overload operator == = {eq_int, eq_vec}
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-overload operator * = {mult_range, mult_int, mult_real}
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-overload operator < = {lt_atom, lt_int}
+$include <prelude.sail>
 
 /* Test splitting required because there's a size calculation in the function */
 
@@ -27,4 +18,4 @@ val run : unit -> unit effect {escape}
 function run () = {
     foo(2);
     foo(4);
-}
-\ No newline at end of file
+}
diff --git a/test/mono/not-yet/union-exist_manual b/test/mono/not-yet/union-exist_manual
deleted file mode 100644
index d35c3d48..00000000
--- a/test/mono/not-yet/union-exist_manual
+++ /dev/null
@@ -1 +0,0 @@
-union-exist.sail -mono_split union-exist.sail:9:v
-\ No newline at end of file
diff --git a/test/mono/not-yet/union-exist b/test/mono/pass/union-exist
index ebb89267..ebb89267 100644
--- a/test/mono/not-yet/union-exist
+++ b/test/mono/pass/union-exist
diff --git a/test/mono/pass/union-exist2 b/test/mono/pass/union-exist2
new file mode 100644
index 00000000..9852a125
--- /dev/null
+++ b/test/mono/pass/union-exist2
@@ -0,0 +1 @@
+union-exist2.sail -auto_mono
diff --git a/test/mono/pass/union-exist_manual b/test/mono/pass/union-exist_manual
new file mode 100644
index 00000000..54deb7d8
--- /dev/null
+++ b/test/mono/pass/union-exist_manual
@@ -0,0 +1 @@
+union-exist.sail -mono_split union-exist.sail:10:v
diff --git a/test/mono/set.sail b/test/mono/set.sail
index 74d4693e..4b97aeef 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -1,14 +1,5 @@
 default Order dec
-$include <flow.sail>
-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}
+$include <prelude.sail>
 val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
 val extz : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
 function extz(m,v) = extz_vec(m,v)
diff --git a/test/mono/union-exist.sail b/test/mono/union-exist.sail
index f1e01e75..ca953b3c 100644
--- a/test/mono/union-exist.sail
+++ b/test/mono/union-exist.sail
@@ -1,32 +1,23 @@
 default Order dec
-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))
-
+$include <prelude.sail>
 
 union myunion = {
-  MyConstr : {'n, 'n in {8,16}. (atom('n),bits('n))}
+  MyConstr : {'n, 'n in {8,16}. (int('n),bits('n))}
 }
 
 val make : bits(2) -> myunion
 
 function make(v) =
-  /* Can't mention these below without running into exp/nexp parsing conflict! */
-  let eight = 8 in let sixteen = 16 in
-  let r : {'n, 'n in {8,16}. (atom('n),bits('n))} = match v {
-    0b00 => (  eight,  0x12),
-    0b01 => (sixteen,0x1234),
-    0b10 => (  eight,  0x56),
-    0b11 => (sixteen,0x5678)
+  let r : {'n, 'n in {8,16}. (int('n),bits('n))} = match v {
+    0b00 => ( 8,  0x12),
+    0b01 => (16,0x1234),
+    0b10 => ( 8,  0x56),
+    0b11 => (16,0x5678)
   } in MyConstr(r)
 
 val use : myunion -> bits(32)
 
-function use(MyConstr((n,v) as (atom('n),bits('n)))) = extz(v)
+function use(MyConstr(n,v)) = sail_zero_extend(v,32)
 
 val run : unit -> unit effect {escape}
 
diff --git a/test/mono/union-exist2.sail b/test/mono/union-exist2.sail
new file mode 100644
index 00000000..aede3c0d
--- /dev/null
+++ b/test/mono/union-exist2.sail
@@ -0,0 +1,31 @@
+default Order dec
+$include <prelude.sail>
+
+union myunion = {
+  MyConstr : {'n 'm 'o, 'n in {8,16} & 'o in {8,16} & 'n <= 'm & 'm <= 'o. (int('n),bits('n),int('o),bits('o),int('m))}
+}
+
+val make : bits(2) -> myunion
+
+function make(v) =
+  let (n,v,m) : {'n 'm, 'n in {8,16} & 'm in {8,16} & 'n <= 'm. (int('n),bits('n),int('m))} = match v {
+    0b00 => ( 8,  0x12, 8),
+    0b01 => (16,0x1234,16),
+    0b10 => ( 8,  0x56,16),
+    0b11 => (16,0x5678,16)
+  } in
+  let w = sail_zero_extend(0x5,m) in
+  MyConstr(n,v,m,w,m)
+
+val use : myunion -> bits(32)
+
+function use(MyConstr(n,v,_,_,_)) = sail_zero_extend(v,32)
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(use(make(0b00)) == 0x00000012);
+  assert(use(make(0b01)) == 0x00001234);
+  assert(use(make(0b10)) == 0x00000056);
+  assert(use(make(0b11)) == 0x00005678);
+}
diff --git a/test/mono/varpatterns.sail b/test/mono/varpatterns.sail
index b2c9e7ee..a583cbfc 100644
--- a/test/mono/varpatterns.sail
+++ b/test/mono/varpatterns.sail
@@ -1,32 +1,5 @@
-$include <smt.sail>
-$include <flow.sail>
 default Order dec
-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
-overload operator == = {eq_int, eq_vec}
-val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
-function neq_vec (x, y) = not_bool(eq_vec(x, y))
-overload operator != = {neq_atom, neq_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)*/
-val UInt = {
-  ocaml: "uint",
-  lem: "uint",
-  interpreter: "uint",
-  c: "sail_uint"
-} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
-val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
-val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
-  (bits('m), int, atom('n)) -> bits('n)
+$include <prelude.sail>
 
 /* Test constant propagation on some variable patterns in let expressions */
 
@@ -35,7 +8,7 @@ val test : bool -> unit effect {escape}
 function test(b) = {
     let 'n : {|8,16|} = if b then 8 else 16;
     let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
-    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
+    assert(unsigned(x) == (match n { 8 => 18, 16 => 4660 }) : int, "unsigned");
 }
 
 val test2 : bool -> unit effect {escape}
@@ -43,7 +16,7 @@ val test2 : bool -> unit effect {escape}
 function test2(b) = {
     let 'n = (if b then 8 else 16) : {|8,16|};
     let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
-    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
+    assert(unsigned(x) == (match n { 8 => 18, 16 => 4660 }) : int, "unsigned");
 }
 
 val test_mult : {|4,8|} -> unit effect {escape}
@@ -51,7 +24,7 @@ val test_mult : {|4,8|} -> unit effect {escape}
 function test_mult('m) = {
     let 'n = 2 * 'm;
     let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
-    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
+    assert(unsigned(x) == (match n { 8 => 18, 16 => 4660 }) : int, "unsigned");
 }
 
 val run : unit -> unit effect {escape}
@@ -63,4 +36,4 @@ function run() = {
     test2(false);
     test_mult(4);
     test_mult(8);
-}
-\ No newline at end of file
+}
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
index d077cd80..f9328394 100755
--- a/test/ocaml/run_tests.sh
+++ b/test/ocaml/run_tests.sh
@@ -91,25 +91,26 @@ done
 
 finish_suite "Ocaml trace testing"
 
-cd $DIR
-
-for i in `ls -d */`;
-do
-    cd $DIR/$i;
-    if $SAILDIR/sail -no_warn -undefined_gen -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null;
-    then
-	if diff expect result;
-	then
-	    green "interpreted $i" "ok"
-	else
-	    red "bad output $i" "fail"
-	fi;
-	rm result
-    else
-	red "interpreter crashed on $i" "fail"
-    fi
-done
-
-finish_suite "Interpreter testing"
+# FIXME: Renable these!
+#cd $DIR
+#
+#for i in `ls -d */`;
+#do
+#    cd $DIR/$i;
+#    if $SAILDIR/sail -no_warn -undefined_gen -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null;
+#    then
+#	if diff expect result;
+#	then
+#	    green "interpreted $i" "ok"
+#	else
+#	    red "bad output $i" "fail"
+#	fi;
+#	rm result
+#    else
+#	red "interpreter crashed on $i" "fail"
+#    fi
+#done
+#
+#finish_suite "Interpreter testing"
 
 printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/typecheck/pass/zero_length_bv.sail b/test/typecheck/pass/zero_length_bv.sail
new file mode 100644
index 00000000..332b8aae
--- /dev/null
+++ b/test/typecheck/pass/zero_length_bv.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let x: bits(0) = [];
+  if x == sail_zeros(0) then {
+    print_endline("ok")
+  };
+  let x: vector(0, dec, string) = [];
+  ()
+}
+\ No newline at end of file