Split the function used to declare side-effects from the standard one.

This ensures that side-effect declarations come with their body, in prevision
of the decoupling of the Safe_typign API for CEP 40.

9 files changed, 93 insertions, 42 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8c4bd16ae3..046ea86872 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -99,9 +99,6 @@ type primitive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
-(** Dummy wrapper type discriminable from unit *)
-type 'a seff_wrap = { seff_wrap : 'a }
-
 type constant_entry =
   | DefinitionEntry : definition_entry -> constant_entry
   | ParameterEntry : parameter_entry -> constant_entry
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 43aafac809..d2a7703648 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -572,11 +572,6 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
 
 let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
-(** Insertion of constants and parameters in environment *)
-type 'a effect_entry =
-| EffectEntry : private_constants Entries.seff_wrap effect_entry
-| PureEntry : unit effect_entry
-
 type global_declaration =
 | ConstantEntry : Entries.constant_entry -> global_declaration
 | OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
@@ -811,9 +806,9 @@ let export_private_constants ce senv =
   let senv = List.fold_left add_constant_aux senv bodies in
   (ce, exported), senv
 
-let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment =
+let add_constant l decl senv =
   let kn = Constant.make2 senv.modpath l in
-    let cb = 
+    let cb =
       match decl with
       | OpaqueEntry ce ->
         let handle env body eff =
@@ -859,10 +854,31 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
-  let eff : a = match side_effect with
-  | PureEntry -> ()
-  | EffectEntry ->
-    let body, univs = match cb.const_body with
+  kn, senv
+
+let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment =
+  let kn = Constant.make2 senv.modpath l in
+    let cb =
+      match decl with
+      | OpaqueEff ce ->
+        let handle _env body () = body, Univ.ContextSet.empty, 0 in
+        let cb, ctx = Term_typing.translate_opaque senv.env kn ce in
+        let map pf = Term_typing.check_delayed handle ctx pf in
+        let pf = Future.chain ce.Entries.opaque_entry_body map in
+        { cb with const_body = OpaqueDef pf }
+      | DefinitionEff ce ->
+        Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce)
+    in
+  let senv, cb, body = match cb.const_body with
+  | Def _ as const_body -> senv, { cb with const_body }, const_body
+  | OpaqueDef c ->
+    let senv, o = push_opaque_proof c senv in
+    senv, { cb with const_body = OpaqueDef o }, cb.const_body
+  | Undef _ | Primitive _ -> assert false
+  in
+  let senv = add_constant_aux senv (kn, cb) in
+  let eff =
+    let body, univs = match body with
     | (Primitive _ | Undef _) -> assert false
     | Def c -> (Def c, cb.const_universes)
     | OpaqueDef o ->
@@ -884,7 +900,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
       seff_constant = kn;
       seff_body = cb;
     } in
-    { Entries.seff_wrap = SideEffects.add eff empty_private_constants }
+    SideEffects.add eff empty_private_constants
   in
   (kn, eff), senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6e5c9c55ae..c60e7e893f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -73,24 +73,27 @@ val is_joined_environment : safe_environment -> bool
 
 (** Insertion of global axioms or definitions *)
 
-type 'a effect_entry =
-| EffectEntry : private_constants Entries.seff_wrap effect_entry
-| PureEntry : unit effect_entry
-
 type global_declaration =
 | ConstantEntry : Entries.constant_entry -> global_declaration
 | OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
+type side_effect_declaration =
+| DefinitionEff : Entries.definition_entry -> side_effect_declaration
+| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+
 type exported_private_constant = Constant.t
 
 val export_private_constants :
   private_constants Entries.proof_output ->
   (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
 
-(** returns the main constant plus a certificate of its validity *)
+(** returns the main constant *)
 val add_constant :
-  side_effect:'a effect_entry -> Label.t -> global_declaration ->
-    (Constant.t * 'a) safe_transformer
+  Label.t -> global_declaration -> Constant.t safe_transformer
+
+(** Similar to add_constant but also returns a certificate *)
+val add_private_constant :
+  Label.t -> side_effect_declaration -> (Constant.t * private_constants) safe_transformer
 
 (** Adding an inductive type *)
 
diff --git a/library/global.ml b/library/global.ml
index 24cfc57f28..98d3e9cb1f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -103,7 +103,8 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
-let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d)
+let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d)
+let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index d689771f0a..f8b1f35f4d 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -51,7 +51,9 @@ val export_private_constants :
   Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
 
 val add_constant :
-  side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
+  Id.t -> Safe_typing.global_declaration -> Constant.t
+val add_private_constant :
+  Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants
 val add_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index edeb27ab88..03ab0a1c13 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -149,9 +149,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     let (_, info) = CErrors.push src in
     iraise (e, info)
   in
