Merge branch 'sail2' into rmem_interpreter

4 files changed, 56 insertions, 0 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