8 files changed, 124 insertions, 7 deletions

diff --git a/test/typecheck/future/bool_constraint.sail b/test/typecheck/future/bool_constraint.sail
index 53994630..cce078ef 100644
--- a/test/typecheck/future/bool_constraint.sail
+++ b/test/typecheck/future/bool_constraint.sail
@@ -7,4 +7,39 @@ val foo : forall ('n : Int) ('b : Bool).
 
 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/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index e4e4fa55..a647ef00 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1,3 +1,3 @@
 Type error at no location information available
 
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8)
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index 622b5fd7..d8bad777 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1,3 +1,3 @@
 Type error at no location information available
 
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8)
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index c7e06dc7..43096686 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch
 
 val test : forall 'size. atom('size) -> unit
 
-type variable 'size is already bound
+type variable ('size : Int) is already bound
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 06df7dc5..95073799 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -4,13 +4,13 @@ Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, charact
 
 No overloadings for vector_access, tried:
   bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 3)
+    Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 3)
     
     Try adding named type variables for 
     
     
   plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 'ex44#ex43# & ('ex44#ex43# + 1) <= 3)
+    Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 3)
     
     Try adding named type variables for 
     
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 050e90e4..afa04343 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -4,13 +4,13 @@ Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, charact
 
 No overloadings for vector_access, tried:
   bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 4)
+    Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 4)
     
     Try adding named type variables for 
     
     
   plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 'ex44#ex43# & ('ex44#ex43# + 1) <= 4)
+    Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 4)
     
     Try adding named type variables for 
     
diff --git a/test/typecheck/pass/tautology.sail b/test/typecheck/pass/tautology.sail
new file mode 100644
index 00000000..f1c8bade
--- /dev/null
+++ b/test/typecheck/pass/tautology.sail
@@ -0,0 +1,65 @@
+
+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 tautologies :  forall ('p : Bool) ('q : Bool) ('r : Bool). (bool('p), bool('q), bool('r)) -> unit effect {escape}
+
+function tautologies(p, q, r) = {
+  _not_prove(constraint('p));
+  _not_prove(constraint('q));
+  _not_prove(constraint('r));
+
+  // implication definition
+  _prove(constraint(not('p) | 'q --> ('p --> 'q)));
+  _prove(constraint(('p --> 'q) --> not('p) | 'q));
+  _prove(constraint(('p --> 'q) <--> not('p) | 'q));
+
+  // implication properties
+  _prove(constraint('p --> 'p));
+  _prove(constraint(('p --> 'q) & ('q --> 'r) --> ('p --> 'r)));
+  _prove(constraint(('p --> 'q) & 'p --> 'q));
+
+  _prove(constraint('p & 'q <--> 'q & 'p));
+  _prove(constraint('p | 'q <--> 'q | 'p));
+  _prove(constraint(('p <--> 'q) <--> ('q <--> 'p)));
+
+  // excluded middle
+  _prove(constraint('p | not('p)));
+
+  // de Morgan
+  _prove(constraint(not('p | 'q) <--> not('p) & not('q)));
+  _prove(constraint(not('p & 'q) <--> not('p) | not('q)));
+
+  // contradiction
+  _prove(constraint('p & not('p) --> false));
+  {
+    assert(constraint('p & not('p)));
+    _prove(constraint(false))
+  };
+  _not_prove(constraint(false));
+
+  _prove(constraint(('p <--> 'q) & ('p | 'q) --> ('p & 'q)));
+  _prove(constraint(('p & 'q --> 'r) <--> ('p --> 'q --> 'r)));
+
+  {
+    assert(constraint('p));
+    _prove(constraint('p))
+  };
+  _not_prove(constraint('p));
+
+  {
+    assert(constraint('p));
+    assert(constraint('p --> 'q));
+    _prove(constraint('q));
+    assert(constraint('q --> 'r));
+    _prove(constraint('r))
+  };
+  _not_prove(constraint('q));
+}
\ No newline at end of file
diff --git a/test/typecheck/update_errors.sh b/test/typecheck/update_errors.sh
new file mode 100755
index 00000000..ba436daf
--- /dev/null
+++ b/test/typecheck/update_errors.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+
+
+for i in `ls $DIR/pass/ | grep sail`;
+do
+    shopt -s nullglob;
+    for file in $DIR/pass/${i%.sail}/*.sail;
+    do
+	pushd $DIR/pass > /dev/null;
+	$SAILDIR/sail ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
+	popd > /dev/null
+    done
+done