Abstract away the implementation of side-effects in Safe_typing.

5 files changed, 27 insertions, 46 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index a3d32267a7..adb3f6bd29 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -108,21 +108,7 @@ type module_entry =
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
 
-
-type seff_env =
-  [ `Nothing
-  (* The proof term and its universes.
-     Same as the constant_body's but not in an ephemeron *)
-  | `Opaque of Constr.t * Univ.ContextSet.t ]
-
 (** Not used by the kernel. *)
 type side_effect_role =
   | Subproof
   | Schema of inductive * string
-
-type side_eff = {
-  seff_constant : Constant.t;
-  seff_body : Declarations.constant_body;
-  seff_env : seff_env;
-  seff_role : side_effect_role;
-}
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 673f025c75..7b573e3146 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -228,6 +228,12 @@ let check_engagement env expected_impredicative_set =
 
 (** {6 Stm machinery } *)
 
+type seff_env =
+  [ `Nothing
+  (* The proof term and its universes.
+     Same as the constant_body's but not in an ephemeron *)
+  | `Opaque of Constr.t * Univ.ContextSet.t ]
+
 let get_opaque_body env cbo =
   match cbo.const_body with
   | Undef _ -> assert false
@@ -238,9 +244,16 @@ let get_opaque_body env cbo =
         (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
+type side_eff = {
+  seff_constant : Constant.t;
+  seff_body : Declarations.constant_body;
+  seff_env : seff_env;
+  seff_role : Entries.side_effect_role;
+}
+
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
-  eff      : Entries.side_eff list;
+  eff      : side_eff list;
 }
 
 module SideEffects :
@@ -254,7 +267,6 @@ end =
 struct
 
 module SeffOrd = struct
-open Entries
 type t = side_effect
 let compare e1 e2 =
   let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in
@@ -282,6 +294,14 @@ let side_effects_of_private_constants l =
   let ans = List.rev (SideEffects.repr l) in
   List.map_append (fun { eff; _ } -> eff) ans
 
+let push_private_constants env eff =
+  let eff = side_effects_of_private_constants eff in
+  let add_if_undefined env eff =
+    try ignore(Environ.lookup_constant eff.seff_constant env); env
+    with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+  in
+  List.fold_left add_if_undefined env eff
+
 let empty_private_constants = SideEffects.empty
 let add_private mb eff effs =
   let from_env = CEphemeron.create mb in
@@ -289,7 +309,6 @@ let add_private mb eff effs =
 let concat_private = SideEffects.concat
 
 let make_eff env cst r =
-  let open Entries in
   let cbo = Environ.lookup_constant cst env.env in
   {
     seff_constant = cst;
@@ -309,7 +328,6 @@ let private_con_of_scheme ~kind env cl =
   add_private env.revstruct eff empty_private_constants
 
 let universes_of_private eff =
-  let open Entries in
   let fold acc eff =
     let acc = match eff.seff_env with
     | `Nothing -> acc
@@ -588,7 +606,6 @@ let add_constant_aux ~in_section senv (kn, cb) =
 let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty
 
 let inline_side_effects env body side_eff =
-  let open Entries in
   let open Constr in
   (** First step: remove the constants that are still in the environment *)
   let filter { eff = se; from_env = mb } =
@@ -725,7 +742,6 @@ let constant_entry_of_side_effect cb u =
     const_entry_inline_code = cb.const_inline_code }
 
 let turn_direct orig =
-  let open Entries in
   let cb = orig.seff_body in
   if Declareops.is_opaque cb then
     let p = match orig.seff_env with
@@ -738,7 +754,6 @@ let turn_direct orig =
   else orig
 
 let export_eff eff =
-  let open Entries in
   (eff.seff_constant, eff.seff_body, eff.seff_role)
 
 let export_side_effects mb env c =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46c97c1fb8..6fcdef9a10 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,11 +43,6 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 
 type private_constants
 
-val side_effects_of_private_constants :
-  private_constants -> Entries.side_eff list
-(** Return the list of individual side-effects in the order of their
-    creation. *)
-
 val empty_private_constants : private_constants
 val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
@@ -62,6 +57,9 @@ val inline_private_constants_in_constr :
 val inline_private_constants_in_definition_entry :
   Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
+val push_private_constants : Environ.env -> private_constants -> Environ.env
+(** Push the constants in the environment if not already there. *)
+
 val universes_of_private : private_constants -> Univ.ContextSet.t list
 
 val is_curmod_library : safe_environment -> bool
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 06e6b89df1..4a9404aa96 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -44,17 +44,6 @@ let typecheck_evar ev env sigma =
   let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
   sigma
 
-(* Get the side-effect's constant declarations to update the monad's
-  * environmnent *)
-let add_if_undefined env eff =
-  let open Entries in
-  try ignore(Environ.lookup_constant eff.seff_constant env); env
-  with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
-
-(* Add the side effects to the monad's environment, if not already done. *)
-let add_side_effects env eff =
-  List.fold_left add_if_undefined env eff
-
 let generic_refine ~typecheck f gl =
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
@@ -71,8 +60,7 @@ let generic_refine ~typecheck f gl =
   let evs = Evd.save_future_goals sigma in
   (* Redo the effects in sigma in the monad's env *)
   let privates_csts = Evd.eval_side_effects sigma in
-  let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
-  let env = add_side_effects env sideff in
+  let env = Safe_typing.push_private_constants env privates_csts in
   (* Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1c7cc5e636..fe895098c0 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -75,13 +75,7 @@ let adjust_guardness_conditions const = function
 	  List.interval 0 (List.length ((lam_assum c))))
 	  lemma_guard (Array.to_list fixdefs) in
 *)
-              let fold env eff =
-                try
-                  let _ = Environ.lookup_constant eff.seff_constant env in
-                  env
-                with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
-              in
-              let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in
+              let env = Safe_typing.push_private_constants env eff in
               let indexes =
                 search_guard env
                   possible_indexes fixdecls in