Merge PR #10151: Clean up the API for side-effects

Reviewed-by: SkySkimmer
Ack-by: gares

10 files changed, 87 insertions, 141 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/modops.ml b/kernel/modops.ml
index 4f992d3972..4fdd7ab334 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -608,11 +608,7 @@ let clean_bounded_mod_expr sign =
 (** {6 Stm machinery } *)
 let join_constant_body except otab cb =
   match cb.const_body with
-  | OpaqueDef o ->
-      (match Opaqueproof.uuid_opaque otab o with
-      | Some uuid when not(Future.UUIDSet.mem uuid except) ->
-          Opaqueproof.join_opaque otab o
-      | _ -> ())
+  | OpaqueDef o -> Opaqueproof.join_opaque ~except otab o
   | _ -> ()
 
 let join_structure except otab s =
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 303cb06c55..57059300b8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -87,19 +87,18 @@ let discharge_direct_opaque ~cook_constr ci = function
   | Direct (d,cu) ->
       Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
 
-let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> ignore(Future.join cu)
+let join except cu = match except with
+| None -> ignore (Future.join cu)
+| Some except ->
+  if Future.UUIDSet.mem (Future.uuid cu) except then ()
+  else ignore (Future.join cu)
+
+let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
+  | Direct (_,cu) -> join except cu
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
         let fp = snd (Int.Map.find i prfs) in
-        ignore(Future.join fp)
-
-let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Some (Future.uuid cu)
-  | Indirect (_,dp,i) ->
-      if DirPath.equal dp odp
-      then Some (Future.uuid (snd (Int.Map.find i prfs)))
-      else None
+        join except fp
 
 let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
@@ -128,16 +127,6 @@ let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
       then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
       else !get_univ dp i
 
-let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Future.chain cu fst
-  | Indirect (l,dp,i) ->
-      let pt =
-        if DirPath.equal dp odp
-        then Future.chain (snd (Int.Map.find i prfs)) fst
-        else !get_opaque dp i in
-      Future.chain pt (fun c ->
-        force_constr (List.fold_right subst_substituted l (from_val c)))
- 
 module FMap = Future.UUIDMap
 
 let a_constr = Future.from_val (mkRel 1)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5ea6da649b..d47c0bbb3c 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,7 +39,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val get_proof : opaquetab -> opaque -> constr Future.computation
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
@@ -60,8 +59,7 @@ type cooking_info = {
 val discharge_direct_opaque :
   cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
 
-val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
-val join_opaque : opaquetab -> opaque -> unit
+val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : opaquetab ->
   Constr.t Future.computation array *
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 673f025c75..75375812c0 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
@@ -240,7 +246,10 @@ let get_opaque_body env cbo =
 
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
-  eff      : Entries.side_eff list;
+  seff_constant : Constant.t;
+  seff_body : Declarations.constant_body;
+  seff_env : seff_env;
+  seff_role : Entries.side_effect_role;
 }
 
 module SideEffects :
@@ -254,11 +263,9 @@ 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
-  List.compare cmp e1.eff e2.eff
+  Constant.CanOrd.compare e1.seff_constant e2.seff_constant
 end
 
 module SeffSet = Set.Make(SeffOrd)
@@ -279,37 +286,37 @@ end
 type private_constants = SideEffects.t
 
 let side_effects_of_private_constants l =
-  let ans = List.rev (SideEffects.repr l) in
-  List.map_append (fun { eff; _ } -> eff) ans
+  List.rev (SideEffects.repr l)
+
+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
-  SideEffects.add { eff; from_env } effs
 let concat_private = SideEffects.concat
 
-let make_eff env cst r =
-  let open Entries in
+let private_constant env role cst =
+  (** The constant must be the last entry of the safe environment *)
+  let () = match env.revstruct with
+  | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst))
+  | _ -> assert false
+  in
+  let from_env = CEphemeron.create env.revstruct in
   let cbo = Environ.lookup_constant cst env.env in
-  {
+  let eff = {
+    from_env = from_env;
     seff_constant = cst;
     seff_body = cbo;
     seff_env = get_opaque_body env.env cbo;
-    seff_role = r;
-  }
-
-let private_con_of_con env c =
-  let open Entries in
-  let eff = [make_eff env c Subproof] in
-  add_private env.revstruct eff empty_private_constants
-
-let private_con_of_scheme ~kind env cl =
-  let open Entries in
-  let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in
-  add_private env.revstruct eff empty_private_constants
+    seff_role = role;
+  } in
+  SideEffects.add 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,22 +595,17 @@ 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 } =
-    let map e = (e.seff_constant, e.seff_body, e.seff_env) in
-    let cbl = List.map map se in
-    let not_exists (c,_,_) =
-      try ignore(Environ.lookup_constant c env); false
-      with Not_found -> true in
-    let cbl = List.filter not_exists cbl in
-    (cbl, mb)
+  let filter e =
+    let cb = (e.seff_constant, e.seff_body, e.seff_env) in
+    try ignore (Environ.lookup_constant e.seff_constant env); None
+    with Not_found -> Some (cb, e.from_env)
   in
   (* CAVEAT: we assure that most recent effects come first *)
