9 files changed, 239 insertions, 0 deletions

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/future/bool_constraint.sail b/test/typecheck/pass/bool_constraint/v3.sail
index cce078ef..966ad2d5 100644
--- a/test/typecheck/future/bool_constraint.sail
+++ b/test/typecheck/pass/bool_constraint/v3.sail
@@ -2,6 +2,9 @@ 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)}
 
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