10 files changed, 153 insertions, 3 deletions
diff --git a/test/c/nonexistent_pragma.expect b/test/c/nonexistent_pragma.expect
new file mode 100644
index 00000000..9daeafb9
--- /dev/null
+++ b/test/c/nonexistent_pragma.expect
@@ -0,0 +1 @@
+test
diff --git a/test/c/nonexistent_pragma.sail b/test/c/nonexistent_pragma.sail
new file mode 100644
index 00000000..da4b99f7
--- /dev/null
+++ b/test/c/nonexistent_pragma.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$not_a_valid_pragma test
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  print_endline("test")
+}
+
diff --git a/test/c/unroll.expect b/test/c/unroll.expect
new file mode 100644
index 00000000..355943c1
--- /dev/null
+++ b/test/c/unroll.expect
@@ -0,0 +1,6 @@
+fac(4) = 24
+fac(5) = 120
+fac(6) = 720
+fac2(4) = 24
+fac2(5) = 120
+fac2(6) = 720
diff --git a/test/c/unroll.sail b/test/c/unroll.sail
new file mode 100644
index 00000000..c68bb49d
--- /dev/null
+++ b/test/c/unroll.sail
@@ -0,0 +1,37 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* It's hard to test that this optimization does the right thing, but
+we can at least test that it doesn't do the wrong thing. */
+
+$optimize unroll 20
+val fac : forall 'n, 'n >= 0. int('n) -> int
+function fac(n) = {
+  if n == 0 then {
+    1
+  } else {
+    n * fac(n - 1)
+  }
+}
+
+$optimize unroll 2
+val fac2 : forall 'n, 'n >= 0. int('n) -> int
+function fac2(n) = {
+  if n == 0 then {
+    1
+  } else {
+    n * fac2(n - 1)
+  }
+}
+
+val "print_int" : (string, int) -> unit
+
+function main((): unit) -> unit = {
+  print_int("fac(4) = ", fac(4));
+  print_int("fac(5) = ", fac(5));
+  print_int("fac(6) = ", fac(6));
+  print_int("fac2(4) = ", fac2(4));
+  print_int("fac2(5) = ", fac2(5));
+  print_int("fac2(6) = ", fac2(6))
+}
+\ No newline at end of file
diff --git a/test/isabelle/Makefile b/test/isabelle/Makefile
index 43028fed..1f488db1 100644
--- a/test/isabelle/Makefile
+++ b/test/isabelle/Makefile
@@ -1,7 +1,13 @@
-CHERI_DIR = ../../cheri
-AARCH64_DIR = ../../aarch64
+LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib
+ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),)
+$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable)
+endif
+
+SAIL_ISA_LIB = ../../lib/isabelle
+CHERI_DIR ?= ../../../sail-cheri-mips/cheri
+AARCH64_DIR ?= ../../aarch64
 TGTS = run_cheri.native run_aarch64.native
-SESSION_DIRS = -d $(CHERI_DIR) -d $(AARCH64_DIR) -d .
+SESSION_DIRS = -d $(LEM_ISA_LIB) -d $(SAIL_ISA_LIB) -d $(CHERI_DIR) -d $(AARCH64_DIR) -d .
 
 .PHONY: all clean
 
diff --git a/test/mono/castrequnion.sail b/test/mono/castrequnion.sail
new file mode 100644
index 00000000..4729fb11
--- /dev/null
+++ b/test/mono/castrequnion.sail
@@ -0,0 +1,58 @@
+default Order dec
+$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
+
+function foo(x) =
+  let y : bits(16) = sail_zero_extend(x,16) in
+  match 'n {
+    16 => None(),
+    32 => Some(y@y),
+    64 => let z = y@y@y@y in let dfsf = 4 in Some(z)
+  }
+
+union Result ('a : Type) = {
+  Value : ('a, int),
+  Complaint : string
+}
+
+/* Getting ahead of myself: the 2*'n isn't supported yet, although shouldn't it end up in the form below?
+*/
+val bar : forall 'n, 'n in {8,16,32}. bits('n) -> Result(bits(2*'n))
+
+function bar(x) =
+  match 'n {
+    8 => Complaint("No bytes"),
+   16 => Value(x@x, unsigned(x)),
+   32 => Value(sail_sign_extend(x,64), unsigned(x))
+  }
+/*
+val bar : forall 'n 'm, 'n in {8,16,32} & 'm == 2*'n. bits('n) -> Result(bits('m))
+
+function bar(x) =
+  match 'n {
+    8 => Complaint("No bytes"),
+   16 => Value(x@x, unsigned(x)),
+   32 => Value(sail_sign_extend(x,64), unsigned(x))
+  }
+*/
+
+val cmp : forall 'n. (option(bits('n)), option(bits('n))) -> bool
+
+function cmp (None(),None()) = true
+and cmp (None(),Some(_)) = false
+and cmp (Some(_),None()) = false
+and cmp (Some(x),Some(y)) = x == y
+
+overload operator == = {cmp}
+
+val run : unit -> unit effect {escape}
+
+function run() = {
+  assert((foo(0x12) : option(bits(16))) == None());
+  assert((foo(0x12) : option(bits(32))) == Some(0x00120012));
+  assert((foo(0x12) : option(bits(64))) == Some(0x0012001200120012));
+}
diff --git a/test/mono/flow_extend.sail b/test/mono/flow_extend.sail
new file mode 100644
index 00000000..7e118993
--- /dev/null
+++ b/test/mono/flow_extend.sail
@@ -0,0 +1,16 @@
+default Order dec
+$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 byte_extend : forall 'n, 'n >= 8. (bits(8), int('n)) -> bits('n)
+
+function byte_extend (v, n) = if (n == 8) then v else sail_zero_extend(v, n)
+
+val run : unit -> unit effect {escape}
+
+function run() = {
+  assert(byte_extend(0x12,8) == 0x12);
+  assert(byte_extend(0x12,16) == 0x0012);
+}
diff --git a/test/mono/pass/castrequnion b/test/mono/pass/castrequnion
new file mode 100644
index 00000000..9b2a2f38
--- /dev/null
+++ b/test/mono/pass/castrequnion
@@ -0,0 +1 @@
+castrequnion.sail -auto_mono
diff --git a/test/mono/pass/flow_extend b/test/mono/pass/flow_extend
new file mode 100644
index 00000000..fea386e5
--- /dev/null
+++ b/test/mono/pass/flow_extend
@@ -0,0 +1 @@
+flow_extend.sail -auto_mono
diff --git a/test/typecheck/pass/nonexistent_pragma.sail b/test/typecheck/pass/nonexistent_pragma.sail
new file mode 100644
index 00000000..da4b99f7
--- /dev/null
+++ b/test/typecheck/pass/nonexistent_pragma.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+
+$not_a_valid_pragma test
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  print_endline("test")
+}
+