From 568f3b69d407f7b5a47d1fdd6ca2bbf3edb5be72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 May 2018 14:51:49 +0200
Subject: Further cleaning of the side-effect API.

We remove internal functions and types from the API.
---
 kernel/entries.ml      |  6 +-----
 kernel/safe_typing.ml  | 23 +++++++++--------------
 kernel/safe_typing.mli |  2 +-
 kernel/term_typing.ml  | 13 +++++++++++--
 kernel/term_typing.mli |  4 ++--
 5 files changed, 24 insertions(+), 24 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 493550e5e5..53284e0e9a 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -120,6 +120,7 @@ type seff_env =
      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
@@ -130,8 +131,3 @@ type side_eff = {
   seff_env : seff_env;
   seff_role : side_effect_role;
 }
-
-type side_effect = {
-  from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff list;
-}
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1547a11390..f2b5ed4383 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -233,28 +233,23 @@ let make_eff env cst r =
 let private_con_of_con env c =
   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
+  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
-  let from_env = CEphemeron.create env.revstruct in
-  add_private { eff; from_env; } empty_private_constants
+  add_private env.revstruct eff empty_private_constants
 
 let universes_of_private 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
+  let fold acc eff =
+    let acc = match eff.seff_env with
+    | `Nothing -> acc
+    | `Opaque (_, ctx) -> ctx :: acc
     in
-    List.fold_left fold acc eff
+    match eff.seff_body.const_universes with
+    | Monomorphic_const ctx -> ctx :: acc
+    | Polymorphic_const _ -> acc
   in
   List.fold_left fold [] (Term_typing.uniq_seff eff)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c8df57911f..990e07da45 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -44,7 +44,7 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 type private_constants
 
 val side_effects_of_private_constants :
-  private_constants -> Entries.side_effect list
+  private_constants -> Entries.side_eff list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 79511e4253..84fc505c4f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -27,6 +27,11 @@ module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
+type side_effect = {
+  from_env : Declarations.structure_body CEphemeron.key;
+  eff      : side_eff list;
+}
+
 module SideEffects :
 sig
   type t
@@ -66,10 +71,14 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 let uniq_seff_rev = SideEffects.repr
-let uniq_seff l = List.rev (SideEffects.repr l)
+let uniq_seff l =
+  let ans = List.rev (SideEffects.repr l) in
+  List.map_append (fun { eff } -> eff) ans
 
 let empty_seff = SideEffects.empty
-let add_seff = SideEffects.add
+let add_seff mb eff effs =
+  let from_env = CEphemeron.create mb in
+  SideEffects.add { eff; from_env } effs
 let concat_seff = SideEffects.concat
 
 let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 3ebc41357e..b05e05e4dc 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -38,11 +38,11 @@ val inline_entry_side_effects :
     yet type checked proof. *)
 
 val empty_seff : side_effects
-val add_seff : side_effect -> side_effects -> side_effects
+val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects
 val concat_seff : side_effects -> side_effects -> side_effects
 (** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
     [e1] must be more recent than those of [e2]. *)
-val uniq_seff : side_effects -> side_effect list
+val uniq_seff : side_effects -> side_eff list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
-- 
cgit v1.2.3