From 62f487344be062fd897a22a13f87530db136b92a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 1 May 2024 17:39:20 +0200 Subject: [PATCH] Laxer kernel typing rule for template inductive types. Under the view that template types are an optimization of sort-polymorphic inductive types, the requirement that the sort of an argument lives below the global template universe of the corresponding parameter is spurious. --- kernel/inductive.ml | 121 ++++++++++++++++++++++++++++++------------ kernel/inductive.mli | 8 +-- kernel/typeops.ml | 36 ++++++++++--- pretyping/retyping.ml | 12 +++-- pretyping/typing.ml | 25 ++++++++- 5 files changed, 153 insertions(+), 49 deletions(-) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 957a2476a0bf8..17142882e74c0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -209,10 +209,59 @@ let subst_univs_sort subs = function let fold accu (u, n) = Universe.sup accu (supern u n) in Sorts.sort_of_univ (List.fold_left fold (supern u n) rest) -let instantiate_universes ctx (templ, ar) args = +let get_arity c = + let decls, c = Term.decompose_prod_decls c in + match kind c with + | Sort (Sorts.Type u) -> + begin match Universe.level u with + | Some l -> (decls, l) + | None -> assert false + end + | _ -> assert false + +let rec subst_univs_ctx accu subs ctx params = match ctx, params with +| [], [] -> accu +| (LocalDef _ as decl) :: ctx, params -> + subst_univs_ctx (decl :: accu) subs ctx params +| (LocalAssum _ as decl) :: ctx, None :: params -> + subst_univs_ctx (decl :: accu) subs ctx params +| LocalAssum (na, t) :: ctx, Some _ :: params -> + let (decls, u) = get_arity t in + let u = subst_univs_sort subs (Sorts.sort_of_univ (Universe.make u)) in + let decl = LocalAssum (na, Term.it_mkProd_or_LetIn (mkSort u) decls) in + subst_univs_ctx (decl :: accu) subs ctx params +| _, [] | [], _ -> assert false + +let instantiate_template_constraints subst templ = + let _, cstrs = templ.template_context in + let fold (u, cst, v) accu = + (* v is not a local universe by the unbounded from below property *) + let u = subst_univs_sort subst (Sorts.sort_of_univ (Universe.make u)) in + match u with + | Sorts.QSort _ | Sorts.SProp -> assert false + | Sorts.Prop -> accu + | Sorts.Set -> Constraints.add (Univ.Level.set, cst, v) accu + | Sorts.Type u -> + let fold accu (u, n) = match n, cst with + | 0, _ -> Constraints.add (u, cst, v) accu + | 1, Le -> Constraints.add (u, Lt, v) accu + | 1, (Eq | Lt) -> assert false (* FIXME? *) + | _ -> assert false + in + List.fold_left fold accu (Univ.Universe.repr u) + in + Constraints.fold fold cstrs Constraints.empty + +let instantiate_template_universes (mib, _mip) args = + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in + let ctx = List.rev mib.mind_params_ctxt in let subst = make_subst (ctx,templ.template_param_levels,args) in - let ty = subst_univs_sort subst ar.template_level in - (ctx, ty) + let ctx = subst_univs_ctx [] subst ctx templ.template_param_levels in + let cstrs = instantiate_template_constraints subst templ in + (cstrs, ctx, subst) (* Type of an inductive type *) @@ -232,33 +281,26 @@ let check_instance mib u = let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = check_instance mib u; match mip.mind_arity with - | RegularArity a -> subst_instance_constr u a.mind_user_arity + | RegularArity a -> + let cst = instantiate_inductive_constraints mib u in + subst_instance_constr u a.mind_user_arity, cst | TemplateArity ar -> - let templ = match mib.mind_template with - | None -> assert false - | Some t -> t - in - let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes ctx (templ, ar) paramtyps in - (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. - the situation where a non-Prop singleton inductive becomes Prop - when applied to Prop params *) - if not polyprop && not (Sorts.is_prop ar.template_level) && Sorts.is_prop s - then raise (SingletonInductiveBecomesProp mip.mind_typename); - Term.mkArity (List.rev ctx,s) + let cst, params, subst = instantiate_template_universes (mib, mip) paramtyps in + let ctx = (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) @ params in + let s = subst_univs_sort subst ar.template_level in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (Sorts.is_prop ar.template_level) && Sorts.is_prop s + then raise (SingletonInductiveBecomesProp mip.mind_typename); + Term.mkArity (ctx, s), cst let type_of_inductive pind = - type_of_inductive_gen pind [] + let (ty, _cst) = type_of_inductive_gen pind [] in + ty -let constrained_type_of_inductive ((mib,_mip),u as pind) = - let ty = type_of_inductive pind in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - -let constrained_type_of_inductive_knowing_parameters ((mib,_mip),u as pind) args = - let ty = type_of_inductive_gen pind args in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) +let constrained_type_of_inductive pind = + type_of_inductive_gen pind [] let type_of_inductive_knowing_parameters ?(polyprop=true) mip args = type_of_inductive_gen ~polyprop mip args @@ -266,17 +308,30 @@ let type_of_inductive_knowing_parameters ?(polyprop=true) mip args = (************************************************************************) (* Type of a constructor *) -let type_of_constructor (cstr, u) (mib,mip) = +let type_of_constructor_gen (cstr, u) (mib,mip) paramtyps = check_instance mib u; let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); - subst_instance_constr u mip.mind_user_lc.(i-1) - -let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) = - let ty = type_of_constructor cstru ind in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) + match mip.mind_arity with + | RegularArity _ -> + let cst = instantiate_inductive_constraints mib u in + subst_instance_constr u mip.mind_user_lc.(i-1), cst + | TemplateArity _ar -> + let cst, params, _ = instantiate_template_universes (mib, mip) paramtyps in + let _, typ = Term.decompose_prod_n_decls (List.length mib.mind_params_ctxt) mip.mind_user_lc.(i - 1) in + let typ = Term.it_mkProd_or_LetIn typ params in + typ, cst + +let type_of_constructor pcstr ind = + let (ty, _cst) = type_of_constructor_gen pcstr ind [] in + ty + +let constrained_type_of_constructor cstru ind = + type_of_constructor_gen cstru ind [] + +let type_of_constructor_knowing_parameters cstr specif args = + type_of_constructor_gen cstr specif args let arities_of_constructors (_,u) (_,mip) = let map (ctx, c) = diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 221b933aecfca..3557f6b3dc287 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -52,9 +52,10 @@ type template_univ = type param_univs = (expected:Univ.Level.t -> template_univ) list +val instantiate_template_universes : mind_specif -> param_univs -> + Constraints.t * rel_context * template_univ Univ.Level.Map.t + val constrained_type_of_inductive : mind_specif puniverses -> types constrained -val constrained_type_of_inductive_knowing_parameters : - mind_specif puniverses -> param_univs -> types constrained val relevance_of_ind_body : one_inductive_body -> UVars.Instance.t -> Sorts.relevance @@ -63,7 +64,7 @@ val relevance_of_inductive : env -> pinductive -> Sorts.relevance val type_of_inductive : mind_specif puniverses -> types val type_of_inductive_knowing_parameters : - ?polyprop:bool -> mind_specif puniverses -> param_univs -> types + ?polyprop:bool -> mind_specif puniverses -> param_univs -> types constrained val quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool (** For squashing. *) @@ -81,6 +82,7 @@ val is_primitive_record : mind_specif -> bool val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained val type_of_constructor : pconstructor -> mind_specif -> types +val type_of_constructor_knowing_parameters : pconstructor -> mind_specif -> param_univs -> types constrained (** Return constructor types in normal form *) val arities_of_constructors : pinductive -> mind_specif -> types array diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b22216083ef93..f7a7acef3711e 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -417,11 +417,11 @@ let make_param_univs env indu spec args argtys = let type_of_inductive_knowing_parameters env (ind,u as indu) args argst = let (mib,_mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - (spec,u) (make_param_univs env indu spec args argst) - in - check_constraints cst env; + let () = assert (Option.has_some mib.mind_template) in + let () = check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps in + let param_univs = make_param_univs env indu spec args argst in + let t, cst = Inductive.type_of_inductive_knowing_parameters (spec,u) param_univs in + let () = check_constraints cst env in t let type_of_inductive env (ind,u) = @@ -433,6 +433,16 @@ let type_of_inductive env (ind,u) = (* Constructors. *) +let type_of_constructor_knowing_parameters env (c, u as cu) args argst = + let ind = inductive_of_constructor c in + let (mib, _ as spec) = lookup_mind_specif env ind in + let () = assert (Option.has_some mib.mind_template) in + let () = check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps in + let param_univs = make_param_univs env (ind, u) spec args argst in + let t, cst = Inductive.type_of_constructor_knowing_parameters cu spec param_univs in + let () = check_constraints cst env in + t + let type_of_constructor env (c,_u as cu) = let (mib, _ as specif) = lookup_mind_specif env (inductive_of_constructor c) in let () = check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps in @@ -655,6 +665,8 @@ let rec execute env cstr = match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> type_of_inductive_knowing_parameters env ind args argst + | Construct ((ind, _), _ as cstr) when Environ.template_polymorphic_ind ind env -> + type_of_constructor_knowing_parameters env cstr args argst | _ -> (* No template polymorphism *) execute env f @@ -711,11 +723,19 @@ let rec execute env cstr = in let mib, mip = Inductive.lookup_mind_specif env ci.ci_ind in - let cst = Inductive.instantiate_inductive_constraints mib u in - let () = check_constraints cst env in let pmst = execute_array env pms in + let cst, params = match mib.mind_template with + | None -> + let cst = Inductive.instantiate_inductive_constraints mib u in + cst, mib.mind_params_ctxt + | Some _ -> + let args = make_param_univs env (ci.ci_ind, u) (mib, mip) pms pmst in + let (cst, params, _) = instantiate_template_universes (mib, mip) args in + cst, params + in + let () = check_constraints cst env in let paramsubst = - try type_of_parameters env mib.mind_params_ctxt u pms pmst + try type_of_parameters env params u pms pmst with ArgumentsMismatch -> error_elim_arity env (ci.ci_ind, u) c None in let (pctx, pt) = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 3a47d0aef8a57..28c93cf5fe305 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -217,11 +217,15 @@ let retype ?(polyprop=true) sigma = let u = EInstance.kind sigma u in let mip = lookup_mind_specif env ind in let paramtyps = make_param_univs env sigma (ind,u) args in - EConstr.of_constr - (Inductive.type_of_inductive_knowing_parameters - ~polyprop (mip, u) paramtyps) + let (ty, _) = Inductive.type_of_inductive_knowing_parameters ~polyprop (mip, u) paramtyps in + EConstr.of_constr ty | Construct (cstr, u) -> - type_of_constructor env (cstr, u) + let u = EInstance.kind sigma u in + let (ind, _) = cstr in + let mip = lookup_mind_specif env ind in + let paramtyps = make_param_univs env sigma (ind, u) args in + let (ty, _) = Inductive.type_of_constructor_knowing_parameters (cstr, u) mip paramtyps in + EConstr.of_constr ty | _ -> assert false and make_param_univs env sigma indu args = diff --git a/pretyping/typing.ml b/pretyping/typing.ml index ccbf40494a687..a10683f68a05c 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -55,6 +55,13 @@ let inductive_type_knowing_parameters env sigma (ind,u as indu) jl = let paramstyp = make_param_univs env sigma indu mspec jl in Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp +let constructor_type_knowing_parameters env sigma (cstr, u) jl = + let u0 = Unsafe.to_instance u in + let (ind, _) = cstr in + let mspec = lookup_mind_specif env ind in + let paramstyp = make_param_univs env sigma (ind, u) mspec jl in + Inductive.type_of_constructor_knowing_parameters (cstr, u0) mspec paramstyp + let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with | Sort s -> sigma, {utj_val = j.uj_val; utj_type = s } @@ -111,7 +118,8 @@ let checked_appvect env sigma f args = let checked_applist env sigma f args = checked_appvect env sigma f (Array.of_list args) let judge_of_applied_inductive_knowing_parameters_nocheck env sigma funj ind argjv = - let ar = inductive_type_knowing_parameters env sigma ind argjv in + let ar, csts = inductive_type_knowing_parameters env sigma ind argjv in + let sigma = Evd.add_constraints sigma csts in let typ = hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) in sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ } @@ -119,6 +127,16 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv = let (sigma, j) = judge_of_apply env sigma funj argjv in judge_of_applied_inductive_knowing_parameters_nocheck env sigma funj ind argjv +let judge_of_applied_constructor_knowing_parameters_nocheck env sigma funj cstr argjv = + let ar, csts = constructor_type_knowing_parameters env sigma cstr argjv in + let sigma = Evd.add_constraints sigma csts in + let typ = hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) in + sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ } + +let judge_of_applied_constructor_knowing_parameters env sigma funj ind argjv = + let (sigma, j) = judge_of_apply env sigma funj argjv in + judge_of_applied_constructor_knowing_parameters_nocheck env sigma funj ind argjv + let check_branch_types env sigma (ind,u) cj (lfj,explft) = if not (Int.equal (Array.length lfj) (Array.length explft)) then error_number_branches env sigma cj (Array.length explft); @@ -543,6 +561,9 @@ let rec execute env sigma cstr = | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> let sigma, fj = execute env sigma f in judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl + | Construct (cstr, u) when EInstance.is_empty u && Environ.template_polymorphic_ind (fst cstr) env -> + let sigma, fj = execute env sigma f in + judge_of_applied_constructor_knowing_parameters env sigma fj (cstr, u) jl | _ -> (* No template polymorphism *) let sigma, fj = execute env sigma f in @@ -781,6 +802,8 @@ let rec recheck_against env sigma good c = (match EConstr.kind sigma f with | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> maybe_changed (judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl) + | Construct (cstr, u) when EInstance.is_empty u && Environ.template_polymorphic_ind (fst cstr) env -> + maybe_changed (judge_of_applied_constructor_knowing_parameters env sigma fj (cstr, u) jl) | _ -> (* No template polymorphism *) maybe_changed (judge_of_apply env sigma fj jl))