Share the role type between the implementations of side-effects.

We simply exploit a type isomorphism to remove the use of dedicated algebraic
types in the kernel which are actually not necessary.

12 files changed, 103 insertions, 158 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index e79cc60798..c6de5b2a1b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -150,8 +150,8 @@ let register_side_effect (c, role) =
   ignore(add_leaf id o);
   update_tables c;
   match role with
-  | Safe_typing.Subproof -> ()
-  | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
+  | Subproof -> ()
+  | Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
 
 let declare_constant_common id cst =
   let o = inConstant cst in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3e6c4858e0..5db5de21b4 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -292,13 +292,6 @@ let hcons_mind mib =
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_universes = hcons_mind_universes mib.mind_universes }
 
-(** {6 Stm machinery } *)
-
-let string_of_side_effect { Entries.eff } = match eff with
-  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")"
-  | Entries.SEscheme (cl,_) ->
-      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")"
-
 (** Hashconsing of modules *)
 
 let hcons_functorize hty he hself f = match f with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index fb46112ea7..7170a8b642 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -11,7 +11,6 @@
 open Declarations
 open Mod_subst
 open Univ
-open Entries
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -39,10 +38,6 @@ val constant_is_polymorphic : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
-(** Side effects *)
-
-val string_of_side_effect : side_effect -> string
-
 (** {6 Inductive types} *)
 
 val eq_recarg : recarg -> recarg -> bool
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 724ed9ec7d..493550e5e5 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -120,11 +120,18 @@ type seff_env =
      Same as the constant_body's but not in an ephemeron *)
   | `Opaque of Constr.t * Univ.ContextSet.t ]
 
-type side_eff =
-  | SEsubproof of Constant.t * Declarations.constant_body * seff_env
-  | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string
+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;
+}
 
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff;
+  eff      : side_eff list;
 }
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 12c82e20de..1547a11390 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -210,13 +210,8 @@ let get_opaque_body env cbo =
         (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
-type private_constant = Entries.side_effect
 type private_constants = Term_typing.side_effects
 
-type private_constant_role = Term_typing.side_effect_role =
-  | Subproof
-  | Schema of inductive * string
-
 let empty_private_constants = Term_typing.empty_seff
 let add_private = Term_typing.add_seff
 let concat_private = Term_typing.concat_seff
@@ -225,44 +220,43 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
 let side_effects_of_private_constants = Term_typing.uniq_seff
 
+let make_eff env cst r =
+  let open Entries in
+  let cbo = Environ.lookup_constant cst env.env in
+  {
+    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 cbo = Environ.lookup_constant c env.env in
-  { Entries.from_env = CEphemeron.create env.revstruct;
-    Entries.eff      = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
+  let open Entries in
+  let eff = [make_eff env c Subproof] in
+  let from_env = CEphemeron.create env.revstruct in
+  add_private { eff; from_env; } empty_private_constants
 
 let private_con_of_scheme ~kind env cl =
-  { Entries.from_env = CEphemeron.create env.revstruct;
-    Entries.eff      = Entries.SEscheme(
-      List.map (fun (i,c) ->
-        let cbo = Environ.lookup_constant c env.env in
-        i, c, cbo, get_opaque_body env.env cbo) cl,
-      kind) }
+  let open Entries in
+  let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in
+  let from_env = CEphemeron.create env.revstruct in
+  add_private { eff; from_env; } empty_private_constants
 
 let universes_of_private eff =
-  let open Declarations in
-  List.fold_left
-    (fun acc { Entries.eff } ->
-       match eff with
-       | Entries.SEscheme (l,s) ->
-         List.fold_left
-           (fun acc (_,_,cb,c) ->
-              let acc = match c with
-                | `Nothing -> acc
-                | `Opaque (_, ctx) -> ctx :: acc
-              in
-              match cb.const_universes with
-              | Monomorphic_const ctx ->
-                ctx :: acc
-              | Polymorphic_const _ -> acc
-           )
-           acc l
-       | Entries.SEsubproof (c, cb, e) ->
-         match cb.const_universes with
-              | Monomorphic_const ctx ->
-                ctx :: acc
-              | Polymorphic_const _ -> acc
-    )
-    [] (Term_typing.uniq_seff eff)
+  let open Entries in
+  let fold acc { eff } =
+    let fold acc eff =
+      let acc = match eff.seff_env with
+      | `Nothing -> acc
+      | `Opaque (_, ctx) -> ctx :: acc
+      in
+      match eff.seff_body.const_universes with
+      | Monomorphic_const ctx -> ctx :: acc
+      | Polymorphic_const _ -> acc
+    in
+    List.fold_left fold acc eff
+  in
+  List.fold_left fold [] (Term_typing.uniq_seff eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
@@ -489,7 +483,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  Constant.t * private_constant_role
+  Constant.t * Entries.side_effect_role
 
 let add_constant_aux no_section senv (kn, cb) =
   let l = pi3 (Constant.repr3 kn) in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 4078a9092d..c8df57911f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -41,29 +41,20 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 
 (** {6 Stm machinery } *)
 
-type private_constant
 type private_constants
 
-type private_constant_role =
-  | Subproof
-  | Schema of inductive * string
-
 val side_effects_of_private_constants :
   private_constants -> Entries.side_effect list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
 val empty_private_constants : private_constants
-val add_private : private_constant -> private_constants -> private_constants
-(** Add a constant to a list of private constants. The former must be more
-    recent than all constants appearing in the latter, i.e. one should not
-    create a dependency cycle. *)
 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_constant
-val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant
+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 mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
@@ -105,7 +96,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  Constant.t * private_constant_role
+  Constant.t * Entries.side_effect_role
 
 val export_private_constants : in_section:bool ->
   private_constants Entries.definition_entry ->
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index bad4497312..79511e4253 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -27,17 +27,6 @@ module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
-let equal_eff e1 e2 =
-  let open Entries in
-  match e1, e2 with
-  | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } ->
-        Names.Constant.equal c1 c2
-  | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } ->
-        CList.for_all2eq
-          (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2)
-          cl1 cl2
-  | _ -> false
-
 module SideEffects :
 sig
   type t
@@ -48,17 +37,11 @@ sig
 end =
 struct
 
-let compare_seff e1 e2 = match e1, e2 with
-| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2
-| SEscheme (cl1, _), SEscheme (cl2, _) ->
-  let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in
-  CList.compare cmp cl1 cl2
-| SEsubproof _, SEscheme _ -> -1
-| SEscheme _, SEsubproof _ -> 1
-
 module SeffOrd = struct
 type t = side_effect
-let compare e1 e2 = compare_seff e1.eff e2.eff
+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
 end
 
 module SeffSet = Set.Make(SeffOrd)
@@ -94,11 +77,8 @@ let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
 let inline_side_effects env body ctx side_eff =
   (** First step: remove the constants that are still in the environment *)
   let filter { eff = se; from_env = mb } =
-    let cbl = match se with
-    | SEsubproof (c, cb, b) -> [c, cb, b]
-    | SEscheme (cl,_) ->
-      List.map (fun (_, c, cb, b) -> c, cb, b) cl
-    in
+    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 
@@ -468,58 +448,50 @@ let constant_entry_of_side_effect cb u =
     const_entry_inline_code = cb.const_inline_code }
 ;;
 
-let turn_direct (kn,cb,u,r as orig) =
-  match cb.const_body, u with
-  | OpaqueDef _, `Opaque (b,c) ->
-      let pt = Future.from_val (b,c) in
-      kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r
-   | _ -> orig
-;;
-
-type side_effect_role =
-  | Subproof
-  | Schema of inductive * string
+let turn_direct orig =
+  let cb = orig.seff_body in
+  if Declareops.is_opaque cb then
+    let p = match orig.seff_env with
+    | `Opaque (b, c) -> (b, c)
+    | _ -> assert false
+    in
+    let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
+    let cb = { cb with const_body } in
+    { orig with seff_body = cb }
+  else orig
 
 type exported_side_effect = 
   Constant.t * constant_body * side_effect_role
 
+let export_eff eff =
+  (eff.seff_constant, eff.seff_body, eff.seff_role)
+
 let export_side_effects mb env c =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = { c with
         const_entry_body = Future.chain body
           (fun (b_ctx, _) -> b_ctx, ()) } in
-      let not_exists (c,_,_,_) =
-        try ignore(Environ.lookup_constant c env); false
+      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 = match se with
-          | SEsubproof (c,cb,b) -> [c,cb,b,Subproof]
-          | SEscheme (cl,k) ->
-              List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in
-        let cbl = List.filter not_exists cbl in
-        if cbl = [] then acc, sl
+        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 seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in
       let trusted = check_signatures mb signatures in
-      let push_seff env = function
-        | kn, cb, `Nothing, _ ->
-          begin
-            let env = Environ.add_constant kn cb env in
-            match cb.const_universes with
-            | Monomorphic_const ctx ->
-              Environ.push_context_set ~strict:true ctx env
-            | Polymorphic_const _ -> env
-          end
-        | kn, cb, `Opaque(_, ctx), _ ->
-          begin
-            let env = Environ.add_constant kn cb env in
-            match cb.const_universes with
-            | Monomorphic_const cstctx ->
-              let env = Environ.push_context_set ~strict:true cstctx env in
-              Environ.push_context_set ~strict:true ctx env
-            | Polymorphic_const _ -> env
-          end
+      let push_seff env eff =
+        let { seff_constant = kn; seff_body = cb } = eff in
+        let env = Environ.add_constant kn cb env in
+        match cb.const_universes with
+        | Polymorphic_const _ -> env
+        | Monomorphic_const ctx ->
+          let ctx = match eff.seff_env with
+          | `Nothing -> ctx
+          | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
+          in
+          Environ.push_context_set ~strict:true ctx env
       in
       let rec translate_seff sl seff acc env =
         match seff with
