diff options
| -rw-r--r-- | checker/checkInductive.ml | 33 | ||||
| -rw-r--r-- | checker/checkTypes.mli | 2 | ||||
| -rw-r--r-- | checker/values.ml | 10 | ||||
| -rw-r--r-- | kernel/cooking.ml | 24 | ||||
| -rw-r--r-- | kernel/declarations.ml | 7 | ||||
| -rw-r--r-- | kernel/declareops.ml | 7 | ||||
| -rw-r--r-- | kernel/environ.ml | 8 | ||||
| -rw-r--r-- | kernel/indTyping.ml | 104 | ||||
| -rw-r--r-- | kernel/indTyping.mli | 1 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 7 | ||||
| -rw-r--r-- | kernel/inductive.ml | 10 | ||||
| -rw-r--r-- | kernel/inductive.mli | 3 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 6 |
14 files changed, 142 insertions, 86 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index b93b03ec16..c4c6d9bb4f 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -20,7 +20,7 @@ exception InductiveMismatch of MutInd.t * string let check mind field b = if not b then raise (InductiveMismatch (mind,field)) -let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = +let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = let open Entries in let nparams = List.length mb.mind_params_ctxt in (* include letins *) let mind_entry_record = match mb.mind_record with @@ -33,20 +33,9 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = inductive types. The set of monomorphic constraints is already part of the graph at that point, but we need to emulate a broken bound variable mechanism for template inductive types. *) - let fold accu ind = match ind.mind_arity with - | RegularArity _ -> accu - | TemplateArity ar -> - match accu with - | None -> Some ar.template_context - | Some ctx -> - (* Ensure that all template contexts agree. This is enforced by the - kernel. *) - let () = check mind "mind_arity" (ContextSet.equal ctx ar.template_context) in - Some ctx - in - let univs = match Array.fold_left fold None mb.mind_packets with + let univs = match mb.mind_template with | None -> ContextSet.empty - | Some ctx -> ctx + | Some ctx -> ctx.template_context in Monomorphic_entry univs | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) @@ -95,13 +84,18 @@ let check_arity env ar1 ar2 = match ar1, ar2 with | RegularArity ar, RegularArity {mind_user_arity;mind_sort} -> Constr.equal ar.mind_user_arity mind_user_arity && Sorts.equal ar.mind_sort mind_sort - | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} -> - List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && - ContextSet.equal template_context ar.template_context && + | TemplateArity ar, TemplateArity {template_level} -> UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> assert false +let check_template ar1 ar2 = match ar1, ar2 with +| None, None -> true +| Some ar, Some {template_context; template_param_levels} -> + List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && + ContextSet.equal template_context ar.template_context +| None, Some _ | Some _, None -> false + let check_kelim k1 k2 = Sorts.family_leq k1 k2 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost @@ -163,10 +157,10 @@ let check_same_record r1 r2 = match r1, r2 with | (NotRecord | FakeRecord | PrimRecord _), _ -> false let check_inductive env mind mb = - let entry = to_entry mind mb in + let entry = to_entry mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; mind_nparams; mind_nparams_rec; mind_params_ctxt; - mind_universes; mind_variance; mind_sec_variance; + mind_universes; mind_template; mind_variance; mind_sec_variance; mind_private; mind_typing_flags; } = (* Locally set typing flags for further typechecking *) @@ -197,6 +191,7 @@ let check_inductive env mind mb = check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); ignore mind_universes; (* Indtypes did the necessary checking *) + check "mind_template" (check_template mb.mind_template mind_template); check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal) mb.mind_variance mind_variance); check "mind_sec_variance" (Option.is_empty mind_sec_variance); diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli index ac9ea2fb31..9ef6ff017c 100644 --- a/checker/checkTypes.mli +++ b/checker/checkTypes.mli @@ -17,4 +17,4 @@ open Environ (*s Typing functions (not yet tagged as safe) *) val check_polymorphic_arity : - env -> rel_context -> template_arity -> unit + env -> rel_context -> template_universes -> unit diff --git a/checker/values.ml b/checker/values.ml index ed730cff8e..cba96e6636 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -227,8 +227,11 @@ let v_oracle = v_pred v_cst; |] -let v_pol_arity = - v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|] +let v_template_arity = + v_tuple "template_arity" [|v_univ|] + +let v_template_universes = + v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) @@ -265,7 +268,7 @@ let v_mono_ind_arity = v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|] let v_ind_arity = v_sum "inductive_arity" 0 - [|[|v_mono_ind_arity|];[|v_pol_arity|]|] + [|[|v_mono_ind_arity|];[|v_template_arity|]|] let v_one_ind = v_tuple "one_inductive_body" [|v_id; @@ -301,6 +304,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; v_rctxt; v_univs; (* universes *) + Opt v_template_universes; Opt (Array v_variance); Opt (Array v_variance); Opt v_bool; diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 31dd26d2ba..13ee353c6b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -295,20 +295,14 @@ let abstract_projection ~params expmod hyps t = t let cook_one_ind ~ntypes - (section_decls,_ as hyps) expmod mip = + hyps expmod mip = let mind_arity = match mip.mind_arity with | RegularArity {mind_user_arity=arity;mind_sort=sort} -> let arity = abstract_as_type (expmod arity) hyps in let sort = destSort (expmod (mkSort sort)) in RegularArity {mind_user_arity=arity; mind_sort=sort} - | TemplateArity {template_param_levels=levels;template_level;template_context} -> - let sec_levels = CList.map_filter (fun d -> - if RelDecl.is_local_assum d then Some None - else None) - section_decls - in - let levels = List.rev_append sec_levels levels in - TemplateArity {template_param_levels=levels;template_level;template_context} + | TemplateArity {template_level} -> + TemplateArity {template_level} in let mind_arity_ctxt = let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in @@ -386,6 +380,17 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = in Some (Array.append newvariance variance), Some sec_variance in + let mind_template = match mib.mind_template with + | None -> None + | Some {template_param_levels=levels; template_context} -> + let sec_levels = CList.map_filter (fun d -> + if RelDecl.is_local_assum d then Some None + else None) + section_decls + in + let levels = List.rev_append sec_levels levels in + Some {template_param_levels=levels; template_context} + in { mind_packets; mind_record; @@ -396,6 +401,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = mind_nparams_rec = mib.mind_nparams_rec + nnewparams; mind_params_ctxt; mind_universes; + mind_template; mind_variance; mind_sec_variance; mind_private = mib.mind_private; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index ac130d018d..11a07ee5cf 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -30,8 +30,11 @@ type engagement = set_predicativity *) type template_arity = { - template_param_levels : Univ.Level.t option list; template_level : Univ.Universe.t; +} + +type template_universes = { + template_param_levels : Univ.Level.t option list; template_context : Univ.ContextSet.t; } @@ -218,6 +221,8 @@ type mutual_inductive_body = { mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_template : template_universes option; + mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) mind_sec_variance : Univ.Variance.t array option; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a3adac7a11..a1122d1279 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -46,9 +46,10 @@ let map_decl_arity f g = function | TemplateArity a -> TemplateArity (g a) let hcons_template_arity ar = + { template_level = Univ.hcons_univ ar.template_level; } + +let hcons_template_universe ar = { template_param_levels = ar.template_param_levels; - (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) - template_level = Univ.hcons_univ ar.template_level; template_context = Univ.hcons_universe_context_set ar.template_context } let universes_context = function @@ -247,6 +248,7 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; + mind_template = mib.mind_template; mind_variance = mib.mind_variance; mind_sec_variance = mib.mind_sec_variance; mind_private = mib.mind_private; @@ -323,6 +325,7 @@ let hcons_mind mib = { mib with mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; + mind_template = Option.Smart.map hcons_template_universe mib.mind_template; mind_universes = hcons_universes mib.mind_universes } (** Hashconsing of modules *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 501ac99ff3..1b5a77cc96 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -590,11 +590,11 @@ let template_polymorphic_ind (mind,i) env = | TemplateArity _ -> true | RegularArity _ -> false -let template_polymorphic_variables (mind,i) env = - match (lookup_mind mind env).mind_packets.(i).mind_arity with - | TemplateArity { Declarations.template_param_levels = l; _ } -> +let template_polymorphic_variables (mind, _) env = + match (lookup_mind mind env).mind_template with + | Some { Declarations.template_param_levels = l; _ } -> List.map_filter (fun level -> level) l - | RegularArity _ -> [] + | None -> [] let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 1d72d1bd6e..d5aadd0c02 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -222,7 +222,66 @@ let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = else if not @@ Univ.LSet.is_empty univs then Some (univs, params) else None -let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let get_param_levels ctx params arity splayed_lc = + let min_univ = match arity with + | RegularArity _ -> + CErrors.user_err + Pp.(strbrk "Ill-formed template mutual inductive declaration: all types must be template.") + | TemplateArity ar -> ar.template_level + in + let ctor_levels = + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + Array.fold_left + (fun levels (d,c) -> + let levels = + List.fold_left (fun levels d -> + Context.Rel.Declaration.fold_constr add_levels d levels) + levels d + in + add_levels c levels) + param_levels + splayed_lc + in + match template_polymorphic_univs ~ctor_levels ctx params min_univ with + | None -> + CErrors.user_err + Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") + | Some (_, param_levels) -> + param_levels + +let get_template univs params data = + let ctx = match univs with + | Monomorphic ctx -> ctx + | Polymorphic _ -> + CErrors.anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in + (* For each type in the block, compute potential template parameters *) + let params = List.map (fun ((arity, _), (_, splayed_lc), _) -> get_param_levels ctx params arity splayed_lc) data in + (* Pick the lower bound of template parameters. Note that in particular, if + one of the the inductive types from the block is Prop-valued, then no + parameters are template. *) + let fold min params = + let map u v = match u, v with + | (None, _) | (_, None) -> None + | Some u, Some v -> + let () = assert (Univ.Level.equal u v) in + Some u + in + List.map2 map min params + in + let params = match params with + | [] -> assert false + | hd :: rem -> List.fold_left fold hd rem + in + { template_param_levels = params; template_context = ctx } + +let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) = if not (Universe.Set.is_empty univ_info.missing) then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ))); let arity = Vars.subst_univs_level_constr usubst arity in @@ -238,37 +297,7 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let arity = match univ_info.ind_min_univ with | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ} - | Some min_univ -> - let ctx = match univs with - | Monomorphic ctx -> ctx - | Polymorphic _ -> - CErrors.anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in - let ctor_levels = - let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in - let param_levels = - List.fold_left (fun levels d -> match d with - | LocalAssum _ -> levels - | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) - Univ.LSet.empty params - in - Array.fold_left - (fun levels (d,c) -> - let levels = - List.fold_left (fun levels d -> - Context.Rel.Declaration.fold_constr add_levels d levels) - levels d - in - add_levels c levels) - param_levels - splayed_lc - in - match template_polymorphic_univs ~ctor_levels ctx params min_univ with - | None -> - CErrors.user_err - Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") - | Some (_, param_levels) -> - TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } + | Some min_univ -> TemplateArity { template_level = min_univ; } in let kelim = allowed_sorts univ_info in @@ -350,7 +379,14 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let data = List.map (abstract_packets univs usubst params) data in + let data = List.map (abstract_packets usubst) data in + let template = + let check ((arity, _), _, _) = match arity with + | TemplateArity _ -> true + | RegularArity _ -> false + in + if List.exists check data then Some (get_template univs params data) else None + in let env_ar_par = let ctx = Environ.rel_context env_ar_par in @@ -359,4 +395,4 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, variance, record, params, Array.of_list data + env_ar_par, univs, template, variance, record, params, Array.of_list data diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index a625caec83..babb82c39e 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option -> mutual_inductive_entry -> env * universes + * template_universes option * Univ.Variance.t array option * Names.Id.t array option option * Constr.rel_context diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b6b8e5265c..58e5e76b61 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -466,7 +466,7 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev rs), Array.of_list (List.rev pbs) -let build_inductive env ~sec_univs names prv univs variance +let build_inductive env ~sec_univs names prv univs template variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) @@ -538,6 +538,7 @@ let build_inductive env ~sec_univs names prv univs variance mind_params_ctxt = paramsctxt; mind_packets = packets; mind_universes = univs; + mind_template = template; mind_variance = variance; mind_sec_variance = sec_variance; mind_private = prv; @@ -562,7 +563,7 @@ let build_inductive env ~sec_univs names prv univs variance let check_inductive env ~sec_univs kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, variance, record, paramsctxt, inds) = + let (env_ar_par, univs, template, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env ~sec_univs mie in (* Then check positivity conditions *) @@ -575,6 +576,6 @@ let check_inductive env ~sec_univs kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env ~sec_univs names mie.mind_entry_private univs variance + build_inductive env ~sec_univs names mie.mind_entry_private univs template variance paramsctxt kn record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1be86f2bf8..6325779675 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -185,8 +185,8 @@ let make_subst = exception SingletonInductiveBecomesProp of Id.t -let instantiate_universes ctx ar args = - let subst = make_subst (ctx,ar.template_param_levels,args) in +let instantiate_universes ctx (templ, ar) args = + let subst = make_subst (ctx,templ.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) @@ -215,8 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | 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 ar paramtyps 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 *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b690fe1157..90571844b9 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : Constr.rel_context -> - template_arity -> param_univs -> Constr.rel_context * Sorts.t - (** {6 Debug} *) type size = Large | Strict diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aafd662f7d..c9ccd668ca 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f = match EConstr.kind sigma f with | Ind (ind, u) | Construct ((ind, _), u) -> let mib,oib = Inductive.lookup_mind_specif env ind in - (match oib.mind_arity with - | RegularArity _ -> assert false - | TemplateArity templ -> templ.template_param_levels) + (match mib.mind_template with + | None -> assert false + | Some templ -> templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index a4406aeba1..01994a35c7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -681,13 +681,17 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = match mip.mind_arity with | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity) | TemplateArity ar -> + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in let _,scl = splay_arity env sigma conclty in let scl = EConstr.ESorts.kind sigma scl in let ctx = List.rev mip.mind_arity_ctxt in let evdref = ref sigma in let ctx = instantiate_universes - env evdref scl ar.template_level (ctx,ar.template_param_levels) in + env evdref scl ar.template_level (ctx,templ.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) let type_of_projection_constant env (p,u) = |