From 9f6e238fac96a123e7cb2bb2b2caec104bc4b916 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 18 Aug 2019 19:46:50 +0200 Subject: Declare universes for variables outside of Declare.declare_variable (letins still declare universes in declare_variable as they use entries) The section check_same_poly is moved to declare_universe_context (it makes more sense there, universe polymorphism doesn't apply to the variables/letins themselves) --- tactics/declare.ml | 12 +++++------- tactics/declare.mli | 2 +- vernac/comAssumption.ml | 3 ++- vernac/lemmas.ml | 3 ++- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/tactics/declare.ml b/tactics/declare.ml index e418240d3a..3ec6f884be 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -302,7 +302,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry - | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } + | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; } (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) @@ -315,11 +315,10 @@ let declare_variable ~name ~kind d = if Decls.variable_exists name then raise (AlreadyDeclared (None, name)); - let impl,opaque,poly = match d with (* Fails if not well-typed *) - | SectionLocalAssum {typ;univs;poly;impl} -> - let () = declare_universe_context ~poly univs in + let impl,opaque = match d with (* Fails if not well-typed *) + | SectionLocalAssum {typ;impl} -> let () = Global.push_named_assum (name,typ) in - impl, true, poly + impl, true | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) @@ -342,8 +341,7 @@ let declare_variable ~name ~kind d = secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (name, se) in - Glob_term.Explicit, de.proof_entry_opaque, - poly + Glob_term.Explicit, de.proof_entry_opaque in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); Decls.(add_variable_data name {opaque;kind}); diff --git a/tactics/declare.mli b/tactics/declare.mli index 4cb876cecb..d479b75a28 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -36,7 +36,7 @@ type 'a proof_entry = { type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } + | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; } type 'a constant_entry = | DefinitionEntry of 'a proof_entry diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e3f90ab98c..f6debd8777 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -50,7 +50,8 @@ match scope with | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs in let kind = Decls.IsAssumption kind in - let decl = SectionLocalAssum {typ; univs; poly; impl} in + let () = Declare.declare_universe_context ~poly univs in + let decl = SectionLocalAssum {typ; impl} in let () = declare_variable ~name ~kind decl in let () = assumption_message name in let r = GlobRef.VarRef name in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 42d1a1f3fc..b4875bbdd2 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -265,7 +265,8 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect Univ.ContextSet.of_context univs | Monomorphic_entry univs -> univs in - let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in + let () = Declare.declare_universe_context ~poly univs in + let c = Declare.SectionLocalAssum {typ=t_i; impl} in let () = Declare.declare_variable ~name ~kind c in GlobRef.VarRef name, impargs | Global local -> -- cgit v1.2.3 From 5685e37442e49ce77831a371c471716c3ccb0a2b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 18 Aug 2019 21:18:18 +0200 Subject: Move do_primitive from comassumption to its own module. Primitives don't have anything to do with assumptions. --- vernac/comAssumption.ml | 27 --------------------------- vernac/comAssumption.mli | 2 -- vernac/comPrimitive.ml | 37 +++++++++++++++++++++++++++++++++++++ vernac/comPrimitive.mli | 11 +++++++++++ vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 2 +- 6 files changed, 50 insertions(+), 30 deletions(-) create mode 100644 vernac/comPrimitive.ml create mode 100644 vernac/comPrimitive.mli diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index f6debd8777..a56cf9ab9a 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -190,33 +190,6 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = in () -let do_primitive id prim typopt = - if Lib.sections_are_opened () then - CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections."); - if Dumpglob.dump () then Dumpglob.dump_definition id false "ax"; - let env = Global.env () in - let evd = Evd.from_env env in - let evd, typopt = Option.fold_left_map - (interp_type_evars_impls ~impls:empty_internalization_env env) - evd typopt - in - let evd = Evd.minimize_universes evd in - let uvars, impls, typopt = match typopt with - | None -> Univ.LSet.empty, [], None - | Some (ty,impls) -> - EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) - in - let evd = Evd.restrict_universe_context evd uvars in - let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in - let entry = { prim_entry_type = typopt; - prim_entry_univs = uctx; - prim_entry_content = prim; - } - in - let _kn : Names.Constant.t = - declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (PrimitiveEntry entry) in - Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") - let named_of_rel_context l = let open EConstr.Vars in let open RelDecl in diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 2715bd8305..44db47e1cc 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -47,5 +47,3 @@ val context : poly:bool -> local_binder_expr list -> unit - -val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml new file mode 100644 index 0000000000..06fafddafb --- /dev/null +++ b/vernac/comPrimitive.ml @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Univ.LSet.empty, [], None + | Some (ty,impls) -> + EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) + in + let evd = Evd.restrict_universe_context evd uvars in + let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in + let entry = Entries.{ + prim_entry_type = typopt; + prim_entry_univs = uctx; + prim_entry_content = prim; + } + in + let _kn : Names.Constant.t = + Declare.declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry) in + Flags.if_verbose Feedback.msg_info Pp.(Names.Id.print id.CAst.v ++ str " is declared") diff --git a/vernac/comPrimitive.mli b/vernac/comPrimitive.mli new file mode 100644 index 0000000000..c0db1cc464 --- /dev/null +++ b/vernac/comPrimitive.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* CPrimitives.op_or_type -> Constrexpr.constr_expr option -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 4868182bb3..d9d993f5b5 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -26,6 +26,7 @@ Indschemes Obligations ComDefinition Classes +ComPrimitive ComAssumption ComInductive ComFixpoint diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bc47ad8699..87abb9da59 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2607,7 +2607,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacPrimitive (id, prim, typopt) -> VtDefault(fun () -> unsupported_attributes atts; - ComAssumption.do_primitive id prim typopt) + ComPrimitive.do_primitive id prim typopt) | VernacComments l -> VtDefault(fun () -> unsupported_attributes atts; -- cgit v1.2.3 From 2cdccb3f050b68fdfa36ab1ac444b7507564cb77 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 19 Aug 2019 16:15:40 +0200 Subject: Cleanup ComAssumption The general idea is to move tests on scope=Discharge and on Lib.sections_are_opened up in the call stack. This allows better control over the universe manipulation. There are some corner case behaviour change, eg: - [Context (foo:=bla)] outside a section correctly declares an axiom (fix #10668) - (not observable) universes for [Variable A B : Type] in section are declared only once - universes and universe names for [Axiom A B : Type] are declared only once. This changes the qualification of the universe name: before it was the last axiom (so [B.u0]), now it's the first one ([A.u0]). Probably nobody cares about this. - context outside section uses different [kind] I'm not sure why context outside a section behaves differently based on whether we're in a module type, I tried to preserve it but maybe we should uniformize. The universe manipulation for Axiom (in the declare_assumptions function) is a bit awkward, maybe when there are multiple monomorphic axioms instead of trying to attach the universes to the first one we should just declare them separately like with Context. OTOH unlike with context dropping the universe names seems incorrect. --- vernac/comAssumption.ml | 258 +++++++++++++++++++++++++---------------------- vernac/comAssumption.mli | 37 +++++-- 2 files changed, 166 insertions(+), 129 deletions(-) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a56cf9ab9a..42c6250919 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -11,7 +11,6 @@ open CErrors open Util open Vars -open Declare open Names open Context open Constrexpr_ops @@ -41,28 +40,20 @@ let should_axiom_into_instance = let open Decls in function true | Definitional | Logical | Conjectural -> !axiom_into_instance -let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=name} = -let open DeclareDef in -match scope with -| Discharge -> - let univs = match univs with - | Monomorphic_entry univs -> univs - | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs - in +let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let kind = Decls.IsAssumption kind in - let () = Declare.declare_universe_context ~poly univs in - let decl = SectionLocalAssum {typ; impl} in - let () = declare_variable ~name ~kind decl in - let () = assumption_message name in + let decl = Declare.SectionLocalAssum {typ; impl} in + let () = Declare.declare_variable ~name ~kind decl in + let () = Declare.assumption_message name in let r = GlobRef.VarRef name in let () = maybe_declare_manual_implicits true r imps in let env = Global.env () in let sigma = Evd.from_env env in let () = Classes.declare_instance env sigma None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in - (r,Univ.Instance.empty) + () -| Global local -> +let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} = let do_instance = should_axiom_into_instance kind in let inl = let open Declaremods in match nl with | NoInline -> None @@ -71,15 +62,18 @@ match scope with in let kind = Decls.IsAssumption kind in let decl = Declare.ParameterEntry (None,(typ,univs),inl) in - let kn = declare_constant ~name ~local ~kind decl in + let kn = Declare.declare_constant ~name ~local ~kind decl in let gr = GlobRef.ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = Declare.declare_univ_binders gr pl in - let () = assumption_message name in + let () = Declare.assumption_message name in let env = Global.env () in let sigma = Evd.from_env env in let () = if do_instance then Classes.declare_instance env sigma None false gr in - let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in + let local = match local with + | Declare.ImportNeedQualified -> true + | Declare.ImportDefaultBehavior -> false + in let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in let inst = match univs with | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs @@ -91,22 +85,45 @@ let interp_assumption ~program_mode sigma env impls c = let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in sigma, (ty, impls) -(* When monomorphic the universe constraints are declared with the first declaration only. *) -let next_uctx = - let empty_uctx = Monomorphic_entry Univ.ContextSet.empty in +(* When monomorphic the universe constraints and universe names are + declared with the first declaration only. *) +let next_univs = + let empty_univs = Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders in function - | Polymorphic_entry _ as uctx -> uctx - | Monomorphic_entry _ -> empty_uctx + | Polymorphic_entry _, _ as univs -> univs + | Monomorphic_entry _, _ -> empty_univs -let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl = - let refs, _ = - List.fold_left (fun (refs,uctx) id -> - let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in - ref::refs, next_uctx uctx) - ([],uctx) idl - in - List.rev refs +let context_set_of_entry = function + | Polymorphic_entry (_,uctx) -> Univ.ContextSet.of_context uctx + | Monomorphic_entry uctx -> uctx +let declare_assumptions ~poly ~scope ~kind univs nl l = + let open DeclareDef in + let () = match scope with + | Discharge -> + (* declare universes separately for variables *) + Declare.declare_universe_context ~poly (context_set_of_entry (fst univs)) + | Global _ -> () + in + let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) -> + (* NB: here univs are ignored when scope=Discharge *) + let typ = replace_vars subst typ in + let univs,subst' = + List.fold_left_map (fun univs id -> + let refu = match scope with + | Discharge -> + declare_variable is_coe ~kind typ imps Glob_term.Explicit id; + GlobRef.VarRef id.CAst.v, Univ.Instance.empty + | Global local -> + declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id + in + next_univs univs, (id.CAst.v, Constr.mkRef refu)) + univs idl + in + subst'@subst, next_univs univs) + ([], univs) l + in + () let maybe_error_many_udecls = function | ({CAst.loc;v=id}, Some _) -> @@ -176,112 +193,113 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = IMO, thus I think we should adapt `prepare_parameter` to handle this case too. *) let sigma = Evd.restrict_universe_context sigma uvars in - let uctx = Evd.check_univ_decl ~poly sigma udecl in + let univs = Evd.check_univ_decl ~poly sigma udecl in let ubinders = Evd.universe_binders sigma in - let _, _ = List.fold_left (fun (subst,uctx) ((is_coe,idl),typ,imps) -> - let typ = replace_vars subst typ in - let refs = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in - let subst' = List.map2 - (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) - idl refs - in - subst'@subst, next_uctx uctx) - ([], uctx) l - in - () + declare_assumptions ~poly ~scope ~kind (univs,ubinders) nl l let named_of_rel_context l = - let open EConstr.Vars in - let open RelDecl in let acc, ctx = List.fold_right (fun decl (subst, ctx) -> - let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in - let d = match decl with - | LocalAssum (_,t) -> id, None, substl subst t - | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in - (EConstr.mkVar id :: subst, d :: ctx)) + let d = RelDecl.(to_tuple (map_constr (EConstr.Vars.substl subst) decl)) in + let id, _, _ as d = on_pi1 (fun annot -> + match binder_name annot with + | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") + | Name id -> id) + d + in + (EConstr.mkVar id :: subst, d :: ctx)) l ([], []) in ctx +let context_insection sigma ~poly ctx = + let uctx = Evd.universe_context_set sigma in + let () = Declare.declare_universe_context ~poly uctx in + let fn = function + | name, None, t, impl -> + let kind = Decls.Context in + declare_variable false ~kind t [] impl (CAst.make name) + | name, Some b, t, impl -> + (* We need to get poly right for check_same_poly *) + let univs = if poly then Polymorphic_entry ([| |], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty + in + let entry = Declare.definition_entry ~univs ~types:t b in + let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge + ~kind:Decls.Definition UnivNames.empty_binders entry [] + in + () + in + List.iter fn ctx + +let context_nosection sigma ~poly ctx = + let univs = + match ctx, poly with + | [_], _ | _, true -> Evd.univ_entry ~poly sigma + | _, false -> + (* Multiple monomorphic axioms: declare universes separately to + avoid redeclaring them. *) + let uctx = Evd.universe_context_set sigma in + let () = Declare.declare_universe_context ~poly uctx in + Monomorphic_entry Univ.ContextSet.empty + in + let fn (name,b,t,_impl) = + let kind = Decls.(IsAssumption Logical) in + let decl = match b with + | None -> + Declare.ParameterEntry (None,(t,univs),None) + | Some b -> + let entry = Declare.definition_entry ~univs ~types:t b in + Declare.DefinitionEntry entry + in + (* let local = Declare.ImportNeedQualified in *) + let cst = Declare.declare_constant ~name ~kind ~local:Declare.ImportNeedQualified decl in + let () = Declare.assumption_message name in + let env = Global.env () in + (* why local when is_modtype? *) + let () = if Lib.is_modtype() || Option.is_empty b then + Classes.declare_instance env sigma None (Lib.is_modtype()) (GlobRef.ConstRef cst) + in + () + in + List.iter fn ctx + let context ~poly l = let env = Global.env() in let sigma = Evd.from_env env in - let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in + let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in - let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in - let ctx = - try named_of_rel_context fullctx - with e when CErrors.noncritical e -> - user_err Pp.(str "Anonymous variables not allowed in contexts.") - in - let univs = - match ctx with - | [] -> assert false - | [_] -> Evd.univ_entry ~poly sigma - | _::_::_ -> - if Lib.sections_are_opened () - then - (* More than 1 variable in a section: we can't associate - universes to any specific variable so we declare them - separately. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context ~poly uctx; - if poly then Polymorphic_entry ([||], Univ.UContext.empty) - else Monomorphic_entry Univ.ContextSet.empty - end - else if poly then - (* Multiple polymorphic axioms: they are all polymorphic the same way. *) - Evd.univ_entry ~poly sigma - else - (* Multiple monomorphic axioms: declare universes separately - to avoid redeclaring them. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context ~poly uctx; - Monomorphic_entry Univ.ContextSet.empty - end - in - let fn (name, b, t) = - let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in - if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - (* Declare the universe context once *) - let kind = Decls.(IsAssumption Logical) in - let decl = match b with - | None -> - Declare.ParameterEntry (None,(t,univs),None) - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - Declare.DefinitionEntry entry - in - let cst = Declare.declare_constant ~name ~kind decl in - let env = Global.env () in - Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst); - () - else + let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in + let ctx = named_of_rel_context ctx in + (* reorder, evar-normalize and add implicit status *) + let ctx = List.rev_map (fun (name,b,t) -> + let b = Option.map (EConstr.to_constr sigma) b in + let t = EConstr.to_constr sigma t in let test x = match x.CAst.v with | Some (Name id',_) -> Id.equal name id' | _ -> false in - let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in - let scope = - if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in - match b with - | None -> - let _, _ = - declare_assumption false ~scope ~poly ~kind:Decls.Context t - univs UnivNames.empty_binders [] impl - Declaremods.NoInline (CAst.make name) - in - () - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - let _gr = DeclareDef.declare_definition - ~name ~scope:DeclareDef.Discharge - ~kind:Decls.Definition UnivNames.empty_binders entry [] in - () + let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in + name,b,t,impl) + ctx in - List.iter fn (List.rev ctx) + if Lib.sections_are_opened () + then context_insection sigma ~poly ctx + else context_nosection sigma ~poly ctx + +(* Deprecated *) +let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl name = +let open DeclareDef in +match scope with +| Discharge -> + let univs = match univs with + | Monomorphic_entry univs -> univs + | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs + in + let () = Declare.declare_universe_context ~poly univs in + declare_variable is_coe ~kind typ imps impl name; + GlobRef.VarRef name.CAst.v, Univ.Instance.empty +| Global local -> + declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl name diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 44db47e1cc..ae9edefcac 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -23,27 +23,46 @@ val do_assumptions -> (ident_decl list * constr_expr) with_coercion list -> unit -(** returns [false] if the assumption is neither local to a section, - nor in a module type and meant to be instantiated. *) -val declare_assumption +val declare_variable : coercion_flag - -> poly:bool - -> scope:DeclareDef.locality -> kind:Decls.assumption_object_kind -> Constr.types - -> Entries.universes_entry - -> UnivNames.universe_binders -> Impargs.manual_implicits -> Glob_term.binding_kind + -> variable CAst.t + -> unit + +val declare_axiom + : coercion_flag + -> poly:bool + -> local:Declare.import_status + -> kind:Decls.assumption_object_kind + -> Constr.types + -> Entries.universes_entry * UnivNames.universe_binders + -> Impargs.manual_implicits -> Declaremods.inline -> variable CAst.t -> GlobRef.t * Univ.Instance.t (** Context command *) -(** returns [false] if, for lack of section, it declares an assumption - (unless in a module type). *) val context : poly:bool -> local_binder_expr list -> unit + +(** Deprecated *) +val declare_assumption + : coercion_flag + -> poly:bool + -> scope:DeclareDef.locality + -> kind:Decls.assumption_object_kind + -> Constr.types + -> Entries.universes_entry + -> UnivNames.universe_binders + -> Impargs.manual_implicits + -> Glob_term.binding_kind + -> Declaremods.inline + -> variable CAst.t + -> GlobRef.t * Univ.Instance.t +[@@ocaml.deprecated "Use declare_variable or declare_axiom instead."] -- cgit v1.2.3 From d7f11221f797e501fe3bcdb06fe7ef3f559869c3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 19 Aug 2019 16:46:20 +0200 Subject: Fix #10669 incorrect substitution in context outside section --- test-suite/bugs/closed/bug_10669.v | 12 ++++++ test-suite/output/UnivBinders.out | 4 +- vernac/comAssumption.ml | 76 +++++++++++++++++++------------------- 3 files changed, 52 insertions(+), 40 deletions(-) create mode 100644 test-suite/bugs/closed/bug_10669.v diff --git a/test-suite/bugs/closed/bug_10669.v b/test-suite/bugs/closed/bug_10669.v new file mode 100644 index 0000000000..433e300acb --- /dev/null +++ b/test-suite/bugs/closed/bug_10669.v @@ -0,0 +1,12 @@ + +Context (A0:Type) (B0:A0). +Definition foo0 := B0. + +Set Universe Polymorphism. +Context (A1:Type) (B1:A1). +Definition foo1 := B1. + +Section S. + Context (A2:Type) (B2:A2). + Definition foo2 := B2. +End S. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index a89fd64999..d13ea707bb 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -157,12 +157,12 @@ Type@{UnivBinders.58} -> Type@{i} axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axbar -axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i} +axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo' -axbar' : Type@{axbar'.u0} -> Type@{axbar'.i} +axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 42c6250919..8cf5e3a8b4 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -53,6 +53,10 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in () +let instance_of_univ_entry = function + | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs + | Monomorphic_entry _ -> Univ.Instance.empty + let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} = let do_instance = should_axiom_into_instance kind in let inl = let open Declaremods in match nl with @@ -75,10 +79,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name | Declare.ImportDefaultBehavior -> false in let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in - let inst = match univs with - | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs - | Monomorphic_entry _ -> Univ.Instance.empty - in + let inst = instance_of_univ_entry univs in (gr,inst) let interp_assumption ~program_mode sigma env impls c = @@ -197,40 +198,33 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = let ubinders = Evd.universe_binders sigma in declare_assumptions ~poly ~scope ~kind (univs,ubinders) nl l -let named_of_rel_context l = - let acc, ctx = - List.fold_right - (fun decl (subst, ctx) -> - let d = RelDecl.(to_tuple (map_constr (EConstr.Vars.substl subst) decl)) in - let id, _, _ as d = on_pi1 (fun annot -> - match binder_name annot with - | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") - | Name id -> id) - d - in - (EConstr.mkVar id :: subst, d :: ctx)) - l ([], []) - in ctx +let context_subst subst (name,b,t,impl) = + name, Option.map (Vars.substl subst) b, Vars.substl subst t, impl let context_insection sigma ~poly ctx = let uctx = Evd.universe_context_set sigma in let () = Declare.declare_universe_context ~poly uctx in - let fn = function - | name, None, t, impl -> - let kind = Decls.Context in - declare_variable false ~kind t [] impl (CAst.make name) - | name, Some b, t, impl -> - (* We need to get poly right for check_same_poly *) - let univs = if poly then Polymorphic_entry ([| |], Univ.UContext.empty) - else Monomorphic_entry Univ.ContextSet.empty - in - let entry = Declare.definition_entry ~univs ~types:t b in - let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.Definition UnivNames.empty_binders entry [] - in - () + let fn subst (name,_,_,_ as d) = + let d = context_subst subst d in + let () = match d with + | name, None, t, impl -> + let kind = Decls.Context in + declare_variable false ~kind t [] impl (CAst.make name) + | name, Some b, t, impl -> + (* We need to get poly right for check_same_poly *) + let univs = if poly then Polymorphic_entry ([| |], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty + in + let entry = Declare.definition_entry ~univs ~types:t b in + let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge + ~kind:Decls.Definition UnivNames.empty_binders entry [] + in + () + in + Constr.mkVar name :: subst in - List.iter fn ctx + let _ : Vars.substl = List.fold_left fn [] ctx in + () let context_nosection sigma ~poly ctx = let univs = @@ -243,7 +237,8 @@ let context_nosection sigma ~poly ctx = let () = Declare.declare_universe_context ~poly uctx in Monomorphic_entry Univ.ContextSet.empty in - let fn (name,b,t,_impl) = + let fn subst d = + let (name,b,t,_impl) = context_subst subst d in let kind = Decls.(IsAssumption Logical) in let decl = match b with | None -> @@ -260,9 +255,10 @@ let context_nosection sigma ~poly ctx = let () = if Lib.is_modtype() || Option.is_empty b then Classes.declare_instance env sigma None (Lib.is_modtype()) (GlobRef.ConstRef cst) in - () + Constr.mkConstU (cst,instance_of_univ_entry univs) :: subst in - List.iter fn ctx + let _ : Vars.substl = List.fold_left fn [] ctx in + () let context ~poly l = let env = Global.env() in @@ -272,9 +268,13 @@ let context ~poly l = let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in - let ctx = named_of_rel_context ctx in (* reorder, evar-normalize and add implicit status *) - let ctx = List.rev_map (fun (name,b,t) -> + let ctx = List.rev_map (fun d -> + let {binder_name=name}, b, t = RelDecl.to_tuple d in + let name = match name with + | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") + | Name id -> id + in let b = Option.map (EConstr.to_constr sigma) b in let t = EConstr.to_constr sigma t in let test x = match x.CAst.v with -- cgit v1.2.3 From 8398ec48072b0bbe5e571a8d1f1f6c1ace9270f4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 5 Oct 2019 12:16:34 +0200 Subject: Remove "is_polymorphic_univ" checks in upper layers. There were 2: - when declaring a constraint to avoid monomorphic constraint referring to polymorphic univs, this check is redundant with the check in Section.ml - when declaring a universe context to avoid redeclaring universes, this is not necessary after recent commits. --- kernel/section.mli | 2 -- library/lib.ml | 3 --- library/lib.mli | 2 -- tactics/declare.ml | 30 +++++------------------------- 4 files changed, 5 insertions(+), 32 deletions(-) diff --git a/kernel/section.mli b/kernel/section.mli index fc3ac141e4..56b4d9ba8f 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -83,5 +83,3 @@ val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list (** Section segments of all declarations from this section. *) val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool - -val is_polymorphic_univ : Level.t -> 'a t -> bool diff --git a/library/lib.ml b/library/lib.ml index 991e23eb3a..0d9efe2d5d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -425,9 +425,6 @@ let extract_worklist info = let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () -let is_polymorphic_univ u = - Section.is_polymorphic_univ u (sections ()) - let replacement_context () = Section.replacement_context (Global.env ()) (sections ()) diff --git a/library/lib.mli b/library/lib.mli index d3315b0f2e..59d77480e9 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -183,8 +183,6 @@ val is_in_section : GlobRef.t -> bool val replacement_context : unit -> Opaqueproof.work_list -val is_polymorphic_univ : Univ.Level.t -> bool - (** {6 Discharge: decrease the section level if in the current section } *) (* XXX Why can't we use the kernel functions ? *) diff --git a/tactics/declare.ml b/tactics/declare.ml index 3ec6f884be..32447f31c1 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -52,11 +52,7 @@ let name_instance inst = let declare_universe_context ~poly ctx = if poly then - (* FIXME: some upper layers declare universes several times, we hack around - by checking whether the universes already exist. *) - let (univs, cstr) = ctx in - let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in - let uctx = Univ.ContextSet.to_context (univs, cstr) in + let uctx = Univ.ContextSet.to_context ctx in let nas = name_instance (Univ.UContext.instance uctx) in Global.push_section_context (nas, uctx) else @@ -606,28 +602,12 @@ let do_universe ~poly l = let do_constraint ~poly l = let open Univ in let u_of_id x = - let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Lib.is_polymorphic_univ level, level - in - let in_section = Lib.sections_are_opened () in - let () = - if poly && not in_section then - CErrors.user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic constraints outside sections") - in - let check_poly p p' = - if poly then () - else if p || p' then - CErrors.user_err ~hdr:"Constraint" - (str "Cannot declare a global constraint on " ++ - str "a polymorphic universe, use " - ++ str "Polymorphic Constraint instead") + Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in let constraints = List.fold_left (fun acc (l, d, r) -> - let p, lu = u_of_id l and p', ru = u_of_id r in - check_poly p p'; - Constraint.add (lu, d, ru) acc) - Constraint.empty l + let lu = u_of_id l and ru = u_of_id r in + Constraint.add (lu, d, ru) acc) + Constraint.empty l in let uctx = ContextSet.add_constraints constraints ContextSet.empty in declare_universe_context ~poly uctx -- cgit v1.2.3