6 files changed, 74 insertions, 1 deletions
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index b1df7010..75791bfd 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -93,6 +93,33 @@ function assign3(x) = {
   y
 }
 
+/* Test that matching on a variable which happens to fix a bitvector variable's
+   size updates the environment properly. */
+
+val assign4 : forall 'm, 'm in {1,2}. (implicit('m),bits(8*'m)) -> bits(8*'m)
+
+function assign4(m,x) = {
+  y : bits(8*'m) = x;
+  match m {
+    1 => y = y + 0x01,
+    2 => y[7..0] = 0x89
+  };
+  y
+}
+
+/* The same as assign4, except with a distinct type variable. */
+
+val assign5 : forall 'm 'n, 'm in {1,2} & 'n == 8 * 'm. (implicit('m),bits('n)) -> bits('n)
+
+function assign5(m,x) = {
+  y : bits('n) = x;
+  match m {
+    1 => y = y + 0x01,
+    2 => y[7..0] = 0x89
+  };
+  y
+}
+
 /* Adding casts for top-level pattern matches */
 
 val foo2 : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (atom('n), bits('m)) -> bits('n) effect pure
@@ -140,6 +167,10 @@ function run () = {
     assert(assign2(0x1234) == 0x00001234);
     assert(assign3(0x12) == 0x13);
     assert(assign3(0x1234) == 0x1289);
+    assert(assign4(0x12) == 0x13);
+    assert(assign4(0x1234) == 0x1289);
+    assert(assign5(0x12) == 0x13);
+    assert(assign5(0x1234) == 0x1289);
     assert(foo2(32,0x12) == 0x00120012);
     assert(foo2(64,0x12) == 0x0012001200120012);
     assert(foo3(4,0x12) == 0x00120012);
diff --git a/test/mono/nonlinearpat.sail b/test/mono/nonlinearpat.sail
new file mode 100644
index 00000000..e0aaeff3
--- /dev/null
+++ b/test/mono/nonlinearpat.sail
@@ -0,0 +1,17 @@
+default Order dec
+$include <prelude.sail>
+
+val test : forall 'n, 'n in {8,16}. (int('n),int('n),bits(1)) -> bits(64) effect pure
+
+function test(x,y,b) = {
+  let 'z = x + y in
+  let v : bits('z) = sail_zero_extend(b,z) in
+  sail_zero_extend(v,64)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(test(8,8,0b0) == 0x0000000000000000);
+  assert(test(16,16,0b1) == 0x0000000000000001);
+}
diff --git a/test/mono/pass/nonlinearpat b/test/mono/pass/nonlinearpat
new file mode 100644
index 00000000..3f235d60
--- /dev/null
+++ b/test/mono/pass/nonlinearpat
@@ -0,0 +1 @@
+nonlinearpat.sail -auto_mono
diff --git a/test/mono/pass/union_split b/test/mono/pass/union_split
new file mode 100644
index 00000000..cdd2763d
--- /dev/null
+++ b/test/mono/pass/union_split
@@ -0,0 +1 @@
+union_split.sail -auto_mono
diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh
index d2023229..f95dc7d5 100755
--- a/test/mono/run_tests.sh
+++ b/test/mono/run_tests.sh
@@ -72,7 +72,7 @@ do
                "$SAILDIR/src/gen_lib/sail2_values.lem" \
                "$SAILDIR/src/gen_lib/sail2_operators.lem" \
                "$SAILDIR/src/gen_lib/sail2_operators_mwords.lem" \
-               "$SAILDIR/src/lem_interp/sail2_instr_kinds.lem" \
+               "$SAILDIR/src/gen_lib/sail2_instr_kinds.lem" \
                "$SAILDIR/src/gen_lib/sail2_prompt.lem" \
                "$SAILDIR/src/gen_lib/sail2_state_monad.lem" \
                "$SAILDIR/src/gen_lib/sail2_state.lem" \
diff --git a/test/mono/union_split.sail b/test/mono/union_split.sail
new file mode 100644
index 00000000..2403e644
--- /dev/null
+++ b/test/mono/union_split.sail
@@ -0,0 +1,23 @@
+default Order dec
+$include <prelude.sail>
+
+/* Simple case split example on a variant datatype */
+
+union ast = {
+  SomeOp : {'n, 'n in {8,16}. (int('n),bits('n))}
+}
+
+val execute : ast -> bits(32)
+
+function execute(SomeOp(n as int('n),v)) = {
+  a : bits('n) = sail_zero_extend(0x12,n);
+  b : bits('n) = and_vec(v, a);
+  sail_zero_extend(b,32)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(execute(SomeOp(8,0x11)) == 0x00000010);
+  assert(execute(SomeOp(16,0x3333)) == 0x00000012);
+}