Merge branch 'sail2' into mappings

7 files changed, 15 insertions, 12 deletions

diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
index d93143f0..2021bf67 100644
--- a/test/typecheck/pass/arm_FPEXC1.sail
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -1,12 +1,12 @@
 default Order dec
 
-val vector_access = {ocaml: "access", lem: "access_vec_dec"}: forall ('n : Int).
+val vector_access = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int).
   (vector('n, dec, bit), int) -> bit
 
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
   (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit)
 
-val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (vector('n, dec, bit), atom('m), atom('o), vector('m - ('o - 1), dec, bit)) -> vector('n, dec, bit)
 
 register _FPEXC32_EL2 : vector(32, dec, bit)
diff --git a/test/typecheck/pass/atomcase.sail b/test/typecheck/pass/atomcase.sail
index 4e030a60..d2549e01 100644
--- a/test/typecheck/pass/atomcase.sail
+++ b/test/typecheck/pass/atomcase.sail
@@ -2,7 +2,7 @@ default Order dec
 
 infix 4 ==
 
-val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
+val eq_atom = {ocaml: "eq_atom", lem: "eq", coq: "Z.eqb"}: forall ('n : Int) ('m : Int).
   (atom('n), atom('m)) -> bool
 
 overload operator == = {eq_atom}
diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail
index 991cd828..261e3b44 100644
--- a/test/typecheck/pass/deinfix_plus.sail
+++ b/test/typecheck/pass/deinfix_plus.sail
@@ -1,6 +1,6 @@
 default Order inc
 
-val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
+val bv_add = {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall ('n : Int).
   (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
 
 overload operator + = {bv_add}
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
index 47343e02..96b1ecf1 100644
--- a/test/typecheck/pass/exist_pattern.sail
+++ b/test/typecheck/pass/exist_pattern.sail
@@ -8,14 +8,14 @@ register x : nat
 
 register y : nat
 
-val eq_int = {lem: "eq"} : (int, int) -> bool
-val eq_vec = {lem: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool
+val eq_int = {lem: "eq", coq: "Z.eqb"} : (int, int) -> bool
+val eq_vec = {lem: "eq_vec", coq: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool
 
 overload operator == = {eq_int, eq_vec}
 
-val "and_bool" : (bool, bool) -> bool
+val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n.
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc", coq: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n.
   (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit)
 
 type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)}
diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail
index 6763922a..dc625084 100644
--- a/test/typecheck/pass/nzcv.sail
+++ b/test/typecheck/pass/nzcv.sail
@@ -10,6 +10,6 @@ function test nzcv = {
   Z = 0b0;
   C = 0b0;
   V = 0b0;
-  (N, Z, C, V) = nzcv;
+  (N @ Z @ C @ V) = nzcv;
   ()
 }
diff --git a/test/typecheck/pass/simple_record_access.sail b/test/typecheck/pass/simple_record_access.sail
index a6e34c8b..76cbbaed 100644
--- a/test/typecheck/pass/simple_record_access.sail
+++ b/test/typecheck/pass/simple_record_access.sail
@@ -1,4 +1,5 @@
 $include <flow.sail>
+$include <vector_inc.sail>
 
 enum signal = {LOW, HIGH}
 
diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail
index c148e6da..84b4f7b4 100644
--- a/test/typecheck/pass/while_PM.sail
+++ b/test/typecheck/pass/while_PM.sail
@@ -22,10 +22,12 @@ val vector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n.
 
 register GPR00 : vector(64, dec, bit)
 
+/* FIXME: Currently this doesn't work in lem
 function test b : bit -> unit = {
-  i : int = 0;
+  i : range(0, 64) = 0;
   while i < 64 do {
     GPR00[i] = b;
-    i = i + 1
+    i = i + 1;
   }
 }
+*/
\ No newline at end of file