From 3fcf0930874d7200f2503ac7084b1d6669d59540 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Jul 2017 17:46:15 +0200 Subject: Remove a horrendous hack in Declare to retrieve exported side-effects. Instead of relying on a mutable state in the object pushed on the libstack, we export an API in the kernel that exports the side-effects of a given entry in the global environment. --- interp/declare.ml | 80 ++++++++++++++++++++++++-------------------------- kernel/safe_typing.ml | 26 +++++++--------- kernel/safe_typing.mli | 8 +++-- library/global.ml | 1 + library/global.mli | 7 +++-- 5 files changed, 61 insertions(+), 61 deletions(-) diff --git a/interp/declare.ml b/interp/declare.ml index 8cafb5f3a..d82b8f215 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -106,10 +106,7 @@ 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 + cst_was_seff : bool; } type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind @@ -150,15 +147,13 @@ let cache_constant ((sp,kn), obj) = let _,dir,_ = repr_kn kn 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 CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") 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 + Global.add_constant dir id obj.cst_decl + 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 @@ -179,7 +174,7 @@ let discharge_constant ((sp, kn), obj) = let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } + Some { obj with cst_was_seff = false; 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 = @@ -191,14 +186,13 @@ let dummy_constant cst = { cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; - cst_exported = []; - cst_was_seff = cst.cst_was_seff; + cst_was_seff = false; } let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = - declare_object_full { (default_object "CONSTANT") with +let (inConstant : constant_obj -> obj) = + declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -209,31 +203,14 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f +let update_tables c = + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c) + let declare_constant_common id cst = - 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 (PureEntry, 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; - let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in - 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 update_tables c; @@ -258,23 +235,42 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e | Monomorphic_const_entry _ -> false | Polymorphic_const_entry _ -> true in - let export = (* We deal with side effects *) + let in_section = Lib.sections_are_opened () in + let export, decl = (* We deal with side effects *) match cd with | DefinitionEntry de when export_seff || not de.const_entry_opaque || is_poly de -> - let bo = de.const_entry_body in - let _, seff = Future.force bo in - Safe_typing.empty_private_constants <> seff - | _ -> false + (** This globally defines the side-effects in the environment. We mark + exported constants as being side-effect not to redeclare them at + caching time. *) + let cd, export = Global.export_private_constants ~in_section cd in + export, ConstantEntry (PureEntry, cd) + | _ -> [], ConstantEntry (EffectEntry, cd) + in + let iter_eff (c, cd, role) = + let o = inConstant { + cst_decl = ConstantEntry (PureEntry, cd); + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + cst_was_seff = true + } in + let id = Label.to_id (pi3 (Constant.repr3 c)) in + ignore(add_leaf id o); + update_tables c; + let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in + match role with + | Safe_typing.Subproof -> () + | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] in + let () = List.iter iter_eff export in let cst = { - cst_decl = ConstantEntry (EffectEntry export,cd); + cst_decl = decl; cst_hyps = [] ; cst_kind = kind; cst_locl = local; - cst_exported = []; cst_was_seff = false; } in let kn = declare_constant_common id cst in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6dbc22395..ccd6e9cf9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -494,11 +494,10 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type 'a effect_entry = -| EffectEntry : bool -> private_constants effect_entry +| EffectEntry : private_constants effect_entry | PureEntry : unit effect_entry type global_declaration = - (* bool: export private constants *) | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe @@ -527,24 +526,21 @@ let add_constant_aux no_section senv (kn, cb) = in senv'' +let export_private_constants ~in_section ce senv = + let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in + let bodies = List.map (fun (kn, cb, _, _) -> (kn, cb)) exported in + let exported = List.map (fun (kn, _, ce, r) -> (kn, ce, r)) exported in + let no_section = not in_section in + let senv = List.fold_left (add_constant_aux no_section) senv bodies in + (ce, exported), 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 (EffectEntry true, ce) -> - let exports, ce = - Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (PureEntry, 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 (EffectEntry _, ce) -> + | ConstantEntry (EffectEntry, ce) -> Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce | ConstantEntry (PureEntry, ce) -> Term_typing.translate_constant Term_typing.Pure senv.env kn ce @@ -552,7 +548,7 @@ let add_constant dir l decl senv = 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 + kn, senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2a454400f..715226107 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -95,7 +95,7 @@ val push_named_def : (** Insertion of global axioms or definitions *) type 'a effect_entry = -| EffectEntry : bool -> private_constants effect_entry (* bool: export private constants *) +| EffectEntry : private_constants effect_entry | PureEntry : unit effect_entry type global_declaration = @@ -105,11 +105,15 @@ type global_declaration = type exported_private_constant = constant * unit Entries.constant_entry * private_constant_role +val export_private_constants : in_section:bool -> + private_constants Entries.constant_entry -> + (unit Entries.constant_entry * exported_private_constant list) safe_transformer + (** 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 * exported_private_constant list) safe_transformer + constant safe_transformer (** Adding an inductive type *) diff --git a/library/global.ml b/library/global.ml index 5b17855dc..00a3a4986 100644 --- a/library/global.ml +++ b/library/global.ml @@ -86,6 +86,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index 48bcfa989..c777691d1 100644 --- a/library/global.mli +++ b/library/global.mli @@ -34,9 +34,12 @@ val set_typing_flags : Declarations.typing_flags -> unit val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set +val export_private_constants : in_section:bool -> + Safe_typing.private_constants Entries.constant_entry -> + unit Entries.constant_entry * Safe_typing.exported_private_constant list + val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> - constant * Safe_typing.exported_private_constant list + DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive -- cgit v1.2.3