diff options
| -rw-r--r-- | src/initial_check.ml | 2 | ||||
| -rw-r--r-- | src/parse_ast.ml | 2 | ||||
| -rw-r--r-- | src/parser.mly | 6 | ||||
| -rw-r--r-- | src/pretty_print_common.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 4 |
5 files changed, 14 insertions, 2 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index b831e288..728056ab 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -331,6 +331,8 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) | Parse_ast.NC_and (nc1, nc2) -> NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) + | Parse_ast.NC_true -> NC_true + | Parse_ast.NC_false -> NC_false ), l) (* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *) diff --git a/src/parse_ast.ml b/src/parse_ast.ml index c2e550f4..8ce5e77d 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -165,6 +165,8 @@ n_constraint_aux = (* constraint over kind $_$ *) | NC_nat_set_bounded of kid * (int) list | NC_or of n_constraint * n_constraint | NC_and of n_constraint * n_constraint + | NC_true + | NC_false and n_constraint = diff --git a/src/parser.mly b/src/parser.mly index f2d986b1..d6da6e63 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -455,6 +455,8 @@ tup_typ: exist_typ: | Exist tyvars Comma nexp_constraint Dot tup_typ { tloc (ATyp_exist ($2, $4, $6)) } + | Exist tyvars Dot tup_typ + { tloc (ATyp_exist ($2, NC_aux (NC_true, loc ()), $4)) } | tup_typ { $1 } @@ -1095,6 +1097,10 @@ nexp_constraint2: { NC_aux(NC_nat_set_bounded($1,$4), loc ()) } | tyvar IN Lcurly nums Rcurly { NC_aux(NC_nat_set_bounded($1,$4), loc ()) } + | True + { NC_aux (NC_true, loc ()) } + | False + { NC_aux (NC_false, loc ()) } | Lparen nexp_constraint Rparen { $2 } diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index 9c870b05..57a06e74 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -228,6 +228,8 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = parens (separate space [nexp_constraint nc1; string "|"; nexp_constraint nc2]) | NC_and (nc1, nc2) -> separate space [nexp_constraint nc1; string "&"; nexp_constraint nc2] + | NC_true -> string "true" + | NC_false -> string "false" (* expose doc_typ, doc_atomic_typ, doc_nexp and doc_nexp_constraint *) in typ, atomic_typ, nexp, nexp_constraint diff --git a/src/type_check.ml b/src/type_check.ml index bf907e41..ff65c453 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1431,7 +1431,7 @@ let rec unify l env typ1 typ2 = match destructure_exist env typ2 with | Some (kids, nc, typ2) -> let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in - let unifiers = unify_typ l typ1 typ2 in + let (unifiers, _, _) = unify l env typ1 typ2 in typ_debug (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)); unifiers, kids, Some nc | None -> @@ -2208,7 +2208,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = begin subtyp l env typ typ_annot; subtyp l env typ_annot vtyp; - annot_lexp (LEXP_cast (typ_annot, v)) typ, env + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env end | Register vtyp -> begin |