diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 18 | ||||
| -rw-r--r-- | kernel/declarations.ml | 4 | ||||
| -rw-r--r-- | kernel/declareops.ml | 1 | ||||
| -rw-r--r-- | kernel/environ.ml | 16 | ||||
| -rw-r--r-- | kernel/environ.mli | 3 | ||||
| -rw-r--r-- | kernel/indTyping.ml | 17 | ||||
| -rw-r--r-- | kernel/indTyping.mli | 1 |
7 files changed, 10 insertions, 50 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f1eb000c88..31dd26d2ba 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -258,17 +258,6 @@ let cook_constant { from = cb; info } = (********************************) (* Discharging mutual inductive *) -let template_level_of_var ~template_check d = - (* When [template_check], a universe from a section variable may not - be in the universes from the inductive (it must be pre-declared) - so always [None]. *) - if template_check then None - else - let c = Term.strip_prod_assum (RelDecl.get_type d) in - match kind c with - | Sort (Type u) -> Univ.Universe.level u - | _ -> None - let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c) let abstract_rel_ctx (section_decls,subst) ctx = @@ -305,7 +294,7 @@ let abstract_projection ~params expmod hyps t = let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in t -let cook_one_ind ~template_check ~ntypes +let cook_one_ind ~ntypes (section_decls,_ as hyps) expmod mip = let mind_arity = match mip.mind_arity with | RegularArity {mind_user_arity=arity;mind_sort=sort} -> @@ -314,7 +303,7 @@ let cook_one_ind ~template_check ~ntypes 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 (template_level_of_var ~template_check d) + if RelDecl.is_local_assum d then Some None else None) section_decls in @@ -362,14 +351,13 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = let removed_vars = Context.Named.to_vars section_decls in let section_decls, _ as hyps = abstract_context section_decls in let nnewparams = Context.Rel.nhyps section_decls in - let template_check = mib.mind_typing_flags.check_template in let mind_params_ctxt = let ctx = Context.Rel.map expmod mib.mind_params_ctxt in abstract_rel_ctx hyps ctx in let ntypes = mib.mind_ntypes in let mind_packets = - Array.map (cook_one_ind ~template_check ~ntypes hyps expmod) + Array.map (cook_one_ind ~ntypes hyps expmod) mib.mind_packets in let mind_record = match mib.mind_record with diff --git a/kernel/declarations.ml b/kernel/declarations.ml index c550b0d432..ac130d018d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -89,10 +89,6 @@ type typing_flags = { indices_matter: bool; (** The universe of an inductive type must be above that of its indices. *) - check_template : bool; - (* If [false] then we don't check that the universes template-polymorphic - inductive parameterize on are necessarily local and unbounded from below. - This potentially introduces inconsistencies. *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 047027984d..a3adac7a11 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -26,7 +26,6 @@ let safe_flags oracle = { enable_VM = true; enable_native_compiler = true; indices_matter = true; - check_template = true; } (** {6 Arities } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index f04863386f..87f2f234da 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -275,7 +275,6 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let indices_matter env = env.env_typing_flags.indices_matter -let check_template env = env.env_typing_flags.check_template let universes env = env.env_stratification.env_universes let universes_lbound env = env.env_stratification.env_universes_lbound @@ -449,7 +448,6 @@ let same_flags { share_reduction; enable_VM; enable_native_compiler; - check_template; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -458,8 +456,7 @@ let same_flags { indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && - enable_native_compiler == alt.enable_native_compiler && - check_template == alt.check_template + enable_native_compiler == alt.enable_native_compiler [@warning "+9"] let set_typing_flags c env = (* Unsafe *) @@ -591,9 +588,6 @@ let polymorphic_pind (ind,u) env = let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes -let template_checked_ind (mind,_i) env = - (lookup_mind mind env).mind_typing_flags.check_template - let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true @@ -802,14 +796,6 @@ let get_template_polymorphic_variables env r = | IndRef ind -> template_polymorphic_variables ind env | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env -let is_template_checked env r = - let open Names.GlobRef in - match r with - | VarRef _id -> false - | ConstRef _c -> false - | IndRef ind -> template_checked_ind ind env - | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env - let is_type_in_type env r = let open Names.GlobRef in match r with diff --git a/kernel/environ.mli b/kernel/environ.mli index bd5a000c2b..e80d0a9b9f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -112,7 +112,6 @@ val is_impredicative_set : env -> bool val type_in_type : env -> bool val deactivated_guard : env -> bool val indices_matter : env -> bool -val check_template : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool @@ -274,7 +273,6 @@ val type_in_type_ind : inductive -> env -> bool val template_polymorphic_ind : inductive -> env -> bool val template_polymorphic_variables : inductive -> env -> Univ.Level.t list val template_polymorphic_pind : pinductive -> env -> bool -val template_checked_ind : inductive -> env -> bool (** {5 Modules } *) @@ -373,7 +371,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat val is_polymorphic : env -> Names.GlobRef.t -> bool val is_template_polymorphic : env -> GlobRef.t -> bool val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list -val is_template_checked : env -> GlobRef.t -> bool val is_type_in_type : env -> GlobRef.t -> bool (** Native compiler *) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 113ee787f2..cc15109f06 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -197,7 +197,7 @@ let unbounded_from_below u cstrs = (starting from the most recent and ignoring let-definitions) is not contributing to the inductive type's sort or is Some u_k if its level is u_k and is contributing. *) -let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = +let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = let check_level l = Univ.LSet.mem l (Univ.ContextSet.levels uctx) && unbounded_from_below l (Univ.ContextSet.constraints uctx) && @@ -205,27 +205,23 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc in let univs = Univ.Universe.levels concl in let univs = - if template_check then - Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs - else univs (* Doesn't check the universes can be generalized *) + Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> - if template_check then (match Univ.Universe.level u with | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None | None -> None) - else Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in params, univs -let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets univs usubst params ((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 @@ -267,9 +263,9 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp splayed_lc in let param_levels, concl_levels = - template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ + template_polymorphic_univs ~ctor_levels ctx params min_univ in - if template_check && List.for_all (fun x -> Option.is_empty x) param_levels + if List.for_all (fun x -> Option.is_empty x) param_levels && Univ.LSet.is_empty concl_levels then CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") @@ -356,8 +352,7 @@ 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 template_check = Environ.check_template env in - let data = List.map (abstract_packets ~template_check univs usubst params) data in + let data = List.map (abstract_packets univs usubst params) data in let env_ar_par = let ctx = Environ.rel_context env_ar_par in diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 8dea8f046d..723ba5459e 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -40,7 +40,6 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option (* Utility function to compute the actual universe parameters of a template polymorphic inductive *) val template_polymorphic_univs : - template_check:bool -> ctor_levels:Univ.LSet.t -> Univ.ContextSet.t -> Constr.rel_context -> |