From 2720db38d74e3e8d26077ad03d79221f0734465c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Jun 2019 00:16:10 +0200 Subject: Move Declare to tactics folder. Nobody really knows where this module should belong, it seems. My personal theory is that it should live in vernac instead, but due to nasty interactions with abstract-like tactics, we have to put it somewhere below. --- interp/declare.ml | 609 -------------------------------------------------- interp/declare.mli | 93 -------- interp/interp.mllib | 1 - tactics/declare.ml | 609 ++++++++++++++++++++++++++++++++++++++++++++++++++ tactics/declare.mli | 93 ++++++++ tactics/tactics.mllib | 1 + 6 files changed, 703 insertions(+), 703 deletions(-) delete mode 100644 interp/declare.ml delete mode 100644 interp/declare.mli create mode 100644 tactics/declare.ml create mode 100644 tactics/declare.mli diff --git a/interp/declare.ml b/interp/declare.ml deleted file mode 100644 index 77313a54de..0000000000 --- a/interp/declare.ml +++ /dev/null @@ -1,609 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* () - | ImportDefaultBehavior -> - let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con) - -let exists_name id = - variable_exists id || Global.exists_objlabel (Label.of_id id) - -let check_exists id = - if exists_name id then alreadydeclared (Id.print id ++ str " already exists") - -let cache_constant ((sp,kn), obj) = - (* Invariant: the constant must exist in the logical environment, except when - redefining it when exiting a section. See [discharge_constant]. *) - let id = basename sp in - let kn' = - match obj.cst_decl with - | None -> - if Global.exists_objlabel (Label.of_id (basename sp)) - then Constant.make1 kn - else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".") - | Some r -> - Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r - in - assert (Constant.equal kn' (Constant.make1 kn)); - Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); - let cst = Global.lookup_constant kn' in - add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - add_constant_kind (Constant.make1 kn) obj.cst_kind - -let discharge_constant ((sp, kn), obj) = - let con = Constant.make1 kn in - let from = Global.lookup_constant con in - let info = cooking_info (section_segment_of_constant con) in - (* This is a hack: when leaving a section, we lose the constant definition, so - we have to store it in the libobject to be able to retrieve it after. *) - Some { obj with cst_decl = Some { from; info } } - -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant cst = { - cst_decl = None; - cst_kind = cst.cst_kind; - cst_locl = cst.cst_locl; -} - -let classify_constant cst = Substitute (dummy_constant cst) - -let (inConstant : constant_obj -> obj) = - declare_object { (default_object "CONSTANT") with - cache_function = cache_constant; - load_function = load_constant; - open_function = open_constant; - classify_function = classify_constant; - subst_function = ident_subst_function; - discharge_function = discharge_constant } - -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f - -let update_tables c = - declare_constant_implicits c; - Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) - -let register_constant kn kind local = - let o = inConstant { - cst_decl = None; - cst_kind = kind; - cst_locl = local; - } in - let id = Label.to_id (Constant.label kn) in - let _ = add_leaf id o in - update_tables kn - -let register_side_effect (c, role) = - let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in - match role with - | None -> () - | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] - -let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); - const_entry_secctx = None; - const_entry_type = types; - const_entry_universes = univs; - const_entry_opaque = opaque; - const_entry_feedback = None; - const_entry_inline_code = inline} - -let get_roles export eff = - let map c = - let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in - (c, role) - in - List.map map export - -let define_constant ~side_effect ?(export_seff=false) id cd = - (* Logically define the constant and its subproofs, no libobject tampering *) - let is_poly de = match de.const_entry_universes with - | Monomorphic_entry _ -> false - | Polymorphic_entry _ -> true - in - let in_section = Lib.sections_are_opened () in - let export, decl = (* We deal with side effects *) - match cd with - | DefinitionEntry de when - export_seff || - not de.const_entry_opaque || - is_poly de -> - (* This globally defines the side-effects in the environment. *) - let body, eff = Future.force de.const_entry_body in - let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in - let export = get_roles export eff in - let de = { de with const_entry_body = Future.from_val (body, ()) } in - export, ConstantEntry (PureEntry, DefinitionEntry de) - | DefinitionEntry de -> - let map (body, eff) = body, eff.Evd.seff_private in - let body = Future.chain de.const_entry_body map in - let de = { de with const_entry_body = body } in - [], ConstantEntry (EffectEntry, DefinitionEntry de) - | ParameterEntry _ | PrimitiveEntry _ as cd -> - [], ConstantEntry (PureEntry, cd) - in - let kn, eff = Global.add_constant ~side_effect ~in_section id decl in - kn, eff, export - -let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) = - let () = check_exists id in - let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in - (* Register the libobjects attached to the constants and its subproofs *) - let () = List.iter register_side_effect export in - let () = register_constant kn kind local in - kn - -let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = - let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in - let () = assert (List.is_empty export) in - let () = register_constant kn kind local in - let seff_roles = match role with - | None -> Cmap.empty - | Some r -> Cmap.singleton kn r - in - let eff = { Evd.seff_private = eff; Evd.seff_roles; } in - kn, eff - -let declare_definition ?(internal=UserIndividualRequest) - ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) - id ?types (body,univs) = - let cb = - definition_entry ?types ~univs ~opaque body - in - declare_constant ~internal ~local id - (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) - -(** Declaration of section variables and local definitions *) -type section_variable_entry = - | SectionLocalDef of Evd.side_effects definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) - -type variable_declaration = DirPath.t * section_variable_entry * logical_kind - -let cache_variable ((sp,_),o) = - match o with - | Inl ctx -> Global.push_context_set false ctx - | Inr (id,(p,d,mk)) -> - (* Constr raisonne sur les noms courts *) - if variable_exists id then - alreadydeclared (Id.print id ++ str " already exists"); - - let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) - | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty,poly),ctx) in - let impl = if impl then Implicit else Explicit in - impl, true, poly, ctx - | SectionLocalDef (de) -> - (* The body should already have been forced upstream because it is a - section-local definition, but it's not enforced by typing *) - let (body, eff) = Future.force de.const_entry_body in - let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in - let eff = get_roles export eff in - let () = List.iter register_side_effect eff in - let poly, univs = match de.const_entry_universes with - | Monomorphic_entry uctx -> false, uctx - | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx - in - let univs = Univ.ContextSet.union uctx univs in - (* We must declare the universe constraints before type-checking the - term. *) - let () = Global.push_context_set (not poly) univs in - let se = { - secdef_body = body; - secdef_secctx = de.const_entry_secctx; - secdef_feedback = de.const_entry_feedback; - secdef_type = de.const_entry_type; - } in - let () = Global.push_named_def (id, se) in - Explicit, de.const_entry_opaque, - poly, univs in - Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl poly ctx; - add_variable_data id (p,opaq,ctx,poly,mk) - -let discharge_variable (_,o) = match o with - | Inr (id,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) - | Inl _ -> Some o - -type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration) union - -let inVariable : variable_obj -> obj = - declare_object { (default_object "VARIABLE") with - cache_function = cache_variable; - discharge_function = discharge_variable; - classify_function = (fun _ -> Dispose) } - -(* for initial declaration *) -let declare_variable id obj = - let oname = add_leaf id (inVariable (Inr (id,obj))) in - declare_var_implicits id; - Notation.declare_ref_arguments_scope Evd.empty (VarRef id); - oname - -(** Declaration of inductive blocks *) -let declare_inductive_argument_scopes kn mie = - List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); - for j=1 to List.length lc do - Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j)); - done) mie.mind_entry_inds - -let inductive_names sp kn mie = - let (dp,_) = repr_path sp in - let kn = Global.mind_of_delta_kn kn in - let names, _ = - List.fold_left - (fun (names, n) ind -> - let ind_p = (kn,n) in - let names, _ = - List.fold_left - (fun (names, p) l -> - let sp = - Libnames.make_path dp l - in - ((sp, ConstructRef (ind_p,p)) :: names, p+1)) - (names, 1) ind.mind_entry_consnames in - let sp = Libnames.make_path dp ind.mind_entry_typename - in - ((sp, IndRef ind_p) :: names, n+1)) - ([], 0) mie.mind_entry_inds - in names - -let load_inductive i ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names - -let open_inductive i ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names - -let cache_inductive ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter check_exists (List.map (fun p -> basename (fst p)) names); - let id = basename sp in - let kn' = Global.add_mind id mie in - assert (MutInd.equal kn' (MutInd.make1 kn)); - let mind = Global.lookup_mind kn' in - add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names - -let discharge_inductive ((sp,kn),mie) = - let mind = Global.mind_of_delta_kn kn in - let mie = Global.lookup_mind mind in - let info = cooking_info (section_segment_of_mutual_inductive mind) in - Some (Cooking.cook_inductive info mie) - -let dummy_one_inductive_entry mie = { - mind_entry_typename = mie.mind_entry_typename; - mind_entry_arity = mkProp; - mind_entry_template = false; - mind_entry_consnames = mie.mind_entry_consnames; - mind_entry_lc = [] -} - -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry m = { - mind_entry_params = []; - mind_entry_record = None; - mind_entry_finite = Declarations.BiFinite; - mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = default_univ_entry; - mind_entry_variance = None; - mind_entry_private = None; -} - -(* reinfer subtyping constraints for inductive after section is dischared. *) -let rebuild_inductive mind_ent = - let env = Global.env () in - InferCumulativity.infer_inductive env mind_ent - -let inInductive : mutual_inductive_entry -> obj = - declare_object {(default_object "INDUCTIVE") with - cache_function = cache_inductive; - load_function = load_inductive; - open_function = open_inductive; - classify_function = (fun a -> Substitute (dummy_inductive_entry a)); - subst_function = ident_subst_function; - discharge_function = discharge_inductive; - rebuild_function = rebuild_inductive } - -let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c - -let load_prim _ p = cache_prim p - -let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c - -let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) - -let inPrim : (Projection.Repr.t * Constant.t) -> obj = - declare_object { - (default_object "PRIMPROJS") with - cache_function = cache_prim ; - load_function = load_prim; - subst_function = subst_prim; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_prim } - -let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) - -let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = - let id = Label.to_id label in - let univs, u = match univs with - | Monomorphic_entry _ -> - (* Global constraints already defined through the inductive *) - default_univ_entry, Univ.Instance.empty - | Polymorphic_entry (nas, ctx) -> - Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx - in - let term = Vars.subst_instance_constr u term in - let types = Vars.subst_instance_constr u types in - let entry = definition_entry ~types ~univs term in - let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in - let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - declare_primitive_projection p cst - - -let declare_projections univs mind = - let env = Global.env () in - let mib = Environ.lookup_mind mind env in - match mib.mind_record with - | PrimRecord info -> - let iter_ind i (_, labs, _, _) = - let ind = (mind, i) in - let projs = Inductiveops.compute_projections env ind in - Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs - in - let () = Array.iteri iter_ind info in - true - | FakeRecord -> false - | NotRecord -> false - -(* for initial declaration *) -let declare_mind mie = - let id = match mie.mind_entry_inds with - | ind::_ -> ind.mind_entry_typename - | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in - let (sp,kn as oname) = add_leaf id (inInductive mie) in - let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mie.mind_entry_universes mind in - declare_mib_implicits mind; - declare_inductive_argument_scopes mind mie; - oname, isprim - -(* Declaration messages *) - -let pr_rank i = pr_nth (i+1) - -let fixpoint_message indexes l = - Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "no recursive definition.") - | [id] -> Id.print id ++ str " is recursively defined" ++ - (match indexes with - | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" - | _ -> mt ()) - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are recursively defined" ++ - match indexes with - | Some a -> spc () ++ str "(decreasing respectively on " ++ - prvect_with_sep pr_comma pr_rank a ++ - str " arguments)" - | None -> mt ())) - -let cofixpoint_message l = - Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "No corecursive definition.") - | [id] -> Id.print id ++ str " is corecursively defined" - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are corecursively defined")) - -let recursive_message isfix i l = - (if isfix then fixpoint_message i else cofixpoint_message) l - -let definition_message id = - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") - -let assumption_message id = - (* Changing "assumed" to "declared", "assuming" referring more to - the type of the object than to the name of the object (see - discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") - -(** Monomorphic universes need to survive sections. *) - -let input_universe_context : Univ.ContextSet.t -> Libobject.obj = - declare_object @@ local_object "Monomorphic section universes" - ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) - ~discharge:(fun (_, x) -> Some x) - -let declare_universe_context poly ctx = - if poly then - (Global.push_context_set true ctx; Lib.add_section_context ctx) - else - Lib.add_anonymous_leaf (input_universe_context ctx) - -(** Global universes are not substitutive objects but global objects - bound at the *library* or *module* level. The polymorphic flag is - used to distinguish universes declared in polymorphic sections, which - are discharged and do not remain in scope. *) - -type universe_source = - | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) - | QualifiedUniv of Id.t (* global universe introduced by some global value *) - | UnqualifiedUniv (* other global universe *) - -type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list - -let check_exists sp = - if Nametab.exists_universe sp then - alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") - else () - -let qualify_univ i dp src id = - match src with - | BoundUniv | UnqualifiedUniv -> - i, Libnames.make_path dp id - | QualifiedUniv l -> - let dp = DirPath.repr dp in - Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id - -let do_univ_name ~check i dp src (id,univ) = - let i, sp = qualify_univ i dp src id in - if check then check_exists sp; - Nametab.push_universe i sp univ - -let cache_univ_names ((sp, _), (src, univs)) = - let depth = sections_depth () in - let dp = pop_dirpath_n depth (dirpath sp) in - List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs - -let load_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs - -let open_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs - -let discharge_univ_names = function - | _, (BoundUniv, _) -> None - | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x - -let input_univ_names : universe_name_decl -> Libobject.obj = - declare_object - { (default_object "Global universe name state") with - cache_function = cache_univ_names; - load_function = load_univ_names; - open_function = open_univ_names; - discharge_function = discharge_univ_names; - subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); - classify_function = (fun a -> Substitute a) } - -let declare_univ_binders gr pl = - if Global.is_polymorphic gr then - () - else - let l = match gr with - | ConstRef c -> Label.to_id @@ Constant.label c - | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") - | ConstructRef _ -> - anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on an constructor reference") - in - let univs = Id.Map.fold (fun id univ univs -> - match Univ.Level.name univ with - | None -> assert false (* having Prop/Set/Var as binders is nonsense *) - | Some univ -> (id,univ)::univs) pl [] - in - Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) - -let do_universe poly l = - let in_section = Lib.sections_are_opened () in - let () = - if poly && not in_section then - user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic universes outside sections") - in - let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in - let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) - Univ.LSet.empty l, Univ.Constraint.empty - in - let () = declare_universe_context poly ctx in - let src = if poly then BoundUniv else UnqualifiedUniv in - Lib.add_anonymous_leaf (input_univ_names (src, 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 - 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 - user_err ~hdr:"Constraint" - (str "Cannot declare a global constraint on " ++ - str "a polymorphic universe, use " - ++ str "Polymorphic Constraint instead") - 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 - in - let uctx = ContextSet.add_constraints constraints ContextSet.empty in - declare_universe_context poly uctx diff --git a/interp/declare.mli b/interp/declare.mli deleted file mode 100644 index 0f64235048..0000000000 --- a/interp/declare.mli +++ /dev/null @@ -1,93 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* variable_declaration -> Libobject.object_name - -(** Declaration of global constructions - i.e. Definition/Theorem/Axiom/Parameter/... *) - -type constant_declaration = Evd.side_effects constant_entry * logical_kind - -type internal_flag = - | UserAutomaticRequest - | InternalTacticRequest - | UserIndividualRequest - -(* Default definition entries, transparent with no secctx or proj information *) -val definition_entry : ?fix_exn:Future.fix_exn -> - ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry - -(** [declare_constant id cd] declares a global declaration - (constant/parameter) with name [id] in the current section; it returns - the full path of the declaration - - internal specify if the constant has been created by the kernel or by the - user, and in the former case, if its errors should be silent *) -val declare_constant : - ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t - -val declare_private_constant : - ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects - -val declare_definition : - ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:import_status -> Id.t -> ?types:constr -> - constr Entries.in_universes_entry -> Constant.t - -(** Since transparent constants' side effects are globally declared, we - * need that *) -val set_declare_scheme : - (string -> (inductive * Constant.t) array -> unit) -> unit - -(** [declare_mind me] declares a block of inductive types with - their constructors in the current section; it returns the path of - the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool - -(** Declaration messages *) - -val definition_message : Id.t -> unit -val assumption_message : Id.t -> unit -val fixpoint_message : int array option -> Id.t list -> unit -val cofixpoint_message : Id.t list -> unit -val recursive_message : bool (** true = fixpoint *) -> - int array option -> Id.t list -> unit - -val exists_name : Id.t -> bool - -(** Global universe contexts, names and constraints *) -val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit - -val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit - -val do_universe : polymorphic -> lident list -> unit -val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit diff --git a/interp/interp.mllib b/interp/interp.mllib index 52978a2ab6..33573edcce 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -17,4 +17,3 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Declare diff --git a/tactics/declare.ml b/tactics/declare.ml new file mode 100644 index 0000000000..a5b3c6cb45 --- /dev/null +++ b/tactics/declare.ml @@ -0,0 +1,609 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* () + | ImportDefaultBehavior -> + let con = Global.constant_of_delta_kn kn in + Nametab.push (Nametab.Exactly i) sp (ConstRef con) + +let exists_name id = + variable_exists id || Global.exists_objlabel (Label.of_id id) + +let check_exists id = + if exists_name id then alreadydeclared (Id.print id ++ str " already exists") + +let cache_constant ((sp,kn), obj) = + (* Invariant: the constant must exist in the logical environment, except when + redefining it when exiting a section. See [discharge_constant]. *) + let id = basename sp in + let kn' = + match obj.cst_decl with + | None -> + if Global.exists_objlabel (Label.of_id (basename sp)) + then Constant.make1 kn + else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".") + | Some r -> + Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r + in + assert (Constant.equal kn' (Constant.make1 kn)); + Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); + let cst = Global.lookup_constant kn' in + add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; + add_constant_kind (Constant.make1 kn) obj.cst_kind + +let discharge_constant ((sp, kn), obj) = + let con = Constant.make1 kn in + let from = Global.lookup_constant con in + let info = cooking_info (section_segment_of_constant con) in + (* This is a hack: when leaving a section, we lose the constant definition, so + we have to store it in the libobject to be able to retrieve it after. *) + Some { obj with cst_decl = Some { from; info } } + +(* Hack to reduce the size of .vo: we keep only what load/open needs *) +let dummy_constant cst = { + cst_decl = None; + cst_kind = cst.cst_kind; + cst_locl = cst.cst_locl; +} + +let classify_constant cst = Substitute (dummy_constant cst) + +let (inConstant : constant_obj -> obj) = + declare_object { (default_object "CONSTANT") with + cache_function = cache_constant; + load_function = load_constant; + open_function = open_constant; + classify_function = classify_constant; + subst_function = ident_subst_function; + discharge_function = discharge_constant } + +let declare_scheme = ref (fun _ _ -> assert false) +let set_declare_scheme f = declare_scheme := f + +let update_tables c = + declare_constant_implicits c; + Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) + +let register_constant kn kind local = + let o = inConstant { + cst_decl = None; + cst_kind = kind; + cst_locl = local; + } in + let id = Label.to_id (Constant.label kn) in + let _ = add_leaf id o in + update_tables kn + +let register_side_effect (c, role) = + let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in + match role with + | None -> () + | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] + +let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty +let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = + { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); + const_entry_secctx = None; + const_entry_type = types; + const_entry_universes = univs; + const_entry_opaque = opaque; + const_entry_feedback = None; + const_entry_inline_code = inline} + +let get_roles export eff = + let map c = + let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in + (c, role) + in + List.map map export + +let define_constant ~side_effect ?(export_seff=false) id cd = + (* Logically define the constant and its subproofs, no libobject tampering *) + let is_poly de = match de.const_entry_universes with + | Monomorphic_entry _ -> false + | Polymorphic_entry _ -> true + in + let in_section = Lib.sections_are_opened () in + let export, decl = (* We deal with side effects *) + match cd with + | DefinitionEntry de when + export_seff || + not de.const_entry_opaque || + is_poly de -> + (* This globally defines the side-effects in the environment. *) + let body, eff = Future.force de.const_entry_body in + let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in + let export = get_roles export eff in + let de = { de with const_entry_body = Future.from_val (body, ()) } in + export, ConstantEntry (PureEntry, DefinitionEntry de) + | DefinitionEntry de -> + let map (body, eff) = body, eff.Evd.seff_private in + let body = Future.chain de.const_entry_body map in + let de = { de with const_entry_body = body } in + [], ConstantEntry (EffectEntry, DefinitionEntry de) + | ParameterEntry _ | PrimitiveEntry _ as cd -> + [], ConstantEntry (PureEntry, cd) + in + let kn, eff = Global.add_constant ~side_effect ~in_section id decl in + kn, eff, export + +let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) = + let () = check_exists id in + let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in + (* Register the libobjects attached to the constants and its subproofs *) + let () = List.iter register_side_effect export in + let () = register_constant kn kind local in + kn + +let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = + let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in + let () = assert (List.is_empty export) in + let () = register_constant kn kind local in + let seff_roles = match role with + | None -> Cmap.empty + | Some r -> Cmap.singleton kn r + in + let eff = { Evd.seff_private = eff; Evd.seff_roles; } in + kn, eff + +let declare_definition ?(internal=UserIndividualRequest) + ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) + id ?types (body,univs) = + let cb = + definition_entry ?types ~univs ~opaque body + in + declare_constant ~internal ~local id + (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) + +(** Declaration of section variables and local definitions *) +type section_variable_entry = + | SectionLocalDef of Evd.side_effects definition_entry + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) + +type variable_declaration = DirPath.t * section_variable_entry * logical_kind + +let cache_variable ((sp,_),o) = + match o with + | Inl ctx -> Global.push_context_set false ctx + | Inr (id,(p,d,mk)) -> + (* Constr raisonne sur les noms courts *) + if variable_exists id then + alreadydeclared (Id.print id ++ str " already exists"); + + let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) + | SectionLocalAssum ((ty,ctx),poly,impl) -> + let () = Global.push_named_assum ((id,ty,poly),ctx) in + let impl = if impl then Implicit else Explicit in + impl, true, poly, ctx + | SectionLocalDef (de) -> + (* The body should already have been forced upstream because it is a + section-local definition, but it's not enforced by typing *) + let (body, eff) = Future.force de.const_entry_body in + let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in + let eff = get_roles export eff in + let () = List.iter register_side_effect eff in + let poly, univs = match de.const_entry_universes with + | Monomorphic_entry uctx -> false, uctx + | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx + in + let univs = Univ.ContextSet.union uctx univs in + (* We must declare the universe constraints before type-checking the + term. *) + let () = Global.push_context_set (not poly) univs in + let se = { + secdef_body = body; + secdef_secctx = de.const_entry_secctx; + secdef_feedback = de.const_entry_feedback; + secdef_type = de.const_entry_type; + } in + let () = Global.push_named_def (id, se) in + Explicit, de.const_entry_opaque, + poly, univs in + Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); + add_section_variable id impl poly ctx; + add_variable_data id (p,opaq,ctx,poly,mk) + +let discharge_variable (_,o) = match o with + | Inr (id,_) -> + if variable_polymorphic id then None + else Some (Inl (variable_context id)) + | Inl _ -> Some o + +type variable_obj = + (Univ.ContextSet.t, Id.t * variable_declaration) union + +let inVariable : variable_obj -> obj = + declare_object { (default_object "VARIABLE") with + cache_function = cache_variable; + discharge_function = discharge_variable; + classify_function = (fun _ -> Dispose) } + +(* for initial declaration *) +let declare_variable id obj = + let oname = add_leaf id (inVariable (Inr (id,obj))) in + declare_var_implicits id; + Notation.declare_ref_arguments_scope Evd.empty (VarRef id); + oname + +(** Declaration of inductive blocks *) +let declare_inductive_argument_scopes kn mie = + List.iteri (fun i {mind_entry_consnames=lc} -> + Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); + for j=1 to List.length lc do + Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j)); + done) mie.mind_entry_inds + +let inductive_names sp kn mie = + let (dp,_) = repr_path sp in + let kn = Global.mind_of_delta_kn kn in + let names, _ = + List.fold_left + (fun (names, n) ind -> + let ind_p = (kn,n) in + let names, _ = + List.fold_left + (fun (names, p) l -> + let sp = + Libnames.make_path dp l + in + ((sp, ConstructRef (ind_p,p)) :: names, p+1)) + (names, 1) ind.mind_entry_consnames in + let sp = Libnames.make_path dp ind.mind_entry_typename + in + ((sp, IndRef ind_p) :: names, n+1)) + ([], 0) mie.mind_entry_inds + in names + +let load_inductive i ((sp,kn),mie) = + let names = inductive_names sp kn mie in + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names + +let open_inductive i ((sp,kn),mie) = + let names = inductive_names sp kn mie in + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names + +let cache_inductive ((sp,kn),mie) = + let names = inductive_names sp kn mie in + List.iter check_exists (List.map (fun p -> basename (fst p)) names); + let id = basename sp in + let kn' = Global.add_mind id mie in + assert (MutInd.equal kn' (MutInd.make1 kn)); + let mind = Global.lookup_mind kn' in + add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names + +let discharge_inductive ((sp,kn),mie) = + let mind = Global.mind_of_delta_kn kn in + let mie = Global.lookup_mind mind in + let info = cooking_info (section_segment_of_mutual_inductive mind) in + Some (Cooking.cook_inductive info mie) + +let dummy_one_inductive_entry mie = { + mind_entry_typename = mie.mind_entry_typename; + mind_entry_arity = mkProp; + mind_entry_template = false; + mind_entry_consnames = mie.mind_entry_consnames; + mind_entry_lc = [] +} + +(* Hack to reduce the size of .vo: we keep only what load/open needs *) +let dummy_inductive_entry m = { + mind_entry_params = []; + mind_entry_record = None; + mind_entry_finite = Declarations.BiFinite; + mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; + mind_entry_universes = default_univ_entry; + mind_entry_variance = None; + mind_entry_private = None; +} + +(* reinfer subtyping constraints for inductive after section is dischared. *) +let rebuild_inductive mind_ent = + let env = Global.env () in + InferCumulativity.infer_inductive env mind_ent + +let inInductive : mutual_inductive_entry -> obj = + declare_object {(default_object "INDUCTIVE") with + cache_function = cache_inductive; + load_function = load_inductive; + open_function = open_inductive; + classify_function = (fun a -> Substitute (dummy_inductive_entry a)); + subst_function = ident_subst_function; + discharge_function = discharge_inductive; + rebuild_function = rebuild_inductive } + +let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c + +let load_prim _ p = cache_prim p + +let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c + +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) + +let inPrim : (Projection.Repr.t * Constant.t) -> obj = + declare_object { + (default_object "PRIMPROJS") with + cache_function = cache_prim ; + load_function = load_prim; + subst_function = subst_prim; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_prim } + +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) + +let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = + let id = Label.to_id label in + let univs, u = match univs with + | Monomorphic_entry _ -> + (* Global constraints already defined through the inductive *) + default_univ_entry, Univ.Instance.empty + | Polymorphic_entry (nas, ctx) -> + Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx + in + let term = Vars.subst_instance_constr u term in + let types = Vars.subst_instance_constr u types in + let entry = definition_entry ~types ~univs term in + let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in + declare_primitive_projection p cst + + +let declare_projections univs mind = + let env = Global.env () in + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | PrimRecord info -> + let iter_ind i (_, labs, _, _) = + let ind = (mind, i) in + let projs = Inductiveops.compute_projections env ind in + Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs + in + let () = Array.iteri iter_ind info in + true + | FakeRecord -> false + | NotRecord -> false + +(* for initial declaration *) +let declare_mind mie = + let id = match mie.mind_entry_inds with + | ind::_ -> ind.mind_entry_typename + | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in + let (sp,kn as oname) = add_leaf id (inInductive mie) in + let mind = Global.mind_of_delta_kn kn in + let isprim = declare_projections mie.mind_entry_universes mind in + declare_mib_implicits mind; + declare_inductive_argument_scopes mind mie; + oname, isprim + +(* Declaration messages *) + +let pr_rank i = pr_nth (i+1) + +let fixpoint_message indexes l = + Flags.if_verbose Feedback.msg_info (match l with + | [] -> anomaly (Pp.str "no recursive definition.") + | [id] -> Id.print id ++ str " is recursively defined" ++ + (match indexes with + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) + | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prvect_with_sep pr_comma pr_rank a ++ + str " arguments)" + | None -> mt ())) + +let cofixpoint_message l = + Flags.if_verbose Feedback.msg_info (match l with + | [] -> anomaly (Pp.str "No corecursive definition.") + | [id] -> Id.print id ++ str " is corecursively defined" + | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ + spc () ++ str "are corecursively defined")) + +let recursive_message isfix i l = + (if isfix then fixpoint_message i else cofixpoint_message) l + +let definition_message id = + Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") + +let assumption_message id = + (* Changing "assumed" to "declared", "assuming" referring more to + the type of the object than to the name of the object (see + discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) + Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") + +(** Monomorphic universes need to survive sections. *) + +let input_universe_context : Univ.ContextSet.t -> Libobject.obj = + declare_object @@ local_object "Monomorphic section universes" + ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) + ~discharge:(fun (_, x) -> Some x) + +let declare_universe_context poly ctx = + if poly then + (Global.push_context_set true ctx; Lib.add_section_context ctx) + else + Lib.add_anonymous_leaf (input_universe_context ctx) + +(** Global universes are not substitutive objects but global objects + bound at the *library* or *module* level. The polymorphic flag is + used to distinguish universes declared in polymorphic sections, which + are discharged and do not remain in scope. *) + +type universe_source = + | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) + | QualifiedUniv of Id.t (* global universe introduced by some global value *) + | UnqualifiedUniv (* other global universe *) + +type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list + +let check_exists sp = + if Nametab.exists_universe sp then + alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") + else () + +let qualify_univ i dp src id = + match src with + | BoundUniv | UnqualifiedUniv -> + i, Libnames.make_path dp id + | QualifiedUniv l -> + let dp = DirPath.repr dp in + Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id + +let do_univ_name ~check i dp src (id,univ) = + let i, sp = qualify_univ i dp src id in + if check then check_exists sp; + Nametab.push_universe i sp univ + +let cache_univ_names ((sp, _), (src, univs)) = + let depth = sections_depth () in + let dp = pop_dirpath_n depth (dirpath sp) in + List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs + +let load_univ_names i ((sp, _), (src, univs)) = + List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs + +let open_univ_names i ((sp, _), (src, univs)) = + List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs + +let discharge_univ_names = function + | _, (BoundUniv, _) -> None + | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x + +let input_univ_names : universe_name_decl -> Libobject.obj = + declare_object + { (default_object "Global universe name state") with + cache_function = cache_univ_names; + load_function = load_univ_names; + open_function = open_univ_names; + discharge_function = discharge_univ_names; + subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); + classify_function = (fun a -> Substitute a) } + +let declare_univ_binders gr pl = + if Global.is_polymorphic gr then + () + else + let l = match gr with + | ConstRef c -> Label.to_id @@ Constant.label c + | IndRef (c, _) -> Label.to_id @@ MutInd.label c + | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") + | ConstructRef _ -> + anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on an constructor reference") + in + let univs = Id.Map.fold (fun id univ univs -> + match Univ.Level.name univ with + | None -> assert false (* having Prop/Set/Var as binders is nonsense *) + | Some univ -> (id,univ)::univs) pl [] + in + Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) + +let do_universe poly l = + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err ~hdr:"Constraint" + (str"Cannot declare polymorphic universes outside sections") + in + let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in + let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) + Univ.LSet.empty l, Univ.Constraint.empty + in + let () = declare_universe_context poly ctx in + let src = if poly then BoundUniv else UnqualifiedUniv in + Lib.add_anonymous_leaf (input_univ_names (src, 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 + 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 + user_err ~hdr:"Constraint" + (str "Cannot declare a global constraint on " ++ + str "a polymorphic universe, use " + ++ str "Polymorphic Constraint instead") + 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 + in + let uctx = ContextSet.add_constraints constraints ContextSet.empty in + declare_universe_context poly uctx diff --git a/tactics/declare.mli b/tactics/declare.mli new file mode 100644 index 0000000000..233f0674ec --- /dev/null +++ b/tactics/declare.mli @@ -0,0 +1,93 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* variable_declaration -> Libobject.object_name + +(** Declaration of global constructions + i.e. Definition/Theorem/Axiom/Parameter/... *) + +type constant_declaration = Evd.side_effects constant_entry * logical_kind + +type internal_flag = + | UserAutomaticRequest + | InternalTacticRequest + | UserIndividualRequest + +(* Default definition entries, transparent with no secctx or proj information *) +val definition_entry : ?fix_exn:Future.fix_exn -> + ?opaque:bool -> ?inline:bool -> ?types:types -> + ?univs:Entries.universes_entry -> + ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry + +(** [declare_constant id cd] declares a global declaration + (constant/parameter) with name [id] in the current section; it returns + the full path of the declaration + + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent *) +val declare_constant : + ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t + +val declare_private_constant : + ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects + +val declare_definition : + ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> + ?local:import_status -> Id.t -> ?types:constr -> + constr Entries.in_universes_entry -> Constant.t + +(** Since transparent constants' side effects are globally declared, we + * need that *) +val set_declare_scheme : + (string -> (inductive * Constant.t) array -> unit) -> unit + +(** [declare_mind me] declares a block of inductive types with + their constructors in the current section; it returns the path of + the whole block and a boolean indicating if it is a primitive record. *) +val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool + +(** Declaration messages *) + +val definition_message : Id.t -> unit +val assumption_message : Id.t -> unit +val fixpoint_message : int array option -> Id.t list -> unit +val cofixpoint_message : Id.t list -> unit +val recursive_message : bool (** true = fixpoint *) -> + int array option -> Id.t list -> unit + +val exists_name : Id.t -> bool + +(** Global universe contexts, names and constraints *) +val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit + +val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit + +val do_universe : polymorphic -> lident list -> unit +val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 1861c5b99b..6dd749aa0d 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +Declare Dnet Dn Btermdn -- cgit v1.2.3 From f597952e1b216ca5adf9f782c736f4cfe705ef02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 16 Jun 2019 19:09:25 +0200 Subject: Duplicate the type of constant entries in Proof_global. This allows to desynchronize the kernel-facing API from the proof-facing one. --- engine/uState.ml | 4 +- engine/uState.mli | 2 +- plugins/funind/functional_principles_types.ml | 16 ++--- plugins/funind/functional_principles_types.mli | 2 +- plugins/funind/indfun_common.ml | 5 +- plugins/funind/indfun_common.mli | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/invfun.mli | 2 +- plugins/funind/recdef.ml | 1 - plugins/ltac/rewrite.ml | 4 +- proofs/pfedit.ml | 5 +- proofs/pfedit.mli | 2 +- proofs/proof_global.ml | 30 ++++++--- proofs/proof_global.mli | 14 +++- tactics/abstract.ml | 20 +++--- tactics/abstract.mli | 4 +- tactics/declare.ml | 74 ++++++++++++++-------- tactics/declare.mli | 9 ++- tactics/ind_tables.ml | 15 ++--- tactics/leminv.ml | 1 - .../misc/poly-capture-global-univs/src/evilImpl.ml | 4 +- vernac/class.ml | 1 - vernac/classes.ml | 5 +- vernac/comAssumption.ml | 6 +- vernac/comDefinition.ml | 5 +- vernac/comDefinition.mli | 3 +- vernac/comProgramFixpoint.ml | 1 - vernac/declareDef.ml | 3 +- vernac/declareDef.mli | 4 +- vernac/declareObl.ml | 20 +++--- vernac/declareObl.mli | 2 +- vernac/indschemes.ml | 16 ++--- vernac/lemmas.ml | 39 ++++++------ vernac/obligations.ml | 7 +- vernac/record.ml | 17 ++--- 35 files changed, 195 insertions(+), 152 deletions(-) diff --git a/engine/uState.ml b/engine/uState.ml index 6a1282203a..bd61112f08 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -452,9 +452,9 @@ let restrict ctx vars = let uctx' = restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } -let demote_seff_univs entry uctx = +let demote_seff_univs universes uctx = let open Entries in - match entry.const_entry_universes with + match universes with | Polymorphic_entry _ -> uctx | Monomorphic_entry (univs, _) -> let seff = LSet.union uctx.uctx_seff_univs univs in diff --git a/engine/uState.mli b/engine/uState.mli index 204e97eb15..9689f2e961 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -100,7 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t universes are preserved. *) val restrict : t -> Univ.LSet.t -> t -val demote_seff_univs : 'a Entries.definition_entry -> t -> t +val demote_seff_univs : Entries.universes_entry -> t -> t type rigid = | UnivRigid diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 48eac96ab3..d49d657d38 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -19,7 +19,6 @@ open Vars open Namegen open Names open Pp -open Entries open Tactics open Context.Rel.Declaration open Indfun_common @@ -371,7 +370,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) ignore( Declare.declare_constant name - (DefinitionEntry ce, + (Declare.DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; @@ -471,7 +470,7 @@ let get_funs_constant mp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects definition_entry list = +let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -541,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def with Option.IsNone -> (* non recursive definition *) false in - let const = {const with const_entry_opaque = opacity } in + let const = {const with Proof_global.proof_entry_opaque = opacity } in (* The others are just deduced *) if List.is_empty other_princ_types then @@ -552,7 +551,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def let sorts = Array.of_list sorts in List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in + let open Proof_global in + let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = @@ -596,9 +596,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - const_entry_body = + proof_entry_body = (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - const_entry_type = Some scheme_type + proof_entry_type = Some scheme_type } ) other_fun_princ_types @@ -638,7 +638,7 @@ let build_scheme fas = ignore (Declare.declare_constant princ_id - (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 3f70e870ab..b4f6f92f9c 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -34,7 +34,7 @@ val generate_functional_principle : exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*Sorts.family) list -> Evd.side_effects Entries.definition_entry list + (pconstant*Sorts.family) list -> Evd.side_effects Proof_global.proof_entry list val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 732a0d818f..17c79e0e6c 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -118,14 +118,13 @@ let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (* Copy of the standard save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) -open Entries open Decl_kinds open Declare let definition_message = Declare.definition_message let save id const ?hook uctx (locality,_,kind) = - let fix_exn = Future.fix_exn_of const.const_entry_body in + let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in let r = match locality with | Discharge -> let k = Kindops.logical_kind_of_goal_kind kind in @@ -134,7 +133,7 @@ let save id const ?hook uctx (locality,_,kind) = VarRef id | Global local -> let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id ~local (DefinitionEntry const, k) in + let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in ConstRef kn in DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r; diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 8dd990775b..1d096fa488 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -44,7 +44,7 @@ val jmeq_refl : unit -> EConstr.constr val save : Id.t - -> Evd.side_effects Entries.definition_entry + -> Evd.side_effects Proof_global.proof_entry -> ?hook:DeclareDef.Hook.t -> UState.t -> Decl_kinds.goal_kind diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e7e523bb32..2020881c7c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -786,7 +786,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Array.of_list (List.map (fun entry -> - (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type )) + (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type )) ) (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index 8394ac2823..96601785b6 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -15,5 +15,5 @@ val invfun : val derive_correctness : (Evd.evar_map ref -> (Constr.pconstant * Sorts.family) list -> - 'a Entries.definition_entry list) -> + 'a Proof_global.proof_entry list) -> Constr.pconstant list -> Names.inductive list -> unit diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b049e3607c..2647e7449b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -17,7 +17,6 @@ open EConstr open Vars open Namegen open Environ -open Entries open Pp open Names open Libnames diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 4c29d73038..f977ba34d2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1902,7 +1902,7 @@ let declare_projection n instance_id r = Declare.definition_entry ~types:typ ~univs term in ignore(Declare.declare_constant n - (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) + (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in @@ -1979,7 +1979,7 @@ let add_morphism_as_parameter atts m n : unit = let uctx, instance = build_morphism_signature env evd m in let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id - (Entries.ParameterEntry + (Declare.ParameterEntry (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e8164a14a7..cb4eabcc85 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -11,7 +11,6 @@ open Pp open Util open Names -open Entries open Environ open Evd @@ -127,7 +126,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehav let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> - let univs = UState.demote_seff_univs entry universes in + let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in entry, status, univs | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") @@ -141,7 +140,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let gk = Global ImportDefaultBehavior, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in - let body, eff = Future.force ce.const_entry_body in + let body, eff = Future.force ce.Proof_global.proof_entry_body in let (cb, ctx) = if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) else body diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 2d3b66ff9f..d01704926a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -61,7 +61,7 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind -> EConstr.types -> unit Proofview.tactic -> - Evd.side_effects Entries.definition_entry * bool * + Evd.side_effects Proof_global.proof_entry * bool * UState.t val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0b1a7fcc03..4490fbdd64 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -24,9 +24,21 @@ module NamedDecl = Context.Named.Declaration (*** Proof Global Environment ***) +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + type proof_object = { id : Names.Id.t; - entries : Evd.side_effects Entries.definition_entry list; + entries : Evd.side_effects proof_entry list; persistence : Decl_kinds.goal_kind; universes: UState.t; } @@ -231,14 +243,14 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in - {Entries. - const_entry_body = body; - const_entry_secctx = section_vars; - const_entry_feedback = feedback_id; - const_entry_type = Some typ; - const_entry_inline_code = false; - const_entry_opaque = opaque; - const_entry_universes = univs; } + { + proof_entry_body = body; + proof_entry_secctx = section_vars; + proof_entry_feedback = feedback_id; + proof_entry_type = Some typ; + proof_entry_inline_code = false; + proof_entry_opaque = opaque; + proof_entry_universes = univs; } in let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in { id = name; entries = entries; persistence = strength; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 15685bd9b6..4e1aa64e7b 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -31,9 +31,21 @@ val compact_the_proof : t -> t function which takes a [proof_object] together with a [proof_end] (i.e. an proof ending command) and registers the appropriate values. *) +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + type proof_object = { id : Names.Id.t; - entries : Evd.side_effects Entries.definition_entry list; + entries : Evd.side_effects proof_entry list; persistence : Decl_kinds.goal_kind; universes: UState.t; } diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 8f66032873..e4fa5e84b4 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -70,19 +70,19 @@ let rec shrink ctx sign c t accu = | _ -> assert false let shrink_entry sign const = - let open Entries in - let typ = match const.const_entry_type with + let open Proof_global in + let typ = match const.proof_entry_type with | None -> assert false | Some t -> t in (* The body has been forced by the call to [build_constant_by_tactic] *) - let () = assert (Future.is_over const.const_entry_body) in - let ((body, uctx), eff) = Future.force const.const_entry_body in + let () = assert (Future.is_over const.proof_entry_body) in + let ((body, uctx), eff) = Future.force const.proof_entry_body in let (body, typ, ctx) = decompose (List.length sign) body typ [] in let (body, typ, args) = shrink ctx sign body typ [] in let const = { const with - const_entry_body = Future.from_val ((body, uctx), eff); - const_entry_type = Some typ; + proof_entry_body = Future.from_val ((body, uctx), eff); + proof_entry_type = Some typ; } in (const, args) @@ -152,7 +152,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in + let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) @@ -161,20 +161,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl in let cst, eff = Impargs.with_implicit_protection cst () in - let inst = match const.Entries.const_entry_universes with + let inst = match const.Proof_global.proof_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> (* We mimic what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) - let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in + let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in let () = assert (Univ.ContextSet.is_empty body_uctx) in EInstance.make (Univ.UContext.instance ctx) in let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let effs = Evd.concat_side_effects eff - Entries.(snd (Future.force const.const_entry_body)) in + Proof_global.(snd (Future.force const.proof_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> tacK lem args diff --git a/tactics/abstract.mli b/tactics/abstract.mli index c474a01d1c..e278729f89 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P save path *) val shrink_entry : ('a, 'b) Context.Named.Declaration.pt list - -> 'c Entries.definition_entry - -> 'c Entries.definition_entry * Constr.t list + -> 'c Proof_global.proof_entry + -> 'c Proof_global.proof_entry * Constr.t list diff --git a/tactics/declare.ml b/tactics/declare.ml index a5b3c6cb45..81663b9b99 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -42,6 +42,11 @@ type constant_obj = { cst_locl : import_status; } +type 'a constant_entry = + | DefinitionEntry of 'a Proof_global.proof_entry + | ParameterEntry of parameter_entry + | PrimitiveEntry of primitive_entry + type constant_declaration = Evd.side_effects constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) @@ -146,13 +151,26 @@ let register_side_effect (c, role) = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); - const_entry_secctx = None; - const_entry_type = types; - const_entry_universes = univs; - const_entry_opaque = opaque; - const_entry_feedback = None; - const_entry_inline_code = inline} + let open Proof_global in + { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); + proof_entry_secctx = None; + proof_entry_type = types; + proof_entry_universes = univs; + proof_entry_opaque = opaque; + proof_entry_feedback = None; + proof_entry_inline_code = inline} + +let cast_proof_entry e = + let open Proof_global in + { + const_entry_body = e.proof_entry_body; + const_entry_secctx = e.proof_entry_secctx; + const_entry_feedback = e.proof_entry_feedback; + const_entry_type = e.proof_entry_type; + const_entry_universes = e.proof_entry_universes; + const_entry_opaque = e.proof_entry_opaque; + const_entry_inline_code = e.proof_entry_inline_code; + } let get_roles export eff = let map c = @@ -162,8 +180,9 @@ let get_roles export eff = List.map map export let define_constant ~side_effect ?(export_seff=false) id cd = + let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) - let is_poly de = match de.const_entry_universes with + let is_poly de = match de.proof_entry_universes with | Monomorphic_entry _ -> false | Polymorphic_entry _ -> true in @@ -172,21 +191,25 @@ let define_constant ~side_effect ?(export_seff=false) id cd = match cd with | DefinitionEntry de when export_seff || - not de.const_entry_opaque || + not de.proof_entry_opaque || is_poly de -> (* This globally defines the side-effects in the environment. *) - let body, eff = Future.force de.const_entry_body in + let body, eff = Future.force de.proof_entry_body in let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in let export = get_roles export eff in - let de = { de with const_entry_body = Future.from_val (body, ()) } in - export, ConstantEntry (PureEntry, DefinitionEntry de) + let de = { de with proof_entry_body = Future.from_val (body, ()) } in + let de = cast_proof_entry de in + export, ConstantEntry (PureEntry, Entries.DefinitionEntry de) | DefinitionEntry de -> let map (body, eff) = body, eff.Evd.seff_private in - let body = Future.chain de.const_entry_body map in - let de = { de with const_entry_body = body } in - [], ConstantEntry (EffectEntry, DefinitionEntry de) - | ParameterEntry _ | PrimitiveEntry _ as cd -> - [], ConstantEntry (PureEntry, cd) + let body = Future.chain de.proof_entry_body map in + let de = { de with proof_entry_body = body } in + let de = cast_proof_entry de in + [], ConstantEntry (EffectEntry, Entries.DefinitionEntry de) + | ParameterEntry e -> + [], ConstantEntry (PureEntry, Entries.ParameterEntry e) + | PrimitiveEntry e -> + [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e) in let kn, eff = Global.add_constant ~side_effect ~in_section id decl in kn, eff, export @@ -217,11 +240,11 @@ let declare_definition ?(internal=UserIndividualRequest) definition_entry ?types ~univs ~opaque body in declare_constant ~internal ~local id - (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) + (DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of section variables and local definitions *) type section_variable_entry = - | SectionLocalDef of Evd.side_effects definition_entry + | SectionLocalDef of Evd.side_effects Proof_global.proof_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -242,11 +265,12 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let (body, eff) = Future.force de.const_entry_body in + let open Proof_global in + let (body, eff) = Future.force de.proof_entry_body in let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in let eff = get_roles export eff in let () = List.iter register_side_effect eff in - let poly, univs = match de.const_entry_universes with + let poly, univs = match de.proof_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in @@ -256,12 +280,12 @@ let cache_variable ((sp,_),o) = let () = Global.push_context_set (not poly) univs in let se = { secdef_body = body; - secdef_secctx = de.const_entry_secctx; - secdef_feedback = de.const_entry_feedback; - secdef_type = de.const_entry_type; + secdef_secctx = de.proof_entry_secctx; + secdef_feedback = de.proof_entry_feedback; + secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (id, se) in - Explicit, de.const_entry_opaque, + Explicit, de.proof_entry_opaque, poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; diff --git a/tactics/declare.mli b/tactics/declare.mli index 233f0674ec..692eca8dde 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,9 +23,14 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of Evd.side_effects definition_entry + | SectionLocalDef of Evd.side_effects Proof_global.proof_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) +type 'a constant_entry = + | DefinitionEntry of 'a Proof_global.proof_entry + | ParameterEntry of parameter_entry + | PrimitiveEntry of primitive_entry + type variable_declaration = DirPath.t * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> Libobject.object_name @@ -44,7 +49,7 @@ type internal_flag = val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry + ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 9b8ad8191e..8526bdd373 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -23,7 +23,6 @@ open Constr open CErrors open Util open Declare -open Entries open Decl_kinds open Pp @@ -122,15 +121,15 @@ let define internal role id c poly univs = let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in let entry = { - const_entry_body = + Proof_global.proof_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Evd.empty_side_effects); - const_entry_secctx = None; - const_entry_type = None; - const_entry_universes = univs; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; + proof_entry_secctx = None; + proof_entry_type = None; + proof_entry_universes = univs; + proof_entry_opaque = false; + proof_entry_inline_code = false; + proof_entry_feedback = None; } in let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in let () = match internal with diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 61608c577c..d8f4b66d0e 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -22,7 +22,6 @@ open Namegen open Evd open Printer open Reductionops -open Entries open Inductiveops open Tacmach.New open Clenv diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index adabb7a0a0..8447cf10db 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -11,7 +11,7 @@ let evil t f = let te = Declare.definition_entry ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu in - let tc = Declare.declare_constant t (DefinitionEntry te, k) in + let tc = Declare.declare_constant t (Declare.DefinitionEntry te, k) in let tc = mkConst tc in let fe = Declare.definition_entry @@ -19,4 +19,4 @@ let evil t f = ~types:(Term.mkArrowR tc tu) (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1)) in - ignore (Declare.declare_constant f (DefinitionEntry fe, k)) + ignore (Declare.declare_constant f (Declare.DefinitionEntry fe, k)) diff --git a/vernac/class.ml b/vernac/class.ml index 420baf7966..d5c75ed809 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -17,7 +17,6 @@ open Constr open Context open Vars open Termops -open Entries open Environ open Classops open Declare diff --git a/vernac/classes.ml b/vernac/classes.ml index 442f139827..d6a2f2727a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -29,7 +29,6 @@ module NamedDecl = Context.Named.Declaration (*i*) open Decl_kinds -open Entries let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] @@ -324,7 +323,7 @@ let declare_instance_constant info global imps ?hook id decl poly sigma term ter in let uctx = Evd.check_univ_decl ~poly sigma decl in let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in - let cdecl = (DefinitionEntry entry, kind) in + let cdecl = (Declare.DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); @@ -339,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in + (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (ConstRef cst) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 3eb5eacd46..b0297b7c51 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -68,7 +68,7 @@ match local with | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in + let decl = (Declare.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 @@ -273,10 +273,10 @@ let context poly l = (* Declare the universe context once *) let decl = match b with | None -> - (ParameterEntry (None,(t,univs),None), IsAssumption Logical) + (Declare.ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> let entry = Declare.definition_entry ~univs ~types:t b in - (DefinitionEntry entry, IsAssumption Logical) + (Declare.DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in let env = Global.env () in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 853f2c9aa3..b3cc0a4236 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -10,7 +10,6 @@ open Pp open Util -open Entries open Redexpr open Constrintern open Pretyping @@ -86,12 +85,12 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = in if program_mode then let env = Global.env () in - let (c,ctx), sideff = Future.force ce.const_entry_body in + let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in - let typ = match ce.const_entry_type with + let typ = match ce.Proof_global.proof_entry_type with | Some t -> EConstr.of_constr t | None -> Retyping.get_type_of env evd c in diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index af09a83f02..256abed6a1 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Entries open Decl_kinds open Redexpr open Constrexpr @@ -41,5 +40,5 @@ val interp_definition -> red_expr option -> constr_expr -> constr_expr option - -> Evd.side_effects definition_entry * + -> Evd.side_effects Proof_global.proof_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 23c98c97f9..6c1c23eacb 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -13,7 +13,6 @@ open CErrors open Util open Constr open Context -open Entries open Vars open Declare open Names diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 42327d6bdd..a467c22ede 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -10,7 +10,6 @@ open Decl_kinds open Declare -open Entries open Globnames open Impargs @@ -38,7 +37,7 @@ end (* Locality stuff *) let declare_definition ident (local, p, k) ?hook_data ce pl imps = - let fix_exn = Future.fix_exn_of ce.const_entry_body in + let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in let gr = match local with | Discharge -> let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 6f9608f04a..ac4f44608b 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -43,7 +43,7 @@ val declare_definition : Id.t -> definition_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> Evd.side_effects Entries.definition_entry + -> Evd.side_effects Proof_global.proof_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> GlobRef.t @@ -64,7 +64,7 @@ val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Entries.definition_entry + Evd.evar_map * Evd.side_effects Proof_global.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 30aa347692..4936c9838d 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -155,18 +155,18 @@ let declare_obligation prg obl body ty uctx = ((body, Univ.ContextSet.empty), Evd.empty_side_effects) 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 = uctx - ; const_entry_opaque = opaque - ; const_entry_inline_code = false - ; const_entry_feedback = None } + Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body + ; proof_entry_secctx = None + ; proof_entry_type = ty + ; proof_entry_universes = uctx + ; proof_entry_opaque = opaque + ; proof_entry_inline_code = false + ; proof_entry_feedback = None } in (* ppedrot: seems legit to have obligations as local *) let constant = Declare.declare_constant obl.obl_name ~local:ImportNeedQualified - (DefinitionEntry ce, IsProof Property) + (Declare.DefinitionEntry ce, IsProof Property) in if not opaque then add_hint (Locality.make_section_locality None) prg constant; @@ -498,8 +498,8 @@ let obligation_terminator opq entries uctx { name; num; auto } = match entries with | [entry] -> let env = Global.env () in - let ty = entry.Entries.const_entry_type in - let body, eff = Future.force entry.const_entry_body in + let ty = entry.proof_entry_type in + let body, eff = Future.force entry.proof_entry_body in let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 70a4601ac6..f4495181b3 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -78,7 +78,7 @@ type obligation_qed_info = val obligation_terminator : Proof_global.opacity_flag - -> Evd.side_effects Entries.definition_entry list + -> Evd.side_effects Proof_global.proof_entry list -> UState.t -> obligation_qed_info -> unit (** [obligation_terminator] part 2 of saving an obligation *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 80b3df84db..b393f33d5d 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -21,7 +21,6 @@ open CErrors open Util open Names open Declarations -open Entries open Term open Constr open Inductive @@ -104,15 +103,16 @@ let () = let define ~poly id internal sigma c t = let f = declare_constant ~internal in let univs = Evd.univ_entry ~poly sigma in + let open Proof_global in let kn = f id (DefinitionEntry - { const_entry_body = c; - const_entry_secctx = None; - const_entry_type = t; - const_entry_universes = univs; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; + { proof_entry_body = c; + proof_entry_secctx = None; + proof_entry_type = t; + proof_entry_universes = univs; + proof_entry_opaque = false; + proof_entry_inline_code = false; + proof_entry_feedback = None; }, Decl_kinds.IsDefinition Scheme) in definition_message id; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 400e0dfa3e..73403d9417 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -107,8 +107,9 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - { const with const_entry_body = - Future.chain const.const_entry_body + let open Proof_global in + { const with proof_entry_body = + Future.chain const.proof_entry_body (fun ((body, ctx), eff) -> match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> @@ -448,12 +449,12 @@ let save_lemma_admitted ?proof ~(lemma : t) = | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); - let { const_entry_secctx; const_entry_type } = List.hd entries in - if const_entry_type = None then + let { proof_entry_secctx; proof_entry_type } = List.hd entries in + if proof_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); - let typ = Option.get const_entry_type in + let typ = Option.get proof_entry_type in let ctx = UState.univ_entry ~poly:(pi2 k) universes in - let sec_vars = if get_keep_admitted_vars () then const_entry_secctx else None in + let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in finish_admitted id k (sec_vars, (typ, ctx), None) universes hook | None -> let pftree = Proof_global.get_proof lemma.proof in @@ -500,15 +501,15 @@ let finish_proved opaque idopt po hook compute_guard = | Transparent -> false, true | Opaque -> true, false in - assert (is_opaque == const.const_entry_opaque); + assert (is_opaque == const.proof_entry_opaque); let id = match idopt with | None -> id | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + let fix_exn = Future.fix_exn_of const.proof_entry_body in let () = try let const = adjust_guardness_conditions const compute_guard in let k = Kindops.logical_kind_of_goal_kind kind in - let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in + let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in let r = match locality with | Discharge -> let c = SectionLocalDef const in @@ -550,8 +551,8 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Entries.const_entry_opaque = false } in - let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in + let f_def = { f_def with Proof_global.proof_entry_opaque = false } in + let f_def = Declare.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in let f_kn_term = mkConst f_kn in (* In the type and body of the proof of [suchthat] there can be @@ -561,22 +562,22 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = - match Entries.(lemma_def.const_entry_type) with + match Proof_global.(lemma_def.proof_entry_type) with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain Entries.(lemma_def.const_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = let open Entries in + let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = let open Proof_global in { lemma_def with - const_entry_body = lemma_body ; - const_entry_type = Some lemma_type ; - const_entry_opaque = opaque ; } + proof_entry_body = lemma_body ; + proof_entry_type = Some lemma_type ; + proof_entry_opaque = opaque ; } in let lemma_def = - Entries.DefinitionEntry lemma_def , + Declare.DefinitionEntry lemma_def , Decl_kinds.(IsProof Proposition) in ignore (Declare.declare_constant name lemma_def) @@ -597,7 +598,7 @@ let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 = | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) in let entry, args = Abstract.shrink_entry local_context entry in - let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in + let cst = Declare.declare_constant id (Declare.DefinitionEntry entry, kind) in let sigma, app = Evarutil.new_global sigma (ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in sigma, cst) sigma0 diff --git a/vernac/obligations.ml b/vernac/obligations.ml index cd8d22ac9a..aa15718452 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -9,7 +9,6 @@ (************************************************************************) open Printf -open Entries open Decl_kinds (** @@ -418,11 +417,11 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.const_entry_body in + let (body, eff) = Future.force entry.Proof_global.proof_entry_body in let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx') + Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in @@ -682,7 +681,7 @@ let admit_prog prg = let x = subst_deps_obl obls x in let ctx = UState.univ_entry ~poly:false prg.prg_ctx in let kn = Declare.declare_constant x.obl_name ~local:ImportNeedQualified - (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) + (Declare.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 7cc8d9e9b9..9e3353bc54 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -342,16 +342,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try + let open Proof_global in let entry = { - const_entry_body = + proof_entry_body = Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects); - const_entry_secctx = None; - const_entry_type = Some projtyp; - const_entry_universes = ctx; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None } in - let k = (DefinitionEntry entry,IsDefinition kind) in + proof_entry_secctx = None; + proof_entry_type = Some projtyp; + proof_entry_universes = ctx; + proof_entry_opaque = false; + proof_entry_inline_code = false; + proof_entry_feedback = None } in + let k = (Declare.DefinitionEntry entry,IsDefinition kind) in let kn = declare_constant ~internal:InternalTacticRequest fid k in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in -- cgit v1.2.3 From 4ceadecf179e9210eed42ef4847aa5ab8fa28bd6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 19 Jun 2019 21:17:09 +0200 Subject: Take advantage of the change of entry representation to split opacity status. Mere isomorphism for now, but will allow more invariants ultimately. --- kernel/entries.ml | 2 +- kernel/safe_typing.ml | 10 +++++++++- kernel/term_typing.ml | 13 +++++-------- tactics/declare.ml | 11 +++++++---- 4 files changed, 22 insertions(+), 14 deletions(-) diff --git a/kernel/entries.ml b/kernel/entries.ml index de1ce609fd..1a25337512 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -68,7 +68,6 @@ type 'a definition_entry = { const_entry_feedback : Stateid.t option; const_entry_type : types option; const_entry_universes : universes_entry; - const_entry_opaque : bool; const_entry_inline_code : bool } type section_def_entry = { @@ -91,6 +90,7 @@ type primitive_entry = { type 'a constant_entry = | DefinitionEntry of 'a definition_entry + | OpaqueEntry of 'a definition_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a980d22e42..c99edccda7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -688,13 +688,21 @@ let constant_entry_of_side_effect eff = | OpaqueDef b -> b | Def b -> Mod_subst.force_constr b | _ -> assert false in + if Declareops.is_opaque cb then + OpaqueEntry { + const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some cb.const_type; + const_entry_universes = univs; + const_entry_inline_code = cb.const_inline_code } + else DefinitionEntry { const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; - const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } let export_eff eff = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 165feca1b6..e28849c953 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -115,9 +115,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; + | OpaqueEntry ({ const_entry_type = typ; const_entry_universes = Monomorphic_entry univs; _ } as c) -> + let typ = match typ with None -> assert false | Some typ -> typ 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 = Typeops.infer_type env typ in @@ -155,12 +155,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } - (** Similar case for polymorphic entries. TODO: also delay type-checking of - the body. *) + (** Similar case for polymorphic entries. *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; + | OpaqueEntry ({ const_entry_type = typ; const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let typ = match typ with None -> assert false | Some typ -> typ in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let env = push_context ~strict:false uctx env in let tj = Typeops.infer_type env typ in @@ -200,7 +199,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in (* Opaque constants must be provided with a non-empty const_entry_type, and thus should have been treated above. *) - let () = assert (not c.const_entry_opaque) in let body, ctx = match trust with | Pure -> let (body, ctx), () = Future.join body in @@ -375,7 +373,6 @@ let translate_local_def env _id centry = const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; - const_entry_opaque = false; const_entry_inline_code = false; } in let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in diff --git a/tactics/declare.ml b/tactics/declare.ml index 81663b9b99..b35d4a5d66 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -168,7 +168,6 @@ let cast_proof_entry e = const_entry_feedback = e.proof_entry_feedback; const_entry_type = e.proof_entry_type; const_entry_universes = e.proof_entry_universes; - const_entry_opaque = e.proof_entry_opaque; const_entry_inline_code = e.proof_entry_inline_code; } @@ -198,14 +197,18 @@ let define_constant ~side_effect ?(export_seff=false) id cd = let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in - let de = cast_proof_entry de in - export, ConstantEntry (PureEntry, Entries.DefinitionEntry de) + let cd = match de.proof_entry_opaque with + | true -> Entries.OpaqueEntry (cast_proof_entry de) + | false -> Entries.DefinitionEntry (cast_proof_entry de) + in + export, ConstantEntry (PureEntry, cd) | DefinitionEntry de -> + let () = assert (de.proof_entry_opaque) in let map (body, eff) = body, eff.Evd.seff_private in let body = Future.chain de.proof_entry_body map in let de = { de with proof_entry_body = body } in let de = cast_proof_entry de in - [], ConstantEntry (EffectEntry, Entries.DefinitionEntry de) + [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) | ParameterEntry e -> [], ConstantEntry (PureEntry, Entries.ParameterEntry e) | PrimitiveEntry e -> -- cgit v1.2.3 From be3bba54e39a316ded975b7c5ac5723fed41aa88 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 19 Jun 2019 21:24:36 +0200 Subject: Enforce that transparent entries are forced beforehand. --- kernel/entries.ml | 6 +++--- kernel/safe_typing.ml | 2 +- kernel/term_typing.ml | 12 ++++-------- tactics/declare.ml | 16 ++++++++++++++-- 4 files changed, 22 insertions(+), 14 deletions(-) diff --git a/kernel/entries.ml b/kernel/entries.ml index 1a25337512..3f33df3f74 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -61,7 +61,7 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation type 'a definition_entry = { - const_entry_body : 'a const_entry_body; + const_entry_body : 'a; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) @@ -89,8 +89,8 @@ type primitive_entry = { } type 'a constant_entry = - | DefinitionEntry of 'a definition_entry - | OpaqueEntry of 'a definition_entry + | DefinitionEntry of constr Univ.in_universe_context_set definition_entry + | OpaqueEntry of 'a const_entry_body definition_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c99edccda7..ab58321ac7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff = const_entry_inline_code = cb.const_inline_code } else DefinitionEntry { - const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + const_entry_body = (p, Univ.ContextSet.empty); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e28849c953..3b689953c8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -196,13 +196,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in - (* Opaque constants must be provided with a non-empty const_entry_type, - and thus should have been treated above. *) - let body, ctx = match trust with - | Pure -> - let (body, ctx), () = Future.join body in - body, ctx + let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in + let () = match trust with + | Pure -> () | SideEffects _ -> assert false in let env, usubst, univs = match c.const_entry_universes with @@ -366,7 +362,7 @@ let translate_recipe env _kn r = let translate_local_def env _id centry = let open Cooking in - let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in + let body = (centry.secdef_body, Univ.ContextSet.empty) in let centry = { const_entry_body = body; const_entry_secctx = centry.secdef_secctx; diff --git a/tactics/declare.ml b/tactics/declare.ml index b35d4a5d66..2178a7c54c 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -161,6 +161,18 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_inline_code = inline} let cast_proof_entry e = + let open Proof_global in + let (body, ctx), () = Future.force e.proof_entry_body in + { + const_entry_body = (body, ctx); + const_entry_secctx = e.proof_entry_secctx; + const_entry_feedback = e.proof_entry_feedback; + const_entry_type = e.proof_entry_type; + const_entry_universes = e.proof_entry_universes; + const_entry_inline_code = e.proof_entry_inline_code; + } + +let cast_opaque_proof_entry e = let open Proof_global in { const_entry_body = e.proof_entry_body; @@ -198,7 +210,7 @@ let define_constant ~side_effect ?(export_seff=false) id cd = let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = match de.proof_entry_opaque with - | true -> Entries.OpaqueEntry (cast_proof_entry de) + | true -> Entries.OpaqueEntry (cast_opaque_proof_entry de) | false -> Entries.DefinitionEntry (cast_proof_entry de) in export, ConstantEntry (PureEntry, cd) @@ -207,7 +219,7 @@ let define_constant ~side_effect ?(export_seff=false) id cd = let map (body, eff) = body, eff.Evd.seff_private in let body = Future.chain de.proof_entry_body map in let de = { de with proof_entry_body = body } in - let de = cast_proof_entry de in + let de = cast_opaque_proof_entry de in [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) | ParameterEntry e -> [], ConstantEntry (PureEntry, Entries.ParameterEntry e) -- cgit v1.2.3 From bbec0ea51b4dfef1ddb09a2f876323aa1547f643 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Jun 2019 08:14:28 +0200 Subject: Dedicated type for opaque entries in the kernel. Even more invariants can be enforced this way. --- kernel/entries.ml | 12 +++++++++++- kernel/safe_typing.ml | 12 ++++++------ kernel/term_typing.ml | 20 ++++++++++---------- tactics/declare.ml | 12 ++++++------ 4 files changed, 33 insertions(+), 23 deletions(-) diff --git a/kernel/entries.ml b/kernel/entries.ml index 3f33df3f74..62aab7c391 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -77,6 +77,16 @@ type section_def_entry = { secdef_type : types option; } +type 'a opaque_entry = { + opaque_entry_body : 'a; + (* List of section variables *) + opaque_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + opaque_entry_feedback : Stateid.t option; + opaque_entry_type : types option; + opaque_entry_universes : universes_entry; + opaque_entry_inline_code : bool } + type inline = int option (* inlining level, None for no inlining *) type parameter_entry = @@ -90,7 +100,7 @@ type primitive_entry = { type 'a constant_entry = | DefinitionEntry of constr Univ.in_universe_context_set definition_entry - | OpaqueEntry of 'a const_entry_body definition_entry + | OpaqueEntry of 'a const_entry_body opaque_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ab58321ac7..5dac469a40 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -690,12 +690,12 @@ let constant_entry_of_side_effect eff = | _ -> assert false in if Declareops.is_opaque cb then OpaqueEntry { - const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - const_entry_secctx = None; - const_entry_feedback = None; - const_entry_type = Some cb.const_type; - const_entry_universes = univs; - const_entry_inline_code = cb.const_inline_code } + opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + opaque_entry_secctx = None; + opaque_entry_feedback = None; + opaque_entry_type = Some cb.const_type; + opaque_entry_universes = univs; + opaque_entry_inline_code = cb.const_inline_code } else DefinitionEntry { const_entry_body = (p, Univ.ContextSet.empty); diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3b689953c8..2c31a237ce 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -115,11 +115,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. *) - | OpaqueEntry ({ const_entry_type = typ; - const_entry_universes = Monomorphic_entry univs; _ } as c) -> + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> let typ = match typ with None -> assert false | Some typ -> typ in let env = push_context_set ~strict:true univs env in - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in let proofterm = Future.chain body begin fun ((body,uctx),side_eff) -> @@ -151,16 +151,16 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = tyj.utj_val; cook_universes = Monomorphic univs; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = c.opaque_entry_inline_code; + cook_context = c.opaque_entry_secctx; } (** Similar case for polymorphic entries. *) - | OpaqueEntry ({ const_entry_type = typ; - const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> let typ = match typ with None -> assert false | Some typ -> typ in - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let env = push_context ~strict:false uctx env in let tj = Typeops.infer_type env typ in let sbst, auctx = Univ.abstract_universes nas uctx in @@ -189,8 +189,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = typ; cook_universes = Polymorphic auctx; cook_relevance = Sorts.relevance_of_sort tj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = c.opaque_entry_inline_code; + cook_context = c.opaque_entry_secctx; } (** Other definitions have to be processed immediately. *) diff --git a/tactics/declare.ml b/tactics/declare.ml index 2178a7c54c..d4fdff76bf 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -175,12 +175,12 @@ let cast_proof_entry e = let cast_opaque_proof_entry e = let open Proof_global in { - const_entry_body = e.proof_entry_body; - const_entry_secctx = e.proof_entry_secctx; - const_entry_feedback = e.proof_entry_feedback; - const_entry_type = e.proof_entry_type; - const_entry_universes = e.proof_entry_universes; - const_entry_inline_code = e.proof_entry_inline_code; + opaque_entry_body = e.proof_entry_body; + opaque_entry_secctx = e.proof_entry_secctx; + opaque_entry_feedback = e.proof_entry_feedback; + opaque_entry_type = e.proof_entry_type; + opaque_entry_universes = e.proof_entry_universes; + opaque_entry_inline_code = e.proof_entry_inline_code; } let get_roles export eff = -- cgit v1.2.3 From c20eb3a73c4868533bb50555d1979f5b9d821256 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Jun 2019 08:22:28 +0200 Subject: Enforce that opaque entries carry their type. --- kernel/entries.ml | 2 +- kernel/safe_typing.ml | 2 +- kernel/term_typing.ml | 2 -- tactics/declare.ml | 6 +++++- 4 files changed, 7 insertions(+), 5 deletions(-) diff --git a/kernel/entries.ml b/kernel/entries.ml index 62aab7c391..6016510189 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -83,7 +83,7 @@ type 'a opaque_entry = { opaque_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; - opaque_entry_type : types option; + opaque_entry_type : types; opaque_entry_universes : universes_entry; opaque_entry_inline_code : bool } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 5dac469a40..6cb7a22a15 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -693,7 +693,7 @@ let constant_entry_of_side_effect eff = opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); opaque_entry_secctx = None; opaque_entry_feedback = None; - opaque_entry_type = Some cb.const_type; + opaque_entry_type = cb.const_type; opaque_entry_universes = univs; opaque_entry_inline_code = cb.const_inline_code } else diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2c31a237ce..86d79ba044 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -117,7 +117,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | OpaqueEntry ({ opaque_entry_type = typ; opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> - let typ = match typ with None -> assert false | Some typ -> typ in let env = push_context_set ~strict:true univs env in let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in @@ -159,7 +158,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | OpaqueEntry ({ opaque_entry_type = typ; opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> - let typ = match typ with None -> assert false | Some typ -> typ in let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let env = push_context ~strict:false uctx env in let tj = Typeops.infer_type env typ in diff --git a/tactics/declare.ml b/tactics/declare.ml index d4fdff76bf..3840aa6be1 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -174,11 +174,15 @@ let cast_proof_entry e = let cast_opaque_proof_entry e = let open Proof_global in + let typ = match e.proof_entry_type with + | None -> assert false + | Some typ -> typ + in { opaque_entry_body = e.proof_entry_body; opaque_entry_secctx = e.proof_entry_secctx; opaque_entry_feedback = e.proof_entry_feedback; - opaque_entry_type = e.proof_entry_type; + opaque_entry_type = typ; opaque_entry_universes = e.proof_entry_universes; opaque_entry_inline_code = e.proof_entry_inline_code; } -- cgit v1.2.3 From 5de7daa41e677798e4169a3e6350af0df12017e8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Jun 2019 09:32:25 +0200 Subject: Remove the unused opaque_entry_inline_code field from opaque entries. --- kernel/entries.ml | 2 +- kernel/safe_typing.ml | 2 +- kernel/term_typing.ml | 4 ++-- tactics/declare.ml | 1 - 4 files changed, 4 insertions(+), 5 deletions(-) diff --git a/kernel/entries.ml b/kernel/entries.ml index 6016510189..f73111d35f 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -85,7 +85,7 @@ type 'a opaque_entry = { opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; opaque_entry_universes : universes_entry; - opaque_entry_inline_code : bool } +} type inline = int option (* inlining level, None for no inlining *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6cb7a22a15..a0cc2974d9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -695,7 +695,7 @@ let constant_entry_of_side_effect eff = opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; - opaque_entry_inline_code = cb.const_inline_code } + } else DefinitionEntry { const_entry_body = (p, Univ.ContextSet.empty); diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 86d79ba044..eca22869d2 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -150,7 +150,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = tyj.utj_val; cook_universes = Monomorphic univs; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.opaque_entry_inline_code; + cook_inline = false; cook_context = c.opaque_entry_secctx; } @@ -187,7 +187,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = typ; cook_universes = Polymorphic auctx; cook_relevance = Sorts.relevance_of_sort tj.utj_type; - cook_inline = c.opaque_entry_inline_code; + cook_inline = false; cook_context = c.opaque_entry_secctx; } diff --git a/tactics/declare.ml b/tactics/declare.ml index 3840aa6be1..fdb8155038 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -184,7 +184,6 @@ let cast_opaque_proof_entry e = opaque_entry_feedback = e.proof_entry_feedback; opaque_entry_type = typ; opaque_entry_universes = e.proof_entry_universes; - opaque_entry_inline_code = e.proof_entry_inline_code; } let get_roles export eff = -- cgit v1.2.3 From fd2daea8c6f2ab36125964c4e085377fd2ebdde3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Jun 2019 09:39:28 +0200 Subject: Code simplification for definition_entry type. --- kernel/entries.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kernel/entries.ml b/kernel/entries.ml index f73111d35f..2d29c3ee19 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -60,8 +60,8 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -type 'a definition_entry = { - const_entry_body : 'a; +type definition_entry = { + const_entry_body : constr Univ.in_universe_context_set; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) @@ -99,7 +99,7 @@ type primitive_entry = { } type 'a constant_entry = - | DefinitionEntry of constr Univ.in_universe_context_set definition_entry + | DefinitionEntry of definition_entry | OpaqueEntry of 'a const_entry_body opaque_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -- cgit v1.2.3 From b3bfb59281b35fc2a48e5293727977cc260d44c0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 24 Jun 2019 11:07:22 +0200 Subject: Add overlays. --- dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh diff --git a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh new file mode 100644 index 0000000000..3122f953de --- /dev/null +++ b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "10406" ] || [ "$CI_BRANCH" = "desync-entry-proof" ]; then + + equations_CI_REF=desync-entry-proof + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + quickchick_CI_REF=desync-entry-proof + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + +fi -- cgit v1.2.3