From 6a40f1a1fca791c141c9c4e71dbb1876812666a6 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 12 Dec 2018 18:02:16 +0000
Subject: Add a test for flow typing as found in the ARM 32-bit instructions

---
 test/typecheck/future/bool_constraint.sail    | 45 ------------------------
 test/typecheck/pass/bool_constraint.sail      | 50 +++++++++++++++++++++++++++
 test/typecheck/pass/bool_constraint/v1.expect | 27 +++++++++++++++
 test/typecheck/pass/bool_constraint/v1.sail   | 48 +++++++++++++++++++++++++
 test/typecheck/pass/bool_constraint/v2.expect |  5 +++
 test/typecheck/pass/bool_constraint/v2.sail   | 48 +++++++++++++++++++++++++
 test/typecheck/pass/bool_constraint/v3.expect |  5 +++
 test/typecheck/pass/bool_constraint/v3.sail   | 48 +++++++++++++++++++++++++
 test/typecheck/pass/bool_constraint/v4.expect |  5 +++
 test/typecheck/pass/bool_constraint/v4.sail   | 48 +++++++++++++++++++++++++
 10 files changed, 284 insertions(+), 45 deletions(-)
 delete mode 100644 test/typecheck/future/bool_constraint.sail
 create mode 100644 test/typecheck/pass/bool_constraint.sail
 create mode 100644 test/typecheck/pass/bool_constraint/v1.expect
 create mode 100644 test/typecheck/pass/bool_constraint/v1.sail
 create mode 100644 test/typecheck/pass/bool_constraint/v2.expect
 create mode 100644 test/typecheck/pass/bool_constraint/v2.sail
 create mode 100644 test/typecheck/pass/bool_constraint/v3.expect
 create mode 100644 test/typecheck/pass/bool_constraint/v3.sail
 create mode 100644 test/typecheck/pass/bool_constraint/v4.expect
 create mode 100644 test/typecheck/pass/bool_constraint/v4.sail

(limited to 'test')

diff --git a/test/typecheck/future/bool_constraint.sail b/test/typecheck/future/bool_constraint.sail
deleted file mode 100644
index cce078ef..00000000
--- a/test/typecheck/future/bool_constraint.sail
+++ /dev/null
@@ -1,45 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-val foo : forall ('n : Int) ('b : Bool).
-  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
-
-function foo(b, n) = {
-  if b then n else 3
-}
-
-/* We now allow type synonyms for kinds other that Type */
-
-type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
-
-infixr 1 -->
-
-type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
-
-infix 1 <-->
-
-type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
-
-val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> 'q. bool('q)}
-
-/* This example mimics 32-bit ARM instructions where a flag in the
-function argument restricts a type variable in a specific branch of
-the code */
-
-val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
-  (bool('b), int('n)) -> unit
-
-function test(cond, n) = {
-  if cond then {
-    _prove(constraint('n <= 14))
-  } else {
-    ()
-  };
-
-  if my_not(cond) then {
-    ()
-  } else {
-    _prove(constraint('n <= 14))
-  }
-}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint.sail b/test/typecheck/pass/bool_constraint.sail
new file mode 100644
index 00000000..de6bf4b7
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    _not_prove(constraint('n <= 14));
+    _prove(constraint('n <= 15))
+  };
+
+  if my_not(cond) then {
+    _not_prove(constraint('n <= 14));
+    _prove(constraint('n <= 15))
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
new file mode 100644
index 00000000..3e2c7bde
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -0,0 +1,27 @@
+Type error at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
+
+  if b then n else 4
+
+Tried performing type coercion from int(4) to {'m, ('b & 'm == 'n | not('b) & 'm == 3). int('m)} on 4
+Coercion failed because:
+  int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
+  in context
+  * 4 == 'ex41#m
+  * not('b)
+  where
+  * 'b bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
+
+function foo(b, n) = {
+  if b then n else 4
+}
+
+  * 'ex41#m bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
+
+  if b then n else 4
+
+  * 'n bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
+
+function foo(b, n) = {
+  if b then n else 4
+}
+
diff --git a/test/typecheck/pass/bool_constraint/v1.sail b/test/typecheck/pass/bool_constraint/v1.sail
new file mode 100644
index 00000000..46badd52
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v1.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 4
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect
new file mode 100644
index 00000000..847ef329
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v2.expect
@@ -0,0 +1,5 @@
+Type error at file "bool_constraint/v2.sail", line 38, character 5 to line 38, character 32
+
+    _prove(constraint('n <= 14))
+
+Cannot prove 'n <= 14
diff --git a/test/typecheck/pass/bool_constraint/v2.sail b/test/typecheck/pass/bool_constraint/v2.sail
new file mode 100644
index 00000000..1506bbbd
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v2.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 16 & implies('b, 'n <= 15).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect
new file mode 100644
index 00000000..ca87fac1
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "bool_constraint/v3.sail", line 46, character 5 to line 46, character 32
+
+    _prove(constraint('n <= 14))
+
+Cannot prove 'n <= 14
diff --git a/test/typecheck/pass/bool_constraint/v3.sail b/test/typecheck/pass/bool_constraint/v3.sail
new file mode 100644
index 00000000..966ad2d5
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v3.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> 'q. bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 14))
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect
new file mode 100644
index 00000000..07363175
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v4.expect
@@ -0,0 +1,5 @@
+Type error at file "bool_constraint/v4.sail", line 46, character 5 to line 46, character 32
+
+    _prove(constraint('n <= 13))
+
+Cannot prove 'n <= 13
diff --git a/test/typecheck/pass/bool_constraint/v4.sail b/test/typecheck/pass/bool_constraint/v4.sail
new file mode 100644
index 00000000..9f68bf91
--- /dev/null
+++ b/test/typecheck/pass/bool_constraint/v4.sail
@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+
+/* Test returning an existential with a mixed boolean/integer
+constraint */
+
+val foo : forall ('n : Int) ('b : Bool).
+  (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
+
+function foo(b, n) = {
+  if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+  (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+  if cond then {
+    _prove(constraint('n <= 14))
+  } else {
+    ()
+  };
+
+  if my_not(cond) then {
+    ()
+  } else {
+    _prove(constraint('n <= 13))
+  }
+}
\ No newline at end of file
-- 
cgit v1.2.3