From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 14:50:07 +0200 Subject: When declaring constants/inductives use ContextSet if monomorphic. Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved. --- API/API.mli | 11 +++++----- checker/cic.mli | 4 ++-- checker/mod_checking.ml | 2 +- checker/values.ml | 6 ++--- interp/declare.ml | 6 +++-- kernel/declarations.ml | 6 ++--- kernel/declareops.ml | 4 ++-- kernel/entries.ml | 10 +++++---- kernel/indtypes.ml | 9 ++++---- kernel/mod_typing.ml | 26 ++++++++++++---------- kernel/safe_typing.ml | 12 +++++----- kernel/term_typing.ml | 46 ++++++++++++++++++++++----------------- kernel/term_typing.mli | 2 +- kernel/univ.ml | 1 + kernel/univ.mli | 5 ++++- kernel/vconv.ml | 2 +- plugins/ltac/rewrite.ml | 6 ++++- printing/prettyp.ml | 14 ++++++------ printing/printer.ml | 4 ++++ printing/printer.mli | 1 + proofs/proof_global.ml | 12 +++++----- tactics/ind_tables.ml | 5 ++--- test-suite/output/UnivBinders.out | 2 +- vernac/classes.ml | 34 +++++++++++++++++++---------- vernac/command.ml | 15 ++++++++----- vernac/indschemes.ml | 6 ++--- vernac/lemmas.ml | 19 ++++++++++++---- vernac/obligations.ml | 45 ++++++++++++++++++++++---------------- vernac/record.ml | 36 +++++++++++++++--------------- 29 files changed, 205 insertions(+), 146 deletions(-) diff --git a/API/API.mli b/API/API.mli index 5c7860671..ad5d5490b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1417,7 +1417,7 @@ sig | TemplateArity of 'b type constant_universes = - | Monomorphic_const of Univ.UContext.t + | Monomorphic_const of Univ.ContextSet.t | Polymorphic_const of Univ.AUContext.t type projection_body = { @@ -1484,7 +1484,7 @@ sig | MEwith of module_alg_expr * with_declaration type abstract_inductive_universes = - | Monomorphic_ind of Univ.UContext.t + | Monomorphic_ind of Univ.ContextSet.t | Polymorphic_ind of Univ.AUContext.t | Cumulative_ind of Univ.ACumulativityInfo.t @@ -1551,7 +1551,7 @@ sig | LocalAssumEntry of constr type inductive_universes = - | Monomorphic_ind_entry of Univ.UContext.t + | Monomorphic_ind_entry of Univ.ContextSet.t | Polymorphic_ind_entry of Univ.UContext.t | Cumulative_ind_entry of Univ.CumulativityInfo.t @@ -1580,8 +1580,9 @@ sig type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation type constant_universes_entry = - | Monomorphic_const_entry of Univ.UContext.t + | Monomorphic_const_entry of Univ.ContextSet.t | Polymorphic_const_entry of Univ.UContext.t + type 'a in_constant_universes_entry = 'a * constant_universes_entry type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -1592,7 +1593,7 @@ sig const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } - type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline + type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline type projection_entry = { proj_entry_ind : MutInd.t; diff --git a/checker/cic.mli b/checker/cic.mli index 354650964..4a0e706aa 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -208,7 +208,7 @@ type constant_def = | OpaqueDef of lazy_constr type constant_universes = - | Monomorphic_const of Univ.universe_context + | Monomorphic_const of Univ.ContextSet.t | Polymorphic_const of Univ.abstract_universe_context (** The [typing_flags] are instructions to the type-checker which @@ -303,7 +303,7 @@ type one_inductive_body = { } type abstract_inductive_universes = - | Monomorphic_ind of Univ.universe_context + | Monomorphic_ind of Univ.ContextSet.t | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 63e28448f..4357a690e 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -29,7 +29,7 @@ let check_constant_declaration env kn cb = (** [env'] contains De Bruijn universe variables *) let env' = match cb.const_universes with - | Monomorphic_const ctx -> push_context ~strict:true ctx env + | Monomorphic_const ctx -> push_context_set ~strict:true ctx env | Polymorphic_const auctx -> let ctx = Univ.AUContext.repr auctx in push_context ~strict:false ctx env diff --git a/checker/values.ml b/checker/values.ml index 9e16c8435..5a371164c 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 f4b00c567a972ae950b9ed10c533fda5 checker/cic.mli +MD5 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli *) @@ -215,7 +215,7 @@ let v_projbody = let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool|] -let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|] +let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; @@ -265,7 +265,7 @@ let v_mind_record = Annot ("mind_record", let v_ind_pack_univs = v_sum "abstract_inductive_universes" 0 - [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|] + [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|] let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; diff --git a/interp/declare.ml b/interp/declare.ml index dc77981f2..15999f1d1 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -207,7 +207,9 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = let univs = if poly then Polymorphic_const_entry univs - else Monomorphic_const_entry univs + else + (* FIXME be smarter about this *) + Monomorphic_const_entry (Univ.ContextSet.of_context univs) in { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; @@ -340,7 +342,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_record = None; mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty; + mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; }) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b95796fd8..d5312c500 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -63,7 +63,7 @@ type constant_def = | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) type constant_universes = - | Monomorphic_const of Univ.UContext.t + | Monomorphic_const of Univ.ContextSet.t | Polymorphic_const of Univ.AUContext.t (** The [typing_flags] are instructions to the type-checker which @@ -168,9 +168,9 @@ type one_inductive_body = { } type abstract_inductive_universes = - | Monomorphic_ind of Univ.UContext.t + | Monomorphic_ind of Univ.ContextSet.t | Polymorphic_ind of Univ.AUContext.t - | Cumulative_ind of Univ.ACumulativityInfo.t + | Cumulative_ind of Univ.ACumulativityInfo.t type mutual_inductive_body = { diff --git a/kernel/declareops.ml b/kernel/declareops.ml index f5c26b33d..d8768a0fc 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -126,7 +126,7 @@ let hcons_const_def = function let hcons_const_universes cbu = match cbu with | Monomorphic_const ctx -> - Monomorphic_const (Univ.hcons_universe_context ctx) + Monomorphic_const (Univ.hcons_universe_context_set ctx) | Polymorphic_const ctx -> Polymorphic_const (Univ.hcons_abstract_universe_context ctx) @@ -274,7 +274,7 @@ let hcons_mind_packet oib = let hcons_mind_universes miu = match miu with - | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx) + | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx) | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) diff --git a/kernel/entries.ml b/kernel/entries.ml index 185dba409..c44a17df2 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -35,9 +35,9 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; *) type inductive_universes = - | Monomorphic_ind_entry of Univ.UContext.t + | Monomorphic_ind_entry of Univ.ContextSet.t | Polymorphic_ind_entry of Univ.UContext.t - | Cumulative_ind_entry of Univ.CumulativityInfo.t + | Cumulative_ind_entry of Univ.CumulativityInfo.t type one_inductive_entry = { mind_entry_typename : Id.t; @@ -65,9 +65,11 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation type constant_universes_entry = - | Monomorphic_const_entry of Univ.UContext.t + | Monomorphic_const_entry of Univ.ContextSet.t | Polymorphic_const_entry of Univ.UContext.t +type 'a in_constant_universes_entry = 'a * constant_universes_entry + type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -82,7 +84,7 @@ type 'a definition_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.Named.t option * bool * types Univ.in_universe_context * inline + Context.Named.t option * types in_constant_universes_entry * inline type projection_entry = { proj_entry_ind : MutInd.t; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 083b0ae40..8e9b606a5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -265,13 +265,12 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let univctx = + let env' = match mie.mind_entry_universes with - | Monomorphic_ind_entry ctx -> ctx - | Polymorphic_ind_entry ctx -> ctx - | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi + | Monomorphic_ind_entry ctx -> push_context_set ctx env + | Polymorphic_ind_entry ctx -> push_context ctx env + | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env in - let env' = push_context univctx env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 8568bf14b..f7e755f00 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -79,18 +79,20 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = environment, because they do not appear in the type of the definition. Any inconsistency will be raised at a later stage when joining the environment. *) - let env' = Environ.push_context ~strict:true ctx env' in - let c',cst = match cb.const_body with - | Undef _ | OpaqueDef _ -> - let j = Typeops.infer env' c in - let typ = cb.const_type in - let cst' = Reduction.infer_conv_leq env' (Environ.universes env') - j.uj_type typ in - j.uj_val, cst' - | Def cs -> - let c' = Mod_subst.force_constr cs in - c, Reduction.infer_conv env' (Environ.universes env') c c' - in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) + let env' = Environ.push_context ~strict:true ctx env' in + let c',cst = match cb.const_body with + | Undef _ | OpaqueDef _ -> + let j = Typeops.infer env' c in + let typ = cb.const_type in + let cst' = Reduction.infer_conv_leq env' (Environ.universes env') + j.uj_type typ in + j.uj_val, cst' + | Def cs -> + let c' = Mod_subst.force_constr cs in + c, Reduction.infer_conv env' (Environ.universes env') c c' + in + let ctx = Univ.ContextSet.of_context ctx in + c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx | Polymorphic_const uctx -> let subst, ctx = Univ.abstract_universes ctx in let c = Vars.subst_univs_level_constr subst c in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0e416b3e5..0e41bfc3c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -249,14 +249,14 @@ let universes_of_private eff = in match cb.const_universes with | Monomorphic_const ctx -> - (Univ.ContextSet.of_context ctx) :: acc + ctx :: acc | Polymorphic_const _ -> acc ) acc l | Entries.SEsubproof (c, cb, e) -> match cb.const_universes with | Monomorphic_const ctx -> - (Univ.ContextSet.of_context ctx) :: acc + ctx :: acc | Polymorphic_const _ -> acc ) [] (Term_typing.uniq_seff eff) @@ -389,7 +389,6 @@ let push_named_def (id,de) senv = | Monomorphic_const_entry _ -> false | Polymorphic_const_entry _ -> true in - let univs = Univ.ContextSet.of_context univs in let c, univs = match c with | Def c -> Mod_subst.force_constr c, univs | OpaqueDef o -> @@ -425,9 +424,8 @@ let labels_of_mib mib = let globalize_constant_universes env cb = match cb.const_universes with - | Monomorphic_const ctx -> - let cstrs = Univ.ContextSet.of_context ctx in - Now (false, cstrs) :: + | Monomorphic_const cstrs -> + Now (false, cstrs) :: (match cb.const_body with | (Undef _ | Def _) -> [] | OpaqueDef lc -> @@ -443,7 +441,7 @@ let globalize_constant_universes env cb = let globalize_mind_universes mb = match mb.mind_universes with | Monomorphic_ind ctx -> - [Now (false, Univ.ContextSet.of_context ctx)] + [Now (false, ctx)] | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)] | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 4617f2d5f..70dd6438d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -125,11 +125,10 @@ let inline_side_effects env body ctx side_eff = | _ -> assert false in match cb.const_universes with - | Monomorphic_const cnstctx -> + | Monomorphic_const univs -> (** Abstract over the term at the top of the proof *) let ty = cb.const_type in let subst = Cmap_env.add c (Inr var) subst in - let univs = Univ.ContextSet.of_context cnstctx in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) | Polymorphic_const auctx -> @@ -228,19 +227,25 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) -let abstract_constant_universes abstract uctx = - if not abstract then +let abstract_constant_universes abstract = function + | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx - else - let sbst, auctx = Univ.abstract_universes uctx in - sbst, Polymorphic_const auctx + | Polymorphic_const_entry uctx -> + if not abstract then + Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx) + else + let sbst, auctx = Univ.abstract_universes uctx in + sbst, Polymorphic_const auctx let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = match dcl with - | ParameterEntry (ctx,poly,(t,uctx),nl) -> - let env = push_context ~strict:(not poly) uctx env in + | ParameterEntry (ctx,(t,uctx),nl) -> + let env = match uctx with + | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env + | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env + in let j = infer env t in - let abstract = poly && not (Option.is_empty kn) in + let abstract = not (Option.is_empty kn) in let usubst, univs = abstract_constant_universes abstract uctx in @@ -262,7 +267,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_universes = Monomorphic_const_entry univs } as c) -> - let env = push_context ~strict:true univs env in + let env = push_context_set ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = @@ -301,21 +306,22 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let poly, univs = match c.const_entry_universes with + let poly, univsctx = match c.const_entry_universes with | Monomorphic_const_entry univs -> false, univs - | Polymorphic_const_entry univs -> true, univs + | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs in - let univsctx = Univ.ContextSet.of_context univs in let ctx = Univ.ContextSet.union univsctx ctx in let body, ctx, _ = match trust with | Pure -> body, ctx, [] | SideEffects _ -> inline_side_effects env body ctx side_eff in let env = push_context_set ~strict:(not poly) ctx env in - let abstract = poly && not (Option.is_empty kn) in - let usubst, univs = - abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) - in + let abstract = not (Option.is_empty kn) in + let ctx = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) + else Monomorphic_const_entry ctx + in + let usubst, univs = abstract_constant_universes abstract ctx in let j = infer env body in let typ = match typ with | None -> @@ -556,7 +562,7 @@ let export_side_effects mb env ce = let env = Environ.add_constant kn cb env in match cb.const_universes with | Monomorphic_const ctx -> - Environ.push_context ~strict:true ctx env + Environ.push_context_set ~strict:true ctx env | Polymorphic_const _ -> env end | kn, cb, `Opaque(_, ctx), _ -> @@ -564,7 +570,7 @@ let export_side_effects mb env ce = let env = Environ.add_constant kn cb env in match cb.const_universes with | Monomorphic_const cstctx -> - let env = Environ.push_context ~strict:true cstctx env in + let env = Environ.push_context_set ~strict:true cstctx env in Environ.push_context_set ~strict:true ctx env | Polymorphic_const _ -> env end diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 9b35bfc6e..55da4197e 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -19,7 +19,7 @@ type _ trust = | SideEffects : structure_body -> side_effects trust val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry -> - constant_def * types * Univ.UContext.t + constant_def * types * Univ.ContextSet.t val translate_local_assum : env -> types -> types diff --git a/kernel/univ.ml b/kernel/univ.ml index 7fe4f8274..64afb95d5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1053,6 +1053,7 @@ struct let constraints (univs, cst) = cst let levels (univs, cst) = univs + let size (univs,_) = LSet.cardinal univs end type universe_context_set = ContextSet.t diff --git a/kernel/univ.mli b/kernel/univ.mli index 8d46a8bee..c06ce2446 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -310,7 +310,7 @@ sig (** Keeps the order of the instances *) val union : t -> t -> t - (* the number of universes in the context *) + (** the number of universes in the context *) val size : t -> int end @@ -423,6 +423,9 @@ sig val constraints : t -> constraints val levels : t -> LSet.t + + (** the number of universes in the context *) + val size : t -> int end (** A set of universes with universe constraints. diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 0e452621c..578a89371 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let mib = Environ.lookup_mind mi env in let ulen = match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx + | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx | Declarations.Cumulative_ind cumi -> Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index f6523d28c..a2f5a4577 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1972,9 +1972,13 @@ let add_morphism_infer glob m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then + let uctx = if poly + then Entries.Polymorphic_const_entry (UState.context uctx) + else Entries.Monomorphic_const_entry (UState.context_set uctx) + in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry - (None,poly,(instance,UState.context uctx),None), + (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8fc00ed96..b4ac94103 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -556,26 +556,26 @@ let print_constant with_values sep sp = Vars.subst_instance_constr inst cb.const_type in let univs = + let open Entries in let otab = Global.opaque_tables () in match cb.const_body with | Undef _ | Def _ -> begin match cb.const_universes with - | Monomorphic_const ctx -> ctx + | Monomorphic_const ctx -> Monomorphic_const_entry ctx | Polymorphic_const ctx -> let inst = Univ.AUContext.instance ctx in - Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) + Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)) end | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with | Monomorphic_const ctx -> - let uctxs = Univ.ContextSet.of_context ctx in - Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + Monomorphic_const_entry (Univ.ContextSet.union body_uctxs ctx) | Polymorphic_const ctx -> assert(Univ.ContextSet.is_empty body_uctxs); let inst = Univ.AUContext.instance ctx in - Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) + Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)) in let ctx = Evd.evar_universe_context_of_binders @@ -589,12 +589,12 @@ let print_constant with_values sep sp = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_universe_ctx sigma univs + Printer.pr_constant_universes sigma univs | Some (c, ctx) -> let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ - Printer.pr_universe_ctx sigma univs) + Printer.pr_constant_universes sigma univs) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ diff --git a/printing/printer.ml b/printing/printer.ml index 4d5cfcba3..ae6292024 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -270,6 +270,10 @@ let pr_universe_ctx sigma c = else mt() +let pr_constant_universes sigma = function + | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx + | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx + let pr_cumulativity_info sigma cumi = if !Detyping.print_universes && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then diff --git a/printing/printer.mli b/printing/printer.mli index a3d0eaac2..67128da40 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -122,6 +122,7 @@ val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t +val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index ea0408169..905173efc 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -331,7 +331,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in + let univctx = UState.check_univ_decl universes universe_decl in let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to @@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in + let univs = UState.check_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) else (* Since the proof is computed now, we can simply have 1 set of @@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in + let univs = UState.check_univ_decl ctx universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) let bodyunivs = constrain_variables univctx (Future.force univs) in - let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in + let univs = UState.check_univ_decl bodyunivs universe_decl in (pt,Univ.ContextSet.of_context univs),eff) in let entry_fn p (_, t) = @@ -392,7 +392,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let univs, typ = Future.force univstyp in let univs = if poly then Entries.Polymorphic_const_entry univs - else Entries.Monomorphic_const_entry univs + else + (* FIXME be smarter about the unnecessary context linearisation in make_body *) + Entries.Monomorphic_const_entry (Univ.ContextSet.of_context univs) in {Entries. const_entry_body = body; diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 92c326b1e..e1bf32f3c 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -123,10 +123,9 @@ let define internal id c p univs = let ctx = Evd.normalize_evar_universe_context univs in let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in - let univs = UState.context ctx in let univs = - if p then Polymorphic_const_entry univs - else Monomorphic_const_entry univs + if p then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) in let entry = { const_entry_body = diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 1bacb7513..42fb52a3b 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -50,6 +50,6 @@ Type@{Top.17} -> Type@{v} -> Type@{u} foo is universe polymorphic Monomorphic mono = Type@{u} : Type@{u+1} -(* u |= *) +(* {u} |= *) mono is not universe polymorphic diff --git a/vernac/classes.ml b/vernac/classes.ml index 6f5f96ee2..c99eba2cc 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -200,16 +200,22 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let nf, subst = Evarutil.e_nf_evars_and_universes evars in let termtype = let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - nf t - in - Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); + nf t + in + Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); let ctx = Evd.check_univ_decl !evars decl in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry - (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) - in + let ctx = if poly + then Polymorphic_const_entry ctx + else + (* FIXME be smarter about this *) + Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id + (ParameterEntry + (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + in Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); - instance_hook k pri global imps ?hook (ConstRef cst); id + instance_hook k pri global imps ?hook (ConstRef cst); id end else ( let props = @@ -384,14 +390,20 @@ let context poly l = let uctx = ref (Evd.universe_context_set !evars) in let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let ctx = Univ.ContextSet.to_context !uctx in (* Declare the universe context once *) + let univs = !uctx in let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> - (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context univs) + else Monomorphic_const_entry univs + in + (ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> - let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + (* FIXME be smarter about this *) + let univs = Univ.ContextSet.to_context univs in + let entry = Declare.definition_entry ~poly ~univs ~types:t b in (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in diff --git a/vernac/command.ml b/vernac/command.ml index 80599c534..06d0c8470 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -197,8 +197,11 @@ match local with | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in + let ctx = if p + then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) + else Monomorphic_const_entry ctx + in + let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -206,9 +209,9 @@ match local with let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in - let inst = - if p (* polymorphic *) then Univ.UContext.instance ctx - else Univ.Instance.empty + let inst = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry _ -> Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) @@ -606,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) else Polymorphic_ind_entry uctx else - Monomorphic_ind_entry uctx + Monomorphic_ind_entry (Univ.ContextSet.of_context uctx) in (* Build the mutual inductive entry *) let mind_ent = diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c728c2671..e4ca98749 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,10 +109,10 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let univs = Evd.to_universe_context ctx in let univs = - if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs - else Monomorphic_const_entry univs + if Flags.is_universe_polymorphism () + then Polymorphic_const_entry (Evd.to_universe_context ctx) + else Monomorphic_const_entry (Evd.universe_context_set ctx) in let kn = f id (DefinitionEntry diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 71d80c4db..f59b5fcae 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -242,7 +242,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Global -> false | Discharge -> assert false in - let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in + let ctx = if p + then Polymorphic_const_entry ctx + else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in + let decl = (ParameterEntry (None,(t_i,ctx),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> @@ -491,9 +495,12 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = UState.context (fst universes) in + let ctx = if pi2 k (* polymorphic *) + then Polymorphic_const_entry (UState.context (fst universes)) + else Monomorphic_const_entry (UState.context_set (fst universes)) + in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) + Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> let pftree = Proof_global.give_me_the_proof () in let id, k, typ = Pfedit.current_proof_statement () in @@ -516,8 +523,12 @@ let save_proof ?proof = function let evd = Evd.from_ctx universes in let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in + let ctx = if poly + then Polymorphic_const_entry ctx + else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in let binders = if poly then Some (UState.universe_binders universes) else None in - Admitted(id,k,(sec_vars, poly, (typ, ctx), None), + Admitted(id,k,(sec_vars, (typ, ctx), None), (universes, binders)) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 43af8968f..a9110c76c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -633,12 +633,11 @@ let declare_obligation prg obl body ty uctx = shrink_body body ty else [], body, ty, [||] in let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in let ce = { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = ty; - const_entry_universes = univs; + const_entry_universes = uctx; const_entry_opaque = opaque; const_entry_inline_code = false; const_entry_feedback = None; @@ -647,13 +646,15 @@ let declare_obligation prg obl body ty uctx = let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in - if not opaque then add_hint (Locality.make_section_locality None) prg constant; - definition_message obl.obl_name; - true, { obl with obl_body = - if poly then - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - else - Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) } + if not opaque then add_hint (Locality.make_section_locality None) prg constant; + definition_message obl.obl_name; + let body = match uctx with + | Polymorphic_const_entry uctx -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Monomorphic_const_entry _ -> + Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) + in + true, { obl with obl_body = body } let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind notations obls impls kind reduce hook = @@ -855,7 +856,10 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = UState.context ctx in + let uctx = if pi2 prg.prg_kind + then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) + in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in @@ -967,13 +971,16 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) - in - let uctx = UState.context ctx in - let prg = {prg with prg_ctx = ctx} in - let def, obl' = declare_obligation prg obl t ty uctx in - obls.(i) <- obl'; + solve_by_tac obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) + in + let uctx = if pi2 prg.prg_kind + then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) + in + let prg = {prg with prg_ctx = ctx} in + let def, obl' = declare_obligation prg obl t ty uctx in + obls.(i) <- obl'; if def && not (pi2 prg.prg_kind) then ( (* Declare the term constraints with the first obligation only *) let evd = Evd.from_env (Global.env ()) in @@ -1121,9 +1128,9 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = UState.context prg.prg_ctx in + let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in let kn = Declare.declare_constant x.obl_name ~local:true - (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) + (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } diff --git a/vernac/record.ml b/vernac/record.ml index 0819dadb4..faf277d86 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -270,7 +270,10 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in - let u = Univ.UContext.instance ctx in + let u = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry ctx -> Univ.Instance.empty + in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let indu = indsp, u in let r = mkIndU (indsp,u) in @@ -327,16 +330,12 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let univs = - if poly then Polymorphic_const_entry ctx - else Monomorphic_const_entry ctx - in let entry = { const_entry_body = Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; - const_entry_universes = univs; + const_entry_universes = ctx; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -391,11 +390,14 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in - let poly, ctx = + let template, ctx = match univs with - | Monomorphic_ind_entry ctx -> false, Univ.UContext.empty - | Polymorphic_ind_entry ctx -> true, ctx - | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi) + | Monomorphic_ind_entry ctx -> + template, Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + false, Polymorphic_const_entry ctx + | Cumulative_ind_entry cumi -> + false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) in let binder_name = match name with @@ -405,7 +407,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let mie_ind = { mind_entry_typename = id; mind_entry_arity = arity; - mind_entry_template = not poly && template; + mind_entry_template = template; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in @@ -419,14 +421,13 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t } in let mie = - if poly then - begin + match ctx with + | Polymorphic_const_entry ctx -> let env = Global.env () in let env' = Environ.push_context ctx env in let evd = Evd.from_env env' in Inductiveops.infer_inductive_subtyping env' evd mie - end - else + | Monomorphic_const_entry _ -> mie in let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in @@ -434,6 +435,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in let build = ConstructRef cstr in + let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); rsp @@ -499,7 +501,7 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params else Polymorphic_ind_entry ctx else - Monomorphic_ind_entry ctx + Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) in let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields @@ -626,7 +628,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf else Polymorphic_ind_entry ctx else - Monomorphic_ind_entry ctx + Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) in let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs -- cgit v1.2.3