From 41e6fe10e7d28193fa62711fcdad797b1f0103a0 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 13 May 2019 18:03:35 +0100 Subject: Add feature that allows functions to require type variables are constant can now write e.g. forall (constant 'n : Int) rather than forall ('n: Int) which requires 'n to be a constant integer value whenever the function is called. I added this to the 'addrsize variable on memory reads/writes to absolutely guarantee in the SMT generation that we don't have to worry about the address being a variable length bitvector. --- src/ast_util.ml | 35 ++++++++++++++++--------- src/initial_check.ml | 52 ++++++++++++++++++++++-------------- src/lexer.mll | 1 + src/monomorphise.ml | 2 +- src/ocaml_backend.ml | 7 +++-- src/parse_ast.ml | 5 ++-- src/parser.mly | 27 ++++++++++++------- src/pretty_print_coq.ml | 12 ++++++--- src/pretty_print_lem.ml | 3 ++- src/pretty_print_sail.ml | 50 +++++++++++++++++++++++++++-------- src/slice.ml | 2 +- src/toFromInterp_backend.ml | 6 +++-- src/type_check.ml | 64 +++++++++++++++++++++++++++------------------ src/type_error.ml | 4 +-- 14 files changed, 176 insertions(+), 94 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 12777506..70845468 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -104,7 +104,7 @@ let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux)) let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, body),no_annot)), no_annot) -let mk_qi_nc nc = QI_aux (QI_const nc, Parse_ast.Unknown) +let mk_qi_nc nc = QI_aux (QI_constraint nc, Parse_ast.Unknown) let mk_qi_id k kid = let kopt = @@ -460,9 +460,10 @@ let no_effect = mk_effect [] let quant_add qi typq = match qi, typq with - | QI_aux (QI_const (NC_aux (NC_true, _)), _), _ -> typq + | QI_aux (QI_constraint (NC_aux (NC_true, _)), _), _ -> typq | QI_aux (QI_id _, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qi :: qis), l) - | QI_aux (QI_const nc, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l) + | QI_aux (QI_constant _, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l) + | QI_aux (QI_constraint nc, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l) | _, TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_tq [qi], l) let quant_items : typquant -> quant_item list = function @@ -482,7 +483,7 @@ let quant_split typq = | _ -> [] in let qi_nc = function - | QI_aux (QI_const nc, _) -> [nc] + | QI_aux (QI_constraint nc, _) -> [nc] | _ -> [] in let qis = quant_items typq in @@ -497,9 +498,9 @@ let is_quant_kopt = function | _ -> false let is_quant_constraint = function - | QI_aux (QI_const _, _) -> true + | QI_aux (QI_constraint _, _) -> true | _ -> false - + let unaux_nexp (Nexp_aux (nexp, _)) = nexp let unaux_order (Ord_aux (ord, _)) = ord let unaux_typ (Typ_aux (typ, _)) = typ @@ -859,7 +860,8 @@ let string_of_kinded_id (KOpt_aux (KOpt_kind (k, kid), _)) = "(" ^ string_of_kid let string_of_quant_item_aux = function | QI_id kopt -> string_of_kinded_id kopt - | QI_const constr -> string_of_n_constraint constr + | QI_constant kopts -> "is_constant(" ^ Util.string_of_list ", " string_of_kinded_id kopts ^ ")" + | QI_constraint constr -> string_of_n_constraint constr let string_of_quant_item = function | QI_aux (qi, _) -> string_of_quant_item_aux qi @@ -1374,7 +1376,8 @@ and kopts_of_typ_arg (A_aux (ta,_)) = let kopts_of_quant_item (QI_aux (qi, _)) = match qi with | QI_id kopt -> KOptSet.singleton kopt - | QI_const nc -> kopts_of_constraint nc + | QI_constant kopts -> KOptSet.of_list kopts + | QI_constraint nc -> kopts_of_constraint nc let rec tyvars_of_nexp (Nexp_aux (nexp,_)) = match nexp with @@ -1431,7 +1434,8 @@ and tyvars_of_typ_arg (A_aux (ta,_)) = let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with | QI_id (KOpt_aux (KOpt_kind (_, kid), _)) -> KidSet.singleton kid - | QI_const nc -> tyvars_of_constraint nc + | QI_constant kopts -> KidSet.of_list (List.map kopt_kid kopts) + | QI_constraint nc -> tyvars_of_constraint nc let is_kid_generated kid = String.contains (string_of_kid kid) '#' @@ -1935,11 +1939,16 @@ let subst_kid subst sv v x = |> subst sv (mk_typ_arg (A_order (Ord_aux (Ord_var v, Parse_ast.Unknown)))) |> subst sv (mk_typ_arg (A_typ (mk_typ (Typ_var v)))) +let kopt_subst_kid sv subst (KOpt_aux (KOpt_kind (k, kid), l) as orig) = + if Kid.compare kid sv = 0 then KOpt_aux (KOpt_kind (k, subst), l) else orig + let quant_item_subst_kid_aux sv subst = function - | QI_id (KOpt_aux (KOpt_kind (k, kid), l)) as qid -> - if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_kind (k, subst), l)) else qid - | QI_const nc -> - QI_const (subst_kid constraint_subst sv subst nc) + | QI_id kopt -> + QI_id (kopt_subst_kid sv subst kopt) + | QI_constant kopts -> + QI_constant (List.map (kopt_subst_kid sv subst) kopts) + | QI_constraint nc -> + QI_constraint (subst_kid constraint_subst sv subst nc) let quant_item_subst_kid sv subst (QI_aux (quant, l)) = QI_aux (quant_item_subst_kid_aux sv subst quant, l) diff --git a/src/initial_check.ml b/src/initial_check.ml index 790a6624..ad52751b 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -129,17 +129,18 @@ let format_kind_aux_list = function | [kind] -> string_of_kind_aux kind | kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")" -let to_ast_kopt ctx (P.KOpt_aux (aux, l)) = - let aux, ctx = match aux with - | P.KOpt_none v -> - let v = to_ast_var v in - KOpt_kind (K_aux (K_int, gen_loc l), v), { ctx with kinds = KBindings.add v K_int ctx.kinds } - | P.KOpt_kind (k, v) -> - let v = to_ast_var v in - let k = to_ast_kind k in - KOpt_kind (k, v), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds } +let to_ast_kopts ctx (P.KOpt_aux (aux, l)) = + let mk_kopt v k = + let v = to_ast_var v in + let k = to_ast_kind k in + KOpt_aux (KOpt_kind (k, v), l), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds } in - KOpt_aux (aux, l), ctx + match aux with + | P.KOpt_kind (attr, vs, None) -> + let k = P.K_aux (P.K_int, gen_loc l) in + List.fold_left (fun (kopts, ctx) v -> let kopt, ctx = mk_kopt v k in (kopt :: kopts, ctx)) ([], ctx) vs, attr + | P.KOpt_kind (attr, vs, Some k) -> + List.fold_left (fun (kopts, ctx) v -> let kopt, ctx = mk_kopt v k in (kopt :: kopts, ctx)) ([], ctx) vs, attr let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) = let aux = match aux with @@ -171,7 +172,14 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) = end | P.ATyp_exist (kopts, nc, atyp) -> let kopts, ctx = - List.fold_right (fun kopt (kopts, ctx) -> let kopt, ctx = to_ast_kopt ctx kopt in (kopt :: kopts, ctx)) kopts ([], ctx) + List.fold_right (fun kopt (kopts, ctx) -> + let (kopts', ctx), attr = to_ast_kopts ctx kopt in + match attr with + | None -> + kopts' @ kopts, ctx + | Some attr -> + raise (Reporting.err_typ l (sprintf "Attribute %s cannot appear within an existential type" attr)) + ) kopts ([], ctx) in Typ_exist (kopts, to_ast_constraint ctx nc, to_ast_typ ctx atyp) | P.ATyp_base (id, kind, nc) -> @@ -262,19 +270,25 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) = in NC_aux (aux, l) -let to_ast_quant_item ctx (P.QI_aux (aux, l)) = +let to_ast_quant_items ctx (P.QI_aux (aux, l)) = match aux with - | P.QI_const nc -> QI_aux (QI_const (to_ast_constraint ctx nc), l), ctx + | P.QI_constraint nc -> [QI_aux (QI_constraint (to_ast_constraint ctx nc), l)], ctx | P.QI_id kopt -> - let kopt, ctx = to_ast_kopt ctx kopt in - QI_aux (QI_id kopt, l), ctx + let (kopts, ctx), attr = to_ast_kopts ctx kopt in + match attr with + | Some "constant" -> + QI_aux (QI_constant kopts, l) :: List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx + | Some attr -> + raise (Reporting.err_typ l (sprintf "Unknown attribute %s" attr)) + | None -> + List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx let to_ast_typquant ctx (P.TypQ_aux (aux, l)) = match aux with | P.TypQ_no_forall -> TypQ_aux (TypQ_no_forall, l), ctx | P.TypQ_tq quants -> let quants, ctx = - List.fold_left (fun (qis, ctx) qi -> let qi', ctx = to_ast_quant_item ctx qi in qi' :: qis, ctx) ([], ctx) quants + List.fold_left (fun (qis, ctx) qi -> let qis', ctx = to_ast_quant_items ctx qi in qis' @ qis, ctx) ([], ctx) quants in TypQ_aux (TypQ_tq (List.rev quants), l), ctx @@ -547,9 +561,9 @@ let anon_rec_constructor_typ record_id = function | P.TypQ_aux (P.TypQ_no_forall, l) -> P.ATyp_aux (P.ATyp_id record_id, Generated l) | P.TypQ_aux (P.TypQ_tq quants, l) -> let rec quant_arg = function - | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_none v, l)), _) -> [P.ATyp_aux (P.ATyp_var v, Generated l)] - | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, v), l)), _) -> [P.ATyp_aux (P.ATyp_var v, Generated l)] - | P.QI_aux (P.QI_const _, _) -> [] + | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, vs, _), l)), _) -> + List.map (fun v -> P.ATyp_aux (P.ATyp_var v, Generated l)) vs + | P.QI_aux (P.QI_constraint _, _) -> [] in match List.concat (List.map quant_arg quants) with | [] -> P.ATyp_aux (P.ATyp_id record_id, Generated l) diff --git a/src/lexer.mll b/src/lexer.mll index 43426d77..8000879e 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -147,6 +147,7 @@ let kw_table = ("scattered", (fun x -> Scattered)); ("sizeof", (fun x -> Sizeof)); ("constraint", (fun x -> Constraint)); + ("constant", (fun x -> Constant)); ("struct", (fun x -> Struct)); ("then", (fun x -> Then)); ("true", (fun x -> True)); diff --git a/src/monomorphise.ml b/src/monomorphise.ml index c011f4d0..1e52d708 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3583,7 +3583,7 @@ let rewrite_toplevel_nexps (Defs defs) = | [] -> None | _ -> let new_vars = List.map (fun (kid,nexp) -> QI_aux (QI_id (mk_kopt K_int kid), Generated tq_l)) nexp_map in - let new_constraints = List.map (fun (kid,nexp) -> QI_aux (QI_const (nc_eq (nvar kid) nexp), Generated tq_l)) nexp_map in + let new_constraints = List.map (fun (kid,nexp) -> QI_aux (QI_constraint (nc_eq (nvar kid) nexp), Generated tq_l)) nexp_map in let tqs = TypQ_aux (TypQ_tq (qs @ new_vars @ new_constraints),tq_l) in let vs = VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tqs,typ),ts_l),id,ext_opt,is_cast),ann) in diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 1a77ea12..ba2e5e69 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -153,10 +153,13 @@ and ocaml_typ_arg ctx (A_aux (typ_arg_aux, _) as typ_arg) = | A_typ typ -> ocaml_typ ctx typ | _ -> failwith ("OCaml: unexpected type argument " ^ string_of_typ_arg typ_arg) -let ocaml_typquant typq = +let ocaml_typquant (TypQ_aux (_, l) as typq) = let ocaml_qi = function | QI_aux (QI_id kopt, _) -> zencode_kid (kopt_kid kopt) - | QI_aux (QI_const _, _) -> failwith "Ocaml type quantifiers should no longer contain constraints" + | QI_aux (QI_constraint _, _) -> + raise (Reporting.err_general l "Ocaml: type quantifiers should no longer contain constraints") + | QI_aux (QI_constant _, _) -> + raise (Reporting.err_general l "Ocaml: type quantifiers should no longer contain constrant constraints") in match quant_items typq with | [] -> empty diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 91fb0610..5c3a5382 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -172,8 +172,7 @@ and atyp = and kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) + KOpt_kind of string option * kid list * kind option (* kind-annotated variable *) and kinded_id = @@ -182,7 +181,7 @@ kinded_id = type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of atyp (* A constraint for this type *) + | QI_constraint of atyp (* A constraint for this type *) type diff --git a/src/parser.mly b/src/parser.mly index f764995a..4bc2e5c5 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -181,7 +181,7 @@ let rec desugar_rchain chain s e = %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool 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 +%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield Constant %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure %token InternalPLet InternalReturn @@ -549,7 +549,8 @@ 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 ([mk_kopt (KOpt_none v) $startpos $endpos], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos } + let kopt = mk_kopt (KOpt_kind (None, [v], None)) $startpos $endpos in + mk_typ (ATyp_exist ([kopt], 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 kopt_list Comma typ Dot typ Rcurly @@ -573,11 +574,19 @@ kind: | Bool { K_aux (K_bool, loc $startpos $endpos) } +kid_list: + | kid + { [$1] } + | kid kid_list + { $1 :: $2 } + kopt: - | Lparen kid Colon kind Rparen - { KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) } + | Lparen Constant kid_list Colon kind Rparen + { KOpt_aux (KOpt_kind (Some "constant", $3, Some $5), loc $startpos $endpos) } + | Lparen kid_list Colon kind Rparen + { KOpt_aux (KOpt_kind (None, $2, Some $4), loc $startpos $endpos) } | kid - { KOpt_aux (KOpt_none $1, loc $startpos $endpos) } + { KOpt_aux (KOpt_kind (None, [$1], None), loc $startpos $endpos) } kopt_list: | kopt @@ -587,7 +596,7 @@ kopt_list: typquant: | kopt_list Comma typ - { let qi_nc = QI_aux (QI_const $3, loc $startpos($3) $endpos($3)) in + { let qi_nc = QI_aux (QI_constraint $3, loc $startpos($3) $endpos($3)) in TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1 @ [qi_nc]), loc $startpos $endpos) } | kopt_list { TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1), loc $startpos $endpos) } @@ -1159,9 +1168,9 @@ r_def_body: param_kopt: | kid Colon kind - { KOpt_aux (KOpt_kind ($3, $1), loc $startpos $endpos) } + { KOpt_aux (KOpt_kind (None, [$1], Some $3), loc $startpos $endpos) } | kid - { KOpt_aux (KOpt_none $1, loc $startpos $endpos) } + { KOpt_aux (KOpt_kind (None, [$1], None), loc $startpos $endpos) } param_kopt_list: | param_kopt @@ -1171,7 +1180,7 @@ param_kopt_list: typaram: | Lparen param_kopt_list Rparen Comma typ - { let qi_nc = QI_aux (QI_const $5, loc $startpos($5) $endpos($5)) in + { let qi_nc = QI_aux (QI_constraint $5, loc $startpos($5) $endpos($5)) in mk_typq $2 [qi_nc] $startpos $endpos } | Lparen param_kopt_list Rparen { mk_typq $2 [] $startpos $endpos } diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index f26c74d7..55928e06 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -935,7 +935,8 @@ let doc_quant_item_id ctx delimit (QI_aux (qi,_)) = | K_order -> None | K_bool -> Some (delimit (separate space [doc_var ctx kid; colon; string "bool"])) end - | QI_const nc -> None + | QI_constraint nc -> None + | QI_constant _ -> None let quant_item_id_name ctx (QI_aux (qi,_)) = match qi with @@ -947,19 +948,22 @@ let quant_item_id_name ctx (QI_aux (qi,_)) = | K_order -> None | K_bool -> Some (doc_var ctx kid) end - | QI_const nc -> None + | QI_constraint nc -> None + | QI_constant _ -> None let doc_quant_item_constr ctx delimit (QI_aux (qi,_)) = match qi with | QI_id _ -> None - | QI_const nc -> Some (bquote ^^ braces (doc_arithfact ctx Env.empty nc)) + | QI_constant _ -> None + | QI_constraint nc -> Some (bquote ^^ braces (doc_arithfact ctx Env.empty nc)) (* At the moment these are all anonymous - when used we rely on Coq to fill them in. *) let quant_item_constr_name ctx (QI_aux (qi,_)) = match qi with | QI_id _ -> None - | QI_const nc -> Some underscore + | QI_constant _ -> None + | QI_constraint nc -> Some underscore let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) = match tq with diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index f13b8e1b..ae86a0fd 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1041,7 +1041,8 @@ let doc_typquant_sorts idpp (TypQ_aux (typq,_)) = | QI_id (KOpt_aux (KOpt_kind (K_aux (K_int,_),kid),_)) -> Some (string "`len`") | QI_id (KOpt_aux (KOpt_kind (K_aux (K_type,_),kid),_)) -> Some underscore | QI_id (KOpt_aux (KOpt_kind (K_aux ((K_order|K_bool),_),kid),_)) -> None - | QI_const _ -> None + | QI_constraint _ -> None + | QI_constant _ -> None in if List.exists (function (QI_aux (QI_id (KOpt_aux (KOpt_kind (K_aux (K_int,_),_),_)),_)) -> true | _ -> false) qs then let qs_pp = Util.map_filter q qs in diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index ad44f5b8..da44645c 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -210,21 +210,48 @@ and doc_arg_typs = function | [typ] -> doc_typ typ | typs -> parens (separate_map (comma ^^ space) doc_typ typs) +let doc_kind (K_aux (k, _)) = + string (match k with + | K_int -> "Int" + | K_type -> "Type" + | K_bool -> "Bool" + | K_order -> "Order") + +let rec doc_kopts constants = + let is_in_group is_constant kind kopt = + Kind.compare kind (kopt_kind kopt) = 0 && KOptSet.mem kopt constants = is_constant + in + function + | kopt :: kopts -> + let is_constant = KOptSet.mem kopt constants in + let group, kopts = Util.take_drop (is_in_group is_constant (kopt_kind kopt)) kopts in + let attr = if is_constant then string "constant" ^^ space else empty in + parens (attr ^^ separate space (List.map (fun kopt -> doc_kid (kopt_kid kopt)) (kopt :: group)) + ^^ space ^^ colon + ^^ space ^^ doc_kind (kopt_kind kopt)) + ^^ begin match kopts with + | [] -> empty + | _ -> doc_kopts constants kopts + end + | [] -> empty + let doc_quants quants = - let doc_qi_kopt (QI_aux (qi_aux, _)) = - match qi_aux with - | QI_id kopt when is_int_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])] - | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])] - | QI_id kopt when is_bool_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])] - | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])] - | QI_const nc -> [] + let rec get_constants = function + | QI_aux (QI_constant kopts, _) :: qis -> KOptSet.union (KOptSet.of_list kopts) (get_constants qis) + | _ :: qis -> get_constants qis + | [] -> KOptSet.empty + in + let rec get_kopts = function + | QI_aux (QI_id kopt, _) :: qis -> kopt :: get_kopts qis + | _ :: qis -> get_kopts qis + | [] -> [] in let qi_nc (QI_aux (qi_aux, _)) = match qi_aux with - | QI_const nc -> [nc] + | QI_constraint nc -> [nc] | _ -> [] in - let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in + let kdoc = doc_kopts (get_constants quants) (get_kopts quants) in let ncs = List.concat (List.map qi_nc quants) in match ncs with | [] -> kdoc @@ -238,11 +265,12 @@ let doc_param_quants quants = | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"] | QI_id kopt when is_bool_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"] | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"] - | QI_const nc -> [] + | QI_constraint _ -> [] + | QI_constant _ -> [] in let qi_nc (QI_aux (qi_aux, _)) = match qi_aux with - | QI_const nc -> [nc] + | QI_constraint nc -> [nc] | _ -> [] in let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in diff --git a/src/slice.ml b/src/slice.ml index fa574b7f..78009059 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -217,7 +217,7 @@ let add_def_to_graph graph def = let scan_quant_item self (QI_aux (aux, _)) = match aux with | QI_id _ -> () - | QI_const nc -> + | QI_constraint nc -> IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (constraint_ids nc) in diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml index 6b8fede4..fad45412 100644 --- a/src/toFromInterp_backend.ml +++ b/src/toFromInterp_backend.ml @@ -129,7 +129,8 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = in let fromValueTypq (QI_aux (qi_aux, _)) = match qi_aux with | QI_id (KOpt_aux (KOpt_kind (K_aux (kind_aux, _), kid), _)) -> fromValueKid kid - | QI_const _ -> empty + | QI_constant _ -> empty + | QI_constraint _ -> empty in let fromValueTypqs (TypQ_aux (typq_aux, _)) = match typq_aux with | TypQ_no_forall -> [empty] @@ -283,7 +284,8 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) = in let toValueTypq (QI_aux (qi_aux, _)) = match qi_aux with | QI_id (KOpt_aux (KOpt_kind (K_aux (kind_aux, _), kid), _)) -> toValueKid kid - | QI_const _ -> empty + | QI_constant _ -> empty + | QI_constraint _ -> empty in let toValueTypqs (TypQ_aux (typq_aux, _)) = match typq_aux with | TypQ_no_forall -> [empty] diff --git a/src/type_check.ml b/src/type_check.ml index 0365e2e5..2ce6ea94 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -246,7 +246,8 @@ and strip_quant_item = function | QI_aux (qi_aux, _) -> QI_aux (strip_qi_aux qi_aux, Parse_ast.Unknown) and strip_qi_aux = function | QI_id kinded_id -> QI_id (strip_kinded_id kinded_id) - | QI_const constr -> QI_const (strip_n_constraint constr) + | QI_constant kopts -> QI_constant (List.map strip_kinded_id kopts) + | QI_constraint constr -> QI_constraint (strip_n_constraint constr) and strip_kinded_id = function | KOpt_aux (kinded_id_aux, _) -> KOpt_aux (strip_kinded_id_aux kinded_id_aux, Parse_ast.Unknown) and strip_kinded_id_aux = function @@ -1312,7 +1313,8 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t = let rec add_quant_item env = function | QI_aux (qi, _) -> add_quant_item_aux env qi and add_quant_item_aux env = function - | QI_const constr -> Env.add_constraint constr env + | QI_constraint constr -> Env.add_constraint constr env + | QI_constant _ -> env | QI_id kopt -> Env.add_typ_var l kopt env in match quant with @@ -1811,16 +1813,32 @@ let subst_unifiers unifiers typ = let subst_unifiers_typ_arg unifiers typ_arg = List.fold_left (fun typ_arg (v, arg) -> typ_arg_subst v arg typ_arg) typ_arg (KBindings.bindings unifiers) -let instantiate_quant (v, arg) (QI_aux (aux, l) as qi) = +let instantiate_quant env (v, arg) (QI_aux (aux, l) as qi) = match aux with | QI_id kopt when Kid.compare (kopt_kid kopt) v = 0 -> typ_debug (lazy ("Instantiated " ^ string_of_quant_item qi)); None | QI_id _ -> Some qi - | QI_const nc -> Some (QI_aux (QI_const (constraint_subst v arg nc), l)) + | QI_constant kopts -> + let kopts = + Util.map_filter (fun kopt -> + if Kid.compare (kopt_kid kopt) v = 0 then + begin match arg with + | A_aux (A_nexp nexp, _) -> + if is_nexp_constant (Env.expand_nexp_synonyms env nexp) then None else Some kopt + | _ -> Some kopt + end + else + Some kopt + ) kopts in + begin match kopts with + | [] -> None + | _ -> Some (QI_aux (QI_constant kopts, l)) + end + | QI_constraint nc -> Some (QI_aux (QI_constraint (constraint_subst v arg nc), l)) -let instantiate_quants quants unifier = - List.map (instantiate_quant unifier) quants |> Util.option_these +let instantiate_quants env quants unifier = + List.map (instantiate_quant env unifier) quants |> Util.option_these (* During typechecking, we can run into the following issue, where we have a function like @@ -2374,8 +2392,8 @@ let instantiate_simple_equations = in let rec find_eqs_quant kid (QI_aux (qi,_)) = match qi with - | QI_id _ -> [] - | QI_const nc -> find_eqs kid nc + | QI_id _ | QI_constant _ -> [] + | QI_constraint nc -> find_eqs kid nc in let rec inst_from_eq = function | [] -> KBindings.empty @@ -2561,7 +2579,8 @@ let rec add_constraints constrs env = let solve_quant env = function | QI_aux (QI_id _, _) -> false - | QI_aux (QI_const nc, _) -> prove __POS__ env nc + | QI_aux (QI_constant _, _) -> false + | QI_aux (QI_constraint nc, _) -> prove __POS__ env nc (* When doing implicit type coercion, for performance reasons we want to filter out the possible casts to only those that could @@ -3163,7 +3182,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for pattern " ^ string_of_typ typ)); let unifiers = unify l env goals ret_typ typ in let arg_typ' = subst_unifiers unifiers arg_typ in - let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in + let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in if not (List.for_all (solve_quant env) quants') then typ_raise env l (Err_unresolved_quants (f, quants', Env.get_locals env, Env.get_constraints env)) else (); @@ -3176,7 +3195,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) end | _ -> typ_error env l ("Mal-formed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ) end - + | P_app (f, pats) when Env.is_union_constructor f env -> (* Treat Ctor(x, y) as Ctor((x, y)) *) bind_pat env (P_aux (P_app (f, [mk_pat (P_tup pats)]),(l,()))) typ @@ -3198,7 +3217,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) (* FIXME: There's no obvious goals here *) let unifiers = unify l env (tyvars_of_typ typ2) typ2 typ in let arg_typ' = subst_unifiers unifiers typ1 in - let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in + let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in if (match quants' with [] -> false | _ -> true) then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat) else (); @@ -3216,7 +3235,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ)); let unifiers = unify l env (tyvars_of_typ typ1) typ1 typ in let arg_typ' = subst_unifiers unifiers typ2 in - let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in + let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in if (match quants' with [] -> false | _ -> true) then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat) else (); @@ -3875,7 +3894,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ = typ_debug (lazy (string_of_list ", " (fun (kid, arg) -> string_of_kid kid ^ " => " ^ string_of_typ_arg arg) (KBindings.bindings unifiers))); all_unifiers := unifiers; let typ_args = List.map (subst_unifiers unifiers) typ_args in - List.iter (fun unifier -> quants := instantiate_quants !quants unifier) (KBindings.bindings unifiers); + List.iter (fun unifier -> quants := instantiate_quants env !quants unifier) (KBindings.bindings unifiers); List.iter (fun (v, arg) -> typ_ret := typ_subst v arg !typ_ret) (KBindings.bindings unifiers); typ_debug (lazy ("Quantifiers " ^ Util.string_of_list ", " string_of_quant_item !quants)); @@ -3897,13 +3916,6 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ = [], List.map implicit_to_int typ_args, xs in - let instantiate_quant (v, arg) (QI_aux (aux, l) as qi) = - match aux with - | QI_id kopt when Kid.compare (kopt_kid kopt) v = 0 -> None - | QI_id _ -> Some qi - | QI_const nc -> Some (QI_aux (QI_const (constraint_subst v arg nc), l)) - in - let typ_args = match expected_ret_typ with | None -> typ_args | Some expect when is_exist (Env.expand_synonyms env expect) || is_exist !typ_ret -> typ_args @@ -3915,7 +3927,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ = let unifiers = KBindings.bindings unifiers in typ_debug (lazy (Util.("Unifiers " |> magenta |> clear) ^ Util.string_of_list ", " (fun (v, arg) -> string_of_kid v ^ " => " ^ string_of_typ_arg arg) unifiers)); - List.iter (fun unifier -> quants := instantiate_quants !quants unifier) unifiers; + List.iter (fun unifier -> quants := instantiate_quants env !quants unifier) unifiers; List.iter (fun (v, arg) -> typ_ret := typ_subst v arg !typ_ret) unifiers; List.map (fun typ -> List.fold_left (fun typ (v, arg) -> typ_subst v arg typ) typ unifiers) typ_args with Unification_error _ -> typ_args @@ -3938,7 +3950,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ = let unifiers = KBindings.bindings unifiers in typ_debug (lazy (Util.("Unifiers " |> magenta |> clear) ^ Util.string_of_list ", " (fun (v, arg) -> string_of_kid v ^ " => " ^ string_of_typ_arg arg) unifiers)); - List.iter (fun unifier -> quants := instantiate_quants !quants unifier) unifiers; + List.iter (fun unifier -> quants := instantiate_quants env !quants unifier) unifiers; List.iter (fun (v, arg) -> typ_ret := typ_subst v arg !typ_ret) unifiers; let remaining_typs = List.map (fun typ -> List.fold_left (fun typ (v, arg) -> typ_subst v arg typ) typ unifiers) remaining_typs @@ -4084,7 +4096,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) ( typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for mapping-pattern " ^ string_of_typ typ)); let unifiers = unify l env (tyvars_of_typ ret_typ) ret_typ typ in let arg_typ' = subst_unifiers unifiers arg_typ in - let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in + let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in if (match quants' with [] -> false | _ -> true) then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat) else (); @@ -4114,7 +4126,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) ( typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for mapping-pattern " ^ string_of_typ typ)); let unifiers = unify l env (tyvars_of_typ typ2) typ2 typ in let arg_typ' = subst_unifiers unifiers typ1 in - let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in + let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in if (match quants' with [] -> false | _ -> true) then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat) else (); @@ -4131,7 +4143,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) ( typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for mapping-pattern " ^ string_of_typ typ)); let unifiers = unify l env (tyvars_of_typ typ1) typ1 typ in let arg_typ' = subst_unifiers unifiers typ2 in - let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in + let quants' = List.fold_left (instantiate_quants env) quants (KBindings.bindings unifiers) in if (match quants' with [] -> false | _ -> true) then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat) else (); diff --git a/src/type_error.ml b/src/type_error.ml index e75d2cd4..eed1379a 100644 --- a/src/type_error.ml +++ b/src/type_error.ml @@ -58,7 +58,7 @@ type suggestion = | Suggest_none let rec analyze_unresolved_quant locals ncs = function - | QI_aux (QI_const nc, _) -> + | QI_aux (QI_constraint nc, _) -> let gen_kids = List.filter is_kid_generated (KidSet.elements (tyvars_of_constraint nc)) in if gen_kids = [] then Suggest_add_constraint nc @@ -99,7 +99,7 @@ let rec analyze_unresolved_quant locals ncs = function else Suggest_none - | QI_aux (QI_id kopt, _) -> + | QI_aux (QI_id _, _) | QI_aux (QI_constant _, _) -> Suggest_none let message_of_type_error = -- cgit v1.2.3