Merge PR #10334: Remove the side-effect role from the kernel.

Reviewed-by: gares

2 files changed, 39 insertions, 17 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 7de92ded59..17de06ed57 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -42,7 +42,7 @@ type constant_obj = {
   cst_locl : import_status;
 }
 
-type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
+type constant_declaration = Evd.side_effects 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 *)
@@ -140,12 +140,12 @@ let register_constant kn kind local =
 let register_side_effect (c, role) =
   let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in
   match role with
-  | Subproof -> ()
-  | Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
+  | None -> ()
+  | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|]
 
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
-    ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
+    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
@@ -154,7 +154,14 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let define_constant ?role ?(export_seff=false) id cd =
+let get_roles export eff =
+  let map c =
+    let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
+    (c, role)
+  in
+  List.map map export
+
+let define_constant ~side_effect ?(export_seff=false) id cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let is_poly de = match de.const_entry_universes with
   | Monomorphic_entry _ -> false
@@ -168,26 +175,39 @@ let define_constant ?role ?(export_seff=false) id cd =
         not de.const_entry_opaque ||
         is_poly de ->
       (* This globally defines the side-effects in the environment. *)
-      let body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in
+      let body, eff = Future.force de.const_entry_body in
+      let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
+      let export = get_roles export eff in
       let de = { de with const_entry_body = Future.from_val (body, ()) } in
       export, ConstantEntry (PureEntry, DefinitionEntry de)
-    | _ -> [], ConstantEntry (EffectEntry, cd)
+    | DefinitionEntry de ->
+      let map (body, eff) = body, eff.Evd.seff_private in
+      let body = Future.chain de.const_entry_body map in
+      let de = { de with const_entry_body = body } in
+      [], ConstantEntry (EffectEntry, DefinitionEntry de)
+    | ParameterEntry _ | PrimitiveEntry _ as cd ->
+      [], ConstantEntry (PureEntry, cd)
   in
-  let kn, eff = Global.add_constant ?role ~in_section id decl in
+  let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
   kn, eff, export
 
 let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) =
   let () = check_exists id in
-  let kn, _eff, export = define_constant ~export_seff id cd in
+  let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in
   (* Register the libobjects attached to the constants and its subproofs *)
   let () = List.iter register_side_effect export in
   let () = register_constant kn kind local in
   kn
 
-let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
-  let kn, eff, export = define_constant ~role id cd in
+let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
+  let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in
   let () = assert (List.is_empty export) in
   let () = register_constant kn kind local in
+  let seff_roles = match role with
+  | None -> Cmap.empty
+  | Some r -> Cmap.singleton kn r
+  in
+  let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
 
 let declare_definition ?(internal=UserIndividualRequest)
@@ -201,7 +221,7 @@ let declare_definition ?(internal=UserIndividualRequest)
 
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
-  | SectionLocalDef of Safe_typing.private_constants definition_entry
+  | SectionLocalDef of Evd.side_effects definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -222,7 +242,9 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let ((body, uctx), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in
+      let (body, eff) = Future.force de.const_entry_body in
+      let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
+      let eff = get_roles export eff in
       let () = List.iter register_side_effect eff in
       let poly, univs = match de.const_entry_universes with
       | Monomorphic_entry uctx -> false, uctx
diff --git a/interp/declare.mli b/interp/declare.mli
index 4120a82ca0..e2485d7cf0 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -23,7 +23,7 @@ open Decl_kinds
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of Safe_typing.private_constants definition_entry
+  | SectionLocalDef of Evd.side_effects definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -33,7 +33,7 @@ val declare_variable : variable -> variable_declaration -> Libobject.object_name
 (** Declaration of global constructions 
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
+type constant_declaration = Evd.side_effects constant_entry * logical_kind
 
 type internal_flag =
   | UserAutomaticRequest
@@ -44,7 +44,7 @@ type internal_flag =
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
   ?univs:Entries.universes_entry ->
-  ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
+  ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
@@ -56,7 +56,7 @@ val declare_constant :
  ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
 
 val declare_private_constant :
-  role:side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants
+  ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->