From 47f1892406b5c10d06eb99af40d4523b93b2f254 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 7 Dec 2017 19:53:14 +0000
Subject: More OCaml test cases

Improved handling of try/catch

Better handling of unprovable constraints when the environment contains
false
---
 test/ocaml/trycatch/expect  |  2 ++
 test/ocaml/trycatch/tc.sail | 23 +++++++++++++++++++++++
 test/ocaml/void/expect      |  1 +
 test/ocaml/void/void.sail   | 14 ++++++++++++++
 4 files changed, 40 insertions(+)
 create mode 100644 test/ocaml/trycatch/expect
 create mode 100644 test/ocaml/trycatch/tc.sail
 create mode 100644 test/ocaml/void/expect
 create mode 100644 test/ocaml/void/void.sail

(limited to 'test')

diff --git a/test/ocaml/trycatch/expect b/test/ocaml/trycatch/expect
new file mode 100644
index 00000000..0aab34df
--- /dev/null
+++ b/test/ocaml/trycatch/expect
@@ -0,0 +1,2 @@
+Before throw
+Caught!
diff --git a/test/ocaml/trycatch/tc.sail b/test/ocaml/trycatch/tc.sail
new file mode 100644
index 00000000..b805f3fa
--- /dev/null
+++ b/test/ocaml/trycatch/tc.sail
@@ -0,0 +1,23 @@
+
+scattered union exception
+
+union clause exception = Test_int : int
+
+union clause exception = Test_failure : string
+
+val main : unit -> unit effect {escape}
+
+function main () = {
+  try {
+    print("Before throw");
+    throw(Test_failure("Caught!"));
+    print("Not printed")
+  } catch {
+    Test_failure(msg) => print(msg),
+    _ => print("Unknown exception")
+  }
+}
+
+union clause exception = Test_other
+
+end exception
\ No newline at end of file
diff --git a/test/ocaml/void/expect b/test/ocaml/void/expect
new file mode 100644
index 00000000..559bf40a
--- /dev/null
+++ b/test/ocaml/void/expect
@@ -0,0 +1 @@
+Before
diff --git a/test/ocaml/void/void.sail b/test/ocaml/void/void.sail
new file mode 100644
index 00000000..485ac019
--- /dev/null
+++ b/test/ocaml/void/void.sail
@@ -0,0 +1,14 @@
+
+val void : forall 'n, 'n = 'n + 1. atom('n) -> unit
+
+function void _ = ()
+
+val main : unit -> unit
+
+function main () = {
+  print("Before");
+  if false then {
+    print("After");
+    void(0);
+  }
+}
\ No newline at end of file
-- 
cgit v1.2.3