Add a test case for various simple boolean properties

test/typecheck/pass/tautology.sail constaints tests of various boolean
properties, e.g.

  // de Morgan
  _prove(constraint(not('p | 'q) <--> not('p) & not('q)));
  _prove(constraint(not('p & 'q) <--> not('p) | not('q)));

introduce a new _not_prove case which allows us to assert in tests
that a constraint is not provable. This test essentially tests that
constraints map to sensible problems in the SMT solver, without
testing flow typing or any other features.

Add a script test/typecheck/update_errors.sh, which regenerates the
expected error messages. Testing that type-checking failures is
important, but can be brittle when the error messages change for
inconsequential reasons. This script automates fixing this.

Also ensure that this test case works correctly in Lem

1 files changed, 5 insertions, 3 deletions

diff --git a/src/parser.mly b/src/parser.mly
index 544438c0..1957d7fd 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -78,6 +78,8 @@ let prepend_id str1 = function
 let mk_id i n m = Id_aux (i, loc n m)
 let mk_kid str n m = Kid_aux (Var str, loc n m)
 
+let mk_kopt k n m = KOpt_aux (k, loc n m)
+
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
@@ -550,10 +552,10 @@ atomic_typ:
     { let v = mk_kid "n" $startpos $endpos in
       let atom_id = mk_id (Id "atom") $startpos $endpos in
       let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
-      mk_typ (ATyp_exist ([v], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
-  | Lcurly kid_list Dot typ Rcurly
+      mk_typ (ATyp_exist ([mk_kopt (KOpt_none v) $startpos $endpos], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+  | Lcurly kopt_list Dot typ Rcurly
     { mk_typ (ATyp_exist ($2, ATyp_aux (ATyp_lit (L_aux (L_true, loc $startpos $endpos)), loc $startpos $endpos), $4)) $startpos $endpos }
-  | Lcurly kid_list Comma typ Dot typ Rcurly
+  | Lcurly kopt_list Comma typ Dot typ Rcurly
     { mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos }
   | Lcurly id Colon typ Dot typ Rcurly
     { mk_typ (ATyp_base ($2, $4, $6)) $startpos $endpos }