-  let side_eff = List.map filter (SideEffects.repr side_eff) in
-  let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in
-  let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in
+  let side_eff = List.map_filter filter (SideEffects.repr side_eff) in
+  let sigs = List.rev_map (fun (_, mb) -> mb) side_eff in
+  let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in
   let side_eff = List.rev side_eff in
   (** Most recent side-effects first in side_eff *)
   if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs)
@@ -675,24 +677,22 @@ let inline_private_constants_in_definition_entry env ce =
 let inline_private_constants_in_constr env body side_eff =
   pi1 (inline_side_effects env body side_eff)
 
-let rec is_nth_suffix n l suf =
-  if Int.equal n 0 then l == suf
-  else match l with
-  | [] -> false
-  | _ :: l -> is_nth_suffix (pred n) l suf
+let is_suffix l suf = match l with
+| [] -> false
+| _ :: l -> l == suf
 
 (* Given the list of signatures of side effects, checks if they match.
  * I.e. if they are ordered descendants of the current revstruct.
    Returns the number of effects that can be trusted. *)
 let check_signatures curmb sl =
-  let is_direct_ancestor accu (mb, how_many) =
+  let is_direct_ancestor accu mb =
     match accu with
     | None -> None
     | Some (n, curmb) ->
         try
           let mb = CEphemeron.get mb in
-          if is_nth_suffix how_many mb curmb
-          then Some (n + how_many, mb)
+          if is_suffix mb curmb
+          then Some (n + 1, mb)
           else None
         with CEphemeron.InvalidKey -> None in
   let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
@@ -725,7 +725,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 +737,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 =
@@ -751,10 +749,9 @@ let export_side_effects mb env c =
       let not_exists e =
         try ignore(Environ.lookup_constant e.seff_constant env); false
         with Not_found -> true in
-      let aux (acc,sl) { eff = se; from_env = mb } =
-        let cbl = List.filter not_exists se in
-        if List.is_empty cbl then acc, sl
-        else cbl :: acc, (mb,List.length cbl) :: sl in
+      let aux (acc,sl) e =
+        if not (not_exists e) then acc, sl
+        else e :: acc, e.from_env :: sl in
       let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in
       let trusted = check_signatures mb signatures in
       let push_seff env eff =
@@ -772,10 +769,9 @@ let export_side_effects mb env c =
       let rec translate_seff sl seff acc env =
         match seff with
         | [] -> List.rev acc, ce
-        | cbs :: rest ->
+        | eff :: rest ->
           if Int.equal sl 0 then
-           let env, cbs =
-             List.fold_left (fun (env,cbs) eff ->
+           let env, cb =
               let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
                let ce = constant_entry_of_side_effect ocb u in
                let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
@@ -783,15 +779,14 @@ let export_side_effects mb env c =
                 seff_body = cb;
                 seff_env = `Nothing;
                } in
-               (push_seff env eff, export_eff eff :: cbs))
-             (env,[]) cbs in
-           translate_seff 0 rest (cbs @ acc) env
+               (push_seff env eff, export_eff eff)
+            in
+            translate_seff 0 rest (cb :: acc) env
           else
-           let cbs_len = List.length cbs in
-           let cbs = List.map turn_direct cbs in
-           let env = List.fold_left push_seff env cbs in
-           let ecbs = List.map export_eff cbs in
-           translate_seff (sl - cbs_len) rest (ecbs @ acc) env
+           let cb = turn_direct eff in
+           let env = push_seff env cb in
+           let ecb = export_eff cb in
+           translate_seff (sl - 1) rest (ecb :: acc) env
      in
        translate_seff trusted seff [] env
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46c97c1fb8..d6c7022cf5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,18 +43,13 @@ 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
     [e1] must be more recent than those of [e2]. *)
 
-val private_con_of_con : safe_environment -> Constant.t -> private_constants
-val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants
+val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants
+(** Constant must be the last definition of the safe_environment. *)
 
 val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
@@ -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/tactics/abstract.ml b/tactics/abstract.ml
index 7a61deba0c..499152f39a 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -174,7 +174,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in
-  let eff = private_con_of_con (Global.safe_env ()) cst in
+  let eff = private_constant (Global.safe_env ()) Entries.Subproof cst in
   let effs = concat_private eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 16829482e5..e95778a90d 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -147,9 +147,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
   let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
+  let role = Entries.Schema (ind, kind) in
+  let neff = Safe_typing.private_constant (Global.safe_env ()) role const in
   declare_scheme kind [|ind,const|];
-  const, Safe_typing.concat_private
-     (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
+  const, Safe_typing.concat_private neff eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -163,15 +164,16 @@ let define_mutual_scheme_base kind suff f mode names mind =
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
-  let consts = Array.map2 (fun id cl -> 
-     define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in
+  let fold i effs id cl =
+    let cst = define mode id cl (Declareops.inductive_is_polymorphic mib) ctx in
+    let role = Entries.Schema ((mind, i), kind)in
+    let neff = Safe_typing.private_constant (Global.safe_env ()) role cst in
+    (Safe_typing.concat_private neff effs, cst)
+  in
+  let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
-  consts,
-  Safe_typing.concat_private
-    (Safe_typing.private_con_of_scheme
-      ~kind (Global.safe_env()) (Array.to_list schemes))
-    eff 
+  consts, eff
 
 let define_mutual_scheme kind mode names mind =
   match Hashtbl.find scheme_object_table kind with
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2dae0ad125..317cf487cc 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