Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2

21 files changed, 58 insertions, 36 deletions

diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
index 078beb4a..d93143f0 100644
--- a/test/typecheck/pass/arm_FPEXC1.sail
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -1,11 +1,14 @@
 default Order dec
 
-val vector_access = {ocaml: "bitvector_access_dec", lem: "bitvector_access_dec"}: forall ('n : Int).
+val vector_access = {ocaml: "access", lem: "access_vec_dec"}: forall ('n : Int).
   (vector('n, dec, bit), int) -> bit
 
-val vector_subrange = {ocaml: "bitvector_subrange_dec", lem: "bitvector_subrange_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
+val vector_subrange = {ocaml: "subrange", lem: "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.
+  (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)
 
 val set_FPEXC32_EL2 : vector(32, dec, bit) -> unit effect {wreg}
diff --git a/test/typecheck/pass/atomcase.sail b/test/typecheck/pass/atomcase.sail
index 2ed00a13..4e030a60 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_atom"}: forall ('n : Int) ('m : Int).
+val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
   (atom('n), atom('m)) -> bool
 
 overload operator == = {eq_atom}
diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail
index 4ac0fec4..66fc0025 100644
--- a/test/typecheck/pass/case_simple_constraints.sail
+++ b/test/typecheck/pass/case_simple_constraints.sail
@@ -1,4 +1,4 @@
-val plus = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int).
+val plus = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int).
   (atom('n + 20), atom('m)) -> atom('n + 20 + 'm)
 
 val minus_ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n <= -10.
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
index 7d125d23..178f8003 100644
--- a/test/typecheck/pass/exist_pattern.sail
+++ b/test/typecheck/pass/exist_pattern.sail
@@ -8,9 +8,15 @@ register x : nat
 
 register y : nat
 
-val eq_int : (int, int) -> bool
+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
 
-overload operator == = {eq_int}
+overload operator == = {eq_int, eq_vec}
+
+val "and_bool" : (bool, bool) -> bool
+
+val vector_subrange = {ocaml: "subrange", lem: "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/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail
index 95f9a854..47b26261 100644
--- a/test/typecheck/pass/flow_gt1.sail
+++ b/test/typecheck/pass/flow_gt1.sail
@@ -1,9 +1,9 @@
 default Order inc
 
-val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
 val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail
index d644ce40..3ea9d69b 100644
--- a/test/typecheck/pass/flow_gteq1.sail
+++ b/test/typecheck/pass/flow_gteq1.sail
@@ -1,9 +1,9 @@
 default Order inc
 
-val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
 val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail
index 569ec3aa..e29424be 100644
--- a/test/typecheck/pass/flow_lt1.sail
+++ b/test/typecheck/pass/flow_lt1.sail
@@ -1,9 +1,9 @@
 default Order inc
 
-val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
 val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail
index d5b5cfd0..2c1ad667 100644
--- a/test/typecheck/pass/flow_lt2.sail
+++ b/test/typecheck/pass/flow_lt2.sail
@@ -1,9 +1,9 @@
 default Order inc
 
-val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
 val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail
index 40c09c8e..afc620b6 100644
--- a/test/typecheck/pass/flow_lt_assign.sail
+++ b/test/typecheck/pass/flow_lt_assign.sail
@@ -1,9 +1,9 @@
 default Order inc
 
-val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
 val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail
index 90c4fb17..c61f93e2 100644
--- a/test/typecheck/pass/flow_lteq1.sail
+++ b/test/typecheck/pass/flow_lteq1.sail
@@ -1,9 +1,9 @@
 default Order inc
 
-val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
 val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int).
diff --git a/test/typecheck/pass/foreach_var_updates.sail b/test/typecheck/pass/foreach_var_updates.sail
index 19d491d0..7813cb16 100644
--- a/test/typecheck/pass/foreach_var_updates.sail
+++ b/test/typecheck/pass/foreach_var_updates.sail
@@ -1,8 +1,8 @@
-val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int
+val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int
 
 overload operator + = {add_int}
 
-val sub_int = {ocaml: "sub", lem: "sub"}: (int, int) -> int
+val sub_int = {ocaml: "sub", lem: "integerMinus"}: (int, int) -> int
 
 overload operator - = {sub_int}
 
diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail
index e498cded..6763922a 100644
--- a/test/typecheck/pass/nzcv.sail
+++ b/test/typecheck/pass/nzcv.sail
@@ -1,5 +1,8 @@
 default Order dec
 
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+  (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit)
+
 val test : vector(4, dec, bit) -> unit
 
 function test nzcv = {
diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail
index e1587ebc..94b40885 100644
--- a/test/typecheck/pass/patternrefinement.sail
+++ b/test/typecheck/pass/patternrefinement.sail
@@ -2,8 +2,8 @@ default Order dec
 
 infix 4 ==
 
-val extz = {ocaml: "extz", lem: "extz"}: forall ('n : Int) ('m : Int) ('ord : Order).
-  vector('n, 'ord, bit) -> vector('m, 'ord, bit)
+val extz = {ocaml: "extz", lem: "extz_vec"}: forall ('n : Int) ('m : Int) ('ord : Order).
+  (atom('m), vector('n, 'ord, bit)) -> vector('m, 'ord, bit)
 
 val length = {ocaml: "length", lem: "length"}: forall ('m : Int) ('ord : Order) ('a : Type).
   vector('m, 'ord, 'a) -> atom('m)
@@ -11,7 +11,7 @@ val length = {ocaml: "length", lem: "length"}: forall ('m : Int) ('ord : Order)
 val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order).
   (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool
 
-val eq_atom = {ocaml: "eq_atom", lem: "eq_atom"}: forall ('n : Int) ('m : Int).
+val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
   (atom('n), atom('m)) -> bool
 
 val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool
@@ -22,6 +22,6 @@ val test : forall 'n, 'n in {32, 64}.
   vector('n, dec, bit) -> vector(64, dec, bit)
 
 function test v = match length(v) {
-  32 => extz(v),
+  32 => extz(64, v),
   64 => v
 }
diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail
index 726f9575..1d7e15b1 100644
--- a/test/typecheck/pass/procstate1.sail
+++ b/test/typecheck/pass/procstate1.sail
@@ -2,7 +2,7 @@ default Order dec
 
 infix 4 ==
 
-val operator == : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
+val operator == = {lem: "eq_vec"} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
 
 struct ProcState ('n : Int) = {
   N : vector('n, dec, bit),
diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail
index 9376b2a8..6de87a8c 100644
--- a/test/typecheck/pass/vec_pat1.sail
+++ b/test/typecheck/pass/vec_pat1.sail
@@ -3,12 +3,17 @@ default Order inc
 val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
   (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
 
-val vector_subrange = {ocaml: "bitvector_subrange_inc", lem: "bitvector_subrange_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
   (vector('l, inc, bit), atom('m), atom('o)) -> vector('o + 1 - 'm, inc, bit)
 
-val bitvector_concat : forall ('m : Int) ('p : Int).
+val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('m : Int) ('p : Int).
   (vector('m, inc, bit), vector('p, inc, bit)) -> vector('m + 'p, inc, bit)
 
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (vector('n, inc, bit), vector('n, inc, bit)) -> bool
+
+infix 4 ==
+overload operator == = {eq_vec}
+
 overload operator + = {bv_add}
 
 overload append = {bitvector_concat}
diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail
index 8a1bfae4..d2e2da47 100644
--- a/test/typecheck/pass/vector_append.sail
+++ b/test/typecheck/pass/vector_append.sail
@@ -1,4 +1,4 @@
-val append = "bitvector_concat" : forall ('l1 : Int) ('l2 : Int) ('o : Order), 'l1 >= 0 & 'l2 >= 0.
+val append = {ocaml: "append", lem: "concat_vec"} : forall ('l1 : Int) ('l2 : Int) ('o : Order), 'l1 >= 0 & 'l2 >= 0.
   (vector('l1, 'o, bit), vector('l2, 'o, bit)) -> vector('l1 + 'l2, 'o, bit)
 
 default Order inc
diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail
index 6ce5bf90..427f8dd7 100644
--- a/test/typecheck/pass/vector_append_gen.sail
+++ b/test/typecheck/pass/vector_append_gen.sail
@@ -1,4 +1,4 @@
-val vector_append = "bitvector_concat": forall 'l1 'l2 ('o : Order), 'l1 >= 0 & 'l2 >= 0.
+val vector_append = {ocaml: "append", lem: "concat_vec"}: forall 'l1 'l2 ('o : Order), 'l1 >= 0 & 'l2 >= 0.
   (vector('l1, 'o, bit), vector('l2, 'o, bit)) -> vector('l1 + 'l2, 'o, bit)
 
 default Order inc
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
index aff87df4..50a93cff 100644
--- a/test/typecheck/pass/vector_subrange_gen.sail
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -4,11 +4,13 @@ val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0.
 val vector_append : forall ('l1 : Int) ('l2 : Int) ('o : Order) ('a : Type), 'l1 >= 0 & 'l2 >= 0.
   (vector('l1, 'o, 'a), vector('l2, 'o, 'a)) -> vector('l1 + 'l2, 'o, 'a)
 
-val vector_subrange = "bitvector_subrange_inc" : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l.
   (vector('l, inc, bit), atom('m), atom('o)) -> vector('o - 'm + 1, inc, bit)
 
 val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm)
 
+val "length" : forall ('n : Int). vector('n, inc, bit) -> atom('n)
+
 default Order inc
 
 val test : forall 'n 'm, 'n >= 5.
diff --git a/test/typecheck/pass/while_MP.sail b/test/typecheck/pass/while_MP.sail
index 60b5fb90..32d351e8 100644
--- a/test/typecheck/pass/while_MP.sail
+++ b/test/typecheck/pass/while_MP.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int
+val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int
 
 overload operator + = {add_vec_int, add_range, add_int}
 
diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail
index 39ecdb2b..c148e6da 100644
--- a/test/typecheck/pass/while_PM.sail
+++ b/test/typecheck/pass/while_PM.sail
@@ -7,16 +7,19 @@ val lt_int = {ocaml: "lt", lem: "lt"}: (int, int) -> bool
 
 overload operator < = {lt_range_atom, lt_int}
 
-val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int
+val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int
 
 overload operator + = {add_range, add_int}
 
-val vector_access = "bitvector_access_dec" : forall ('l : Int), 'l >= 0.
+val vector_access = {ocaml: "access", lem: "access_vec_dec"} : forall ('l : Int), 'l >= 0.
   (vector('l, dec, bit), int) -> bit
 
+val vector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n.
+  (vector('n, dec, bit), int, bit) -> vector('n, dec, bit)
+
 register GPR00 : vector(64, dec, bit)
 
 function test b : bit -> unit = {
diff --git a/test/typecheck/pass/while_PP.sail b/test/typecheck/pass/while_PP.sail
index 557bf963..d982241a 100644
--- a/test/typecheck/pass/while_PP.sail
+++ b/test/typecheck/pass/while_PP.sail
@@ -11,10 +11,10 @@ val mult_int : (int, int) -> int
 
 overload operator * = {mult_int}
 
-val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int
+val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int
 
 overload operator + = {add_range, add_int}