diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 27 | ||||
| -rw-r--r-- | src/ast_util.mli | 2 | ||||
| -rw-r--r-- | src/initial_check.ml | 8 | ||||
| -rw-r--r-- | src/lexer.mll | 2 | ||||
| -rw-r--r-- | src/parse_ast.ml | 2 | ||||
| -rw-r--r-- | src/parser.mly | 6 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 36 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 57 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 10 | ||||
| -rw-r--r-- | src/rewrites.ml | 11 | ||||
| -rw-r--r-- | src/sail.ml | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 156 | ||||
| -rw-r--r-- | src/type_check.mli | 4 | ||||
| -rw-r--r-- | src/util.ml | 1 | ||||
| -rw-r--r-- | src/util.mli | 1 |
15 files changed, 225 insertions, 101 deletions
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_coq.ml b/src/pretty_print_coq.ml index 806234d6..f1726ce4 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 @@ -1761,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" @@ -1923,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 @@ -1950,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,_)) 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..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 @@ -354,6 +355,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 +369,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 @@ -585,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/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 -> 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 0e0137db..93f5302a 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 |