Making the side_effects type opaque.

We move it from Entries to Term_typing and export the few functions needed
to manipulate it in this module.

5 files changed, 25 insertions, 15 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index ea7c266bc..5287a009e 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -113,5 +113,3 @@ type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   eff      : side_eff;
 }
-
-type side_effects = side_effect list
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index bc1cb63d8..e3b87bbe1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -206,19 +206,19 @@ let get_opaque_body env cbo =
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
 type private_constant = Entries.side_effect
-type private_constants = private_constant list
+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 = []
-let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs
-let concat_private xs ys = List.fold_right add_private xs ys
+let empty_private_constants = Term_typing.empty_seff
+let add_private = Term_typing.add_seff
+let concat_private = Term_typing.concat_seff
 let mk_pure_proof = Term_typing.mk_pure_proof
 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 x = Term_typing.uniq_seff (List.rev x)
+let side_effects_of_private_constants = Term_typing.uniq_seff
 
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
@@ -248,7 +248,7 @@ let universes_of_private eff =
      | Entries.SEsubproof (c, cb, e) ->
 	if cb.const_polymorphic then acc
 	else Univ.ContextSet.of_context cb.const_universes :: acc)
-   [] eff
+   [] (Term_typing.uniq_seff eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 15ebc7d88..8bc47d6ce 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -47,7 +47,7 @@ type private_constant_role =
   | Schema of inductive * string
 
 val side_effects_of_private_constants :
-  private_constants -> Entries.side_effects
+  private_constants -> Entries.side_effect list
 
 val empty_private_constants : private_constants
 val add_private : private_constant -> private_constants -> private_constants
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b7597ba7f..24da308b4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -37,13 +37,20 @@ let equal_eff e1 e2 =
           cl1 cl2
   | _ -> false
 
-let rec uniq_seff = function
+type side_effects = side_effect list
+
+let rec uniq_seff_aux = function
   | [] -> []
-  | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
+  | x :: xs -> x :: uniq_seff_aux (List.filter (fun y -> not (equal_eff x y)) xs)
 (* The list of side effects is in reverse order (most recent first).
  * To keep the "topological" order between effects we have to uniq-ize from
  * the tail *)
-let uniq_seff l = List.rev (uniq_seff (List.rev l))
+let uniq_seff_rev l = List.rev (uniq_seff_aux (List.rev l))
+let uniq_seff l = List.rev (uniq_seff_aux l)
+
+let empty_seff = []
+let add_seff x xs = if List.mem_f equal_eff x xs then xs else x :: xs
+let concat_seff xs ys = List.fold_right add_seff xs ys
 
 let inline_side_effects env body ctx side_eff =
   let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
@@ -97,7 +104,7 @@ let inline_side_effects env body ctx side_eff =
     t, ctx, (mb,List.length cbl) :: sl
   in
   (* CAVEAT: we assure a proper order *)
-  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff)
 
 (* Given the list of signatures of side effects, checks if they match.
  * I.e. if they are ordered descendants of the current revstruct *)
@@ -427,7 +434,7 @@ let export_side_effects mb env ce =
         let cbl = List.filter not_exists cbl in
         if cbl = [] then acc, sl
         else cbl :: acc, (mb,List.length cbl) :: sl in
-      let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) 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, _ ->
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 89b5fc40e..5330fb32b 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,6 +12,8 @@ open Environ
 open Declarations
 open Entries
 
+type side_effects
+
 val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
   constant_def * types * constant_universes
 
@@ -29,7 +31,10 @@ val inline_entry_side_effects :
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val uniq_seff : side_effects -> side_effects
+val empty_seff : side_effects
+val add_seff : side_effect -> side_effects -> side_effects
+val concat_seff : side_effects -> side_effects -> side_effects
+val uniq_seff : side_effects -> side_effect list
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :