summaryrefslogtreecommitdiff
path: root/test/mono
diff options
context:
space:
mode:
Diffstat (limited to 'test/mono')
-rw-r--r--test/mono/assert.sail1
-rw-r--r--test/mono/builtins.sail2
-rw-r--r--test/mono/castreq.sail14
-rw-r--r--test/mono/castrequnion.sail4
-rw-r--r--test/mono/control_deps.sail4
-rw-r--r--test/mono/exint.sail4
-rw-r--r--test/mono/feature.sail4
-rw-r--r--test/mono/mutrecmono.sail4
-rwxr-xr-xtest/mono/run_tests.sh6
-rw-r--r--test/mono/set.sail9
-rw-r--r--test/mono/times8.sail4
-rw-r--r--test/mono/times8div8.sail5
-rw-r--r--test/mono/varpatterns.sail6
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}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 14:15:18 +0000