From 56fb5bf999d7cc900d6535da4168e220862d3d9c Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 12 Dec 2018 17:37:13 +0000
Subject: 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
---
 src/parse_ast.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/parse_ast.ml')

diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index a5dbf66e..9b855837 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -163,7 +163,7 @@ atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders
  | ATyp_wild
  | ATyp_tup of (atyp) list (* Tuple type *)
  | ATyp_app of id * (atyp) list (* type constructor application *)
- | ATyp_exist of kid list * atyp * atyp
+ | ATyp_exist of kinded_id list * atyp * atyp
  | ATyp_base of id * atyp * atyp
 
 and atyp = 
@@ -175,7 +175,7 @@ kinded_id_aux =  (* optionally kind-annotated identifier *)
    KOpt_none of kid (* identifier *)
  | KOpt_kind of kind * kid (* kind-annotated variable *)
 
-type 
+and
 kinded_id = 
    KOpt_aux of kinded_id_aux * l
 
-- 
cgit v1.2.3