summaryrefslogtreecommitdiff
path: root/test/mono
diff options
context:
space:
mode:
Diffstat (limited to 'test/mono')
-rw-r--r--test/mono/assert2.sail13
-rw-r--r--test/mono/atomsplit.sail13
-rw-r--r--test/mono/not-yet/union-exist_manual1
-rw-r--r--test/mono/pass/union-exist (renamed from test/mono/not-yet/union-exist)0
-rw-r--r--test/mono/pass/union-exist21
-rw-r--r--test/mono/pass/union-exist_manual1
-rw-r--r--test/mono/set.sail11
-rw-r--r--test/mono/union-exist.sail25
-rw-r--r--test/mono/union-exist2.sail31
-rw-r--r--test/mono/varpatterns.sail37
10 files changed, 51 insertions, 82 deletions
diff --git a/test/mono/assert2.sail b/test/mono/assert2.sail
index edf92710..90874b68 100644
--- a/test/mono/assert2.sail
+++ b/test/mono/assert2.sail
@@ -1,14 +1,5 @@
-$include <smt.sail>
-$include <flow.sail>
default Order dec
-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
-overload operator == = {eq_int, eq_vec}
-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}
+$include <prelude.sail>
/* Should find a set constraint below the let */
@@ -28,4 +19,4 @@ val run : unit -> unit effect {escape}
function run () = {
f(8);
f(16);
-} \ No newline at end of file
+}
diff --git a/test/mono/atomsplit.sail b/test/mono/atomsplit.sail
index 6e5d3e3b..23a1b0fb 100644
--- a/test/mono/atomsplit.sail
+++ b/test/mono/atomsplit.sail
@@ -1,14 +1,5 @@
-$include <smt.sail>
-$include <flow.sail>
default Order dec
-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
-overload operator == = {eq_int, eq_vec}
-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}
+$include <prelude.sail>
/* Test splitting required because there's a size calculation in the function */
@@ -27,4 +18,4 @@ val run : unit -> unit effect {escape}
function run () = {
foo(2);
foo(4);
-} \ No newline at end of file
+}
diff --git a/test/mono/not-yet/union-exist_manual b/test/mono/not-yet/union-exist_manual
deleted file mode 100644
index d35c3d48..00000000
--- a/test/mono/not-yet/union-exist_manual
+++ /dev/null
@@ -1 +0,0 @@
-union-exist.sail -mono_split union-exist.sail:9:v \ No newline at end of file
diff --git a/test/mono/not-yet/union-exist b/test/mono/pass/union-exist
index ebb89267..ebb89267 100644
--- a/test/mono/not-yet/union-exist
+++ b/test/mono/pass/union-exist
diff --git a/test/mono/pass/union-exist2 b/test/mono/pass/union-exist2
new file mode 100644
index 00000000..9852a125
--- /dev/null
+++ b/test/mono/pass/union-exist2
@@ -0,0 +1 @@
+union-exist2.sail -auto_mono
diff --git a/test/mono/pass/union-exist_manual b/test/mono/pass/union-exist_manual
new file mode 100644
index 00000000..54deb7d8
--- /dev/null
+++ b/test/mono/pass/union-exist_manual
@@ -0,0 +1 @@
+union-exist.sail -mono_split union-exist.sail:10:v
diff --git a/test/mono/set.sail b/test/mono/set.sail
index 74d4693e..4b97aeef 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -1,14 +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
-val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
-overload operator == = {eq_int, eq_vec}
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
- (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-overload operator * = {mult_range, mult_int, mult_real}
+$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
function extz(m,v) = extz_vec(m,v)
diff --git a/test/mono/union-exist.sail b/test/mono/union-exist.sail
index f1e01e75..ca953b3c 100644
--- a/test/mono/union-exist.sail
+++ b/test/mono/union-exist.sail
@@ -1,32 +1,23 @@
default Order dec
-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
-val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
-overload operator == = {eq_int, eq_vec}
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
- (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
-
+$include <prelude.sail>
union myunion = {
- MyConstr : {'n, 'n in {8,16}. (atom('n),bits('n))}
+ MyConstr : {'n, 'n in {8,16}. (int('n),bits('n))}
}
val make : bits(2) -> myunion
function make(v) =
- /* Can't mention these below without running into exp/nexp parsing conflict! */
- let eight = 8 in let sixteen = 16 in
- let r : {'n, 'n in {8,16}. (atom('n),bits('n))} = match v {
- 0b00 => ( eight, 0x12),
- 0b01 => (sixteen,0x1234),
- 0b10 => ( eight, 0x56),
- 0b11 => (sixteen,0x5678)
+ let r : {'n, 'n in {8,16}. (int('n),bits('n))} = match v {
+ 0b00 => ( 8, 0x12),
+ 0b01 => (16,0x1234),
+ 0b10 => ( 8, 0x56),
+ 0b11 => (16,0x5678)
} in MyConstr(r)
val use : myunion -> bits(32)
-function use(MyConstr((n,v) as (atom('n),bits('n)))) = extz(v)
+function use(MyConstr(n,v)) = sail_zero_extend(v,32)
val run : unit -> unit effect {escape}
diff --git a/test/mono/union-exist2.sail b/test/mono/union-exist2.sail
new file mode 100644
index 00000000..aede3c0d
--- /dev/null
+++ b/test/mono/union-exist2.sail
@@ -0,0 +1,31 @@
+default Order dec
+$include <prelude.sail>
+
+union myunion = {
+ MyConstr : {'n 'm 'o, 'n in {8,16} & 'o in {8,16} & 'n <= 'm & 'm <= 'o. (int('n),bits('n),int('o),bits('o),int('m))}
+}
+
+val make : bits(2) -> myunion
+
+function make(v) =
+ let (n,v,m) : {'n 'm, 'n in {8,16} & 'm in {8,16} & 'n <= 'm. (int('n),bits('n),int('m))} = match v {
+ 0b00 => ( 8, 0x12, 8),
+ 0b01 => (16,0x1234,16),
+ 0b10 => ( 8, 0x56,16),
+ 0b11 => (16,0x5678,16)
+ } in
+ let w = sail_zero_extend(0x5,m) in
+ MyConstr(n,v,m,w,m)
+
+val use : myunion -> bits(32)
+
+function use(MyConstr(n,v,_,_,_)) = sail_zero_extend(v,32)
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+ assert(use(make(0b00)) == 0x00000012);
+ assert(use(make(0b01)) == 0x00001234);
+ assert(use(make(0b10)) == 0x00000056);
+ assert(use(make(0b11)) == 0x00005678);
+}
diff --git a/test/mono/varpatterns.sail b/test/mono/varpatterns.sail
index b2c9e7ee..a583cbfc 100644
--- a/test/mono/varpatterns.sail
+++ b/test/mono/varpatterns.sail
@@ -1,32 +1,5 @@
-$include <smt.sail>
-$include <flow.sail>
default Order dec
-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
-overload operator == = {eq_int, eq_vec}
-val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
-function neq_vec (x, y) = not_bool(eq_vec(x, y))
-overload operator != = {neq_atom, neq_vec}
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
- (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
-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 "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 UInt = {
- ocaml: "uint",
- lem: "uint",
- interpreter: "uint",
- c: "sail_uint"
-} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
-val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
-val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
- (bits('m), int, atom('n)) -> bits('n)
+$include <prelude.sail>
/* Test constant propagation on some variable patterns in let expressions */
@@ -35,7 +8,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 }) : int, "UInt");
+ assert(unsigned(x) == (match n { 8 => 18, 16 => 4660 }) : int, "unsigned");
}
val test2 : bool -> unit effect {escape}
@@ -43,7 +16,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 }) : int, "UInt");
+ assert(unsigned(x) == (match n { 8 => 18, 16 => 4660 }) : int, "unsigned");
}
val test_mult : {|4,8|} -> unit effect {escape}
@@ -51,7 +24,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 }) : int, "UInt");
+ assert(unsigned(x) == (match n { 8 => 18, 16 => 4660 }) : int, "unsigned");
}
val run : unit -> unit effect {escape}
@@ -63,4 +36,4 @@ function run() = {
test2(false);
test_mult(4);
test_mult(8);
-} \ No newline at end of file
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 02:25:19 +0000