Merge branch 'sail2' into rmem_interpreter

13 files changed, 36 insertions, 31 deletions

diff --git a/test/mono/assert.sail b/test/mono/assert.sail
index 46892956..9d941467 100644
--- a/test/mono/assert.sail
+++ b/test/mono/assert.sail
@@ -1,5 +1,6 @@
 $include <smt.sail>
 $include <flow.sail>
+$include <arith.sail>
 default Order dec
 type bits ('n : Int) = vector('n, dec, bit)
 val operator & = "and_bool" : (bool, bool) -> bool
diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail
index 99447d42..770259be 100644
--- a/test/mono/builtins.sail
+++ b/test/mono/builtins.sail
@@ -43,7 +43,7 @@ function test(b) = {
     assert(x != y, "!= by propagation");
     assert(slice(x, 0, 4) == slice(x',0,4), "propagated slice == runtime slice");
     assert(0x3 == slice(y, 4, 4), "literal vs propagated middle slice");
-    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt propagation vs literal");
+    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt propagation vs literal");
     assert(shl_int(5,2) == shl_int(launder_int(5),2), "shl_int");
 }
 
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index 586aa54b..bb1bc952 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -1,5 +1,6 @@
 $include <smt.sail>
 $include <flow.sail>
+$include <arith.sail>
 default Order dec
 type bits ('n : Int) = vector('n, dec, bit)
 val operator & = "and_bool" : (bool, bool) -> bool
@@ -10,8 +11,8 @@ 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}
 val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extzv(v) = extz_vec(sizeof('m),v)
+val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function extzv(m, v) = extz_vec(m,v)
 val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 overload append = {bitvector_concat}
@@ -19,12 +20,13 @@ val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pu
 val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
 overload length = {bitvector_length}
+overload __size = {length}
 
 /* Test generation of casts across case splits (e.g., going from bits('m) to bits(32)) */
 
-val foo : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. bits('m) -> bits('n) effect pure
+val foo : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure
 
-function foo(x) =
+function foo(n, x) =
   let y : bits(16) = extzv(x) in
   match 'n {
     32 => y@y,
@@ -43,9 +45,9 @@ function bar(x) =
    16 => use(x)
   }
 
-val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. bits('m) -> bits('n) effect {undef}
+val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef}
 
-function ret(x) =
+function ret(n, x) =
   let y : bits(16) = extzv(x) in
   match 'n {
     32 => return y@y,
diff --git a/test/mono/castrequnion.sail b/test/mono/castrequnion.sail
index 4729fb11..1eefb2ad 100644
--- a/test/mono/castrequnion.sail
+++ b/test/mono/castrequnion.sail
@@ -4,9 +4,9 @@ $include <prelude.sail>
 val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 
-val foo : forall 'm 'n, 'm in {8,16} & 'n in {16,32,64}. bits('m) -> option(bits('n)) effect pure
+val foo : forall 'm 'n, 'm in {8,16} & 'n in {16,32,64}. (implicit('n), bits('m)) -> option(bits('n)) effect pure
 
-function foo(x) =
+function foo(n, x) =
   let y : bits(16) = sail_zero_extend(x,16) in
   match 'n {
     16 => None(),
diff --git a/test/mono/control_deps.sail b/test/mono/control_deps.sail
index dd3bba65..e97dc0fa 100644
--- a/test/mono/control_deps.sail
+++ b/test/mono/control_deps.sail
@@ -10,8 +10,8 @@ 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}
 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 extz : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function extz(m, v) = extz_vec(m,v)
 val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 overload append = {bitvector_concat}
diff --git a/test/mono/exint.sail b/test/mono/exint.sail
index 65589fb8..639e7d45 100644
--- a/test/mono/exint.sail
+++ b/test/mono/exint.sail
@@ -10,8 +10,8 @@ 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}
 val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extzv(v) = extz_vec(sizeof('m),v)
+val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function extzv(m, v) = extz_vec(m,v)
 val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 overload append = {bitvector_concat}
diff --git a/test/mono/feature.sail b/test/mono/feature.sail
index c7e13e11..c12f79e8 100644
--- a/test/mono/feature.sail
+++ b/test/mono/feature.sail
@@ -10,8 +10,8 @@ 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}
 val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extzv(v) = extz_vec(sizeof('m),v)
+val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function extzv(m, v) = extz_vec(m,v)
 val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 overload append = {bitvector_concat}
diff --git a/test/mono/mutrecmono.sail b/test/mono/mutrecmono.sail
index c5ed1c0d..557a8748 100644
--- a/test/mono/mutrecmono.sail
+++ b/test/mono/mutrecmono.sail
@@ -5,8 +5,8 @@ type bits ('n : Int) = vector('n, dec, bit)
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 overload operator == = {eq_int, eq_vec}
 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 extz : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function extz(m,v) = extz_vec(m,v)
 val UInt = {
   ocaml: "uint",
   lem: "uint",
diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh
index 6a9dedd6..08926aaa 100755
--- a/test/mono/run_tests.sh
+++ b/test/mono/run_tests.sh
@@ -6,9 +6,9 @@ SAILDIR="$DIR/../.."
 TESTSDIR="$DIR"
 OUTPUTDIR="$DIR/test-output"
 
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
+RED='\033[0;91m'
+GREEN='\033[0;92m'
+YELLOW='\033[0;93m'
 NC='\033[0m'
 
 rm -f $DIR/tests.xml
diff --git a/test/mono/set.sail b/test/mono/set.sail
index b7cf4862..74d4693e 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -1,4 +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
@@ -9,11 +10,11 @@ val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n
 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 extz : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function extz(m,v) = extz_vec(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 exts : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function exts(m,v) = exts_vec(m,v)
 
 /* A function which is merely parametrised by a size does not need to be
    monomorphised */
diff --git a/test/mono/times8.sail b/test/mono/times8.sail
index 56b1d209..be672446 100644
--- a/test/mono/times8.sail
+++ b/test/mono/times8.sail
@@ -10,8 +10,8 @@ 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}
 val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extzv(v) = extz_vec(sizeof('m),v)
+val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function extzv(m,v) = extz_vec(m,v)
 val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 overload append = {bitvector_concat}
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail
index 31f63fda..a5fd1c37 100644
--- a/test/mono/times8div8.sail
+++ b/test/mono/times8div8.sail
@@ -1,5 +1,6 @@
 $include <smt.sail>
 $include <flow.sail>
+$include <arith.sail>
 default Order dec
 type bits ('n : Int) = vector('n, dec, bit)
 val operator & = "and_bool" : (bool, bool) -> bool
@@ -10,8 +11,8 @@ 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}
 val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extzv(v) = extz_vec(sizeof('m),v)
+val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+function extzv(m,v) = extz_vec(m,v)
 val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 overload append = {bitvector_concat}
diff --git a/test/mono/varpatterns.sail b/test/mono/varpatterns.sail
index 9de412ac..b2c9e7ee 100644
--- a/test/mono/varpatterns.sail
+++ b/test/mono/varpatterns.sail
@@ -35,7 +35,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 }), "UInt");
+    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
 }
 
 val test2 : bool -> unit effect {escape}
@@ -43,7 +43,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 }), "UInt");
+    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
 }
 
 val test_mult : {|4,8|} -> unit effect {escape}
@@ -51,7 +51,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 }), "UInt");
+    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
 }
 
 val run : unit -> unit effect {escape}