+  let body, effs = Future.force const.Declare.proof_entry_body in
+  (* We drop the side-effects from the entry, they already exist in the ambient environment *)
+  let const = { const with Declare.proof_entry_body = Future.from_val (body, ()) } in
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
-  let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in
+  let cd = { const with Declare.proof_entry_opaque = opaque } in
   let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
@@ -172,8 +175,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   in
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
-  let effs = Evd.concat_side_effects eff
-      (snd (Future.force const.Declare.proof_entry_body)) in
+  let effs = Evd.concat_side_effects eff effs in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 719430e71c..c9da88988f 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -204,7 +204,11 @@ let cast_proof_entry e =
     const_entry_inline_code = e.proof_entry_inline_code;
   }
 
-let cast_opaque_proof_entry e =
+type 'a effect_entry =
+| EffectEntry : private_constants effect_entry
+| PureEntry : unit effect_entry
+
+let cast_opaque_proof_entry (type a) (entry : a effect_entry) (e : a proof_entry) =
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
@@ -218,8 +222,15 @@ let cast_opaque_proof_entry e =
         Id.Set.empty, Id.Set.empty
       else
         let ids_typ = global_vars_set env typ in
-        let (pf, _), eff = Future.force e.proof_entry_body in
-        let env = Safe_typing.push_private_constants env eff in
+        let pf, env = match entry with
+        | PureEntry ->
+          let (pf, _), () = Future.force e.proof_entry_body in
+          pf, env
+        | EffectEntry ->
+          let (pf, _), eff = Future.force e.proof_entry_body in
+          let env = Safe_typing.push_private_constants env eff in
+          pf, env
+        in
         let vars = global_vars_set env pf in
         ids_typ, vars
     in
@@ -247,7 +258,7 @@ let is_unsafe_typing_flags () =
   let flags = Environ.typing_flags (Global.env()) in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
-let define_constant ~side_effect ~name cd =
+let define_constant ~name cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let export, decl, unsafe = match cd with
   | DefinitionEntry de ->
@@ -264,34 +275,44 @@ let define_constant ~side_effect ~name cd =
       let map (body, eff) = body, eff.Evd.seff_private in
       let body = Future.chain de.proof_entry_body map in
       let de = { de with proof_entry_body = body } in
-      let de = cast_opaque_proof_entry de in
+      let de = cast_opaque_proof_entry EffectEntry de in
       [], OpaqueEntry de, false
   | ParameterEntry e ->
     [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
   | PrimitiveEntry e ->
     [], ConstantEntry (Entries.PrimitiveEntry e), false
   in
-  let kn, eff = Global.add_constant ~side_effect name decl in
+  let kn = Global.add_constant name decl in
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();
-  kn, eff, export
+  kn, export
 
 let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
   let () = check_exists name in
-  let kn, (), export = define_constant ~side_effect:PureEntry ~name cd in
+  let kn, export = define_constant ~name 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 ?(local = ImportDefaultBehavior) ~name ~kind cd =
-  let kn, eff, export = define_constant ~side_effect:EffectEntry ~name cd in
-  let () = assert (CList.is_empty export) in
+let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
+  let kn, eff =
+    let de =
+      if not de.proof_entry_opaque then
+        let body, () = Future.force de.proof_entry_body in
+        let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+        DefinitionEff (cast_proof_entry de)
+      else
+        let de = cast_opaque_proof_entry PureEntry de in
+        OpaqueEff de
+    in
+    Global.add_private_constant name de
+  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.Entries.seff_wrap; Evd.seff_roles; } in
+  let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
 
 (** Declaration of section variables and local definitions *)
diff --git a/tactics/declare.mli b/tactics/declare.mli
index f4bfdb1547..a6c1374a77 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -78,7 +78,7 @@ val declare_private_constant
   -> ?local:import_status
   -> name:Id.t
   -> kind:Decls.logical_kind
-  -> Evd.side_effects constant_entry
+  -> unit proof_entry
   -> Constant.t * Evd.side_effects
 
 (** Since transparent constants' side effects are globally declared, we
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 54393dce00..3f824a94bf 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,8 +124,17 @@ let define internal role id c poly univs =
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
-  let entry = Declare.definition_entry ~univs c in
-  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
+  let entry = {
+    Declare.proof_entry_body =
+      Future.from_val ((c,Univ.ContextSet.empty), ());
+    proof_entry_secctx = None;
+    proof_entry_type = None;
+    proof_entry_universes = univs;
+    proof_entry_opaque = false;
+    proof_entry_inline_code = false;
+    proof_entry_feedback = None;
+  } in
+  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
   let () = match internal with
     | InternalTacticRequest -> ()
     | _-> Declare.definition_message id