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.

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