diff options
| author | Matthieu Sozeau | 2019-01-29 15:44:45 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-08-26 16:21:31 +0200 |
| commit | eb3f8225a286aef3a57ad876584b4a927241ff69 (patch) | |
| tree | c06cc7a988191f833394d383f218316565ae7ab6 | |
| parent | 0c6726655ee0ec06a40240cca44202d584506c9c (diff) | |
Make kernel parametric on the lowest universe and fix #9294
This could be Prop (for compat with usual Coq), Set (for HoTT),
or actually an arbitrary "i".
Take lower bound of universes into account in pretyping/engine
Reinstate proper elaboration of SProp <= l constraints:
replacing is_small with equality with lbound is _not_ semantics preserving!
lbound = Set
Elaborate template polymorphic inductives with lower bound Prop
This will make more constraints explicit
Check univ constraints with Prop as lower bound for template inductives
Restrict template polymorphic universes to those not bounded from below
Fixes #9294
fix suggested by Matthieu
Try second fix suggested by Matthieu
Take care of modifying elaboration for record declarations as well.
Rebase and export functions for debug
Remove exported functions used while debugging
Add a new typing flag "check_template" and option "-no-template-checl"
This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).
Update checker to the new typing flags structure
Switch on the new template_check flag to allow old unsafe behavior in
indTyping.
This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.
Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while
Fix `Template Check` option name and test it
Add `Unset Template Check` to Coq89.v
Cooking of inductives and template-check tests
Cleanup test-suite file for template check / universes(template) flags
cookind tests
Move test of `Unset Template Check` to the failure/ dir, but comment it
for now
Template test-suite test explanation
Overlays for PR 9918
Overlay for paramcoq
Add overlay for fiat_parsers (-no-template-check)
Add overlay for fiat_crypto_legacy
Update fiat-crypto legacy overlay
Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.
Remove overlay that should no longer be necessary
The setting in the compat file should handle it
Remove now-merged fiat-crypto-legacy overlay
Update `Print Assumptions` to reflect the typing flag for template checking
Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic
Fix pretty printing to print global universe levels properly
Fix printing of template polymorphic universes
Fix pretty printing for template polymorphism on no universe
Fix interaction of template check and universes(template) flag
Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe
Indtyping fixes for template polymorphic Props
Allow explicit template polymorphism again
Adapt to new indTyping interface
Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).
Fix check of meaningfullness of template polymorphism in the kernel.
It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.
Comment on identity non-template-polymorphism
Remove incorrect universes(template) attributes from ssr
simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).
Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance
Remove incorrect uses of #[universes(template)] from the stdlib
Extraction of micromega changes due to moving an ind decl out of a section
Remove incorrect uses of #[universes(template)] from plugins
Fix test-suite files, removing incorrect #[universes(template)] attributes
Remove incorrect #[universes(template)] attributes in test-suite
Fix test-suite
Remove overlays as they have been merged upstream.
90 files changed, 727 insertions, 351 deletions
diff --git a/checker/values.ml b/checker/values.ml index ac9bc26344..cc9ac1f834 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -219,7 +219,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/engine/evd.ml b/engine/evd.ml index b621a3fe2f..6a721a1a8a 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -702,7 +702,7 @@ let empty = { } let from_env e = - { empty with universes = UState.make (Environ.universes e) } + { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) } let from_ctx ctx = { empty with universes = ctx } diff --git a/engine/uState.ml b/engine/uState.ml index 5ed016e0d0..cb40e6eadd 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -34,6 +34,7 @@ type t = (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) + uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) uctx_weak_constraints : UPairSet.t } @@ -47,6 +48,7 @@ let empty = uctx_univ_variables = LMap.empty; uctx_univ_algebraic = LSet.empty; uctx_universes = initial_sprop_cumulative; + uctx_universes_lbound = Univ.Level.set; uctx_initial_universes = initial_sprop_cumulative; uctx_weak_constraints = UPairSet.empty; } @@ -54,10 +56,12 @@ let elaboration_sprop_cumul = Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration" ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true -let make u = +let make ~lbound u = let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in - { empty with - uctx_universes = u; uctx_initial_universes = u} + { empty with + uctx_universes = u; + uctx_universes_lbound = lbound; + uctx_initial_universes = u} let is_empty ctx = ContextSet.is_empty ctx.uctx_local && @@ -83,7 +87,7 @@ let union ctx ctx' = let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in let declarenew g = - LSet.fold (fun u g -> UGraph.add_universe u false g) newus g + LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g in let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); @@ -99,6 +103,7 @@ let union ctx ctx' = else let cstrsr = ContextSet.constraints ctx'.uctx_local in UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); + uctx_universes_lbound = ctx.uctx_universes_lbound; uctx_weak_constraints = weak} let context_set ctx = ctx.uctx_local @@ -431,18 +436,19 @@ let check_univ_decl ~poly uctx decl = (ContextSet.constraints uctx.uctx_local); ctx -let restrict_universe_context (univs, csts) keep = +let restrict_universe_context ~lbound (univs, csts) keep = let removed = LSet.diff univs keep in if LSet.is_empty removed then univs, csts else let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in let g = UGraph.initial_universes in - let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in + let g = LSet.fold (fun v g -> if Level.is_small v then g else + UGraph.add_universe v ~lbound ~strict:false g) allunivs g in let g = UGraph.merge_constraints csts g in let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in let csts = Constraint.filter (fun (l,d,r) -> - not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in + not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = @@ -450,7 +456,7 @@ let restrict ctx vars = let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars) (fst ctx.uctx_names) vars in - let uctx' = restrict_universe_context ctx.uctx_local vars in + let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in { ctx with uctx_local = uctx' } let demote_seff_univs universes uctx = @@ -497,7 +503,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' = else ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> - try UGraph.add_universe u false g + try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g with UGraph.AlreadyDeclared when sideff -> g) levels g in @@ -544,16 +550,17 @@ let new_univ_variable ?loc rigid name | None -> add_uctx_loc u loc uctx.uctx_names in let initial = - UGraph.add_universe u false uctx.uctx_initial_universes + UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = UGraph.add_universe u false uctx.uctx_universes; + uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false + u uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u -let make_with_initial_binders e us = - let uctx = make e in +let make_with_initial_binders ~lbound e us = + let uctx = make ~lbound e in List.fold_left (fun uctx { CAst.loc; v = id } -> fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) @@ -561,10 +568,10 @@ let make_with_initial_binders e us = let add_global_univ uctx u = let initial = - UGraph.add_universe u true uctx.uctx_initial_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes in let univs = - UGraph.add_universe u true uctx.uctx_universes + UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes in { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local; uctx_initial_universes = initial; @@ -679,8 +686,9 @@ let refresh_undefined_univ_variables uctx = uctx.uctx_univ_variables LMap.empty in let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in - let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g) - (ContextSet.levels ctx') g in + let lbound = uctx.uctx_universes_lbound in + let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) + (ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; @@ -688,14 +696,16 @@ let refresh_undefined_univ_variables uctx = uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; + uctx_universes_lbound = lbound; uctx_initial_universes = initial; uctx_weak_constraints = weak; } in uctx', subst let minimize uctx = let open UnivMinim in + let lbound = uctx.uctx_universes_lbound in let ((vars',algs'), us') = - normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables + normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints in if ContextSet.equal us' uctx.uctx_local then uctx @@ -709,6 +719,7 @@ let minimize uctx = uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; + uctx_universes_lbound = lbound; uctx_initial_universes = uctx.uctx_initial_universes; uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } diff --git a/engine/uState.mli b/engine/uState.mli index 9689f2e961..52e48c4eeb 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -25,9 +25,9 @@ type t val empty : t -val make : UGraph.t -> t +val make : lbound:Univ.Level.t -> UGraph.t -> t -val make_with_initial_binders : UGraph.t -> lident list -> t +val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t val is_empty : t -> bool @@ -88,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t (** {5 Unification} *) -(** [restrict_universe_context (univs,csts) keep] restricts [univs] to +(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to the universes in [keep]. The constraints [csts] are adjusted so that transitive constraints between remaining universes (those in [keep] and those not in [univs]) are preserved. *) -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t (** [restrict uctx ctx] restricts the local universes of [uctx] to [ctx] extended by local named universes and side effect universes diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 1b7c33b9c1..30fdd28997 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -269,11 +269,11 @@ module UPairs = OrderedType.UnorderedPair(Univ.Level) module UPairSet = Set.Make (UPairs) (* TODO check is_small/sprop *) -let normalize_context_set g ctx us algs weak = +let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts + Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles @@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak = let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = LSet.fold (fun v g -> UGraph.add_universe v false g) + let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) ctx UGraph.initial_universes in let add_soft u g = if not (Level.is_small u || LSet.mem u ctx) - then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g + then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g else g in let g = Constraint.fold @@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak = (* We ignore the trivial Prop/Set <= i constraints. *) let noneqs = Constraint.filter - (fun (l,d,r) -> not ((d == Le && Level.is_small l) || + (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 21f6efe86a..72b432e62f 100644 --- a/engine/univMinim.mli +++ b/engine/univMinim.mli @@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val normalize_context_set : UGraph.t -> ContextSet.t -> +val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> diff --git a/engine/univops.mli b/engine/univops.mli index 6cc7868a38..1f1edbed16 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -15,5 +15,5 @@ open Univ val universes_of_constr : constr -> LSet.t [@@ocaml.deprecated "Use [Vars.universes_of_constr]"] -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t [@@ocaml.deprecated "Use [UState.restrict_universe_context]"] diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3f216b0d63..b4798127f9 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -625,7 +625,8 @@ let interp_univ_constraints env evd cstrs = let interp_univ_decl env decl = let open UState in let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in + let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env) + (Environ.universes env) pl) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; univdecl_extensible_instance = decl.univdecl_extensible_instance; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 8d32684b09..44676c9da5 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -87,6 +87,11 @@ 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 391b139496..7225671a1e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -26,6 +26,7 @@ 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 655094e88b..4a2aeea22d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -59,8 +59,9 @@ type globals = { type stratification = { env_universes : UGraph.t; - env_engagement : engagement; env_sprop_allowed : bool; + env_universes_lbound : Univ.Level.t; + env_engagement : engagement } type val_kind = @@ -119,9 +120,9 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; - env_engagement = PredicativeSet; env_sprop_allowed = false; - }; + env_universes_lbound = Univ.Level.set; + env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; indirect_pterms = Opaqueproof.empty_opaquetab; @@ -262,8 +263,15 @@ 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 + +let set_universes_lbound env lbound = + let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in + { env with env_stratification } + let named_context env = env.env_named_context.env_named_ctx let named_context_val env = env.env_named_context let rel_context env = env.env_rel_context.env_rel_ctx @@ -382,29 +390,30 @@ let check_constraints c env = let push_constraints_to_env (_,univs) env = add_constraints univs env -let add_universes strict ctx g = +let add_universes ~lbound ~strict ctx g = let g = Array.fold_left - (fun g v -> UGraph.add_universe v strict g) + (fun g v -> UGraph.add_universe ~lbound ~strict v g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in UGraph.merge_constraints (Univ.UContext.constraints ctx) g let push_context ?(strict=false) ctx env = - map_universes (add_universes strict ctx) env + map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env -let add_universes_set strict ctx g = +let add_universes_set ~lbound ~strict ctx g = let g = Univ.LSet.fold (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) + (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = - map_universes (add_universes_set strict ctx) env + map_universes (add_universes_set ~lbound:(universes_lbound env) ~strict ctx) env let push_subgraph (levels,csts) env = + let lbound = universes_lbound env in let add_subgraph g = - let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in + let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) levels g in let newg = UGraph.merge_constraints csts newg in (if not (Univ.Constraint.is_empty csts) then let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in @@ -428,6 +437,7 @@ let same_flags { share_reduction; enable_VM; enable_native_compiler; + check_template; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -436,7 +446,8 @@ 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 + enable_native_compiler == alt.enable_native_compiler && + check_template == alt.check_template [@warning "+9"] let set_typing_flags c env = (* Unsafe *) @@ -568,11 +579,20 @@ 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 | 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; _ } -> + List.map_filter (fun level -> level) l + | RegularArity _ -> [] + let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env @@ -762,6 +782,22 @@ let is_template_polymorphic env r = | IndRef ind -> template_polymorphic_ind ind env | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env +let get_template_polymorphic_variables env r = + let open Names.GlobRef in + match r with + | VarRef _id -> [] + | ConstRef _c -> [] + | 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 e6d814ac7d..f7de98dcfb 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -51,8 +51,9 @@ type globals type stratification = { env_universes : UGraph.t; - env_engagement : engagement; env_sprop_allowed : bool; + env_universes_lbound : Univ.Level.t; + env_engagement : engagement } type named_context_val = private { @@ -85,6 +86,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t +val universes_lbound : env -> Univ.Level.t +val set_universes_lbound : env -> Univ.Level.t -> env val rel_context : env -> Constr.rel_context val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val @@ -99,6 +102,7 @@ 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 @@ -254,7 +258,9 @@ val type_in_type_ind : inductive -> env -> bool (** Old-style polymorphism *) 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 } *) @@ -346,6 +352,8 @@ 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 c8e04b9fee..06d2e1bb21 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -236,22 +236,53 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} if not ind_squashed then InType else Sorts.family (Sorts.sort_of_univ ind_univ) +(* For a level to be template polymorphic, it must be introduced + by the definition (so have no constraint except lbound <= l) + and not to be constrained from below, so any universe l' <= l + can be used as an instance of l. All bounds from above, i.e. + l <=/< r will be valid for any l' <= l. *) +let unbounded_from_below u cstrs = + Univ.Constraint.for_all (fun (l, d, r) -> + match d with + | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u) + | Lt | Le -> not (Univ.Level.equal r u)) + cstrs + (* Returns the list [x_1, ..., x_n] of levels contributing to template - polymorphism. The elements x_k is None if the k-th parameter (starting - from the most recent and ignoring let-definitions) is not contributing - or is Some u_k if its level is u_k and is contributing. *) -let param_ccls paramsctxt = + polymorphism. The elements x_k is None if the k-th parameter + (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 uctx paramsctxt concl = + let check_level l = + if Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + unbounded_from_below l (Univ.ContextSet.constraints uctx) then + Some l + else None + in + let univs = Univ.Universe.levels concl in + let univs = + if template_check then + Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs + else univs (* Doesn't check the universes can be generalized *) + in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with - | Sort (Type u) -> Univ.Universe.level u + | 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 - List.fold_left fold [] paramsctxt + let params = List.fold_left fold [] paramsctxt in + params, univs -let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = let arity = Vars.subst_univs_level_constr usubst arity in let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in let indices = Vars.subst_univs_level_context usubst indices in @@ -264,14 +295,20 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in let arity = match univ_info.ind_min_univ with - | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ} + | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ} | Some min_univ -> - ((match univs with - | Monomorphic _ -> () + let ctx = match univs with + | Monomorphic ctx -> ctx | Polymorphic _ -> CErrors.anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.")); - TemplateArity {template_param_levels=param_ccls params; template_level=min_univ}) + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in + let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in + if template_check && List.for_all (fun x -> Option.is_empty x) param_levels + && Univ.LSet.is_empty concl_levels then + CErrors.anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") + else + TemplateArity {template_param_levels = param_levels; template_level = min_univ} in let kelim = allowed_sorts univ_info in @@ -286,10 +323,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = mind_check_names mie; assert (List.is_empty (Environ.rel_context env)); + let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in + (* universes *) let env_univs = match mie.mind_entry_universes with - | Monomorphic_entry ctx -> push_context_set ctx env + | Monomorphic_entry ctx -> + let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in + push_context_set ctx env | Polymorphic_entry (_, ctx) -> push_context ctx env in @@ -335,7 +376,8 @@ let typecheck_inductive env (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 template_check = Environ.check_template env in + let data = List.map (abstract_packets ~template_check 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 aaa0d6a149..8da4e2885c 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -33,3 +33,12 @@ val typecheck_inductive : env -> mutual_inductive_entry -> (Constr.rel_context * (Constr.rel_context * Constr.types) array) * Sorts.family) array + +(* Utility function to compute the actual universe parameters + of a template polymorphic inductive *) +val template_polymorphic_univs : + template_check:bool -> + Univ.ContextSet.t -> + Constr.rel_context -> + Univ.Universe.t -> + Univ.Level.t option list * Univ.LSet.t diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 9305a91731..ccc218771a 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -94,7 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = c', Monomorphic Univ.ContextSet.empty, cst | Polymorphic uctx, Some ctx -> let () = - if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then + if not (UGraph.check_subtype ~lbound:(Environ.universes_lbound env) + (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab in (** Terms are compared in a context with De Bruijn universe indices *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 53f228c618..327cb2efeb 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -777,7 +777,7 @@ let infer_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs | Set, Prop -> raise NotConvertible | Set, Type u -> infer_pb Univ.type0_univ u - | Type _u, Prop -> raise NotConvertible + | Type u, Prop -> infer_pb u Univ.type0m_univ | Type u, Set -> infer_pb u Univ.type0_univ | Type u0, Type u1 -> infer_pb u0 u1 diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d47dc0c6e1..d22ec3b7ca 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -97,7 +97,8 @@ let check_universes error env u1 u2 = match u1, u2 with | Monomorphic _, Monomorphic _ -> env | Polymorphic auctx1, Polymorphic auctx2 -> - if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then + let lbound = Environ.universes_lbound env in + if not (UGraph.check_subtype ~lbound (Environ.universes env) auctx2 auctx1) then error (IncompatibleConstraints { got = auctx1; expect = auctx2; } ) else Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 6fde6e9c5f..33336079bb 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -149,10 +149,10 @@ let enforce_leq_alg u v g = cg exception AlreadyDeclared = G.AlreadyDeclared -let add_universe u strict g = +let add_universe u ~lbound ~strict g = let graph = G.add u g.graph in let d = if strict then Lt else Le in - enforce_constraint (Level.set,d,u) {g with graph} + enforce_constraint (lbound,d,u) {g with graph} let add_universe_unconstrained u g = {g with graph=G.add u g.graph} @@ -164,11 +164,11 @@ let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop k (** Subtyping of polymorphic contexts *) -let check_subtype univs ctxT ctx = +let check_subtype ~lbound univs ctxT ctx = if AUContext.size ctxT == AUContext.size ctx then let (inst, cst) = UContext.dest (AUContext.repr ctx) in let cstT = UContext.constraints (AUContext.repr ctxT) in - let push accu v = add_universe v false accu in + let push accu v = add_universe v ~lbound ~strict:false accu in let univs = Array.fold_left push univs (Instance.to_array inst) in let univs = merge_constraints cstT univs in check_constraints cst univs diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e1b5868d55..d90f01d8d1 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t exception AlreadyDeclared -val add_universe : Level.t -> bool -> t -> t +val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t @@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t val domain : t -> LSet.t (** Known universes *) -val check_subtype : AUContext.t check_function +val check_subtype : lbound:Level.t -> AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/library/global.ml b/library/global.ml index 0fc9e11364..6bb4614aa4 100644 --- a/library/global.ml +++ b/library/global.ml @@ -119,6 +119,7 @@ let add_module_parameter mbid mte inl = (** Queries on the global environment *) let universes () = universes (env()) +let universes_lbound () = universes_lbound (env()) let named_context () = named_context (env()) let named_context_val () = named_context_val (env()) @@ -181,6 +182,10 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r let is_template_polymorphic r = is_template_polymorphic (env ()) r +let is_template_checked r = is_template_checked (env ()) r + +let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r + let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = diff --git a/library/global.mli b/library/global.mli index b089b7dd80..d0bd556d70 100644 --- a/library/global.mli +++ b/library/global.mli @@ -22,6 +22,7 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool val universes : unit -> UGraph.t +val universes_lbound : unit -> Univ.Level.t val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Constr.named_context @@ -136,6 +137,8 @@ val is_joined_environment : unit -> bool val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool +val is_template_checked : GlobRef.t -> bool +val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list val is_type_in_type : GlobRef.t -> bool (** {6 Retroknowledge } *) diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 78bfe480b3..2762bb6b32 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -19,6 +19,47 @@ Require Export Ring_theory. Local Open Scope positive_scope. Import RingSyntax. +(** Definition of polynomial expressions *) +#[universes(template)] +Inductive PExpr {C} : Type := +| PEc : C -> PExpr +| PEX : positive -> PExpr +| PEadd : PExpr -> PExpr -> PExpr +| PEsub : PExpr -> PExpr -> PExpr +| PEmul : PExpr -> PExpr -> PExpr +| PEopp : PExpr -> PExpr +| PEpow : PExpr -> N -> PExpr. +Arguments PExpr : clear implicits. + + (* Definition of multivariable polynomials with coefficients in C : + Type [Pol] represents [X1 ... Xn]. + The representation is Horner's where a [n] variable polynomial + (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients + are polynomials with [n-1] variables (C[X2..Xn]). + There are several optimisations to make the repr compacter: + - [Pc c] is the constant polynomial of value c + == c*X1^0*..*Xn^0 + - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables. + variable indices are shifted of j in Q. + == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn} + - [PX P i Q] is an optimised Horner form of P*X^i + Q + with P not the null polynomial + == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn} + + In addition: + - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden + since they can be represented by the simpler form (PX P (i+j) Q) + - (Pinj i (Pinj j P)) is (Pinj (i+j) P) + - (Pinj i (Pc c)) is (Pc c) + *) + +#[universes(template)] +Inductive Pol {C} : Type := +| Pc : C -> Pol +| Pinj : positive -> Pol -> Pol +| PX : Pol -> positive -> Pol -> Pol. +Arguments Pol : clear implicits. + Section MakeRingPol. (* Ring elements *) @@ -96,33 +137,11 @@ Section MakeRingPol. match goal with |- ?t == _ => mul_permut_rec t end). - (* Definition of multivariable polynomials with coefficients in C : - Type [Pol] represents [X1 ... Xn]. - The representation is Horner's where a [n] variable polynomial - (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients - are polynomials with [n-1] variables (C[X2..Xn]). - There are several optimisations to make the repr compacter: - - [Pc c] is the constant polynomial of value c - == c*X1^0*..*Xn^0 - - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables. - variable indices are shifted of j in Q. - == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn} - - [PX P i Q] is an optimised Horner form of P*X^i + Q - with P not the null polynomial - == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn} + Notation PExpr := (PExpr C). + Notation Pol := (Pol C). - In addition: - - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden - since they can be represented by the simpler form (PX P (i+j) Q) - - (Pinj i (Pinj j P)) is (Pinj (i+j) P) - - (Pinj i (Pc c)) is (Pc c) - *) - - #[universes(template)] - Inductive Pol : Type := - | Pc : C -> Pol - | Pinj : positive -> Pol -> Pol - | PX : Pol -> positive -> Pol -> Pol. + Implicit Types pe : PExpr. + Implicit Types P : Pol. Definition P0 := Pc cO. Definition P1 := Pc cI. @@ -152,7 +171,7 @@ Section MakeRingPol. | _ => Pinj j P end. - Definition mkPinj_pred j P:= + Definition mkPinj_pred j P := match j with | xH => P | xO j => Pinj (Pos.pred_double j) P @@ -938,18 +957,6 @@ Qed. rewrite <- IHm; auto. Qed. - (** Definition of polynomial expressions *) - - #[universes(template)] - Inductive PExpr : Type := - | PEc : C -> PExpr - | PEX : positive -> PExpr - | PEadd : PExpr -> PExpr -> PExpr - | PEsub : PExpr -> PExpr -> PExpr - | PEmul : PExpr -> PExpr -> PExpr - | PEopp : PExpr -> PExpr - | PEpow : PExpr -> N -> PExpr. - (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index a99f21ad47..3c72d3268f 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -68,7 +68,7 @@ Require Import EnvRing. Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := match e with | PEc c => c - | PEX _ j => env j + | PEX j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) @@ -80,7 +80,7 @@ Lemma Qeval_expr_simpl : forall env e, Qeval_expr env e = match e with | PEc c => c - | PEX _ j => env j + | PEX j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 75801162a7..cddc140f51 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -289,7 +289,6 @@ destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor). now apply (Rplus_nonneg_nonneg sor). Qed. -#[universes(template)] Inductive Psatz : Type := | PsatzIn : nat -> Psatz | PsatzSquare : PolC -> Psatz @@ -892,7 +891,7 @@ Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C := | Pc c => PEc c | Pinj j p => xdenorm (Pos.add j jmp ) p | PX p j q => PEadd - (PEmul (xdenorm jmp p) (PEpow (PEX _ jmp) (Npos j))) + (PEmul (xdenorm jmp p) (PEpow (PEX jmp) (Npos j))) (xdenorm (Pos.succ jmp) q) end. @@ -961,7 +960,7 @@ Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c). Fixpoint map_PExpr (e : PExpr S) : PExpr C := match e with | PEc c => PEc (C_of_S c) - | PEX _ p => PEX _ p + | PEX p => PEX p | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2) | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2) | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2) diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 56032befba..d6ccf582ae 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -27,7 +27,6 @@ Section S. Context {AA : Type}. (* type of annotations for atoms *) Context {AF : Type}. (* type of formulae identifiers *) - #[universes(template)] Inductive GFormula : Type := | TT : GFormula | FF : GFormula diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 79cb6a3a3e..f93fe021f9 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -27,16 +27,18 @@ Set Implicit Arguments. * As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up. *) +Inductive t {A} : Type := +| Empty : t +| Elt : A -> t +| Branch : t -> A -> t -> t . +Arguments t : clear implicits. + Section MakeVarMap. Variable A : Type. Variable default : A. - #[universes(template)] - Inductive t : Type := - | Empty : t - | Elt : A -> t - | Branch : t -> A -> t -> t . + Notation t := (t A). Fixpoint find (vm : t) (p:positive) {struct vm} : A := match vm with @@ -49,7 +51,6 @@ Section MakeVarMap. end end. - Fixpoint singleton (x:positive) (v : A) : t := match x with | xH => Elt v diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 3ea7635244..c0d22486b5 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -65,7 +65,7 @@ Qed. Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := match e with | PEc c => c - | PEX _ x => env x + | PEX x => env x | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2 | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2 | PEpow e1 n => Z.pow (Zeval_expr env e1) (Z.of_N n) @@ -78,7 +78,7 @@ Definition eval_expr := eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x Fixpoint Zeval_const (e: PExpr Z) : option Z := match e with | PEc c => Some c - | PEX _ x => None + | PEX x => None | PEadd e1 e2 => map_option2 (fun x y => Some (x + y)) (Zeval_const e1) (Zeval_const e2) | PEmul e1 e2 => map_option2 (fun x y => Some (x * y)) @@ -742,7 +742,7 @@ Module Vars. Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t := match e with | PEc _ => Vars.empty - | PEX _ x => Vars.singleton x + | PEX x => Vars.singleton x | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 => let v1 := vars_of_pexpr e1 in let v2 := vars_of_pexpr e2 in @@ -774,10 +774,10 @@ Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type} end. Definition bound_var (v : positive) : Formula Z := - Build_Formula (PEX _ v) OpGe (PEc 0). + Build_Formula (PEX v) OpGe (PEc 0). Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z := - Build_Formula (PEX _ x) OpEq (PEsub (PEX _ y) (PEX _ t)). + Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)). Section BOUND. Context {TX TG ID : Type}. diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index a64a5a84b3..2e97dfea19 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -556,6 +556,15 @@ let zeq_bool x y = | Eq -> true | _ -> false +type 'c pExpr = +| PEc of 'c +| PEX of positive +| PEadd of 'c pExpr * 'c pExpr +| PEsub of 'c pExpr * 'c pExpr +| PEmul of 'c pExpr * 'c pExpr +| PEopp of 'c pExpr +| PEpow of 'c pExpr * n + type 'c pol = | Pc of 'c | Pinj of positive * 'c pol @@ -868,15 +877,6 @@ let rec psquare cO cI cadd cmul ceqb = function let p3 = psquare cO cI cadd cmul ceqb p2 in mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2 -type 'c pExpr = -| PEc of 'c -| PEX of positive -| PEadd of 'c pExpr * 'c pExpr -| PEsub of 'c pExpr * 'c pExpr -| PEmul of 'c pExpr * 'c pExpr -| PEopp of 'c pExpr -| PEpow of 'c pExpr * n - (** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **) let mk_X cO cI j = diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 0ca0d0c12d..6b92445326 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -77,20 +77,24 @@ Lget i (l ++ delta) = Some a. induction l;destruct i;simpl;try congruence;auto. Qed. -Section Store. - -Variable A:Type. - -#[universes(template)] -Inductive Poption : Type:= +Inductive Poption {A} : Type:= PSome : A -> Poption | PNone : Poption. +Arguments Poption : clear implicits. -#[universes(template)] -Inductive Tree : Type := +Inductive Tree {A} : Type := Tempty : Tree | Branch0 : Tree -> Tree -> Tree | Branch1 : A -> Tree -> Tree -> Tree. +Arguments Tree : clear implicits. + +Section Store. + +Variable A:Type. + +Notation Poption := (Poption A). +Notation Tree := (Tree A). + Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption := match T with @@ -179,7 +183,6 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*; destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence. Qed. -#[universes(template)] Record Store : Type := mkStore {index:positive;contents:Tree}. @@ -194,7 +197,6 @@ Lemma get_empty : forall i, get i empty = PNone. intro i; case i; unfold empty,get; simpl;reflexivity. Qed. -#[universes(template)] Inductive Full : Store -> Type:= F_empty : Full empty | F_push : forall a S, Full S -> Full (push a S). diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index b4300da4d5..3736bc47a5 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -730,7 +730,6 @@ Qed. (* The input: syntax of a field expression *) -#[universes(template)] Inductive FExpr : Type := | FEO : FExpr | FEI : FExpr @@ -763,7 +762,6 @@ Strategy expand [FEeval]. (* The result of the normalisation *) -#[universes(template)] Record linear : Type := mk_linear { num : PExpr C; denum : PExpr C; @@ -946,7 +944,6 @@ induction e2; intros p1 p2; now rewrite <- PEpow_mul_r. Qed. -#[universes(template)] Record rsplit : Type := mk_rsplit { rsplit_left : PExpr C; rsplit_common : PExpr C; diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index b024f65988..a98a963207 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -740,7 +740,6 @@ Ltac abstract_ring_morphism set ext rspec := | _ => fail 1 "bad ring structure" end. -#[universes(template)] Record hypo : Type := mkhypo { hypo_type : Type; hypo_proof : hypo_type diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 6a8c514a7b..048c8eecf9 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -32,7 +32,6 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. with coefficients in C : *) -#[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | PX : Pol -> positive -> positive -> Pol -> Pol. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 9d56084fd4..092114ff0b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -121,7 +121,6 @@ Section MakeRingPol. - (Pinj i (Pc c)) is (Pc c) *) - #[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol @@ -909,7 +908,6 @@ Section MakeRingPol. (** Definition of polynomial expressions *) - #[universes(template)] Inductive PExpr : Type := | PEO : PExpr | PEI : PExpr diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 8f24b281c6..dc45853458 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -540,7 +540,6 @@ Section AddRing. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). Variable req : R -> R -> Prop. *) -#[universes(template)] Inductive ring_kind : Type := | Abstract | Computational diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index eb75fca0a1..b456d2eed2 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -151,7 +151,7 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in - let univs = UState.restrict_universe_context univs vars in + let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in let () = Declare.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index bf0761d3ae..376410658a 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -1323,7 +1323,6 @@ Proof. by move=> x y r2xy; apply/orP; right. Qed. (** Variant of simpl_pred specialised to the membership operator. **) -#[universes(template)] Variant mem_pred T := Mem of pred T. (** @@ -1464,7 +1463,6 @@ Implicit Types (mp : mem_pred T). Definition Acoll : collective_pred T := [pred x | ...]. as the collective_pred_of_simpl is _not_ convertible to pred_of_simpl. **) -#[universes(template)] Structure registered_applicative_pred p := RegisteredApplicativePred { applicative_pred_value :> pred T; _ : applicative_pred_value = p @@ -1473,21 +1471,18 @@ Definition ApplicativePred p := RegisteredApplicativePred (erefl p). Canonical applicative_pred_applicative sp := ApplicativePred (applicative_pred_of_simpl sp). -#[universes(template)] Structure manifest_simpl_pred p := ManifestSimplPred { simpl_pred_value :> simpl_pred T; _ : simpl_pred_value = SimplPred p }. Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)). -#[universes(template)] Structure manifest_mem_pred p := ManifestMemPred { mem_pred_value :> mem_pred T; _ : mem_pred_value = Mem [eta p] }. Canonical expose_mem_pred p := ManifestMemPred (erefl (Mem [eta p])). -#[universes(template)] Structure applicative_mem_pred p := ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}. Canonical check_applicative_mem_pred p (ap : registered_applicative_pred p) := @@ -1538,7 +1533,6 @@ End PredicateSimplification. (** Qualifiers and keyed predicates. **) -#[universes(template)] Variant qualifier (q : nat) T := Qualifier of {pred T}. Coercion has_quality n T (q : qualifier n T) : {pred T} := @@ -1573,7 +1567,6 @@ Variable T : Type. Variant pred_key (p : {pred T}) := DefaultPredKey. Variable p : {pred T}. -#[universes(template)] Structure keyed_pred (k : pred_key p) := PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}. @@ -1605,7 +1598,6 @@ Section KeyedQualifier. Variables (T : Type) (n : nat) (q : qualifier n T). -#[universes(template)] Structure keyed_qualifier (k : pred_key q) := PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}. Definition KeyedQualifier k := PackKeyedQualifier k (erefl q). diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 71abafc22f..9ebdf71329 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -209,7 +209,6 @@ Register abstract_key as plugins.ssreflect.abstract_key. Register abstract as plugins.ssreflect.abstract. (** Constants for tactic-views **) -#[universes(template)] Inductive external_view : Type := tactic_view of Type. (** diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 5e600362b4..0ce3752a51 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -391,19 +391,19 @@ Notation "@^~ x" := (fun f => f x) : fun_scope. Definitions and notation for explicit functions with simplification, i.e., which simpl and /= beta expand (this is complementary to nosimpl). **) +#[universes(template)] +Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT. + Section SimplFun. Variables aT rT : Type. -#[universes(template)] -Variant simpl_fun := SimplFun of aT -> rT. +Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x. -Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. +End SimplFun. Coercion fun_of_simpl : simpl_fun >-> Funclass. -End SimplFun. - Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope. Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope. Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope. diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f82b9cef68..b7fefca22b 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -221,14 +221,22 @@ let print_if_is_coercion ref = (*******************) (* *) +let pr_template_variables = function + | [] -> mt () + | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars + let print_polymorphism ref = let poly = Global.is_polymorphic ref in let template_poly = Global.is_template_polymorphic ref in - [ pr_global ref ++ str " is " ++ str - (if poly then "universe polymorphic" + let template_checked = Global.is_template_checked ref in + let template_variables = Global.get_template_polymorphic_variables ref in + [ pr_global ref ++ str " is " ++ + (if poly then str "universe polymorphic" else if template_poly then - "template universe polymorphic" - else "not universe polymorphic") ] + (if not template_checked then str "assumed " else mt()) ++ + str "template universe polymorphic " + ++ h 0 (pr_template_variables template_variables) + else str "not universe polymorphic") ] let print_type_in_type ref = let unsafe = Global.is_type_in_type ref in diff --git a/printing/printer.ml b/printing/printer.ml index e3225fadd5..328082fbc2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -854,6 +854,8 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = @@ -873,10 +875,13 @@ struct Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 + | TemplatePolymorphic m1, TemplatePolymorphic m2 -> + MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 + | _, TemplatePolymorphic _ -> 1 | _ -> -1 let compare x y = @@ -937,6 +942,9 @@ let pr_assumptionset env sigma s = hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") + | TemplatePolymorphic m -> + hov 2 (safe_pr_inductive env m ++ spc () ++ + strbrk"is assumed template polymorphic on all its universe parameters.") | TypeInType gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in diff --git a/printing/printer.mli b/printing/printer.mli index 788f303aee..d62d3789d3 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -192,6 +192,8 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = diff --git a/test-suite/bugs/closed/bug_9294.v b/test-suite/bugs/closed/bug_9294.v new file mode 100644 index 0000000000..a079d672d3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9294.v @@ -0,0 +1,29 @@ +Set Printing Universes. + +Inductive Foo@{i} (A:Type@{i}) : Type := foo : (Set:Type@{i}) -> Foo A. +Arguments foo {_} _. +Print Universes Subgraph (Foo.i). +Definition bar : Foo True -> Set := fun '(foo x) => x. + +Definition foo_bar (n : Foo True) : foo (bar n) = n. +Proof. destruct n;reflexivity. Qed. + +Definition bar_foo (n : Set) : bar (foo n) = n. +Proof. reflexivity. Qed. + +Require Import Hurkens. + +Inductive box (A : Set) : Prop := Box : A -> box A. + +Definition Paradox : False. +Proof. +Fail unshelve refine ( + NoRetractFromSmallPropositionToProp.paradox + (Foo True) + (fun A => foo A) + (fun A => box (bar A)) + _ + _ + False +). +Abort. diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v index bc5cd0fb68..4b6916af55 100644 --- a/test-suite/coqchk/inductive_functor_template.v +++ b/test-suite/coqchk/inductive_functor_template.v @@ -2,7 +2,7 @@ Module Type E. Parameter T : Type. End E. Module F (X:E). - #[universes(template)] Inductive foo := box : X.T -> foo. + Inductive foo := box : X.T -> foo. End F. Module ME. Definition T := nat. End ME. diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v new file mode 100644 index 0000000000..75b2a56169 --- /dev/null +++ b/test-suite/failure/Template.v @@ -0,0 +1,32 @@ +(* +Module TestUnsetTemplateCheck. + Unset Template Check. + + Section Foo. + + Context (A : Type). + + Definition cstr := nat : ltac:(let ty := type of A in exact ty). + + Inductive myind := + | cons : A -> myind. + End Foo. + + (* Can only succeed if no template check is performed *) + Check myind True : Prop. + + Print Assumptions myind. + (* + Axioms: + myind is template polymorphic on all its universe parameters. + *) + About myind. +(* +myind : Type@{Top.60} -> Type@{Top.60} + +myind is assumed template universe polymorphic on Top.60 +Argument scope is [type_scope] +Expands to: Inductive Top.TestUnsetTemplateCheck.myind +*) +End TestUnsetTemplateCheck. +*) diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4e949dcb04..a040b69b44 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -84,7 +84,6 @@ Print f. (* Was enhancement request #5142 (error message reported on the most general return clause heuristic) *) -#[universes(template)] Inductive gadt : Type -> Type := | gadtNat : nat -> gadt nat | gadtTy : forall T, T -> gadt T. diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 6976f35a88..0e84bf3966 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,7 +1,7 @@ (* Submitted by Randy Pollack *) -#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. +Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. Variables (S : Set) (P : pred S) (R : rel S) (x : S). diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index f9398fdca9..1ecd9771eb 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -101,7 +101,7 @@ Section decoder_result. Variable inst : Type. - #[universes(template)] Inductive decoder_result : Type := + Inductive decoder_result : Type := | DecUndefined : decoder_result | DecUnpredictable : decoder_result | DecInst : inst -> decoder_result diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 9b25c2dbd3..61ae4edbd1 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. -#[universes(template)] CoInductive Inf := S { projS : Inf }. +CoInductive Inf := S { projS : Inf }. Definition expand_Inf (x : Inf) := S (projS x). CoFixpoint inf := S inf. Eval compute in inf. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 29614c032a..aeebc0f98b 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). (**********************************************************************) (* Test printing of #4932 *) -#[universes(template)] Inductive ftele : Type := +Inductive ftele : Type := | fb {T:Type} : T -> ftele | fr {T} : (T -> ftele) -> ftele. diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0c1b08f5a3..d671053c07 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -53,7 +53,7 @@ Module Suboptimal. (** This test shows an example which exposes the [let] introduced by the pattern notation in binders. *) -#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. +Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index ab4172711e..e788977fb7 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,6 +1,6 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} -existT is template universe polymorphic +existT is template universe polymorphic on sigT.u0 sigT.u1 Argument A is implicit Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v index 35f36e87d7..14d63d39c4 100644 --- a/test-suite/output/Projections.v +++ b/test-suite/output/Projections.v @@ -6,7 +6,7 @@ Class HostFunction := host_func : Type. Section store. Context `{HostFunction}. - #[universes(template)] Record store := { store_funcs : host_func }. + Record store := { store_funcs : host_func }. End store. Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 4fe7b051f8..d9a649fadc 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -20,12 +20,12 @@ Check {| field := 5 |}. Check build_r 5. Check build_c 5. -#[universes(template)] Record N := C { T : Type; _ : True }. +Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. Check fun x:N => let 'C T p := x in (T,p). -#[universes(template)] Record M := D { U : Type; a := 0; q : True }. +Record M := D { U : Type; a := 0; q : True }. Check fun x:M => let 'D T _ p := x in p. Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v index 99183f2064..9cf6ad35b8 100644 --- a/test-suite/output/ShowMatch.v +++ b/test-suite/output/ShowMatch.v @@ -3,12 +3,12 @@ *) Module A. - #[universes(template)] Inductive foo := f. + Inductive foo := f. Show Match foo. (* no need to disambiguate *) End A. Module B. - #[universes(template)] Inductive foo := f. + Inductive foo := f. (* local foo shadows A.foo, so constructor "f" needs disambiguation *) Show Match A.foo. End B. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 222a808768..a89fd64999 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -68,9 +68,9 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.32} in -let ff := Type@{UnivBinders.34} in tt -> ff - : Type@{max(UnivBinders.31,UnivBinders.33)} +let tt := Type@{UnivBinders.33} in +let ff := Type@{UnivBinders.35} in tt -> ff + : Type@{max(UnivBinders.32,UnivBinders.34)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = @@ -143,16 +143,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.56 UnivBinders.57} : -Type@{UnivBinders.56} -> Type@{i} -(* i UnivBinders.56 UnivBinders.57 |= *) +axfoo@{i UnivBinders.57 UnivBinders.58} : +Type@{UnivBinders.57} -> Type@{i} +(* i UnivBinders.57 UnivBinders.58 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.56 UnivBinders.57} : -Type@{UnivBinders.57} -> Type@{i} -(* i UnivBinders.56 UnivBinders.57 |= *) +axbar@{i UnivBinders.57 UnivBinders.58} : +Type@{UnivBinders.58} -> Type@{i} +(* i UnivBinders.57 UnivBinders.58 |= *) axbar is universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 0eb5db1733..7465442cab 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -#[universes(template)] Record A := { B:Type; b:B->B }. +Record A := { B:Type; b:B->B }. Definition a B := {| B:=B; b:=fun x => x |}. Canonical Structure a. diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 209fedc343..57a4739e9f 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -21,6 +21,6 @@ Print P. (* Note: exact numbers of evars are not important... *) -#[universes(template)] Inductive T (n:nat) : Type := A : T n. +Inductive T (n:nat) : Type := A : T n. Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index cfc25c3346..c38b761f1f 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -46,3 +46,112 @@ Module No. Definition j_lebox (A:Type@{j}) := Box A. Fail Definition box_lti A := Box A : Type@{i}. End No. + +Module DefaultProp. + Inductive identity (A : Type) (a : A) : A -> Type := id_refl : identity A a a. + + (* By default template polymorphism does not interact with inductives + which naturally fall in Prop *) + Check (identity nat 0 0 : Prop). +End DefaultProp. + +Module ExplicitTemplate. + #[universes(template)] + Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a. + + (* Weird intraction of template polymorphism and inductives + which naturally fall in Prop: this one is template polymorphic but not on i: + it just lives in any universe *) + Check (identity Type nat nat : Prop). +End ExplicitTemplate. + +Polymorphic Definition f@{i} : Type@{i} := nat. +Polymorphic Definition baz@{i} : Type@{i} -> Type@{i} := fun x => x. + +Section Foo. + Universe u. + Context (A : Type@{u}). + + Inductive Bar := + | bar : A -> Bar. + + Set Universe Minimization ToSet. + Inductive Baz := + | cbaz : A -> baz Baz -> Baz. + + Inductive Baz' := + | cbaz' : A -> baz@{Set} nat -> Baz'. + + (* 2 constructors, at least in Set *) + Inductive Bazset@{v} := + | cbaz1 : A -> baz@{v} Bazset -> Bazset + | cbaz2 : Bazset. + + Eval compute in ltac:(let T := type of A in exact T). + + Inductive Foo : Type := + | foo : A -> f -> Foo. + +End Foo. + +Set Printing Universes. +(* Cannot fall back to Prop or Set anymore as baz is no longer template-polymorphic *) +Fail Check Bar True : Prop. +Fail Check Bar nat : Set. +About Baz. + +Check cbaz True I. + +(** Neither can it be Set *) +Fail Check Baz nat : Set. + +(** No longer possible for Baz' which contains a type in Set *) +Fail Check Baz' True : Prop. +Fail Check Baz' nat : Set. + +Fail Check Bazset True : Prop. +Fail Check Bazset True : Set. + +(** We can force the universe instantiated in [baz Bazset] to be [u], so Bazset lives in max(Set, u). *) +Constraint u = Bazset.v. +(** As u is global it is already > Set, so: *) +Definition bazsetex@{i | i < u} : Type@{u} := Bazset Type@{i}. + +(* Bazset is closed for universes u = u0, cannot be instantiated with Prop *) +Definition bazseetpar (X : Type@{u}) : Type@{u} := Bazset X. + +(** Would otherwise break singleton elimination and extraction. *) +Fail Check Foo True : Prop. +Fail Check Foo True : Set. + +Definition foo_proj {A} (f : Foo A) : nat := + match f with foo _ _ n => n end. + +Definition ex : Foo True := foo _ I 0. +Check foo_proj ex. + +(** See failure/Template.v for a test of the unsafe Unset Template Check usage *) + +Module AutoTemplateTest. +Set Warnings "+auto-template". +Section Foo. + Universe u'. + Context (A : Type@{u'}). + + (* Not failing as Bar cannot be made template polymorphic at all *) + Inductive Bar := + | bar : A -> Bar. +End Foo. +End AutoTemplateTest. + +Module TestTemplateAttribute. + Section Foo. + Universe u. + Context (A : Type@{u}). + + (* Failing as Bar cannot be made template polymorphic at all *) + Fail #[universes(template)] Inductive Bar := + | bar : A -> Bar. + + End Foo. +End TestTemplateAttribute. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 428af5fcfe..69bd1e6c96 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -286,7 +286,6 @@ Local Open Scope list_scope. (** A compact representation of non-dependent arities, with the codomain singled-out. *) (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *) -#[universes(template)] Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist. Local Infix "::" := Tcons. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 071810acdc..6858706cb3 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -27,7 +27,6 @@ Require Export Coq.Classes.Morphisms. (** A setoid wraps an equivalence. *) -#[universes(template)] Class Setoid A := { equiv : relation A ; setoid_equiv :> Equivalence equiv }. @@ -129,7 +128,6 @@ Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper ( (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *) -#[universes(template)] Class PartialSetoid (A : Type) := { pequiv : relation A ; pequiv_prf :> PER pequiv }. diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 5025bce093..274cb4afd3 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -14,3 +14,6 @@ Local Set Warnings "-deprecated". Require Export Coq.Compat.Coq810. Unset Private Polymorphic Universes. + +(** Unsafe flag, can hide inconsistencies. *) +Global Unset Template Check. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 801be79ba4..8627ff7353 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -45,20 +45,23 @@ Hint Transparent key : core. (** * Trees *) -Section Elt. - -Variable elt : Type. - (** * Trees The fifth field of [Node] is the height of the tree *) #[universes(template)] -Inductive tree := +Inductive tree {elt : Type} := | Leaf : tree | Node : tree -> key -> elt -> tree -> int -> tree. +Arguments tree : clear implicits. -Notation t := tree. +Section Elt. + +Variable elt : Type. + +Notation t := (tree elt). + +Implicit Types m : t. (** * Basic functions on trees: height and cardinal *) @@ -76,7 +79,7 @@ Fixpoint cardinal (m : t) : nat := (** * Empty Map *) -Definition empty := Leaf. +Definition empty : t := Leaf. (** * Emptyness test *) @@ -236,7 +239,6 @@ Fixpoint join l : key -> elt -> t -> t := - [o] is the result of [find x m]. *) -#[universes(template)] Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }. Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). @@ -293,7 +295,6 @@ Variable cmp : elt->elt->bool. (** ** Enumeration of the elements of a tree *) -#[universes(template)] Inductive enumeration := | End : enumeration | More : key -> elt -> t -> enumeration -> enumeration. @@ -338,6 +339,9 @@ Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End). End Elt. Notation t := tree. +Arguments Leaf : clear implicits. +Arguments Node [elt]. + Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). Notation "t #l" := (t_left t) (at level 9, format "t '#l'"). Notation "t #o" := (t_opt t) (at level 9, format "t '#o'"). diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 2af6e5c6a4..b21d809059 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -1024,7 +1024,6 @@ Module E := X. Definition key := E.t. -#[universes(template)] Record slist (elt:Type) := {this :> Raw.t elt; sorted : sort (@Raw.PX.ltk elt) this}. Definition t (elt:Type) : Type := slist elt. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 0c04437581..b9a8b0a73d 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -868,8 +868,6 @@ Module Make (X: DecidableType) <: WS with Module E:=X. Module E := X. Definition key := E.t. - -#[universes(template)] Record slist (elt:Type) := {this :> Raw.t elt; NoDup : NoDupA (@Raw.PX.eqk elt) this}. Definition t (elt:Type) := slist elt. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 1639115cbd..3e0bf1d8ae 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -387,8 +387,10 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined. (** [identity A a] is the family of datatypes on [A] whose sole non-empty member is the singleton datatype [identity A a a] whose sole inhabitant is denoted [identity_refl A a] *) +(** Beware: this inductive actually falls into [Prop], as the sole + constructor has no arguments and [-indices-matter] is not + activated in the standard library. *) -#[universes(template)] Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. Hint Resolve identity_refl: core. diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index c11a0941fa..4c6520feb3 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -73,14 +73,17 @@ End MemoFunction. reused thanks to a temporary hiding of the dependency in a "container" [memo_val]. *) +#[universes(template)] +Inductive memo_val {A : nat -> Type} : Type := + memo_mval: forall n, A n -> memo_val. +Arguments memo_val : clear implicits. + Section DependentMemoFunction. Variable A: nat -> Type. Variable f: forall n, A n. -#[universes(template)] -Inductive memo_val: Type := - memo_mval: forall n, A n -> memo_val. +Notation memo_val := (memo_val A). Fixpoint is_eq (n m : nat) : {n = m} + {True} := match n, m return {n = m} + {True} with diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 407a7ae45d..0daae0391c 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -12,13 +12,13 @@ Set Implicit Arguments. (** Streams *) -Section Streams. +CoInductive Stream (A : Type) := + Cons : A -> Stream A -> Stream A. -Variable A : Type. +Section Streams. + Variable A : Type. -#[universes(template)] -CoInductive Stream : Type := - Cons : A -> Stream -> Stream. + Notation Stream := (Stream A). Definition hd (x:Stream) := match x with diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 4442108ffc..8a71158f4c 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -208,7 +208,6 @@ Definition concat s1 s2 := - [present] is [true] if and only if [s] contains [x]. *) -#[universes(template)] Record triple := mktriple { t_left:t; t_in:bool; t_right:t }. Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 37a169b02e..bf6336ae47 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -48,7 +48,6 @@ Module Type Ops (X:OrderedType)(Info:InfoTyp). Definition elt := X.t. Hint Transparent elt : core. -#[universes(template)] Inductive tree : Type := | Leaf : tree | Node : Info.t -> tree -> X.t -> tree -> tree. @@ -168,7 +167,6 @@ end. (** Enumeration of the elements of a tree. This corresponds to the "samefringe" notion in the literature. *) -#[universes(template)] Inductive enumeration := | End : enumeration | More : elt -> tree -> enumeration -> enumeration. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 29c84d0d1a..33f6b1050c 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -439,7 +439,6 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E. Definition elt := E.t. -#[universes(template)] Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}. Definition t := t_. Arguments Mkt this {is_ok}. diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index 83e9c29b13..6e08378df4 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -18,46 +18,34 @@ Local Open Scope Z_scope. Definition base digits := Z.pow 2 (Zpos digits). Arguments base digits: simpl never. -Section Carry. +#[universes(template)] +Variant carry (A : Type) := +| C0 : A -> carry A +| C1 : A -> carry A. - Variable A : Type. - - #[universes(template)] - Variant carry := - | C0 : A -> carry - | C1 : A -> carry. - - Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c := +Definition interp_carry {A} (sign:Z)(B:Z)(interp:A -> Z) c := match c with | C0 x => interp x | C1 x => sign*B + interp x end. -End Carry. - -Section Zn2Z. - - Variable znz : Type. - - (** From a type [znz] representing a cyclic structure Z/nZ, - we produce a representation of Z/2nZ by pairs of elements of [znz] - (plus a special case for zero). High half of the new number comes - first. +(** From a type [znz] representing a cyclic structure Z/nZ, + we produce a representation of Z/2nZ by pairs of elements of [znz] + (plus a special case for zero). High half of the new number comes + first. *) +#[universes(template)] +Variant zn2z {znz : Type} := +| W0 : zn2z +| WW : znz -> znz -> zn2z. +Arguments zn2z : clear implicits. - #[universes(template)] - Variant zn2z := - | W0 : zn2z - | WW : znz -> znz -> zn2z. - - Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) := +Definition zn2z_to_Z znz (wB:Z) (w_to_Z:znz->Z) (x:zn2z znz) := match x with | W0 => 0 | WW xh xl => w_to_Z xh * wB + w_to_Z xl end. -End Zn2Z. - Arguments W0 {znz}. (** From a cyclic representation [w], we iterate the [zn2z] construct diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 128ee286b8..6da0fe3966 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -137,7 +137,6 @@ Definition IsStepFun (f:R -> R) (a b:R) : Type := { l:Rlist & is_subdivision f a b l }. (** ** Class of step functions *) -#[universes(template)] Record StepFun (a b:R) : Type := mkStepFun {fe :> R -> R; pre : IsStepFun fe a b}. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 5443ff68ed..c94a373ca0 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -116,7 +116,6 @@ Qed. (*******************************) (*********) -#[universes(template)] Record Metric_Space : Type := {Base : Type; dist : Base -> Base -> R; diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index cfcc82d765..d21042884e 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -380,7 +380,6 @@ Proof. apply Rinv_0_lt_compat; prove_sup0. Qed. -#[universes(template)] Record family : Type := mkfamily {ind : R -> Prop; f :> R -> R -> Prop; diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index e1d7d37e42..745db25a54 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -100,11 +100,9 @@ Hint Resolve Totally_ordered_definition Upper_Bound_definition Section Specific_orders. Variable U : Type. - #[universes(template)] Record Cpo : Type := Definition_of_cpo {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}. - #[universes(template)] Record Chain : Type := Definition_of_chain {PO_of_chain : PO U; Chain_cond : Totally_ordered U PO_of_chain (@Carrier_of _ PO_of_chain)}. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index e9233a34e7..6aefcf32c0 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -22,7 +22,6 @@ Section multiset_defs. Hypothesis eqA_equiv : Equivalence eqA. Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. - #[universes(template)] Inductive multiset : Type := Bag : (A -> nat) -> multiset. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index d2fae6db28..e23d9c2f55 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -36,7 +36,6 @@ Section Partial_orders. Definition Rel := Relation U. - #[universes(template)] Record PO : Type := Definition_of_PO { Carrier_of : Ensemble U; Rel_of : Relation U; diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 76e555ed5a..48a852052e 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -42,7 +42,6 @@ Section defs. Let emptyBag := EmptyBag A. Let singletonBag := SingletonBag _ eqA_dec. - #[universes(template)] Inductive Tree := | Tree_Leaf : Tree | Tree_Node : A -> Tree -> Tree -> Tree. @@ -129,8 +128,7 @@ Section defs. (** ** Merging two sorted lists *) - #[universes(template)] - Inductive merge_lem (l1 l2:list A) : Type := + Inductive merge_lem (l1 l2:list A) : Type := merge_exist : forall l:list A, Sorted leA l -> @@ -203,7 +201,6 @@ Section defs. (** ** Specification of heap insertion *) - #[universes(template)] Inductive insert_spec (a:A) (T:Tree) : Type := insert_exist : forall T1:Tree, @@ -237,7 +234,6 @@ Section defs. (** ** Building a heap from a list *) - #[universes(template)] Inductive build_heap (l:list A) : Type := heap_exist : forall T:Tree, @@ -262,7 +258,6 @@ Section defs. (** ** Building the sorted list *) - #[universes(template)] Inductive flat_spec (T:Tree) : Type := flat_exist : forall l:list A, diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index d747258f56..6ddbc8e214 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -14,17 +14,18 @@ Require Import Eqdep. +#[universes(template)] +Inductive WO (A : Type) (B : A -> Type) : Type := + sup : forall (a:A) (f:B a -> WO A B), WO A B. + Section WellOrdering. Variable A : Type. Variable B : A -> Type. - #[universes(template)] - Inductive WO : Type := - sup : forall (a:A) (f:B a -> WO), WO. - + Notation WO := (WO A B). Inductive le_WO : WO -> WO -> Prop := - le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f). + le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup _ _ a f). Theorem wf_WO : well_founded le_WO. Proof. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 577544f971..fee928430c 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -212,7 +212,6 @@ Module MoreInt (Import I:Int). | EZofI : ExprI -> ExprZ | EZraw : Z -> ExprZ. - #[universes(template)] Inductive ExprP : Type := | EPeq : ExprZ -> ExprZ -> ExprP | EPlt : ExprZ -> ExprZ -> ExprP diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 67d70416c8..2750d7dc16 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -32,6 +32,10 @@ let set_type_in_type () = let typing_flags = Environ.typing_flags (Global.env ()) in Global.set_typing_flags { typing_flags with Declarations.check_universes = false } +let set_no_template_check () = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_template = false } + (******************************************************************************) type color = [`ON | `AUTO | `EMACS | `OFF] @@ -535,6 +539,7 @@ let parse_args ~help ~init arglist : t * string list = |"-list-tags" -> set_query oval PrintTags |"-time" -> { oval with config = { oval.config with time = true }} |"-type-in-type" -> set_type_in_type (); oval + |"-no-template-check" -> set_no_template_check (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index cdb2e36fbd..8555d78156 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -82,6 +82,7 @@ let print_usage_common co command = \n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ +\n -no-template-check disable checking of universes constraints on universes parameterizing template polymorphic inductive types\ \n -mangle-names x mangle auto-generated names using prefix x\ \n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\ \n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\ diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index a72e43de01..cb034bdff6 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -353,6 +353,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in - accu - + if not mind.mind_typing_flags.check_template then + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu + else accu in GlobRef.Map_env.fold fold graph ContextObjectMap.empty diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index d414d57c0d..98fe436a22 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -345,7 +345,7 @@ let build_beq_scheme mode kn = Vars.substl subst cores.(i) in create_input fix), - UState.make (Global.universes ())), + UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme @@ -690,7 +690,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = UState.make (Global.universes ()) in + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal @@ -820,7 +820,7 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let ctx = UState.make (Global.universes ()) in + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal @@ -996,7 +996,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let ctx = UState.make (Global.universes ()) in + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index adbe196699..87dab72880 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -114,20 +114,22 @@ let mk_mltype_data sigma env assums arity indname = inductives which are recognized when a "Type" appears at the end of the conlusion in the source syntax. *) -let rec check_anonymous_type ind = +let rec check_type_conclusion ind = let open Glob_term in match DAst.get ind with - | GSort (UAnonymous {rigid=true}) -> true + | GSort (UAnonymous {rigid=true}) -> (Some true) + | GSort (UNamed _) -> (Some false) | GProd ( _, _, _, e) | GLetIn (_, _, _, e) | GLambda (_, _, _, e) | GApp (e, _) - | GCast (e, _) -> check_anonymous_type e - | _ -> false + | GCast (e, _) -> check_type_conclusion e + | _ -> None -let make_conclusion_flexible sigma = function +let make_anonymous_conclusion_flexible sigma = function | None -> sigma - | Some s -> + | Some (false, _) -> sigma + | Some (true, s) -> (match EConstr.ESorts.kind sigma s with | Type u -> (match Univ.universe_level u with @@ -136,17 +138,23 @@ let make_conclusion_flexible sigma = function | None -> sigma) | _ -> sigma) -let interp_ind_arity env sigma ind = +let intern_ind_arity env sigma ind = let c = intern_gen IsType env sigma ind.ind_arity in let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in + let pseudo_poly = check_type_conclusion c in + (constr_loc ind.ind_arity, c, impls, pseudo_poly) + +let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) = let sigma,t = understand_tcc env sigma ~expected_type:IsType c in - let pseudo_poly = check_anonymous_type c in match Reductionops.sort_of_arity env sigma t with | exception Invalid_argument _ -> - user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") + user_err ?loc (str "Not an arity") | s -> - let concl = if pseudo_poly then Some s else None in - sigma, (t, Retyping.relevance_of_sort s, concl, impls) + let concl = match pseudo_poly with + | Some b -> Some (b, s) + | None -> None + in + sigma, (t, Retyping.relevance_of_sort s, concl, impls) let interp_cstrs env sigma impls mldata arity ind = let cnames,ctyps = List.split ind.ind_lc in @@ -251,7 +259,7 @@ let solve_constraints_system levels level_bounds = done; v -let inductive_levels env evd poly arities inds = +let inductive_levels env evd arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> if Sorts.is_prop a || Sorts.is_sprop a then None @@ -286,7 +294,7 @@ let inductive_levels env evd poly arities inds = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative_sort env du then (* Any product is allowed here. *) - evd, arity :: arities + evd, (false, arity) :: arities else (* If in a predicative sort, or asked to infer the type, we take the max of: - indices (if in indices-matter mode) @@ -300,7 +308,6 @@ let inductive_levels env evd poly arities inds = raise (InductiveError LargeNonPropInductiveNotInType) else evd else evd - (* Evd.set_leq_sort env evd (Type cu) du *) in let evd = if len >= 2 && Univ.is_type0m_univ cu then @@ -311,14 +318,14 @@ let inductive_levels env evd poly arities inds = else evd in let duu = Sorts.univ_of_sort du in - let evd = + let template_prop, evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - Evd.set_eq_sort env evd Sorts.prop du - else evd - else Evd.set_eq_sort env evd (sort_of_univ cu) du + true, Evd.set_eq_sort env evd Sorts.prop du + else false, evd + else false, Evd.set_eq_sort env evd (sort_of_univ cu) du in - (evd, arity :: arities)) + (evd, (template_prop, arity) :: arities)) (evd,[]) (Array.to_list levels') destarities sizes in evd, List.rev arities @@ -328,6 +335,17 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg +let template_polymorphism_candidate env uctx params concl = + match uctx with + | Entries.Monomorphic_entry uctx -> + let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in + if not concltemplate then false + else + let template_check = Environ.check_template env in + let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in + let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in + not (template_check && Univ.LSet.is_empty conclunivs) + | Entries.Polymorphic_entry _ -> false let check_param = function | CLocalDef (na, _, _) -> check_named na @@ -345,25 +363,46 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = - check_all_names_different indl; - List.iter check_param paramsl; - if not (List.is_empty uparamsl) && not (List.is_empty notations) - then user_err (str "Inductives with uniform parameters may not have attached notations."); - let sigma, udecl = interp_univ_decl_opt env0 udecl in +let interp_params env udecl uparamsl paramsl = + let sigma, udecl = interp_univ_decl_opt env udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = - interp_context_evars ~program_mode:false env0 sigma uparamsl in + interp_context_evars ~program_mode:false env sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl in - let indnames = List.map (fun ind -> ind.ind_name) indl in - (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in - let params = List.map (RelDecl.get_name %> Name.get_id) assums in + sigma, env_params, (ctx_params, env_uparams, ctx_uparams, + List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl) + +let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = + check_all_names_different indl; + List.iter check_param paramsl; + if not (List.is_empty uparamsl) && not (List.is_empty notations) + then user_err (str "Inductives with uniform parameters may not have attached notations."); + + let indnames = List.map (fun ind -> ind.ind_name) indl in + let sigma, env_params, infos = + interp_params env0 udecl uparamsl paramsl + in (* Interpret the arities *) - let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in + let arities = List.map (intern_ind_arity env_params sigma) indl in + + let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template = + let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in + if not poly && is_template then + (* In case of template polymorphism, we need to compute more constraints *) + let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in + let sigma, env_params, infos = + interp_params env0 udecl uparamsl paramsl + in + let arities = List.map (intern_ind_arity env_params sigma) indl in + sigma, env_params, infos, arities, is_template + else sigma, env_params, infos, arities, is_template + in + + let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in let arities, relevances, arityconcl, indimpls = List.split4 arities in let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in @@ -410,31 +449,34 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let nf = Evarutil.nf_evars_universes sigma in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in - let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in - let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in + let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in + let sigma, arities = inductive_levels env_ar_params sigma arities constructors in let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in - let arities = List.map nf arities in + let arities = List.map (fun (template, arity) -> template, nf arity) arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in - let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in - let sigma = restrict_inductive_universes sigma ctx_params arities constructors in + let arityconcl = List.map (Option.map (fun (anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in + let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in let uctx = Evd.check_univ_decl ~poly sigma udecl in - List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities; + List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities; Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) constructors; (* Build the inductive entries *) - let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) -> + let entries = List.map4 (fun ind (templatearity, arity) concl (cnames,ctypes,cimpls) -> + let template_candidate () = + templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in let template = match template with | Some template -> if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); + if template && not (template_candidate ()) then + user_err Pp.(strbrk "inductive cannot be made template polymorphic on any universe"); template | None -> - should_auto_template ind.ind_name (not poly && - Option.cata (fun s -> not (Sorts.is_small s)) false concl) + should_auto_template ind.ind_name (template_candidate ()) in { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 285be8cd51..7587bd165f 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -62,3 +62,17 @@ val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the inductive under consideration. *) + +val template_polymorphism_candidate : + Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool +(** [template_polymorphism_candidate env uctx params conclsort] is + [true] iff an inductive with params [params] and conclusion + [conclsort] would be definable as template polymorphic. It should + have at least one universe in its monomorphic universe context that + can be made parametric in its conclusion sort, if one is given. + If the [Template Check] flag is false we just check that the conclusion sort + is not small. *) + +val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t +(** [sign_level env sigma ctx] computes the universe level of the context [ctx] + as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *) diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index c5cbb095ca..e7773abaf4 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -541,7 +541,7 @@ let obligation_terminator entries uctx { name; num; auto } = declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) - if defined then UState.make (Global.universes ()) + if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) else ctx in let prg = {prg with prg_ctx} in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 37fe0df0ee..334d9e81fa 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -454,7 +454,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } if not prg.prg_poly (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - let ctx = UState.make (Global.universes ()) in + let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in let ctx' = UState.merge_subst ctx (UState.subst ctx') in Univ.Instance.empty, ctx' else diff --git a/vernac/record.ml b/vernac/record.ml index 86745212e7..cfcbd1d7ae 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -85,10 +85,10 @@ let interp_fields_evars env sigma impls_env nots l = let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> - let univ = + let univ = if is_local_assum d then let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in - Univ.sup (univ_of_sort s) univ + Univ.sup (univ_of_sort s) univ else univ in (EConstr.push_rel d env, univ)) l (env, Univ.Universe.sprop) @@ -101,8 +101,19 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl +let check_anonymous_type ind = + match ind with + | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true + | _ -> false + let typecheck_params_and_fields finite def poly pl ps records = let env0 = Global.env () in + (* Special case elaboration for template-polymorphic inductives, + lower bound on introduced universes is Prop so that we do not miss + any Set <= i constraint for universes that might actually be instantiated with Prop. *) + let is_template = + List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in + let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in let () = let error bk {CAst.loc; v=name} = @@ -111,15 +122,15 @@ let typecheck_params_and_fields finite def poly pl ps records = user_err ?loc ~hdr:"record" (str "Record parameters must be named") | _ -> () in - List.iter + List.iter (function CLocalDef (b, _, _) -> error default_binder_kind b | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps - in + in let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in let fold (sigma, template) (_, t, _, _) = match t with - | Some t -> + | Some t -> let env = EConstr.push_rel_context newps env0 in let poly = match t with @@ -138,7 +149,7 @@ let typecheck_params_and_fields finite def poly pl ps records = (sigma, false), (s, s') else (sigma, false), (s, s')) | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) - | None -> + | None -> let uvarkind = Evd.univ_flexible_alg in let sigma, s = Evd.new_sort_variable uvarkind sigma in (sigma, template), (EConstr.mkSort s, s) @@ -168,23 +179,23 @@ let typecheck_params_and_fields finite def poly pl ps records = let _, univ = compute_constructor_level sigma env_ar newfs in let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in if not def && is_impredicative_sort env0 sort then - sigma, typ + sigma, (univ, typ) else let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in if Univ.is_small_univ univ && Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - Evd.set_eq_sort env_ar sigma Sorts.set sort, EConstr.mkSort (Sorts.sort_of_univ univ) - else sigma, typ + Evd.set_eq_sort env_ar sigma Sorts.set sort, (univ, EConstr.mkSort (Sorts.sort_of_univ univ)) + else sigma, (univ, typ) in let (sigma, typs) = List.fold_left2_map fold sigma typs data in let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf -> let newps = List.map (RelDecl.map_constr_het nf) newps in - let map (impls, newfs) typ = + let map (impls, newfs) (univ, typ) = let newfs = List.map (RelDecl.map_constr_het nf) newfs in let typ = nf typ in - (typ, impls, newfs) + (univ, typ, impls, newfs) in let ans = List.map2 map data typs in newps, ans) @@ -295,7 +306,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let x = make_annot (Name binder_name) mip.mind_relevance in let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in - let primitive = + let primitive = match mib.mind_record with | PrimRecord _ -> true | FakeRecord | NotRecord -> false @@ -310,7 +321,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f | Anonymous -> (None::sp_projs,i,NoProjection fi::subst) | Name fid -> try - let kn, term = + let kn, term = if is_local_assum decl && primitive then let p = Projection.Repr.make indsp ~proj_npars:mib.mind_nparams @@ -354,12 +365,12 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in - applist (mkConstU (kn,u),proj_args) + applist (mkConstU (kn,u),proj_args) in Declare.definition_message fid; kn, constr_fip with Type_errors.TypeError (ctx,te) -> - raise (NotDefinable (BadTypedProj (fid,ctx,te))) + raise (NotDefinable (BadTypedProj (fid,ctx,te))) in let refi = GlobRef.ConstRef kn in Impargs.maybe_declare_manual_implicits false refi impls; @@ -413,29 +424,33 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let binder_name = match name with | None -> - let map (id, _, _, _, _, _, _) = + let map (id, _, _, _, _, _, _, _) = Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) in Array.map_of_list map record_data | Some n -> n in let ntypes = List.length record_data in - let mk_block i (id, idbuild, arity, _, fields, _, _) = + let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) = let nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let template = + let template_candidate () = + ComInductive.template_polymorphism_candidate (Global.env ()) univs params + (Some (Sorts.sort_of_univ min_univ)) + in match template with | Some template, _ -> (* templateness explicitly requested *) if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); + if template && not (template_candidate ()) then + user_err Pp.(strbrk "record cannot be made template polymorphic on any universe"); template | None, template -> (* auto detect template *) - ComInductive.should_auto_template id (template && not poly && - let _, s = Reduction.dest_arity (Global.env()) arity in - not (Sorts.is_small s)) + ComInductive.should_auto_template id (template && template_candidate ()) in { mind_entry_typename = id; mind_entry_arity = arity; @@ -446,7 +461,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let blocks = List.mapi mk_block record_data in let primitive = !primitive_flag && - List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data + List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data in let mie = { mind_entry_params = params; @@ -463,7 +478,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag in - let map i (_, _, _, fieldimpls, fields, is_coe, coers) = + let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) = let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in @@ -478,7 +493,7 @@ let implicits_of_context ctx = List.map (fun name -> CAst.make (Some (name,true))) (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class def cumulative ubinders univs id idbuild paramimpls params arity +let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -493,7 +508,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari let binder = {binder with binder_name=Name binder_name} in let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in - let class_entry = + let class_entry = Declare.definition_entry ~types:class_type ~univs class_body in let cst = Declare.declare_constant ~name:id (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) @@ -518,18 +533,18 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls); Classes.set_typeclass_transparency (EvalConstRef cst) false false; let sub = match List.hd coers with - | Some b -> Some ((if b then Backward else Forward), List.hd priorities) - | None -> None + | Some b -> Some ((if b then Backward else Forward), List.hd priorities) + | None -> None in [cref, [Name proj_name, sub, Some proj_cst]] | _ -> - let record_data = [id, idbuild, arity, fieldimpls, fields, false, + let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false, List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls params template ~kind:Decls.Method ~name:[|binder_name|] record_data in - let coers = List.map2 (fun coe pri -> - Option.map (fun b -> + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) coers priorities in @@ -584,7 +599,7 @@ let add_constant_class env sigma cst = let ctx, _ = decompose_prod_assum ty in let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in - let tc = + let tc = { cl_univs = univs; cl_impl = GlobRef.ConstRef cst; cl_context = (List.map (const None) ctx, ctx); @@ -688,24 +703,24 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records = let template = template, auto_template in match kind with | Class def -> - let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with + let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with | [r], [d] -> r, d | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") in let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in declare_class def cumulative ubinders univs id.CAst.v idbuild - implpars params arity template implfs fields coers priorities + implpars params univ arity template implfs fields coers priorities | _ -> let map impls = implpars @ [CAst.make None] @ impls in - let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in - let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = + let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in + let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) -> { pf_subclass = not (Option.is_empty rf_subclass); pf_canonical = rf_canonical }) cfs in - id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe + id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4ae9d6d54f..6180ab0821 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -606,6 +606,24 @@ let vernac_assumption ~atts discharge kind l nl = | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l +let set_template_check b = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_template = b } + +let is_template_check () = + let typing_flags = Environ.typing_flags (Global.env ()) in + typing_flags.Declarations.check_template + +let () = + let tccheck = + { optdepr = true; + optname = "Template universe check"; + optkey = ["Template"; "Check"]; + optread = (fun () -> is_template_check ()); + optwrite = (fun b -> set_template_check b)} + in + declare_bool_option tccheck + let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false ~name:"Polymorphic inductive cumulativity" @@ -2538,7 +2556,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> vernac_hints ~atts dbnames hints) | VernacSyntacticDefinition (id,c,b) -> - VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) + VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> VtDefault(fun () -> with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags)) |