From d6cd7d2069e780cfc4ae13e98be1d0c802a89b9d Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Fri, 14 Dec 2018 02:26:33 +0000
Subject: A few additional tests

---
 test/typecheck/pass/custom_flow.sail | 43 ++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 test/typecheck/pass/custom_flow.sail

(limited to 'test/typecheck')

diff --git a/test/typecheck/pass/custom_flow.sail b/test/typecheck/pass/custom_flow.sail
new file mode 100644
index 00000000..43c980d6
--- /dev/null
+++ b/test/typecheck/pass/custom_flow.sail
@@ -0,0 +1,43 @@
+val "print_endline" : string -> unit
+
+val operator <= = {
+  coq: "Z.leb",
+  _: "lteq"
+} : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+function test1 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  if n <= m then {
+    _prove(constraint('n <= 'm));
+    print_endline("1");
+  } else {
+    print_endline("2");
+    _prove(constraint('n > 'm));
+  }
+}
+
+val and_bool = {
+  coq: "andb",
+  _: "and_bool"
+} : forall ('p: Bool) ('q: Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+overload operator & = {and_bool}
+
+function test2 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  let x = n <= m & n <= 20;
+  if x then {
+    _prove(constraint('n <= 20));
+    _prove(constraint('n <= 'm));
+    print_endline("3")
+  } else {
+    _prove(constraint('n > 'm | 'n > 20));
+    print_endline("4")
+  }
+}
+
+function main((): unit) -> unit = {
+  test1(1, 2);
+  test1(2, 1);
+  test2(1, 2);
+  test2(2, 1);
+  test2(21, 0)
+}
\ No newline at end of file
-- 
cgit v1.2.3