summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/mono/assert.sail2
-rw-r--r--test/mono/builtins.sail3
-rw-r--r--test/mono/castreq.sail6
-rw-r--r--test/mono/control_deps.sail6
-rw-r--r--test/mono/exint.sail6
-rw-r--r--test/mono/feature.sail6
-rw-r--r--test/mono/itself_rewriting.sail2
-rw-r--r--test/mono/mutrecmono.sail6
-rw-r--r--test/mono/set.sail8
-rw-r--r--test/mono/times8.sail6
-rw-r--r--test/mono/times8div8.sail6
-rw-r--r--test/mono/vector.sail2
12 files changed, 30 insertions, 29 deletions
diff --git a/test/mono/assert.sail b/test/mono/assert.sail
index 9d941467..a7c148bd 100644
--- a/test/mono/assert.sail
+++ b/test/mono/assert.sail
@@ -2,7 +2,7 @@ $include <smt.sail>
$include <flow.sail>
$include <arith.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail
index 770259be..8f00ac56 100644
--- a/test/mono/builtins.sail
+++ b/test/mono/builtins.sail
@@ -1,9 +1,10 @@
+default Order dec
+
$include <smt.sail>
$include <arith.sail>
$include <flow.sail>
$include <vector_dec.sail>
-default Order dec
val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
function neq_vec (x, y) = not_bool(x == y)
overload operator != = {neq_vec}
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index ce7080c4..2cd0ab9c 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -2,7 +2,7 @@ $include <smt.sail>
$include <flow.sail>
$include <arith.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
@@ -10,8 +10,8 @@ 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}
-val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) 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)
diff --git a/test/mono/control_deps.sail b/test/mono/control_deps.sail
index e97dc0fa..c3354840 100644
--- a/test/mono/control_deps.sail
+++ b/test/mono/control_deps.sail
@@ -1,7 +1,7 @@
$include <smt.sail>
$include <flow.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
@@ -9,8 +9,8 @@ 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}
-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
+val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extz : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) 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)
diff --git a/test/mono/exint.sail b/test/mono/exint.sail
index 855b689c..86463d8c 100644
--- a/test/mono/exint.sail
+++ b/test/mono/exint.sail
@@ -1,7 +1,7 @@
$include <smt.sail>
$include <flow.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
@@ -9,8 +9,8 @@ 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}
-val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) 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)
diff --git a/test/mono/feature.sail b/test/mono/feature.sail
index c12f79e8..472de0ba 100644
--- a/test/mono/feature.sail
+++ b/test/mono/feature.sail
@@ -1,7 +1,7 @@
$include <smt.sail>
$include <flow.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
@@ -9,8 +9,8 @@ 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}
-val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) 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)
diff --git a/test/mono/itself_rewriting.sail b/test/mono/itself_rewriting.sail
index f3c5ed62..0501cf1e 100644
--- a/test/mono/itself_rewriting.sail
+++ b/test/mono/itself_rewriting.sail
@@ -1,7 +1,7 @@
$include <smt.sail>
$include <flow.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
diff --git a/test/mono/mutrecmono.sail b/test/mono/mutrecmono.sail
index 557a8748..cc7a69c7 100644
--- a/test/mono/mutrecmono.sail
+++ b/test/mono/mutrecmono.sail
@@ -1,11 +1,11 @@
$include <smt.sail>
$include <flow.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extz : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
function extz(m,v) = extz_vec(m,v)
val UInt = {
ocaml: "uint",
diff --git a/test/mono/set.sail b/test/mono/set.sail
index 4b97aeef..770b5bf1 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -1,10 +1,10 @@
default Order dec
$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
+val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extz : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) 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. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val "exts_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val exts : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
function exts(m,v) = exts_vec(m,v)
/* A function which is merely parametrised by a size does not need to be
diff --git a/test/mono/times8.sail b/test/mono/times8.sail
index be672446..e94d769b 100644
--- a/test/mono/times8.sail
+++ b/test/mono/times8.sail
@@ -1,7 +1,7 @@
$include <smt.sail>
$include <flow.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
@@ -9,8 +9,8 @@ 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}
-val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) 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)
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail
index a5fd1c37..1deb571f 100644
--- a/test/mono/times8div8.sail
+++ b/test/mono/times8div8.sail
@@ -2,7 +2,7 @@ $include <smt.sail>
$include <flow.sail>
$include <arith.sail>
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
@@ -10,8 +10,8 @@ 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}
-val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) 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)
diff --git a/test/mono/vector.sail b/test/mono/vector.sail
index 93cc2d41..1e884908 100644
--- a/test/mono/vector.sail
+++ b/test/mono/vector.sail
@@ -1,5 +1,5 @@
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
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}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 03:52:05 +0000