From c1305bf912ff1cc0920c2bb011fee30623504a34 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 22 Oct 2018 16:03:41 +0100 Subject: Fix lem arguments for functions with tuple arguments Make lem output understand difference between functions taking a tuple and functions taking multiple arguments. Previously it assumed that no functions ever took a tuple as an argument, which is incorrect for mappings. --- src/pretty_print_lem.ml | 57 +++++++++++++++++++++++------------------------- src/pretty_print_sail.ml | 5 +++-- 2 files changed, 30 insertions(+), 32 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 8138a04e..68825c8f 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1228,42 +1228,35 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with else empty) | _ -> raise (Reporting_basic.err_unreachable l __POS__ "register with non-constant indices") -let args_of_typ l env typ = - let typs = match typ with - | Typ_aux (Typ_tup typs, _) -> typs - | typ -> [typ] in +let args_of_typs l env typs = let arg i typ = let id = mk_id ("arg" ^ string_of_int i) in P_aux (P_id id, (l, mk_tannot env typ no_effect)), E_aux (E_id id, (l, mk_tannot env typ no_effect)) in List.split (List.mapi arg typs) -let rec untuple_args_pat fun_typ (P_aux (paux, ((l, _) as annot)) as pat) = +let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) arg_typs = + let env = env_of_annot annot in let identity = (fun body -> body) in - let env = env_of_annot annot in - (* Hack until we get proper multiple-argument-patterns *) - match fun_typ with - | Typ_aux(Typ_fn([_], _, _), _) -> [pat], identity - | _ -> begin - let (Typ_aux (taux, _)) = typ_of_annot annot in - match paux, taux with - | P_tup [], _ -> - let annot = (l, mk_tannot Env.empty unit_typ no_effect) in - [P_aux (P_lit (mk_lit L_unit), annot)], identity - | P_tup pats, _ -> pats, identity - | P_wild, Typ_tup typs -> - let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)) in - List.map wild typs, identity - | P_typ (_, pat), _ -> untuple_args_pat fun_typ pat - | P_as _, Typ_tup _ | P_id _, Typ_tup _ -> - let argpats, argexps = args_of_typ l env (pat_typ_of pat) in - let argexp = E_aux (E_tuple argexps, annot) in - let bindargs (E_aux (_, bannot) as body) = - E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in - argpats, bindargs - | _, _ -> - [pat], identity - end + match paux, arg_typs with + | P_tup [], _ -> + let annot = (l, mk_tannot Env.empty unit_typ no_effect) in + [P_aux (P_lit (mk_lit L_unit), annot)], identity + | P_wild, [Typ_aux (Typ_tup typs, _)] -> + let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)) in + List.map wild typs, identity + | P_typ (_, pat), _ -> untuple_args_pat pat arg_typs + | P_as _, [Typ_aux (Typ_tup _, _)] + | P_id _, [Typ_aux (Typ_tup _, _)] + | P_tup _, [Typ_aux (Typ_tup _, _)] -> + let argpats, argexps = args_of_typs l env arg_typs in + let argexp = E_aux (E_tuple argexps, annot) in + let bindargs (E_aux (_, bannot) as body) = + E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in + argpats, bindargs + | P_tup pats, _ -> pats, identity + | _, _ -> + [pat], identity let doc_rec_lem force_rec (Rec_aux(r,_)) = match r with | Rec_nonrec when not force_rec -> space @@ -1281,12 +1274,16 @@ let doc_fun_body_lem ctxt exp = let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) = let typ = typ_of_annot annot in + let arg_typs = match typ with + | Typ_aux (Typ_fn (arg_typs, typ_ret, _), _) -> arg_typs + | Typ_aux (_, l) -> raise (unreachable l __POS__ "Non-function type for funcl") + in let pat,guard,exp,(l,_) = destruct_pexp pexp in let ctxt = { early_ret = contains_early_return exp; bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ); top_env = env_of_annot annot } in - let pats, bind = untuple_args_pat (typ_of_annot annot) pat in + let pats, bind = untuple_args_pat pat arg_typs in let patspp = separate_map space (doc_pat_lem ctxt true) pats in let _ = match guard with | None -> () diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 8f78b7dc..08ede660 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -354,6 +354,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_throw exp -> string "throw" ^^ parens (doc_exp exp) | E_try (exp, pexps) -> separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps] + | E_return (E_aux (E_lit (L_aux (L_unit, _)), _)) -> string "return()" | E_return exp -> string "return" ^^ parens (doc_exp exp) | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp) | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> @@ -367,8 +368,8 @@ and doc_infix n (E_aux (e_aux, _) as exp) = match Bindings.find op !fixities with | (Infix, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r] | (Infix, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]) - | (InfixL, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r] - | (InfixL, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]) + | (InfixL, m) when m >= n -> separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r] + | (InfixL, m) -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]) | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r] | (InfixR, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) with -- cgit v1.2.3 From 16df05e36d126a1a78e02e20d1dd1320e294d050 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 22 Oct 2018 17:35:51 +0100 Subject: Coq: work around constructors with tupled arguments --- src/pretty_print_coq.ml | 7 +++++++ src/rewrites.ml | 11 ++++++++++- 2 files changed, 17 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 806234d6..99d63b55 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -694,6 +694,13 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty List.map (subst_unifiers unifiers) arg_typs | _ -> assert false in + (* Constructors that were specified without a return type might get + an extra tuple in their type; expand that here if necessary. + TODO: this should go away if we enforce proper arities. *) + let arg_typs = match pats, arg_typs with + | _::_::_, [Typ_aux (Typ_tup typs,_)] -> typs + | _,_ -> arg_typs + in let ppp = doc_unop (doc_id_ctor id) (parens (separate_map comma (doc_pat ctxt true true) (List.combine pats arg_typs))) in if apat_needed then parens ppp else ppp diff --git a/src/rewrites.ml b/src/rewrites.ml index cdb15717..c470d906 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4595,7 +4595,16 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat = (match res_pat with | RP_app (id',residual_args) -> if Id.compare id id' == 0 then - let res_pats' = subpats args residual_args in + let res_pats' = + (* Constructors that were specified without a return type might get + an extra tuple in their type; expand that here if necessary. + TODO: this should go away if we enforce proper arities. *) + match args, residual_args with + | [], [RP_any] + | _::_::_, [RP_any] + -> subpats args (List.map (fun _ -> RP_any) args) + | _,_ -> + subpats args residual_args in List.map (fun rps -> RP_app (id,rps)) res_pats' else [res_pat] | RP_any -> -- cgit v1.2.3 From e489f2d37efa4c320004d35c3025c77e0a0c60d0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 22 Oct 2018 18:29:18 +0100 Subject: Coq: use function type more carefully in untupling And update the RISC-V patch accordingly. --- src/pretty_print_coq.ml | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 99d63b55..f1726ce4 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1768,33 +1768,28 @@ let args_of_typ l env typs = E_aux (E_id id, (l, mk_tannot env typ no_effect)) in List.split (List.mapi arg typs) -let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) = +let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) = let env = env_of_annot annot in - let tup_typs = match typ with - | Typ_aux (Typ_tup typs, _) -> Some typs - | _ -> match Env.expand_synonyms env typ with - | Typ_aux (Typ_tup typs, _) -> Some typs - | _ -> None - in let identity = (fun body -> body) in - match paux, tup_typs with + match paux, typs with | P_tup [], _ -> let annot = (l, mk_tannot Env.empty unit_typ no_effect) in [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity - | P_tup pats, Some typs -> List.combine pats typs, identity - | P_tup pats, _ -> raise (Reporting_basic.err_unreachable l __POS__ "Tuple pattern against non-tuple type") - | P_wild, Some typs -> + | P_tup pats, _ -> List.combine pats typs, identity + | P_wild, _ -> let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)), typ in List.map wild typs, identity - | P_typ (_, pat), _ -> untuple_args_pat typ pat - | P_as _, Some typs | P_id _, Some typs -> + | P_typ (_, pat), _ -> untuple_args_pat typs pat + | P_as _, _::_::_ | P_id _, _::_::_ -> let argpats, argexps = args_of_typ l env typs in let argexp = E_aux (E_tuple argexps, annot) in let bindargs (E_aux (_, bannot) as body) = E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in argpats, bindargs - | _, _ -> + | _, [typ] -> [pat,typ], identity + | _, _ -> + unreachable l __POS__ "Unexpected pattern/type combination" let doc_rec (Rec_aux(r,_)) = match r with | Rec_nonrec -> string "Definition" @@ -1930,7 +1925,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let ids_to_avoid = all_ids pexp in let bound_kids = tyvars_of_typquant tq in let pat,guard,exp,(l,_) = destruct_pexp pexp in - let pats, bind = untuple_args_pat (mk_typ (Typ_tup arg_typs)) pat in (* FIXME is this needed any more? *) + let pats, bind = untuple_args_pat arg_typs pat in (* FIXME is this needed any more? *) let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in @@ -1957,6 +1952,10 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let doc_binder (P_aux (p,ann) as pat, typ) = let env = env_of_annot ann in let exp_typ = Env.expand_synonyms env typ in + let () = + debug ctxt (lazy (" pattern " ^ string_of_pat pat)); + debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ)) + in match p with | P_id id | P_typ (_,P_aux (P_id id,_)) -- cgit v1.2.3 From 5471af45fd04169eb184371dcd8f791e507eab6f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 24 Oct 2018 17:25:47 +0100 Subject: Add constraint synonyms Currently not enabled by default, the flag -Xconstraint_synonyms enables them For generating constraints in ASL parser, we want to be able to give names to the constraints that we attach to certain variables. It's slightly awkward right now when constraints get long complicated because the entire constraint always has to be typed out in full whenever it appears, and there's no way to abstract away from that. This adds constraint synonyms, which work much like type synonyms except for constraints, e.g. constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256 these constraints can then be used instead of the full constraint, e.g. val f : forall 'n, where Size('n). int('n) -> unit Unfortunatly we need to have a keyword to 'call' the constraint synonym otherwise the grammer stops being LR(1). This could be resolved by parsing all constraints into Parse_ast.atyp and then de-sugaring them into constraints, which is what happens for n-expressions already, but that would require quite a bit of work on the parser. To avoid this forcing changes to any other parts of Sail, the intended invariant is that all constraints appearing anywhere in a type-checked AST have no constraint synonyms, so they don't have to worry about matching on NC_app, or calling Env.expand_typquant_synonyms (which isn't even exported for this reason). --- src/ast_util.ml | 27 ++++++-- src/ast_util.mli | 2 + src/initial_check.ml | 8 +++ src/lexer.mll | 2 + src/parse_ast.ml | 2 + src/parser.mly | 6 +- src/pretty_print_sail.ml | 5 +- src/sail.ml | 3 + src/type_check.ml | 156 +++++++++++++++++++++++++++++++++-------------- src/type_check.mli | 4 ++ src/util.ml | 1 + src/util.mli | 1 + 12 files changed, 164 insertions(+), 53 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 1d0689e4..9966742e 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -329,7 +329,7 @@ let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2)) let nc_true = mk_nc NC_true let nc_false = mk_nc NC_false -let rec nc_negate (NC_aux (nc, _)) = +let rec nc_negate (NC_aux (nc, l)) = match nc with | NC_bounded_ge (n1, n2) -> nc_lt n1 n2 | NC_bounded_le (n1, n2) -> nc_gt n1 n2 @@ -343,6 +343,8 @@ let rec nc_negate (NC_aux (nc, _)) = | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int) | NC_set (kid, int :: ints) -> mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints))))) + | NC_app _ -> + raise (Reporting_basic.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym") let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown) @@ -379,6 +381,10 @@ let quant_split typq = let qis = quant_items typq in List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis) +let quant_map_items f = function + | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l) + | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l) + let unaux_nexp (Nexp_aux (nexp, _)) = nexp let unaux_order (Ord_aux (ord, _)) = ord let unaux_typ (Typ_aux (typ, _)) = typ @@ -523,8 +529,8 @@ let def_loc = function | DEF_scattered (SD_aux (_, (l, _))) | DEF_reg_dec (DEC_aux (_, (l, _))) | DEF_fixity (_, _, Id_aux (_, l)) - | DEF_overload (Id_aux (_, l), _) -> - l + | DEF_overload (Id_aux (_, l), _) -> l + | DEF_constraint (Id_aux (_, l), _, _) -> l | DEF_internal_mutrec _ -> Parse_ast.Unknown let string_of_id = function @@ -638,12 +644,17 @@ and string_of_n_constraint = function "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}" + | NC_aux (NC_app (id, nexps), _) -> + "where " ^ string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_nexp nexps ^ ")" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" +let string_of_kinded_id = function + | KOpt_aux (KOpt_none kid, _) -> string_of_kid kid + | KOpt_aux (KOpt_kind (k, kid), _) -> "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")" + let string_of_quant_item_aux = function - | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid - | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")" + | QI_id kopt -> string_of_kinded_id kopt | QI_const constr -> string_of_n_constraint constr let string_of_quant_item = function @@ -884,6 +895,8 @@ module NC = struct | NC_or (nc1,nc2), NC_or (nc3,nc4) | NC_and (nc1,nc2), NC_and (nc3,nc4) -> lex_ord compare compare nc1 nc3 nc2 nc4 + | NC_app (id1, nexps1), NC_app (id2, nexps2) + -> lex_ord (Id.compare) (Util.compare_list Nexp.compare) id1 id2 nexps1 nexps2 | NC_true, NC_true | NC_false, NC_false -> 0 @@ -894,6 +907,7 @@ module NC = struct | NC_set _, _ -> -1 | _, NC_set _ -> 1 | NC_or _, _ -> -1 | _, NC_or _ -> 1 | NC_and _, _ -> -1 | _, NC_and _ -> 1 + | NC_app _, _ -> -1 | _, NC_app _ -> 1 | NC_true, _ -> -1 | _, NC_true -> 1 end @@ -1079,6 +1093,8 @@ let rec tyvars_of_nc (NC_aux (nc, _)) = | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_nc nc1) (tyvars_of_nc nc2) + | NC_app (id, nexps) -> + List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps) | NC_true | NC_false -> KidSet.empty @@ -1338,6 +1354,7 @@ let rec locate_nc l (NC_aux (nc_aux, _)) = | NC_set (kid, nums) -> NC_set (locate_kid l kid, nums) | NC_or (nc1, nc2) -> NC_or (locate_nc l nc1, locate_nc l nc2) | NC_and (nc1, nc2) -> NC_and (locate_nc l nc1, locate_nc l nc2) + | NC_app (id, nexps) -> NC_app (id, List.map (locate_nexp l) nexps) | NC_true -> NC_true | NC_false -> NC_false in diff --git a/src/ast_util.mli b/src/ast_util.mli index bbe9463e..ea287190 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -172,6 +172,7 @@ val nc_negate : n_constraint -> n_constraint val quant_items : typquant -> quant_item list val quant_kopts : typquant -> kinded_id list val quant_split : typquant -> kinded_id list * n_constraint list +val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant (* Functions to map over the annotations in sub-expressions *) val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp @@ -209,6 +210,7 @@ val string_of_typ : typ -> string val string_of_typ_arg : typ_arg -> string val string_of_typ_pat : typ_pat -> string val string_of_n_constraint : n_constraint -> string +val string_of_kinded_id : kinded_id -> string val string_of_quant_item : quant_item -> string val string_of_typquant : typquant -> string val string_of_typschm : typschm -> string diff --git a/src/initial_check.ml b/src/initial_check.ml index 4e6e941d..36513ba1 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -370,6 +370,9 @@ 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_app (id, typs) -> + let nexps = List.map (to_ast_nexp k_env) typs in + NC_app (to_ast_id id, nexps) | Parse_ast.NC_true -> NC_true | Parse_ast.NC_false -> NC_false ), l) @@ -907,6 +910,11 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out | Parse_ast.DEF_reg_dec(dec) -> let d = to_ast_dec envs dec in ((Finished(DEF_reg_dec(d))),envs),partial_defs + | Parse_ast.DEF_constraint (id, kids, nc) -> + let id = to_ast_id id in + let kids = List.map to_ast_var kids in + let nc = to_ast_nexp_constraint k_env nc in + ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs | Parse_ast.DEF_pragma (_, _, l) -> typ_error l "Encountered preprocessor directive in initial check" None None None | Parse_ast.DEF_internal_mutrec _ -> diff --git a/src/lexer.mll b/src/lexer.mll index cc49073c..cbefa601 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -163,6 +163,8 @@ let kw_table = ("do", (fun _ -> Do)); ("mutual", (fun _ -> Mutual)); ("bitfield", (fun _ -> Bitfield)); + ("tuple", (fun _ -> Tuple)); + ("where", (fun _ -> Where)); ("barr", (fun x -> Barr)); ("depend", (fun x -> Depend)); diff --git a/src/parse_ast.ml b/src/parse_ast.ml index a4052d82..3317c196 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -176,6 +176,7 @@ n_constraint_aux = (* constraint over kind $_$ *) | NC_set of kid * (Big_int.num) list | NC_or of n_constraint * n_constraint | NC_and of n_constraint * n_constraint + | NC_app of id * atyp list | NC_true | NC_false @@ -566,6 +567,7 @@ def = (* Top-level definition *) | DEF_scattered of scattered_def (* scattered definition *) | DEF_reg_dec of dec_spec (* register declaration *) | DEF_pragma of string * string * l + | DEF_constraint of id * kid list * n_constraint | DEF_internal_mutrec of fundef list diff --git a/src/parser.mly b/src/parser.mly index b9aae275..070dee50 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -175,7 +175,7 @@ let rec desugar_rchain chain s e = /*Terminals with no content*/ -%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op +%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Tuple Where %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Cast %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield @@ -331,6 +331,8 @@ nc_and: { $1 } atomic_nc: + | Where id Lparen typ_list Rparen + { mk_nc (NC_app ($2, $4)) $startpos $endpos } | True { mk_nc NC_true $startpos $endpos } | False @@ -1402,6 +1404,8 @@ def: { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) } | default_def { DEF_default $1 } + | Constraint id Lparen kid_list Rparen Eq nc + { DEF_constraint ($2, $4, $7) } | Mutual Lcurly fun_def_list Rcurly { DEF_internal_mutrec $3 } | Pragma diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 08ede660..0b0a8305 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -123,6 +123,7 @@ let doc_nc = | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 | NC_set (kid, ints) -> separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] + | NC_app (id, nexps) -> string "where" ^^ space ^^ doc_id id ^^ parens (separate_map (comma ^^ space) doc_nexp nexps) | _ -> parens (nc0 nc) and nc0 (NC_aux (nc_aux, _) as nc) = match nc_aux with @@ -134,7 +135,7 @@ let doc_nc = | _ -> atomic_nc nc in nc0 - + let rec doc_typ (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_id id -> doc_id id @@ -586,6 +587,8 @@ let rec doc_def def = group (match def with | DEF_fixity (prec, n, id) -> fixities := Bindings.add id (prec, Big_int.to_int n) !fixities; separate space [doc_prec prec; doc_int n; doc_id id] + | DEF_constraint (id, kids, nc) -> + separate space [string "constraint"; doc_id id; parens (separate_map (comma ^^ space) doc_kid kids); equals; doc_nc nc] | DEF_overload (id, ids) -> separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] ) ^^ hardline diff --git a/src/sail.ml b/src/sail.ml index 9526d6fe..c1c965fe 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -237,6 +237,9 @@ let options = Arg.align ([ ( "-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers"); + ( "-Xconstraint_synonyms", + Arg.Set Type_check.opt_constraint_synonyms, + " (extension) allow constraint synonyms"); ( "-v", Arg.Set opt_print_version, " print version"); diff --git a/src/type_check.ml b/src/type_check.ml index e1232046..cf1d8ef9 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -69,6 +69,10 @@ let opt_no_effects = ref false assignments in l-expressions *) let opt_no_lexp_bounds_check = ref false +(* opt_constraint_synonyms allows constraint synonyms as toplevel + definitions *) +let opt_constraint_synonyms = ref false + let depth = ref 0 let rec indent n = match n with @@ -163,6 +167,7 @@ and strip_n_constraint_aux = function | NC_set (kid, nums) -> NC_set (strip_kid kid, nums) | NC_or (nc1, nc2) -> NC_or (strip_n_constraint nc1, strip_n_constraint nc2) | NC_and (nc1, nc2) -> NC_and (strip_n_constraint nc1, strip_n_constraint nc2) + | NC_app (id, nexps) -> NC_app (strip_id id, List.map strip_nexp nexps) | NC_true -> NC_true | NC_false -> NC_false and strip_n_constraint = function @@ -245,6 +250,7 @@ and nc_subst_nexp_aux l sv subst = function else set_nc | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2) | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2) + | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps) | NC_false -> NC_false | NC_true -> NC_true @@ -336,6 +342,8 @@ let typquant_subst_kid_aux sv subst = function let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_kid_aux sv subst typq, l) +let adding = Util.("Adding " |> darkgray |> clear) + (**************************************************************************) (* 2. Environment *) (**************************************************************************) @@ -378,6 +386,7 @@ module Env : sig val add_ret_typ : typ -> t -> t val add_typ_synonym : id -> (t -> typ_arg list -> typ) -> t -> t val get_typ_synonym : id -> t -> t -> typ_arg list -> typ + val add_constraint_synonym : id -> kid list -> n_constraint -> t -> t val add_num_def : id -> nexp -> t -> t val get_num_def : id -> t -> nexp val add_overloads : id -> id list -> t -> t @@ -400,7 +409,11 @@ module Env : sig val polymorphic_undefineds : t -> bool val lookup_id : ?raw:bool -> id -> t -> typ lvar val fresh_kid : ?kid:kid -> t -> kid + val expand_synonyms : t -> typ -> typ + val expand_constraint_synonyms : t -> n_constraint -> n_constraint + val expand_typquant_synonyms : t -> typquant -> typquant + val canonicalize : t -> typ -> typ val base_typ_of : t -> typ -> typ val add_smt_op : id -> string -> t -> t @@ -448,6 +461,7 @@ end = struct accessors : (typquant * typ) Bindings.t; externs : (string -> string option) Bindings.t; smt_ops : string Bindings.t; + constraint_synonyms : (kid list * n_constraint) Bindings.t; casts : id list; allow_casts : bool; allow_bindings : bool; @@ -477,6 +491,7 @@ end = struct accessors = Bindings.empty; externs = Bindings.empty; smt_ops = Bindings.empty; + constraint_synonyms = Bindings.empty; casts = []; allow_bindings = true; allow_casts = true; @@ -495,11 +510,11 @@ end = struct let get_typ_var kid env = try snd (KBindings.find kid env.typ_vars) with - | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid) + | Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid) let get_typ_var_loc kid env = try fst (KBindings.find kid env.typ_vars) with - | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid) + | Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid) let get_typ_vars env = KBindings.map snd env.typ_vars let get_typ_var_locs env = KBindings.map fst env.typ_vars @@ -545,12 +560,12 @@ end = struct | Not_found -> [] let add_overloads id ids env = - typ_print (lazy ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]")); + typ_print (lazy (adding ^ "overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]")); let existing = try Bindings.find id env.overloads with Not_found -> [] in { env with overloads = Bindings.add id (existing @ ids) env.overloads } let add_smt_op id str env = - typ_print (lazy ("Adding smt binding " ^ string_of_id id ^ " to " ^ str)); + typ_print (lazy (adding ^ "smt binding " ^ string_of_id id ^ " to " ^ str)); { env with smt_ops = Bindings.add id str env.smt_ops } let get_smt_op (Id_aux (_, l) as id) env = @@ -597,8 +612,28 @@ end = struct then () else typ_error (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id) + let rec expand_constraint_synonyms env (NC_aux (nc_aux, l) as nc) = + let expand = expand_constraint_synonyms env in + match nc_aux with + | NC_app (id, nexps) -> + begin + try + let kids, nc = Bindings.find id env.constraint_synonyms in + let nc = List.fold_left2 (fun nc kid nexp -> nc_subst_nexp kid (unaux_nexp nexp) nc) nc kids nexps in + expand nc + with Not_found -> typ_error l ("Could not expand constraint synonym in " ^ string_of_n_constraint nc) + end + | NC_and (nc1, nc2) -> NC_aux (NC_and (expand nc1, expand nc2), l) + | NC_or (nc1, nc2) -> NC_aux (NC_or (expand nc1, expand nc2), l) + | NC_true | NC_false | NC_set _ | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _ -> nc + + let expand_quant_item_synonyms env = function + | QI_aux (QI_id kopt, l) -> QI_aux (QI_id kopt, l) + | QI_aux (QI_const nc, l) -> QI_aux (QI_const (expand_constraint_synonyms env nc), l) + + let expand_typquant_synonyms env = quant_map_items (expand_quant_item_synonyms env) + let rec expand_synonyms env (Typ_aux (typ, l) as t) = - (* typ_debug (lazy ("Expanding synonyms for " ^ string_of_typ t)); *) match typ with | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l) | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l) @@ -644,7 +679,7 @@ end = struct let kids = List.map rename_kid kids in let nc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid "syn#" kid)) nc) nc !rebindings in let typ = List.fold_left (fun typ kid -> typ_subst_nexp kid (Nexp_var (prepend_kid "syn#" kid)) typ) typ !rebindings in - typ_print (lazy ("Synonym existential: {" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}")); + typ_debug (lazy ("Synonym existential: {" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}")); let env = { env with constraints = nc :: env.constraints } in Typ_aux (Typ_exist (kids, nc, expand_synonyms env typ), l) | Typ_var v -> Typ_aux (Typ_var v, l) @@ -718,7 +753,7 @@ end = struct (* Check if a type, order, n-expression or constraint is well-formed. Throws a type error if the type is badly formed. *) let rec wf_typ ?exs:(exs=KidSet.empty) env typ = - typ_debug (lazy ("Well-formed " ^ string_of_typ typ)); + typ_debug (lazy ("well-formed " ^ string_of_typ typ)); let (Typ_aux (typ_aux, l)) = expand_synonyms env typ in match typ_aux with | Typ_id id when bound_typ_id env id -> @@ -755,7 +790,8 @@ end = struct | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp | Typ_arg_typ typ -> wf_typ ~exs:exs env typ | Typ_arg_order ord -> wf_order env ord - and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l)) = + and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) = + typ_debug (lazy ("well-formed nexp " ^ string_of_nexp nexp)); match nexp_aux with | Nexp_id _ -> () | Nexp_var kid when KidSet.mem kid exs -> () @@ -765,7 +801,7 @@ end = struct | BK_int -> () | kind -> typ_error l ("Constraint is badly formed, " ^ string_of_kid kid ^ " has kind " - ^ string_of_base_kind_aux kind ^ " but should have kind Nat") + ^ string_of_base_kind_aux kind ^ " but should have kind Int") end | Nexp_constant _ -> () | Nexp_app (id, nexps) -> @@ -787,15 +823,28 @@ end = struct ^ string_of_base_kind_aux kind ^ " but should have kind Order") end | Ord_inc | Ord_dec -> () - and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc, _)) = - match nc with + and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc_aux, l) as nc) = + typ_debug (lazy ("well-formed constraint " ^ string_of_n_constraint nc)); + match nc_aux with | NC_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 | NC_not_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 | NC_bounded_ge (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 | NC_bounded_le (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 - | NC_set (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *) + | NC_set (kid, _) when KidSet.mem kid exs -> () + | NC_set (kid, _) -> begin + match get_typ_var kid env with + | BK_int -> () + | kind -> typ_error l ("Set constraint is badly formed, " + ^ string_of_kid kid ^ " has kind " + ^ string_of_base_kind_aux kind ^ " but should have kind Int") + end | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2 | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2 + | NC_app (id, nexps) -> + if not (Bindings.mem id env.constraint_synonyms) then + typ_error l ("Constraint synonym " ^ string_of_id id ^ " is not defined") + else (); + List.iter (wf_nexp ~exs:exs env) nexps | NC_true | NC_false -> () let counter = ref 0 @@ -834,7 +883,8 @@ end = struct let rec update_val_spec id (typq, typ) env = begin let typ = expand_synonyms env typ in - typ_print (lazy ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind (typq, typ))); + let typq = expand_typquant_synonyms env typq in + typ_print (lazy (adding ^ "val spec " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); let env = match typ with | Typ_aux (Typ_bidir (typ1, typ2), _) -> add_mapping id (typq, typ1, typ2) env | _ -> env @@ -854,7 +904,7 @@ end = struct env and add_mapping id (typq, typ1, typ2) env = begin - typ_print (lazy ("Adding mapping " ^ string_of_id id)); + typ_print (lazy (adding ^ "mapping " ^ string_of_id id)); let forwards_id = mk_id (string_of_id id ^ "_forwards") in let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in let backwards_id = mk_id (string_of_id id ^ "_backwards") in @@ -912,7 +962,7 @@ end = struct then typ_error (id_loc id) ("Cannot create enum " ^ string_of_id id ^ ", type name is already bound") else begin - typ_print (lazy ("Adding enum " ^ string_of_id id)); + typ_print (lazy (adding ^ "enum " ^ string_of_id id)); { env with enums = Bindings.add id (IdSet.of_list ids) env.enums } end @@ -930,7 +980,7 @@ end = struct then typ_error (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound") else begin - typ_print (lazy ("Adding record " ^ string_of_id id)); + typ_print (lazy (adding ^ "record " ^ string_of_id id)); let rec record_typ_args = function | [] -> [] | ((QI_aux (QI_id kopt, _)) :: qis) when is_nat_kopt kopt -> @@ -947,7 +997,7 @@ end = struct in let fold_accessors accs (typ, fid) = let acc_typ = mk_typ (Typ_fn ([rectyp], typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in - typ_print (lazy (indent 1 ^ "Adding accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ))); + typ_print (lazy (indent 1 ^ adding ^ "accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ))); Bindings.add (field_name id fid) (typq, acc_typ) accs in { env with records = Bindings.add id (typq, fields) env.records; @@ -987,19 +1037,19 @@ end = struct if Bindings.mem id env.top_val_specs then typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name") else (); - typ_print (lazy ("Adding local binding " ^ string_of_id id ^ " :: " ^ string_of_mtyp mtyp)); + typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp)); { env with locals = Bindings.add id mtyp env.locals } end let add_variant id variant env = begin - typ_print (lazy ("Adding variant " ^ string_of_id id)); + typ_print (lazy (adding ^ "variant " ^ string_of_id id)); { env with variants = Bindings.add id variant env.variants } end let add_union_id id bind env = begin - typ_print (lazy ("Adding union identifier binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind)); + typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind)); { env with union_ids = Bindings.add id bind env.union_ids } end @@ -1008,7 +1058,7 @@ end = struct | Not_found -> fun typ -> typ let add_flow id f env = - typ_print (lazy ("Adding flow constraints for " ^ string_of_id id)); + typ_print (lazy (adding ^ "flow constraints for " ^ string_of_id id)); { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow } let remove_flow id env = @@ -1046,7 +1096,7 @@ end = struct then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound") else begin - typ_print (lazy ("Adding register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ)); + typ_print (lazy (adding ^ "register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ)); { env with registers = Bindings.add id (reff, weff, typ) env.registers } end @@ -1072,10 +1122,10 @@ end = struct let add_typ_var l kid k env = if KBindings.mem kid env.typ_vars - then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound") + then typ_error (kid_loc kid) ("type variable " ^ string_of_kid kid ^ " is already bound") else begin - typ_print (lazy ("Adding kind identifier " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k)); + typ_print (lazy (adding ^ "type variable " ^ string_of_kid kid ^ " : " ^ string_of_base_kind_aux k)); { env with typ_vars = KBindings.add kid (l, k) env.typ_vars } end @@ -1084,7 +1134,7 @@ end = struct then typ_error (id_loc id) ("Num identifier " ^ string_of_id id ^ " is already bound") else begin - typ_print (lazy ("Adding Num identifier " ^ string_of_id id ^ " :: " ^ string_of_nexp nexp)); + typ_print (lazy (adding ^ "Num identifier " ^ string_of_id id ^ " : " ^ string_of_nexp nexp)); { env with num_defs = Bindings.add id nexp env.num_defs } end @@ -1099,7 +1149,8 @@ end = struct match nc_aux with | NC_true -> env | _ -> - typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr)); + let constr = expand_constraint_synonyms env constr in + typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr)); { env with constraints = constr :: env.constraints } let get_ret_typ env = env.ret_typ @@ -1114,7 +1165,7 @@ end = struct let no_bindings env = { env with allow_bindings = false } let add_cast cast env = - typ_print (lazy ("Adding cast " ^ string_of_id cast)); + typ_print (lazy (adding ^ "cast " ^ string_of_id cast)); { env with casts = cast :: env.casts } let add_typ_synonym id synonym env = @@ -1122,12 +1173,22 @@ end = struct then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists") else begin - typ_print (lazy ("Adding type synonym " ^ string_of_id id)); + typ_print (lazy (adding ^ "type synonym " ^ string_of_id id)); { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms } end let get_typ_synonym id env = Bindings.find id env.typ_synonyms + let add_constraint_synonym id kids nc env = + if Bindings.mem id env.constraint_synonyms + then typ_error (id_loc id) ("Constraint synonym " ^ string_of_id id ^ " already exists") + else + begin + typ_print (lazy (adding ^ "constraint synonym " ^ string_of_id id)); + wf_constraint ~exs:(KidSet.of_list kids) env nc; + { env with constraint_synonyms = Bindings.add id (kids, nc) env.constraint_synonyms } + end + let get_default_order env = match env.default_order with | None -> typ_error Parse_ast.Unknown ("No default order has been set") @@ -1186,6 +1247,10 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t = | TypQ_aux (TypQ_no_forall, _) -> env | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants +let expand_bind_synonyms l env (typq, typ) = + Env.expand_typquant_synonyms env typq, Env.expand_synonyms (add_typquant l typq env) typ + + (* Create vectors with the default order from the environment *) let default_order_error_string = @@ -1356,6 +1421,7 @@ let rec nc_constraint env var_of (NC_aux (nc, l)) = (List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant i)) ints) | NC_or (nc1, nc2) -> Constraint.disj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2) | NC_and (nc1, nc2) -> Constraint.conj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2) + | NC_app (id, nexps) -> raise (Reporting_basic.err_unreachable l __POS__ "constraint synonym reached smt generation") | NC_false -> Constraint.literal false | NC_true -> Constraint.literal true @@ -2034,7 +2100,6 @@ let rec instantiate_quants quants kid uvar = match quants with if is_typ_kid kid kinded_id then instantiate_quants quants kid uvar else quant :: instantiate_quants quants kid uvar - | _ -> typ_error Parse_ast.Unknown "Cannot instantiate quantifier" end | ((QI_aux (QI_const nc, l)) :: quants) -> begin @@ -2307,7 +2372,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let checked_msg = crule check_exp env assert_msg string_typ in let env = match assert_constraint env true constr_exp with | Some nc -> - typ_print (lazy ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert")); + typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint nc ^ " for assert")); Env.add_constraint nc env | None -> env in @@ -2739,7 +2804,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with | Typ_tup typs -> typs | _ -> [typ] - in + in match Env.expand_synonyms env ctor_typ with | Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) -> begin @@ -4382,31 +4447,26 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md context. We have to destructure the various kinds of val specs, but the difference is irrelevant for the typechecker. *) let check_val_spec env (VS_aux (vs, (l, _))) = - let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, Some ((env,typ,eff), None)))) in - let (id, quants, typ, env) = match vs with - | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _) as typschm, id, ext_opt, is_cast) -> - typ_debug (lazy ("VS typschm: " ^ string_of_id id ^ ", " ^ string_of_typschm typschm)); + let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, Some ((env, typ, eff), None)))) in + let vs, id, typq, typ, env = match vs with + | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, ext_opt, is_cast) -> + typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); let env = match (ext_opt "smt", ext_opt "#") with | Some op, None -> Env.add_smt_op id op env | _, _ -> env in - Env.wf_typ (add_typquant l quants env) typ; - typ_debug (lazy "CHECKED WELL-FORMED VAL SPEC"); - let env = - (* match ext_opt with - | None -> env - | Some ext -> *) - Env.add_extern id ext_opt env - in + let env = Env.add_extern id ext_opt env in let env = if is_cast then Env.add_cast id env else env in - (id, quants, typ, env) + let typq, typ = expand_bind_synonyms ts_l env (typq, typ) in + let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in + (vs, id, typq, typ, env) in let eff = match typ with - | Typ_aux (Typ_fn (_,_,eff),_) -> eff + | Typ_aux (Typ_fn (_, _, eff), _) -> eff | _ -> no_effect in - [annotate vs typ eff], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant l quants env) typ) env + [annotate vs typ eff], Env.add_val_spec id (typq, typ) env let check_default env (DT_aux (ds, l)) = match ds with @@ -4521,6 +4581,10 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env | DEF_fundef fdef -> check_fundef env fdef | DEF_mapdef mdef -> check_mapdef env mdef + | DEF_constraint (id, kids, nc) when !opt_constraint_synonyms -> + [], Env.add_constraint_synonym id kids nc env + | DEF_constraint (id, _, _) -> + typ_error (id_loc id) "Use -Xconstraint_synonyms to enable constraint synonyms" | DEF_internal_mutrec fdefs -> let defs = List.concat (List.map (fun fdef -> fst (check_fundef env fdef)) fdefs) in let split_fundef (defs, fdefs) def = match def with diff --git a/src/type_check.mli b/src/type_check.mli index 4fe6711c..8d2b02a9 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -67,6 +67,10 @@ val opt_no_effects : bool ref assignments in l-expressions. *) val opt_no_lexp_bounds_check : bool ref +(** [opt_constraint_synonyms] allows constraint synonyms as toplevel + definitions *) +val opt_constraint_synonyms : bool ref + (** {2 Type errors} *) type type_error = diff --git a/src/util.ml b/src/util.ml index b54c13d4..e0366fe7 100644 --- a/src/util.ml +++ b/src/util.ml @@ -408,6 +408,7 @@ let termcode n = let bold str = termcode 1 ^ str +let darkgray str = termcode 90 ^ str let red str = termcode 91 ^ str let green str = termcode 92 ^ str let yellow str = termcode 93 ^ str diff --git a/src/util.mli b/src/util.mli index bb7aa70d..eb4b4bd2 100644 --- a/src/util.mli +++ b/src/util.mli @@ -239,6 +239,7 @@ val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list) (* Terminal color codes *) val termcode : int -> string val bold : string -> string +val darkgray : string -> string val green : string -> string val red : string -> string val red_bg : string -> string -- cgit v1.2.3