@@ -527,18 +499,22 @@ let export_side_effects mb env c =
         | cbs :: rest ->
           if Int.equal sl 0 then
            let env, cbs =
-             List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
+             List.fold_left (fun (env,cbs) eff ->
+              let { seff_constant = kn; seff_body = ocb; seff_env = u } = eff in
                let ce = constant_entry_of_side_effect ocb u in
                let cb = translate_constant Pure env kn ce in
-               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) 
+               let eff = { eff with
+                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
           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 (fun (kn,cb,u,r) ->
-             kn, cb, r) cbs in
+           let ecbs = List.map export_eff cbs in
            translate_seff (sl - cbs_len) rest (ecbs @ acc) env
      in
        translate_seff trusted seff [] env
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 6a0ff072f5..3ebc41357e 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -46,16 +46,10 @@ val uniq_seff : side_effects -> side_effect list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
-val equal_eff : side_effect -> side_effect -> bool
-
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
     constant_body
 
-type side_effect_role =
-  | Subproof
-  | Schema of inductive * string
-
 type exported_side_effect = 
   Constant.t * constant_body * side_effect_role
   
diff --git a/proofs/refine.ml b/proofs/refine.ml
index b64e7a2e5e..05d5eaa9e9 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -49,17 +49,14 @@ let (pr_constrv,pr_constr) =
 
 (* Get the side-effect's constant declarations to update the monad's
   * environmnent *)
-let add_if_undefined kn cb env =
-  try ignore(Environ.lookup_constant kn env); env
-  with Not_found -> Environ.add_constant kn cb env
+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_effect env = function
-  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
-    add_if_undefined kn cb env
-  | { Entries.eff = Entries.SEscheme (l,_) } ->
-    List.fold_left (fun env (_,kn,cb,eff_env) ->
-        add_if_undefined kn cb env) env l
+let add_side_effect env { Entries.eff } =
+  List.fold_left add_if_undefined env eff
 
 let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 21520f5d2b..e4013152e6 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -154,7 +154,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
   let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
   declare_scheme kind [|ind,const|];
-  const, Safe_typing.add_private
+  const, Safe_typing.concat_private
      (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
@@ -174,7 +174,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
   consts,
-  Safe_typing.add_private 
+  Safe_typing.concat_private
     (Safe_typing.private_con_of_scheme
       ~kind (Global.safe_env()) (Array.to_list schemes))
     eff 
@@ -187,7 +187,7 @@ let define_mutual_scheme kind mode names mind =
 
 let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
-  s, Safe_typing.add_private
+  s, Safe_typing.concat_private
       (Safe_typing.private_con_of_scheme
             ~kind (Global.safe_env()) [ind, s])
       Safe_typing.empty_private_constants
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c430edf2e9..2a9d89fe5b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5000,7 +5000,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   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 effs = add_private eff
+  let effs = concat_private eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index ce74f2344a..1b086d69cc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -77,10 +77,8 @@ let adjust_guardness_conditions const = function
                   with Not_found -> false in 
                 if exists c e then e else Environ.add_constant c cb e in
               let env = List.fold_left (fun env { eff } ->
-                match eff with
-                | SEsubproof (c, cb,_) -> add c cb env
-                | SEscheme (l,_) ->
-                    List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
+                let fold acc eff = add eff.seff_constant eff.seff_body acc in
+                List.fold_left fold env eff)
                 env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
                 search_guard env