From ed7af646f2e486b7e96812ba2335e644756b70fd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 27 Oct 2015 13:55:45 -0400 Subject: Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names structure. --- library/declare.ml | 93 +++++++++++++++++++++++++++++++--------------------- library/declare.mli | 4 +-- library/lib.ml | 39 +++++++++++++++------- library/lib.mli | 2 +- library/universes.ml | 3 +- 5 files changed, 87 insertions(+), 54 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 16803b3bf..0004f45a2 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -27,7 +27,7 @@ open Decls open Decl_kinds (** flag for internal message display *) -type internal_flag = +type internal_flag = | UserAutomaticRequest (* kernel action, a message is displayed *) | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) @@ -63,7 +63,7 @@ let cache_variable ((sp,_),o) = add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with - | Inr (id,_) -> + | Inr (id,_) -> if variable_polymorphic id then None else Some (Inl (variable_context id)) | Inl _ -> Some o @@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) = Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = +let dummy_constant_entry = ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { @@ -185,7 +185,7 @@ let declare_constant_common id cst = Notation.declare_ref_arguments_scope (ConstRef c); c -let definition_entry ?(opaque=false) ?(inline=false) ?types +let definition_entry ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; @@ -212,11 +212,11 @@ let declare_sideff env fix_exn se = in let ty_of cb = match cb.Declarations.const_type with - | Declarations.RegularArity t -> Some t + | Declarations.RegularArity t -> Some t | Declarations.TemplateArity _ -> None in let cst_of cb pt = let pt, opaque = pt_opaque_of cb pt in - let univs, subst = + let univs, subst = if cb.const_polymorphic then let univs = Univ.instantiate_univ_context cb.const_universes in univs, Vars.subst_instance_constr (Univ.UContext.instance univs) @@ -240,7 +240,7 @@ let declare_sideff env fix_exn se = } in let exists c = try ignore(Environ.lookup_constant c env); true - with Not_found -> false in + with Not_found -> false in let knl = CList.map_filter (fun (c,cb,pt) -> if exists c then None @@ -287,7 +287,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = - let cb = + let cb = definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id @@ -383,12 +383,12 @@ let inInductive : inductive_obj -> obj = let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> + | Some (Some (_, kns, pjs)) -> + Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) + IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true | Some None | None -> false @@ -442,52 +442,69 @@ let assumption_message id = (** Global universe names, in a different summary *) -type universe_names = +type universe_names = (Univ.universe_level Idmap.t * Id.t Univ.LMap.t) -let input_universes : universe_names -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Global universe name state") with - cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi); - load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi); - discharge_function = (fun (_, a) -> Some a); - classify_function = (fun a -> Keep a) } +(* Discharged or not *) +type universe_decl = polymorphic * (Id.t * Univ.universe_level) list -let do_universe l = +let cache_universes (p, l) = let glob = Universes.global_universe_names () in - let glob', ctx = - List.fold_left (fun ((idl,lid),ctx) (l, id) -> - let lev = Universes.new_univ_level (Global.current_dirpath ()) in - ((Idmap.add id lev idl, Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) + let glob', ctx = + List.fold_left (fun ((idl,lid),ctx) (id, lev) -> + ((Idmap.add id lev idl, Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in Global.push_context_set false ctx; - Lib.add_anonymous_leaf (input_universes glob') + if p then Lib.add_section_context ctx; + Universes.set_global_universe_names glob' + +let input_universes : universe_decl -> Libobject.obj = + declare_object + { (default_object "Global universe name state") with + cache_function = (fun (na, pi) -> cache_universes pi); + load_function = (fun _ (_, pi) -> cache_universes pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); + classify_function = (fun a -> Keep a) } + +let do_universe poly l = + let l = + List.map (fun (l, id) -> + let lev = Universes.new_univ_level (Global.current_dirpath ()) in + (id, lev)) l + in + Lib.add_anonymous_leaf (input_universes (poly, l)) + +type constraint_decl = polymorphic * Univ.constraints + +let cache_constraints (na, (p, c)) = + Global.add_constraints c; + if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty) +let discharge_constraints (_, (p, c as a)) = + if p then None else Some a -let input_constraints : Univ.constraints -> Libobject.obj = - let open Libobject in +let input_constraints : constraint_decl -> Libobject.obj = + let open Libobject in declare_object { (default_object "Global universe constraints") with - cache_function = (fun (na, c) -> Global.add_constraints c); - load_function = (fun _ (_, c) -> Global.add_constraints c); - discharge_function = (fun (_, a) -> Some a); + cache_function = cache_constraints; + load_function = (fun _ -> cache_constraints); + discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let do_constraint l = - let u_of_id = +let do_constraint poly l = + let u_of_id = let names, _ = Universes.global_universe_names () in - fun (loc, id) -> + fun (loc, id) -> try Idmap.find id names with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) in let constraints = List.fold_left (fun acc (l, d, r) -> let lu = u_of_id l and ru = u_of_id r in Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints constraints) - + Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declare.mli b/library/declare.mli index 76538a624..7ed451c3f 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -85,5 +85,5 @@ val exists_name : Id.t -> bool (** Global universe names and constraints *) -val do_universe : Id.t Loc.located list -> unit -val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_universe : polymorphic -> Id.t Loc.located list -> unit +val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/library/lib.ml b/library/lib.ml index f4f52db53..cdc888903 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -392,10 +392,13 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t +type secentry = + | Variable of (Names.Id.t * Decl_kinds.binding_kind * + Decl_kinds.polymorphic * Univ.universe_context_set) + | Context of Univ.universe_context_set + let sectab = - Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * - Decl_kinds.polymorphic * Univ.universe_context_set) list * - Opaqueproof.work_list * abstr_list) list) + Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list) ~name:"section-context" let add_section () = @@ -406,21 +409,29 @@ let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + +let add_section_context ctx = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> + sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = let rec aux = function - | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> let l, r = aux (idl,hyps) in (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r - | ((_,_,poly,ctx)::idl,hyps) -> + | (Variable (_,_,poly,ctx)::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r ctx else r + | (Context ctx :: idl, hyps) -> + let l, r = aux (idl, hyps) in + l, Univ.ContextSet.union r ctx | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) let instance_from_variable_context sign = - let rec inst_rec = function | (id,b,None,_) :: sign -> id :: inst_rec sign | _ :: sign -> inst_rec sign @@ -437,7 +448,8 @@ let add_section_replacement f g hyps = let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl + sectab := (vars,f (Univ.UContext.instance ctx,args) exps, + g (sechyps,subst,ctx) abs)::sl let add_section_kn kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in @@ -457,10 +469,13 @@ let section_segment_of_mutual_inductive kn = let section_instance = function | VarRef id -> - if List.exists (fun (id',_,_,_) -> Names.id_eq id id') - (pi1 (List.hd !sectab)) - then Univ.Instance.empty, [||] - else raise Not_found + let eq = function + | Variable (id',_,_,_) -> Names.id_eq id id' + | Context _ -> false + in + if List.exists eq (pi1 (List.hd !sectab)) + then Univ.Instance.empty, [||] + else raise Not_found | ConstRef con -> Names.Cmap.find con (fst (pi2 (List.hd !sectab))) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> diff --git a/library/lib.mli b/library/lib.mli index 9c4d26c5b..b67b2b873 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -172,7 +172,7 @@ val section_instance : Globnames.global_reference -> Univ.universe_instance * Na val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit - +val add_section_context : Univ.universe_context_set -> unit val add_section_constant : bool (* is_projection *) -> Names.constant -> Context.named_context -> unit val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit diff --git a/library/universes.ml b/library/universes.ml index 0656188eb..30d38eb2a 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -16,7 +16,8 @@ open Univ type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t -let global_universes = Summary.ref ~name:"Global universe names" +let global_universes = + Summary.ref ~name:"Global universe names" ((Idmap.empty, Univ.LMap.empty) : universe_names) let global_universe_names () = !global_universes -- cgit v1.2.3 From 0a1b046d37761fe47435d5041bb5031e3f7d6613 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 10:03:17 +0100 Subject: lib_stack: API to reorder the libstack For discharging it is important that constants occur in the libstack in an order that respects the dependencies among them. This is impossible to achieve for private constants when they are exported globally without this (ugly IMO) api. --- library/lib.ml | 3 +++ library/lib.mli | 1 + 2 files changed, 4 insertions(+) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index cdc888903..297441e6e 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -198,6 +198,9 @@ let split_lib_at_opening sp = let add_entry sp node = lib_stk := (sp,node) :: !lib_stk +let pull_to_head oname = + lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk + let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) diff --git a/library/lib.mli b/library/lib.mli index b67b2b873..bb8831759 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -55,6 +55,7 @@ val segment_of_objects : val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.obj -> unit +val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -- cgit v1.2.3 From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- kernel/declarations.mli | 6 - kernel/declareops.ml | 18 +-- kernel/declareops.mli | 12 +- kernel/entries.mli | 25 +++- kernel/opaqueproof.ml | 5 +- kernel/safe_typing.ml | 103 +++++++++++--- kernel/safe_typing.mli | 41 +++++- kernel/term_typing.ml | 188 ++++++++++++++++++++++--- kernel/term_typing.mli | 33 ++++- library/declare.ml | 151 +++++++++----------- library/declare.mli | 10 +- library/global.mli | 5 +- library/heads.ml | 5 +- library/libobject.ml | 3 + plugins/derive/derive.ml | 4 +- plugins/funind/functional_principles_types.ml | 14 +- plugins/funind/functional_principles_types.mli | 10 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 4 +- pretyping/evd.ml | 26 +--- pretyping/evd.mli | 4 +- proofs/pfedit.ml | 10 +- proofs/pfedit.mli | 6 +- proofs/proof_global.ml | 9 +- proofs/proof_global.mli | 4 +- proofs/proofview.mli | 2 +- stm/lemmas.ml | 5 +- tactics/elimschemes.ml | 20 +-- tactics/eqschemes.ml | 17 +-- tactics/eqschemes.mli | 4 +- tactics/equality.ml | 2 +- tactics/tactics.ml | 6 +- toplevel/auto_ind_decl.ml | 23 ++- toplevel/classes.ml | 2 +- toplevel/command.ml | 8 +- toplevel/command.mli | 10 +- toplevel/discharge.ml | 4 +- toplevel/ind_tables.ml | 22 +-- toplevel/ind_tables.mli | 10 +- toplevel/indschemes.ml | 4 +- toplevel/obligations.ml | 12 +- toplevel/obligations.mli | 4 +- toplevel/record.ml | 6 +- 43 files changed, 547 insertions(+), 312 deletions(-) (limited to 'library') diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 7def963e7..dc5c17a75 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -79,12 +79,6 @@ type constant_body = { const_proj : projection_body option; const_inline_code : bool } -type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] - -type side_effect = - | SEsubproof of constant * constant_body * seff_env - | SEscheme of (inductive * constant * constant_body * seff_env) list * string - (** {6 Representation of mutual inductive types in the kernel } *) type recarg = diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a7051d5c1..248504c1b 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -304,17 +304,7 @@ let hcons_mind mib = (** {6 Stm machinery } *) -let string_of_side_effect = function - | SEsubproof (c,_,_) -> Names.string_of_con c - | SEscheme (cl,_) -> - String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) -type side_effects = side_effect list -let no_seff = ([] : side_effects) -let iter_side_effects f l = List.iter f (List.rev l) -let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l)) -let union_side_effects l1 l2 = l1 @ l2 -let flatten_side_effects l = List.flatten l -let side_effects_of_list l = l -let cons_side_effects x l = x :: l -let side_effects_is_empty = List.is_empty +let string_of_side_effect { Entries.eff } = match eff with + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEscheme (cl,_) -> + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" diff --git a/kernel/declareops.mli b/kernel/declareops.mli index ce65af975..1b8700958 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,6 +9,7 @@ open Declarations open Mod_subst open Univ +open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool val string_of_side_effect : side_effect -> string -type side_effects -val no_seff : side_effects -val iter_side_effects : (side_effect -> unit) -> side_effects -> unit -val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a -val uniquize_side_effects : side_effects -> side_effects -val union_side_effects : side_effects -> side_effects -> side_effects -val flatten_side_effects : side_effects list -> side_effects -val side_effects_of_list : side_effect list -> side_effects -val cons_side_effects : side_effect -> side_effects -> side_effects -val side_effects_is_empty : side_effects -> bool - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool diff --git a/kernel/entries.mli b/kernel/entries.mli index 303d27d35..e058519e9 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -54,11 +54,11 @@ type mutual_inductive_entry = { mind_entry_private : bool option } (** {6 Constants (Definition/Axiom) } *) -type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects -type const_entry_body = proof_output Future.computation +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation -type definition_entry = { - const_entry_body : const_entry_body; +type 'a definition_entry = { + const_entry_body : 'a const_entry_body; (* List of section variables *) const_entry_secctx : Context.section_context option; (* State id on which the completion of type checking is reported *) @@ -78,8 +78,8 @@ type projection_entry = { proj_entry_ind : mutual_inductive; proj_entry_arg : int } -type constant_entry = - | DefinitionEntry of definition_entry +type 'a constant_entry = + | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry @@ -96,3 +96,16 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option + +type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type side_eff = + | SEsubproof of constant * Declarations.constant_body * seff_env + | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string + +type side_effect = { + from_env : Declarations.structure_body Ephemeron.key; + eff : side_eff; +} + +type side_effects = side_effect list diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 9f4361f40..badb15b56 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -43,7 +43,10 @@ let set_indirect_univ_accessor f = (get_univ := f) let create cu = Direct ([],cu) let turn_indirect dp o (prfs,odp) = match o with - | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque") + | Indirect (_,_,i) -> + if not (Int.Map.mem i prfs) + then Errors.anomaly (Pp.str "Indirect in a different table") + else Errors.anomaly (Pp.str "Already an indirect opaque") | Direct (d,cu) -> let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in let id = Int.Map.cardinal prfs in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ec245b064..b71cd31b5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -207,15 +207,55 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -let sideff_of_con env c = +type private_constant = Entries.side_effect +type private_constants = private_constant list + +type private_constant_role = Term_typing.side_effect_role = + | Subproof + | Schema of inductive * string + +let empty_private_constants = [] +let add_private x xs = x :: xs +let concat_private xs ys = xs @ ys +let mk_pure_proof = Term_typing.mk_pure_proof +let inline_private_constants_in_constr = Term_typing.handle_side_effects +let inline_private_constants_in_definition_entry = Term_typing.handle_entry_side_effects +let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) + +let constant_entry_of_private_constant = function + | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> + [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ] + | { Entries.eff = Entries.SEscheme (l,_) } -> + List.map (fun (_,kn,cb,eff_env) -> + kn, Term_typing.constant_entry_of_side_effect cb eff_env) l + +let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in - SEsubproof (c, cbo, get_opaque_body env.env cbo) -let sideff_of_scheme kind env cl = - SEscheme( - List.map (fun (i,c) -> - let cbo = Environ.lookup_constant c env.env in - i, c, cbo, get_opaque_body env.env cbo) cl, - kind) + { Entries.from_env = Ephemeron.create env.revstruct; + Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } + +let private_con_of_scheme ~kind env cl = + { Entries.from_env = Ephemeron.create env.revstruct; + Entries.eff = Entries.SEscheme( + List.map (fun (i,c) -> + let cbo = Environ.lookup_constant c env.env in + i, c, cbo, get_opaque_body env.env cbo) cl, + kind) } + +let universes_of_private eff = + let open Declarations in + List.fold_left (fun acc { Entries.eff } -> + match eff with + | Entries.SEscheme (l,s) -> + List.fold_left (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc in + if cb.const_polymorphic then acc + else (Univ.ContextSet.of_context cb.const_universes) :: acc) + acc l + | Entries.SEsubproof _ -> acc) + [] eff let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -337,7 +377,7 @@ let safe_push_named (id,_,_ as d) env = let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.env id de in + let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -442,19 +482,16 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe -let add_constant dir l decl senv = - let kn = make_con senv.modpath dir l in - let cb = match decl with - | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce - | GlobalRecipe r -> - let cb = Term_typing.translate_recipe senv.env kn r in - if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb - in +type exported_private_constant = + constant * private_constants Entries.constant_entry * private_constant_role + +let add_constant_aux no_section senv (kn, cb) = + let l = pi3 (Constant.repr3 kn) in let cb, otab = match cb.const_body with - | OpaqueDef lc when DirPath.is_empty dir -> + | OpaqueDef lc when no_section -> (* In coqc, opaque constants outside sections will be stored indirectly in a specific table *) let od, otab = @@ -471,7 +508,33 @@ let add_constant dir l decl senv = (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv' | _ -> senv' in - kn, senv'' + senv'' + +let add_constant dir l decl senv = + let kn = make_con senv.modpath dir l in + let no_section = DirPath.is_empty dir in + let seff_to_export, decl = + match decl with + | ConstantEntry (true, ce) -> + let exports, ce = + Term_typing.validate_side_effects_for_export + senv.revstruct senv.env ce in + exports, ConstantEntry (false, ce) + | _ -> [], decl + in + let senv = + List.fold_left (add_constant_aux no_section) senv + (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in + let senv = + let cb = + match decl with + | ConstantEntry (export_seff,ce) -> + Term_typing.translate_constant senv.revstruct senv.env kn ce + | GlobalRecipe r -> + let cb = Term_typing.translate_recipe senv.env kn r in + if no_section then Declareops.hcons_const_body cb else cb in + add_constant_aux no_section senv (kn, cb) in + (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index eac08eb83..2214cf8bb 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -val sideff_of_con : safe_environment -> constant -> Declarations.side_effect -val sideff_of_scheme : - string -> safe_environment -> (inductive * constant) list -> - Declarations.side_effect +type private_constant +type private_constants + +type private_constant_role = + | Subproof + | Schema of inductive * string + +val side_effects_of_private_constants : + private_constants -> Entries.side_effects + +val empty_private_constants : private_constants +val add_private : private_constant -> private_constants -> private_constants +val concat_private : private_constants -> private_constants -> private_constants + +val private_con_of_con : safe_environment -> constant -> private_constant +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant + +val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output +val inline_private_constants_in_constr : + Environ.env -> Constr.constr -> private_constants -> Constr.constr +val inline_private_constants_in_definition_entry : + Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry + +val universes_of_private : private_constants -> Univ.universe_context_set list val is_curmod_library : safe_environment -> bool @@ -63,16 +83,23 @@ val push_named_assum : (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer + Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry + (* bool: export private constants *) + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe +type exported_private_constant = + constant * private_constants Entries.constant_entry * private_constant_role + +(** returns the main constant plus a list of auxiliary constants (empty + unless one requires the side effects to be exported) *) val add_constant : - DirPath.t -> Label.t -> global_declaration -> constant safe_transformer + DirPath.t -> Label.t -> global_declaration -> + (constant * exported_private_constant list) safe_transformer (** Adding an inductive type *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cab99077f..d75bd73fb 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x (* Insertion of constants and parameters in environment. *) -let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff +let mk_pure_proof c = (c, Univ.ContextSet.empty), [] + +let equal_eff e1 e2 = + let open Entries in + match e1, e2 with + | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } -> + Names.Constant.equal c1 c2 + | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } -> + CList.for_all2eq + (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2) + cl1 cl2 + | _ -> false + +let rec uniq_seff = function + | [] -> [] + | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs) +(* The list of side effects is in reverse order (most recent first). + * To keep the "tological" order between effects we have to uniqize from the + * tail *) +let uniq_seff l = List.rev (uniq_seff (List.rev l)) let handle_side_effects env body ctx side_eff = - let handle_sideff (t,ctx) se = + let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = let cbl = match se with | SEsubproof (c,cb,b) -> [c,cb,b] | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in @@ -65,7 +84,7 @@ let handle_side_effects env body ctx side_eff = let rec sub_body c u b i x = match kind_of_term x with | Const (c',u') when eq_constant c c' -> Vars.subst_instance_constr u' b - | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in + | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in let fix_body (c,cb,b) (t,ctx) = match cb.const_body, b with | Def b, _ -> @@ -87,17 +106,60 @@ let handle_side_effects env body ctx side_eff = let t = sub c 1 (Vars.lift 1 t) in mkApp (mkLambda (cname c, b_ty, t), [|b|]), Univ.ContextSet.union ctx - (Univ.ContextSet.of_context cb.const_universes) + (Univ.ContextSet.of_context cb.const_universes) else let univs = cb.const_universes in sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx | _ -> assert false in - List.fold_right fix_body cbl (t,ctx) + let t, ctx = List.fold_right fix_body cbl (t,ctx) in + t, ctx, (mb,List.length cbl) :: sl in (* CAVEAT: we assure a proper order *) - Declareops.fold_side_effects handle_sideff (body,ctx) - (Declareops.uniquize_side_effects side_eff) + List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff) + +let check_signatures curmb sl = + let is_direct_ancestor (sl, curmb) (mb, how_many) = + match curmb with + | None -> None, None + | Some curmb -> + try + let mb = Ephemeron.get mb in + match sl with + | None -> sl, None + | Some n -> + if List.length mb >= how_many && CList.skipn how_many mb == curmb + then Some (n + how_many), Some mb + else None, None + with Ephemeron.InvalidKey -> None, None in + let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in + sl + +let trust_seff sl b e = + let rec aux sl b e acc = + match sl, kind_of_term b with + | (None|Some 0), _ -> b, e, acc + | Some sl, LetIn (n,c,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc) + | Some sl, App(hd,arg) -> + begin match kind_of_term hd with + | Lambda (n,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc) + | _ -> assert false + end + | _ -> assert false + in + aux sl b e [] + +let rec unzip ctx j = + match ctx with + | [] -> j + | `Let (n,c,ty) :: ctx -> + unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) } + | `Cut (n,ty,arg) :: ctx -> + unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let hcons_j j = { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} @@ -105,7 +167,7 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) -let infer_declaration env kn dcl = +let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in @@ -124,9 +186,14 @@ let infer_declaration env kn dcl = let tyj = infer_type env typ in let proofterm = Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> - let body,ctx = handle_side_effects env body ctx side_eff in + let body, ctx, signatures = + handle_side_effects env body ctx side_eff in + let trusted_signatures = check_signatures trust signatures in let env' = push_context_set ctx env in - let j = infer env' body in + let j = + let body, env', zip_ctx = trust_seff trusted_signatures body env' in + let j = infer env' body in + unzip zip_ctx j in let j = hcons_j j in let subst = Univ.LMap.empty in let _typ = constrain_type env' j c.const_entry_polymorphic subst @@ -143,7 +210,7 @@ let infer_declaration env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in let univsctx = Univ.ContextSet.of_context c.const_entry_universes in - let body, ctx = handle_side_effects env body + let body, ctx, _ = handle_side_effects env body (Univ.ContextSet.union univsctx ctx) side_eff in let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in @@ -294,8 +361,93 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (*s Global and local constant declaration. *) -let translate_constant env kn ce = - build_constant_declaration kn env (infer_declaration env (Some kn) ce) +let translate_constant mb env kn ce = + build_constant_declaration kn env + (infer_declaration ~trust:mb env (Some kn) ce) + +let constant_entry_of_side_effect cb u = + let pt = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b, c) -> b, c + | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + | _ -> assert false in + DefinitionEntry { + const_entry_body = Future.from_val (pt, []); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = + (match cb.const_type with RegularArity t -> Some t | _ -> None); + const_entry_polymorphic = cb.const_polymorphic; + const_entry_universes = cb.const_universes; + const_entry_opaque = Declareops.is_opaque cb; + const_entry_inline_code = cb.const_inline_code } +;; + +let turn_direct (kn,cb,u,r as orig) = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b,c) -> + let pt = Future.from_val (b,c) in + kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r + | _ -> orig +;; + +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects Entries.constant_entry * side_effect_role + +let validate_side_effects_for_export mb env ce = + match ce with + | ParameterEntry _ | ProjectionEntry _ -> [], ce + | DefinitionEntry c -> + let { const_entry_body = body } = c in + let _, eff = Future.force body in + let ce = DefinitionEntry { c with + const_entry_body = Future.chain ~greedy:true ~pure:true body + (fun (b_ctx, _) -> b_ctx, []) } in + let not_exists (c,_,_,_) = + try ignore(Environ.lookup_constant c env); false + with Not_found -> true in + let aux (acc,sl) { eff = se; from_env = mb } = + let cbl = match se with + | SEsubproof (c,cb,b) -> [c,cb,b,Subproof] + | SEscheme (cl,k) -> + List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in + let cbl = List.filter not_exists cbl in + if cbl = [] then acc, sl + else cbl :: acc, (mb,List.length cbl) :: sl in + let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in + let trusted = check_signatures mb signatures in + let push_seff env = function + | kn, cb, `Nothing, _ -> + Environ.add_constant kn cb env + | kn, cb, `Opaque(_, ctx), _ -> + let env = Environ.add_constant kn cb env in + Environ.push_context_set + ~strict:(not cb.const_polymorphic) ctx env in + let rec translate_seff sl seff acc env = + match sl, seff with + | _, [] -> List.rev acc, ce + | (None | Some 0), cbs :: rest -> + let env, cbs = + List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> + let ce = constant_entry_of_side_effect ocb u in + let cb = translate_constant mb env kn ce in + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + (env,[]) cbs in + translate_seff sl rest (cbs @ acc) env + | Some sl, cbs :: rest -> + let cbs_len = List.length cbs in + let cbs = List.map turn_direct cbs in + let env = List.fold_left push_seff env cbs in + let ecbs = List.map (fun (kn,cb,u,r) -> + kn, cb, constant_entry_of_side_effect cb u, r) cbs in + translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env + in + translate_seff trusted seff [] env +;; let translate_local_assum env t = let j = infer env t in @@ -305,9 +457,9 @@ let translate_local_assum env t = let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant env r) -let translate_local_def env id centry = +let translate_local_def mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration env None (DefinitionEntry centry) in + infer_declaration ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin match def with @@ -332,9 +484,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie let handle_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx' = handle_side_effects env body ctx side_eff in - (body, ctx'), Declareops.no_seff); + let body, ctx',_ = handle_side_effects env body ctx side_eff in + (body, ctx'), []); } let handle_side_effects env body side_eff = - fst (handle_side_effects env body Univ.ContextSet.empty side_eff) + pi1 (handle_side_effects env body Univ.ContextSet.empty side_eff) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 8d92bcc68..509160ccc 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,23 +12,42 @@ open Environ open Declarations open Entries -val translate_local_def : env -> Id.t -> definition_entry -> +val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes val translate_local_assum : env -> types -> types -val mk_pure_proof : constr -> proof_output +val mk_pure_proof : constr -> side_effects proof_output -val handle_side_effects : env -> constr -> Declareops.side_effects -> constr +val handle_side_effects : env -> constr -> side_effects -> constr (** Returns the term where side effects have been turned into let-ins or beta redexes. *) -val handle_entry_side_effects : env -> definition_entry -> definition_entry +val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry (** Same as {!handle_side_effects} but applied to entries. Only modifies the {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val translate_constant : env -> constant -> constant_entry -> constant_body +val uniq_seff : side_effects -> side_effects + +val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body + +(* Checks weather the side effects in constant_entry can be trusted. + * Returns the list of effects to be exported. + * Note: It forces the Future.computation. *) +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects Entries.constant_entry * side_effect_role + +val validate_side_effects_for_export : + structure_body -> env -> side_effects constant_entry -> + exported_side_effect list * side_effects constant_entry + +val constant_entry_of_side_effect : + constant_body -> seff_env -> side_effects constant_entry val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -37,8 +56,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : env -> constant option -> - constant_entry -> Cooking.result +val infer_declaration : trust:structure_body -> env -> constant option -> + side_effects constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body diff --git a/library/declare.ml b/library/declare.ml index 0004f45a2..63e5a7224 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -35,7 +35,7 @@ type internal_flag = (** Declaration of section variables and local definitions *) type section_variable_entry = - | SectionLocalDef of definition_entry + | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -93,9 +93,13 @@ type constant_obj = { cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; + mutable cst_exported : Safe_typing.exported_private_constant list; + (* mutable: to avoid change the libobject API, since cache_function + * does not return an updated object *) + mutable cst_was_seff : bool } -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) @@ -131,8 +135,17 @@ let check_exists sp = let cache_constant ((sp,kn), obj) = let id = basename sp in let _,dir,_ = repr_kn kn in - let () = check_exists sp in - let kn' = Global.add_constant dir id obj.cst_decl in + let kn' = + if obj.cst_was_seff then begin + obj.cst_was_seff <- false; + if Global.exists_objlabel (Label.of_id (basename sp)) + then constant_of_kn kn + else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) + end else + let () = check_exists sp in + let kn', exported = Global.add_constant dir id obj.cst_decl in + obj.cst_exported <- exported; + kn' in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in @@ -156,20 +169,23 @@ let discharge_constant ((sp, kn), obj) = Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = - ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) +let dummy_constant_entry = + ConstantEntry + (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { cst_decl = dummy_constant_entry; cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; + cst_exported = []; + cst_was_seff = cst.cst_was_seff; } let classify_constant cst = Substitute (dummy_constant cst) -let inConstant : constant_obj -> obj = - declare_object { (default_object "CONSTANT") with +let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = + declare_object_full { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -177,16 +193,40 @@ let inConstant : constant_obj -> obj = 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 declare_constant_common id cst = - let (sp,kn) = add_leaf id (inConstant cst) in + let update_tables c = +(* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *) + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c) in + let o = inConstant cst in + let _, kn as oname = add_leaf id o in + List.iter (fun (c,ce,role) -> + (* handling of private_constants just exported *) + let o = inConstant { + cst_decl = ConstantEntry (false, ce); + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + cst_exported = []; + cst_was_seff = true; } in + let id = Label.to_id (pi3 (Constant.repr3 c)) in + ignore(add_leaf id o); + update_tables c; + match role with + | Safe_typing.Subproof -> () + | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) + (outConstant o).cst_exported; + pull_to_head oname; let c = Global.constant_of_delta_kn kn in - declare_constant_implicits c; - Heads.declare_head (EvalConstRef c); - Notation.declare_ref_arguments_scope (ConstRef c); + update_tables c; c let definition_entry ?(opaque=false) ?(inline=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = + ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; @@ -196,90 +236,25 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f -let declare_sideff env fix_exn se = - let cbl, scheme = match se with - | SEsubproof (c, cb, pt) -> [c, cb, pt], None - | SEscheme (cbl, k) -> - List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in - let id_of c = Names.Label.to_id (Names.Constant.label c) in - let pt_opaque_of cb pt = - match cb, pt with - | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false - | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true - | _ -> assert false - in - let ty_of cb = - match cb.Declarations.const_type with - | Declarations.RegularArity t -> Some t - | Declarations.TemplateArity _ -> None in - let cst_of cb pt = - let pt, opaque = pt_opaque_of cb pt in - let univs, subst = - if cb.const_polymorphic then - let univs = Univ.instantiate_univ_context cb.const_universes in - univs, Vars.subst_instance_constr (Univ.UContext.instance univs) - else cb.const_universes, fun x -> x - in - let pt = (subst (fst pt), snd pt) in - let ty = Option.map subst (ty_of cb) in - { cst_decl = ConstantEntry (DefinitionEntry { - const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff); - const_entry_secctx = Some cb.Declarations.const_hyps; - const_entry_type = ty; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_feedback = None; - const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = univs; - }); - cst_hyps = [] ; - cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; - cst_locl = true; - } in - let exists c = - try ignore(Environ.lookup_constant c env); true - with Not_found -> false in - let knl = - CList.map_filter (fun (c,cb,pt) -> - if exists c then None - else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in - match scheme with - | None -> () - | Some (inds_consts,kind) -> - !declare_scheme kind (Array.of_list - (List.map (fun (c,kn) -> - CList.find_map (fun (x,c',_,_) -> - if Constant.equal c c' then Some (x,kn) else None) inds_consts) - knl)) - let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = - let cd = (* We deal with side effects *) + let export = (* We deal with side effects *) match cd with - | Entries.DefinitionEntry de -> - if export_seff || - not de.const_entry_opaque || - de.const_entry_polymorphic then + | DefinitionEntry de when + export_seff || + not de.const_entry_opaque || + de.const_entry_polymorphic -> let bo = de.const_entry_body in let _, seff = Future.force bo in - if Declareops.side_effects_is_empty seff then cd - else begin - let seff = Declareops.uniquize_side_effects seff in - Declareops.iter_side_effects - (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff; - Entries.DefinitionEntry { de with - const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> - pt, Declareops.no_seff) } - end - else cd - | _ -> cd + Safe_typing.empty_private_constants <> seff + | _ -> false in let cst = { - cst_decl = ConstantEntry cd; + cst_decl = ConstantEntry (export,cd); cst_hyps = [] ; cst_kind = kind; cst_locl = local; + cst_exported = []; + cst_was_seff = false; } in let kn = declare_constant_common id cst in kn diff --git a/library/declare.mli b/library/declare.mli index 7ed451c3f..fdbd23561 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -22,7 +22,7 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of definition_entry + | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -32,7 +32,7 @@ val declare_variable : variable -> variable_declaration -> object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -49,8 +49,8 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects -> - constr -> definition_entry + ?poly:polymorphic -> ?univs:Univ.universe_context -> + ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant @@ -60,7 +60,7 @@ val declare_definition : ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant -(** Since transparent constant's side effects are globally declared, we +(** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : (string -> (inductive * constant) array -> unit) -> unit diff --git a/library/global.mli b/library/global.mli index ac231f7fd..03469bea4 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,10 +31,11 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> Univ.universe_context_set +val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant + DirPath.t -> Id.t -> Safe_typing.global_declaration -> + constant * Safe_typing.exported_private_constant list val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive diff --git a/library/heads.ml b/library/heads.ml index 5c153b067..73d2aa053 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -68,7 +68,10 @@ let kind_of_head env t = | None -> NotImmediatelyComputableHead) | Const (cst,_) -> (try on_subterm k l b (constant_head cst) - with Not_found -> assert false) + with Not_found -> + Errors.anomaly + Pp.(str "constant not found in kind_of_head: " ++ + str (Names.Constant.to_string cst))) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType diff --git a/library/libobject.ml b/library/libobject.ml index 2ee57baf9..85c830ea2 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -108,6 +108,9 @@ let declare_object_full odecl = let declare_object odecl = try fst (declare_object_full odecl) with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) +let declare_object_full odecl = + try declare_object_full odecl + with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index c232ae31a..d6c29283f 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body) - : Entries.const_entry_body = +let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) + : Safe_typing.private_constants Entries.const_entry_body = Future.chain ~pure:true x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9e27ddf2e..c43932324 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -334,7 +334,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) ignore( Declare.declare_constant name - (Entries.DefinitionEntry ce, + (DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; @@ -447,7 +447,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list = +let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr 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.Entries.const_entry_body, const.Entries.const_entry_type in + let first_princ_body,first_princ_type = const.const_entry_body, const.const_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 = @@ -585,9 +585,9 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - Entries.const_entry_body = - (Future.from_val (Term_typing.mk_pure_proof princ_body)); - Entries.const_entry_type = Some scheme_type + const_entry_body = + (Future.from_val (Safe_typing.mk_pure_proof princ_body)); + const_entry_type = Some scheme_type } ) other_fun_princ_types @@ -620,7 +620,7 @@ let build_scheme fas = ignore (Declare.declare_constant princ_id - (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (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 f6e5578d2..bc082f073 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* sorts array -> exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*glob_sort) list -> Entries.definition_entry list + (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 35bd1c36d..aa47e2619 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -149,7 +149,7 @@ let get_locality = function | Global -> false let save with_clean id const (locality,_,kind) hook = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 10daf6e84..23f1da1ba 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr -val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> +val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> unit Lemmas.declaration_hook Ephemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and @@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> *) val get_proof_clean : bool -> Names.Id.t * - (Entries.definition_entry * Decl_kinds.goal_kind) + (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1107c2951..0593bbca8 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -579,7 +579,7 @@ type evar_map = { (** Metas *) metas : clbinding Metamap.t; (** Interactive proofs *) - effects : Declareops.side_effects; + effects : Safe_typing.private_constants; future_goals : Evar.t list; (** list of newly created evars, to be eventually turned into goals if not solved.*) principal_future_goal : Evar.t option; (** if [Some e], [e] must be @@ -768,7 +768,7 @@ let empty = { conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; - effects = Declareops.no_seff; + effects = Safe_typing.empty_private_constants; evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; @@ -1041,22 +1041,8 @@ let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) let emit_universe_side_effects eff u = - Declareops.fold_side_effects - (fun acc eff -> - match eff with - | Declarations.SEscheme (l,s) -> - List.fold_left - (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx - in if cb.Declarations.const_polymorphic then acc - else - merge_uctx true univ_rigid acc - (Univ.ContextSet.of_context cb.Declarations.const_universes)) - acc l - | Declarations.SEsubproof _ -> acc) - u eff + let uctxs = Safe_typing.universes_of_private eff in + List.fold_left (merge_uctx true univ_rigid) u uctxs let add_uctx_names s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l s names_rev) @@ -1399,11 +1385,11 @@ let e_eq_constr_univs evdref t u = (* Side effects *) let emit_side_effects eff evd = - { evd with effects = Declareops.union_side_effects eff evd.effects; + { evd with effects = Safe_typing.concat_private eff evd.effects; universes = emit_universe_side_effects eff evd.universes } let drop_side_effects evd = - { evd with effects = Declareops.no_seff; } + { evd with effects = Safe_typing.empty_private_constants; } let eval_side_effects evd = evd.effects diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 52d7d4212..9379b50b5 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -261,10 +261,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t (** {5 Side-effects} *) -val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map +val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map (** Push a side-effect into the evar map. *) -val eval_side_effects : evar_map -> Declareops.side_effects +val eval_side_effects : evar_map -> Safe_typing.private_constants (** Return the effects contained in the evar map. *) val drop_side_effects : evar_map -> evar_map diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 00ef8ecaf..02dbd1fdc 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -150,10 +150,14 @@ let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in - let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in + let ce = + if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce + else { ce with + const_entry_body = Future.chain ~pure:true ce.const_entry_body + (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in let (cb, ctx), se = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - assert(Declareops.side_effects_is_empty se); + assert(Safe_typing.empty_private_constants = se); cb, status, Evd.evar_universe_context univs' let refine_by_tactic env sigma ty tac = @@ -188,7 +192,7 @@ let refine_by_tactic env sigma ty tac = other goals that were already present during its invocation, so that those goals rely on effects that are not present anymore. Hopefully, this hack will work in most cases. *) - let ans = Term_typing.handle_side_effects env ans neff in + let ans = Safe_typing.inline_private_constants_in_constr env ans neff in ans, sigma (**********************************************************************) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index b1fba132d..fc521ea43 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -69,11 +69,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) val cook_proof : unit -> (Id.t * - (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) (** {6 ... } *) (** [get_pftreestate ()] returns the current focused pending proof. @@ -152,7 +152,7 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> types -> unit Proofview.tactic -> - Entries.definition_entry * bool * Evd.evar_universe_context + Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a0ead42ef..809ed41c7 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -67,7 +67,7 @@ type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; - entries : Entries.definition_entry list; + entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; (* constraints : Univ.constraints; *) @@ -315,13 +315,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let open Universes in let body = c in let typ = - if not (keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff)) then + if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then nf t else t in let used_univs_body = Universes.universes_of_constr body in let used_univs_typ = Universes.universes_of_constr typ in - if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then + if keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in let ctx = Evd.evar_universe_context_set initunivs universes in (* For vi2vo compilation proofs are computed now but we need to @@ -365,7 +366,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = { id = pid; entries = entries; persistence = strength; universes = universes }, fun pr_ending -> Ephemeron.get terminator pr_ending -type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index fcb706cc8..f8615e849 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -58,7 +58,7 @@ type lemma_possible_guards = int list list type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; - entries : Entries.definition_entry list; + entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; (* constraints : Univ.constraints; *) @@ -97,7 +97,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 5a9e7f39f..927df33a0 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -336,7 +336,7 @@ val tclENV : Environ.env tactic (** {7 Put-like primitives} *) (** [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Declareops.side_effects -> unit tactic +val tclEFFECTS : Safe_typing.private_constants -> unit tactic (** [mark_as_unsafe] declares the current tactic is unsafe. *) val mark_as_unsafe : unit tactic diff --git a/stm/lemmas.ml b/stm/lemmas.ml index c49ddfd8e..6c1832688 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -70,11 +70,12 @@ let adjust_guardness_conditions const = function try ignore(Environ.lookup_constant c e); true with Not_found -> false in if exists c e then e else Environ.add_constant c cb e in - let env = Declareops.fold_side_effects (fun env -> function + let env = List.fold_left (fun env { eff } -> + match eff with | SEsubproof (c, cb,_) -> add c cb env | SEscheme (l,_) -> List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Declareops.uniquize_side_effects eff) in + env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard Loc.ghost env possible_indexes fixdecls in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e6a8cbe3a..8a6d93cf7 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -52,7 +52,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in - (c, Evd.evar_universe_context sigma), Declareops.no_seff + (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f7d3ad5d0..b2603315d 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -193,7 +193,7 @@ let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in - (c, ctx), Declareops.no_seff) + (c, ctx), Safe_typing.empty_private_constants) (**********************************************************************) (* Build the involutivity of symmetry for an inductive type *) @@ -412,7 +412,8 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff + in (c, Evd.evar_universe_context_of ctx), + Safe_typing.concat_private eff' eff (**********************************************************************) (* Build the left-to-right rewriting lemma for hypotheses associated *) @@ -660,7 +661,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +671,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +681,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -694,7 +695,7 @@ let rew_l2r_forward_dep_scheme_kind = let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" (fun _ ind -> fix_r2l_forward_rew_scheme - (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) + (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants) (**********************************************************************) (* Non-dependent rewrite from either right-to-left in conclusion or *) @@ -704,7 +705,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants) (* End of rewriting schemes *) @@ -782,4 +783,4 @@ let build_congr env (eq,refl,ctx) ind = let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> (* May fail if equality is not defined *) - build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) + build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 6bb84808a..3fe330730 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -25,7 +25,7 @@ val rew_r2l_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> - constr Evd.in_evar_universe_context * Declareops.side_effects + constr Evd.in_evar_universe_context * Safe_typing.private_constants val build_r2l_forward_rew_scheme : bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : @@ -37,7 +37,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> - constr Evd.in_evar_universe_context * Declareops.side_effects + constr Evd.in_evar_universe_context * Safe_typing.private_constants val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) diff --git a/tactics/equality.ml b/tactics/equality.ml index bc711b81e..674c85af7 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = assert false in let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, Declareops.no_seff + sigma, elim, Safe_typing.empty_private_constants else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1437b2462..0b920066f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4455,9 +4455,9 @@ let abstract_subproof id gk tac = (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in - let open Declareops in - let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in - let effs = cons_side_effects eff + let open Safe_typing in + let eff = private_con_of_con (Global.safe_env ()) cst in + let effs = add_private eff Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in let solve = diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 8ac273c84..7a89b9f54 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -179,12 +179,12 @@ let build_beq_scheme mode kn = let rec aux c = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in match kind_of_term c with - | Rel x -> mkRel (x-nlist+ndx), Declareops.no_seff - | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff + | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants + | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants | Cast (x,_,_) -> aux (applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff + if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants else begin try let eq, eff = @@ -193,9 +193,8 @@ let build_beq_scheme mode kn = let eqa, eff = let eqa, effs = List.split (List.map aux a) in Array.of_list eqa, - Declareops.union_side_effects - (Declareops.flatten_side_effects (List.rev effs)) - eff in + List.fold_left Safe_typing.concat_private eff (List.rev effs) + in let args = Array.append (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in @@ -238,7 +237,7 @@ let build_beq_scheme mode kn = let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (Lazy.force ff) in - let eff = ref Declareops.no_seff in + let eff = ref Safe_typing.empty_private_constants in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in let ar2 = Array.make n (Lazy.force ff) in @@ -256,7 +255,7 @@ let build_beq_scheme mode kn = (nb_cstr_args+ndx+1) cc in - eff := Declareops.union_side_effects eff' !eff; + eff := Safe_typing.concat_private eff' !eff; Array.set eqs ndx (mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] @@ -288,7 +287,7 @@ let build_beq_scheme mode kn = let names = Array.make nb_ind Anonymous and types = Array.make nb_ind mkSet and cores = Array.make nb_ind mkSet in - let eff = ref Declareops.no_seff in + let eff = ref Safe_typing.empty_private_constants in let u = Univ.Instance.empty in for i=0 to (nb_ind-1) do names.(i) <- Name (Id.of_string (rec_name i)); @@ -296,7 +295,7 @@ let build_beq_scheme mode kn = (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb)); let c, eff' = make_one_eq i in cores.(i) <- c; - eff := Declareops.union_side_effects eff' !eff + eff := Safe_typing.concat_private eff' !eff done; (Array.init nb_ind (fun i -> let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in @@ -875,7 +874,7 @@ let compute_dec_tact ind lnamesparrec nparrec = Not_found -> Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.") end >>= fun (lbI,eff'') -> - let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in + let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; intros_using fresh_first_intros; @@ -942,7 +941,7 @@ let make_eq_decidability mode mind = (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in - ([|ans|], ctx), Declareops.no_seff + ([|ans|], ctx), Safe_typing.empty_private_constants let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 805a29e39..e750f0ca2 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -187,7 +187,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro Evarutil.check_evars env Evd.empty !evars termtype; let ctx = Evd.universe_context !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (Entries.ParameterEntry + (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in instance_hook k None global imps ?hook (ConstRef cst); id end diff --git a/toplevel/command.ml b/toplevel/command.ml index d75efeca1..433ef4dcc 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -169,7 +169,7 @@ let declare_definition ident (local, p, k) ce imps hook = gr | Discharge | Local | Global -> declare_global_definition ident ce local k imps in - Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r + Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r let _ = Obligations.declare_definition_ref := declare_definition @@ -178,7 +178,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = if Flags.is_program_mode () then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in - assert(Declareops.side_effects_is_empty sideff); + assert(Safe_typing.empty_private_constants = sideff); assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t @@ -1139,7 +1139,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let ctx = Evd.universe_context ?names:pl evd in ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx) fixnames fixdecls fixtypes fiximps); @@ -1169,7 +1169,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let vars = Universes.universes_of_constr (List.hd fixdecls) in - let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in diff --git a/toplevel/command.mli b/toplevel/command.mli index 94b4af9dd..a031677b4 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -26,17 +26,17 @@ val do_constraint : polymorphic -> (** {6 Hooks for Pcoq} *) -val set_declare_definition_hook : (definition_entry -> unit) -> unit -val get_declare_definition_hook : unit -> (definition_entry -> unit) +val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit +val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit) (** {6 Definitions/Let} *) val interp_definition : lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits + constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Impargs.manual_implicits val declare_definition : Id.t -> definition_kind -> - definition_entry -> Impargs.manual_implicits -> + Safe_typing.private_constants definition_entry -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference val do_definition : Id.t -> definition_kind -> lident list option -> @@ -170,4 +170,4 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> - Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference + Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 7d5d61fb8..b6da21e5a 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -20,8 +20,8 @@ open Cooking (* Discharging mutual inductive *) let detype_param = function - | (Name id,None,p) -> id, Entries.LocalAssum p - | (Name id,Some p,_) -> id, Entries.LocalDef p + | (Name id,None,p) -> id, LocalAssum p + | (Name id,Some p,_) -> id, LocalDef p | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable") (* Replace diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 218c47b28..dde801a7f 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -29,9 +29,9 @@ open Pp (* Registering schemes in the environment *) type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants type 'a scheme_kind = string @@ -124,7 +124,9 @@ let define internal id c p univs = let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in let entry = { - const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff); + const_entry_body = + Future.from_val ((c,Univ.ContextSet.empty), + Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_type = None; const_entry_polymorphic = p; @@ -148,8 +150,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; - const, Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff + const, Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -168,8 +170,8 @@ let define_mutual_scheme_base kind suff f mode names mind = let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, - Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme + Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) (Array.to_list schemes)) eff @@ -181,10 +183,10 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme + s, Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind, s]) - Declareops.no_seff + Safe_typing.empty_private_constants let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = try find_scheme_on_env_too kind ind diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index d0844dd94..abd951c31 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -20,9 +20,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants (** Main functions to register a scheme builder *) @@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string -> val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> constant * Declareops.side_effects + Id.t option -> inductive -> constant * Safe_typing.private_constants val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects + (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index ae8ee7670..0b021254e 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -371,7 +371,7 @@ let do_mutual_induction_scheme lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in (* let decltype = refresh_universes decltype in *) - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in + let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref in @@ -469,7 +469,7 @@ let do_combined_scheme name schemes = schemes in let body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in + let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ)); fixpoint_message None [snd name] diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 665926922..e488f84f8 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -541,7 +541,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff) +let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants) let declare_mutual_definition l = let len = List.length l in @@ -619,7 +619,7 @@ let declare_obligation prg obl body ty uctx = shrink_body body else [], body, [||] in let ce = - { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff); + { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_type = if List.is_empty ctx then ty else None; const_entry_polymorphic = poly; @@ -796,12 +796,12 @@ let solve_by_tac name evi t poly ctx = let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in - let entry = Term_typing.handle_entry_side_effects env entry in - let body, eff = Future.force entry.Entries.const_entry_body in - assert(Declareops.side_effects_is_empty eff); + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, eff = Future.force entry.const_entry_body in + assert(Safe_typing.empty_private_constants = eff); let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); - (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx' + (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 40f124ca3..61a8ee520 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -17,11 +17,11 @@ open Decl_kinds (** Forward declaration. *) val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> - Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref + Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref val declare_definition_ref : (Id.t -> definition_kind -> - Entries.definition_entry -> Impargs.manual_implicits + Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits -> global_reference Lemmas.declaration_hook -> global_reference) ref val check_evars : env -> evar_map -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 60fe76bb8..b1be4c92a 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -160,8 +160,8 @@ let degenerate_decl (na,b,t) = | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match b with - | None -> (id, Entries.LocalAssum t) - | Some b -> (id, Entries.LocalDef b) + | None -> (id, LocalAssum t) + | Some b -> (id, LocalDef b) type record_error = | MissingProj of Id.t * Id.t list @@ -297,7 +297,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field try let entry = { const_entry_body = - Future.from_val (Term_typing.mk_pure_proof proj); + Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; -- cgit v1.2.3 From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 12:36:20 -0400 Subject: Univs: local names handling. Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. --- library/universes.ml | 16 +++++ library/universes.mli | 10 ++- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/merge.ml | 4 +- plugins/funind/recdef.ml | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- pretyping/evd.ml | 30 ++++++--- pretyping/evd.mli | 6 +- printing/prettyp.ml | 38 +++++++----- printing/printer.ml | 8 +-- printing/printer.mli | 4 +- printing/printmod.ml | 38 +++++++----- tactics/leminv.ml | 3 +- tactics/rewrite.ml | 4 +- toplevel/class.ml | 2 +- toplevel/classes.ml | 4 +- toplevel/command.ml | 89 +++++++++++++++------------ toplevel/command.mli | 13 ++-- toplevel/indschemes.ml | 2 +- toplevel/record.ml | 11 ++-- toplevel/vernacentries.ml | 4 +- 21 files changed, 180 insertions(+), 112 deletions(-) (limited to 'library') diff --git a/library/universes.ml b/library/universes.ml index 30d38eb2a..6cccb10ef 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -12,7 +12,9 @@ open Names open Term open Environ open Univ +open Globnames +(** Global universe names *) type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t @@ -27,6 +29,20 @@ let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd !global_universes)) with Not_found -> Level.pr l +(** Local universe names of polymorphic references *) + +type universe_binders = (Id.t * Univ.universe_level) list + +let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" + +let universe_binders_of_global ref = + try + let l = Refmap.find ref !universe_binders_table in l + with Not_found -> [] + +let register_universe_binders ref l = + universe_binders_table := Refmap.add ref l !universe_binders_table + (* To disallow minimization to Set *) let set_minimization = ref true diff --git a/library/universes.mli b/library/universes.mli index 4ff21d45c..45672ef46 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -14,9 +14,10 @@ open Univ val set_minimization : bool ref val is_set_minimization : unit -> bool - + (** Universes *) +(** Global universe name <-> level mapping *) type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t @@ -25,6 +26,13 @@ val set_global_universe_names : universe_names -> unit val pr_with_global_universes : Level.t -> Pp.std_ppcmds +(** Local universe name <-> level mapping *) + +type universe_binders = (Id.t * Univ.universe_level) list + +val register_universe_binders : Globnames.global_reference -> universe_binders -> unit +val universe_binders_of_global : Globnames.global_reference -> universe_binders + (** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c43932324..c47602bda 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -330,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in ignore( Declare.declare_constant name diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 60c58730a..e3455e770 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -884,10 +884,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,impls = Command.interp_mutual_inductive indl [] + let mie,pl,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie impls) + ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca0b9c5fe..5d41ec723 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1509,7 +1509,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = fst (*FIXME*)(interp_constr diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 1c4ba8823..c7185ff25 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd + Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0593bbca8..36d9c25fd 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -356,6 +356,16 @@ let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_loca let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx } let evar_universe_context_subst ctx = ctx.uctx_univ_variables +let add_uctx_names s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l s names_rev) + +let evar_universe_context_of_binders b = + let ctx = empty_evar_universe_context in + let names = + List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc) + ctx.uctx_names b + in { ctx with uctx_names = names } + let instantiate_variable l b v = v := Univ.LMap.add l (Some b) !v @@ -965,19 +975,19 @@ let pr_uctx_level uctx = let universe_context ?names evd = match names with - | None -> Univ.ContextSet.to_context evd.universes.uctx_local + | None -> [], Univ.ContextSet.to_context evd.universes.uctx_local | Some pl -> let levels = Univ.ContextSet.levels evd.universes.uctx_local in - let newinst, left = + let newinst, map, left = List.fold_right - (fun (loc,id) (newinst, acc) -> + (fun (loc,id) (newinst, map, acc) -> let l = try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names) with Not_found -> user_err_loc (loc, "universe_context", str"Universe " ++ pr_id id ++ str" is not bound anymore.") - in (l :: newinst, Univ.LSet.remove l acc)) - pl ([], levels) + in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) + pl ([], [], levels) in if not (Univ.LSet.is_empty left) then let n = Univ.LSet.cardinal left in @@ -985,8 +995,11 @@ let universe_context ?names evd = (str(CString.plural n "Universe") ++ spc () ++ Univ.LSet.pr (pr_uctx_level evd.universes) left ++ spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") - else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst), - Univ.ContextSet.constraints evd.universes.uctx_local) + else + let inst = Univ.Instance.of_array (Array.of_list newinst) in + let ctx = Univ.UContext.make (inst, + Univ.ContextSet.constraints evd.universes.uctx_local) + in map, ctx let restrict_universe_context evd vars = let uctx = evd.universes in @@ -1044,9 +1057,6 @@ let emit_universe_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in List.fold_left (merge_uctx true univ_rigid) u uctxs -let add_uctx_names s l (names, names_rev) = - (UNameMap.add s l names, Univ.LMap.add l s names_rev) - let uctx_new_univ_variable rigid name predicative ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 9379b50b5..3c16b27ad 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -487,6 +487,9 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst +val evar_universe_context_of_binders : + Universes.universe_binders -> evar_universe_context + val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map (** Raises Not_found if not a name for a universe in this map. *) @@ -534,7 +537,8 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context +val universe_context : ?names:(Id.t located) list -> evar_map -> + (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> Univ.universes diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 7e625af0d..84649e6eb 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,12 +73,15 @@ let print_ref reduce ref = in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in + let env = Global.env () in + let bl = Universes.universe_binders_of_global ref in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let inst = - if Global.is_polymorphic ref then Printer.pr_universe_instance univs + if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () in - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype typ ++ - Printer.pr_universe_ctx univs) + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ + Printer.pr_universe_ctx sigma univs) (********************************) (** Printing implicit arguments *) @@ -467,18 +470,19 @@ let gallina_print_section_variable id = print_named_decl id ++ with_line_skip (print_name_infos (VarRef id)) -let print_body = function - | Some c -> pr_lconstr c +let print_body env evd = function + | Some c -> pr_lconstr_env env evd c | None -> (str"") -let print_typed_body (val_0,typ) = - (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ) +let print_typed_body env evd (val_0,typ) = + (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t -let print_instance cb = - if cb.const_polymorphic then pr_universe_instance cb.const_universes +let print_instance sigma cb = + if cb.const_polymorphic then + pr_universe_instance sigma cb.const_universes else mt() let print_constant with_values sep sp = @@ -489,17 +493,23 @@ let print_constant with_values sep sp = let univs = Univ.instantiate_univ_context (Global.universes_of_constant_body cb) in + let ctx = + Evd.evar_universe_context_of_binders + (Universes.universe_binders_of_global (ConstRef sp)) + in + let env = Global.env () and sigma = Evd.from_ctx ctx in + let pr_ltype = pr_ltype_env env sigma in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> str"*** [ " ++ - print_basename sp ++ print_instance cb ++ str " : " ++ cut () ++ pr_ltype typ ++ + print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_universe_ctx univs + Printer.pr_universe_ctx sigma univs | _ -> - print_basename sp ++ print_instance cb ++ str sep ++ cut () ++ - (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ - Printer.pr_universe_ctx univs) + print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ + (if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++ + Printer.pr_universe_ctx sigma univs) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ diff --git a/printing/printer.ml b/printing/printer.ml index f4852b108..202b4f2bc 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -208,10 +208,10 @@ let safe_pr_constr t = let (sigma, env) = get_current_context () in safe_pr_constr_env env sigma t -let pr_universe_ctx c = +let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context Universes.pr_with_global_universes c)) c + (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c else mt() @@ -825,7 +825,7 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () -let pr_universe_instance ctx = +let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}" + str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}" diff --git a/printing/printer.mli b/printing/printer.mli index 25a4aa166..0a44e4f10 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -84,8 +84,8 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds -val pr_universe_instance : Univ.universe_context -> std_ppcmds -val pr_universe_ctx : Univ.universe_context -> std_ppcmds +val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 8031de27d..1d275c1aa 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -72,10 +72,10 @@ let print_params env sigma params = if List.is_empty params then mt () else Printer.pr_rel_context env sigma params ++ brk(1,2) -let print_constructors envpar names types = +let print_constructors envpar sigma names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c) + (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -83,7 +83,7 @@ let print_constructors envpar names types = let build_ind_type env mip = Inductive.type_of_inductive env mip -let print_one_inductive env mib ((_,i) as ind) = +let print_one_inductive env sigma mib ((_,i) as ind) = let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in @@ -95,13 +95,14 @@ let print_one_inductive env mib ((_,i) as ind) = let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in let inst = - if mib.mind_polymorphic then Printer.pr_universe_instance mib.mind_universes + if mib.mind_polymorphic then + Printer.pr_universe_instance sigma mib.mind_universes else mt () in hov 0 ( - pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ - brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes + pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ + brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) @@ -113,11 +114,13 @@ let print_mutual_inductive env mind mib = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in + let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env mib) inds ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + (print_one_inductive env sigma mib) inds ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -146,6 +149,8 @@ let print_record env mind mib = let cstrtype = hnf_prod_applist env cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in + let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = let open Decl_kinds in match mib.mind_finite with @@ -157,16 +162,16 @@ let print_record env mind mib = hov 0 ( Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ - print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++ + print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ str ":= " ++ pr_id mip.mind_consnames.(0)) ++ brk(1,2) ++ hv 2 (str "{ " ++ prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then @@ -267,6 +272,7 @@ let print_body is_impl env mp (l,body) = if cb.const_polymorphic then Univ.UContext.instance cb.const_universes else Univ.Instance.empty in + let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -275,17 +281,17 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) + hov 0 (Printer.pr_ltype_env env sigma (Vars.subst_instance_constr u (Typeops.type_of_constant_type env cb.const_type))) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env Evd.empty + Printer.pr_lconstr_env env sigma (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context cb.const_universes)) + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes)) | SFBmind mib -> try let env = Option.get env in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 42d22bc3c..8ca622171 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -229,7 +229,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = let add_inversion_lemma name env sigma t sort dep inv_op = let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in - let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in + let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) + ~univs:(snd ctx) invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 081170869..e8a7c0f60 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1806,9 +1806,9 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in + let pl, ctx = Evd.universe_context sigma in let cst = - Declare.definition_entry ~types:typ ~poly - ~univs:(Evd.universe_context sigma) term + Declare.definition_entry ~types:typ ~poly ~univs:ctx term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) diff --git a/toplevel/class.ml b/toplevel/class.ml index f925a2d07..da6624032 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -225,7 +225,7 @@ let build_id_coercion idf_opt source poly = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs:(Evd.universe_context sigma) + (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma)) ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index e750f0ca2..c354c7d32 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -185,7 +185,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro nf t in Evarutil.check_evars env Evd.empty !evars termtype; - let ctx = Evd.universe_context !evars in + let pl, ctx = Evd.universe_context !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) @@ -381,7 +381,7 @@ let context poly l = let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in let nstatus = - pi3 (Command.declare_assumption false decl (t, !uctx) [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl Vernacexpr.NoInline (Loc.ghost, id)) in let () = uctx := Univ.ContextSet.empty in diff --git a/toplevel/command.ml b/toplevel/command.ml index 433ef4dcc..73fd3d1a4 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -83,7 +83,7 @@ let interp_definition pl bl p red_option c ctypopt = let evdref = ref (Evd.from_ctx ctx) in let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in let nb_args = List.length ctx in - let imps,ce = + let imps,pl,ce = match ctypopt with None -> let subst = evd_comb0 Evd.nf_univ_variables evdref in @@ -94,8 +94,8 @@ let interp_definition pl bl p red_option c ctypopt = let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Universes.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.universe_context ?names:pl evd in - imps1@(Impargs.lift_implicits nb_args imps2), + let pl, uctx = Evd.universe_context ?names:pl evd in + imps1@(Impargs.lift_implicits nb_args imps2), pl, definition_entry ~univs:uctx ~poly:p body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in @@ -120,14 +120,14 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Universes.universes_of_constr body) (Universes.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.universe_context ?names:pl ctx in - imps1@(Impargs.lift_implicits nb_args impsty), + let pl, uctx = Evd.universe_context ?names:pl ctx in + imps1@(Impargs.lift_implicits nb_args impsty), pl, definition_entry ~types:typ ~poly:p ~univs:uctx body in - red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, imps + red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, pl, imps -let check_definition (ce, evd, imps) = +let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); ce @@ -140,11 +140,12 @@ let get_locality id = function | Local -> true | Global -> false -let declare_global_definition ident ce local k imps = +let declare_global_definition ident ce local k pl imps = let local = get_locality ident local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in + let () = Universes.register_universe_binders gr pl in let () = definition_message ident in gr @@ -152,7 +153,7 @@ let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook -let declare_definition ident (local, p, k) ce imps hook = +let declare_definition ident (local, p, k) ce pl imps hook = let () = !declare_definition_hook ce in let r = match local with | Discharge when Lib.sections_are_opened () -> @@ -168,13 +169,14 @@ let declare_definition ident (local, p, k) ce imps hook = in gr | Discharge | Local | Global -> - declare_global_definition ident ce local k imps in + declare_global_definition ident ce local k pl imps in Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r -let _ = Obligations.declare_definition_ref := declare_definition +let _ = Obligations.declare_definition_ref := + (fun i k c imps hook -> declare_definition i k c [] imps hook) let do_definition ident k pl bl red_option c ctypopt hook = - let (ce, evd, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in + let (ce, evd, pl, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in if Flags.is_program_mode () then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in @@ -192,13 +194,14 @@ let do_definition ident k pl bl red_option c ctypopt hook = ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(declare_definition ident k ce imps + ignore(declare_definition ident k ce pl imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = match local with +let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = +match local with | Discharge when Lib.sections_are_opened () -> let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in @@ -225,6 +228,7 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in + let () = Universes.register_universe_binders gr pl in let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr local p in @@ -241,11 +245,11 @@ let interp_assumption evdref env impls bl c = let ctx = Evd.universe_context_set evd in ((nf ty, ctx), impls) -let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl = +let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = let refs, status, _ = List.fold_left (fun (refs,status,ctx) id -> let ref',u',status' = - declare_assumption is_coe k (c,ctx) imps impl_is_on nl id in + declare_assumption is_coe k (c,ctx) pl imps impl_is_on nl id in (ref',u')::refs, status' && status, Univ.ContextSet.empty) ([],true,ctx) idl in @@ -277,7 +281,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let l = List.map (on_pi2 (nf_evar evd)) l in snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in + let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs @@ -293,9 +297,9 @@ let do_assumptions_bound_univs coe kind nl id pl c = let ty = nf ty in let vars = Universes.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.universe_context ?names:pl evd in + let pl, uctx = Evd.universe_context ?names:pl evd in let uctx = Univ.ContextSet.of_context uctx in - let (_, _, st) = declare_assumption coe kind (ty, uctx) impls false nl id in + let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in st let do_assumptions kind nl l = match l with @@ -314,7 +318,8 @@ let do_assumptions kind nl l = match l with | None -> id | Some _ -> let loc = fst id in - let msg = Pp.str "Assumptions with bound universes can only be defined once at a time." in + let msg = + Pp.str "Assumptions with bound universes can only be defined one at a time." in user_err_loc (loc, "", msg) in (coe, (List.map map idl, c)) @@ -587,7 +592,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = map_rel_context nf ctx_params in let evd = !evdref in - let uctx = Evd.universe_context ?names:pl evd in + let pl, uctx = Evd.universe_context ?names:pl evd in List.iter (check_evars env_params Evd.empty evd) arities; iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -616,7 +621,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; mind_entry_universes = uctx }, - impls + pl, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -665,7 +670,7 @@ let is_recursive mie = List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc | _ -> false -let declare_mutual_inductive_with_eliminations mie impls = +let declare_mutual_inductive_with_eliminations mie pl impls = (* spiwack: raises an error if the structure is supposed to be non-recursive, but isn't *) begin match mie.mind_entry_finite with @@ -680,12 +685,15 @@ let declare_mutual_inductive_with_eliminations mie impls = let (_, kn), prim = declare_mind mie in let mind = Global.mind_of_delta_kn kn in List.iteri (fun i (indimpls, constrimpls) -> - let ind = (mind,i) in - maybe_declare_manual_implicits false (IndRef ind) indimpls; - List.iteri - (fun j impls -> - maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) - constrimpls) + let ind = (mind,i) in + let gr = IndRef ind in + maybe_declare_manual_implicits false gr indimpls; + Universes.register_universe_binders gr pl; + List.iteri + (fun j impls -> + maybe_declare_manual_implicits false + (ConstructRef (ind, succ j)) impls) + constrimpls) impls; let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in if_verbose msg_info (minductive_message warn_prim names); @@ -700,14 +708,14 @@ type one_inductive_impls = let do_mutual_inductive indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,impls = interp_mutual_inductive indl ntns poly prv finite in + let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in (* Declare the mutual inductive block with its associated schemes *) - ignore (declare_mutual_inductive_with_eliminations mie impls); + ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes - + (* 3c| Fixpoints and co-fixpoints *) (* An (unoptimized) function that maps preorders to partial orders... @@ -811,11 +819,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps = +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in - declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r)) + declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) -let _ = Obligations.declare_fix_ref := declare_fix +let _ = Obligations.declare_fix_ref := + (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -1003,7 +1012,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let hook l gr = let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in - let univs = Evd.universe_context !evdref in + let pl, univs = Evd.universe_context !evdref in (*FIXME poly? *) let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in (** FIXME: include locality *) @@ -1140,8 +1149,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - let ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx) + let pl, ctx = Evd.universe_context ?names:pl evd in + ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -1173,8 +1182,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) + let pl, ctx = Evd.universe_context ?names:pl evd in + ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames diff --git a/toplevel/command.mli b/toplevel/command.mli index a031677b4..8e2d9c6fc 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -33,10 +33,11 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit val interp_definition : lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> - constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Impargs.manual_implicits + constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * + Universes.universe_binders * Impargs.manual_implicits val declare_definition : Id.t -> definition_kind -> - Safe_typing.private_constants definition_entry -> Impargs.manual_implicits -> + Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference val do_definition : Id.t -> definition_kind -> lident list option -> @@ -53,7 +54,7 @@ val do_definition : Id.t -> definition_kind -> lident list option -> nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> - Impargs.manual_implicits -> + Universes.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> global_reference * Univ.Instance.t * bool @@ -92,13 +93,13 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> - mutual_inductive_entry * one_inductive_impls list + mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its associated schemes *) val declare_mutual_inductive_with_eliminations : - mutual_inductive_entry -> one_inductive_impls list -> + mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> mutual_inductive (** Entry points for the vernacular commands Inductive and CoInductive *) @@ -169,5 +170,5 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit -val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> +val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 0b021254e..f16e6e3f3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -129,7 +129,7 @@ let define id internal ctx c t = const_entry_secctx = None; const_entry_type = t; const_entry_polymorphic = true; - const_entry_universes = Evd.universe_context ctx; + const_entry_universes = snd (Evd.universe_context ctx); const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/toplevel/record.ml b/toplevel/record.ml index b1be4c92a..dc2c9264b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -153,7 +153,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = let ce t = Evarutil.check_evars env0 Evd.empty evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps); List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs); - Evd.universe_context evars, nf arity, template, imps, newps, impls, newfs + Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs let degenerate_decl (na,b,t) = let id = match na with @@ -376,7 +376,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_polymorphic = poly; mind_entry_private = None; mind_entry_universes = ctx } in - let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in + let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in @@ -532,11 +532,11 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then error "Priorities only allowed for type class substructures"; (* Now, younger decl in params and fields is on top *) - let ctx, arity, template, implpars, params, implfs, fields = + let (pl, ctx), arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in - match kind with + let gr = match kind with | Class def -> let gr = declare_class finite def poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in @@ -549,3 +549,6 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind + in + Universes.register_universe_binders gr pl; + gr diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2879947a9..31bfc004a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1527,7 +1527,7 @@ let vernac_check_may_eval redexp glopt rc = let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let uctx = Evd.universe_context sigma' in + let pl, uctx = Evd.universe_context sigma' in let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = @@ -1542,7 +1542,7 @@ let vernac_check_may_eval redexp glopt rc = let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx uctx) + Printer.pr_universe_ctx sigma uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in -- cgit v1.2.3