From 0da6c4482f2a68d8cde54c5261be6d715d5ce63c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 13 Mar 2018 17:26:40 +0000
Subject: Add test for mutual recursion and monomorphisation

---
 test/mono/mutrecmono.sail | 33 +++++++++++++++++++++++++++++++++
 test/mono/pass/mutrecmono |  1 +
 2 files changed, 34 insertions(+)
 create mode 100644 test/mono/mutrecmono.sail
 create mode 100644 test/mono/pass/mutrecmono

(limited to 'test')

diff --git a/test/mono/mutrecmono.sail b/test/mono/mutrecmono.sail
new file mode 100644
index 00000000..c5ed1c0d
--- /dev/null
+++ b/test/mono/mutrecmono.sail
@@ -0,0 +1,33 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+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. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extz(v) = extz_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 a : {|8,16,32|} -> int
+val b : {|8,16,32|} -> int
+
+function a 'n = if n == 8 then b(n) else let x : bits('n) = extz(0x12) in UInt(x)
+function b 'n = if n == 32 then a(n) else let x : bits('n) = extz(0x34) in UInt(x)
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(a(8) == 52);
+  assert(a(16) == 18);
+  assert(a(32) == 18);
+  assert(b(8) == 52);
+  assert(b(16) == 52);
+  assert(a(32) == 18);
+}
\ No newline at end of file
diff --git a/test/mono/pass/mutrecmono b/test/mono/pass/mutrecmono
new file mode 100644
index 00000000..1ad1508d
--- /dev/null
+++ b/test/mono/pass/mutrecmono
@@ -0,0 +1 @@
+mutrecmono.sail -auto_mono
-- 
cgit v1.2.3