Merge branch 'v8.6' into trunk

5 files changed, 78 insertions, 24 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 77081947e..1e07c9690 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 2312f891c..caaaff1b8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -208,19 +208,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
@@ -250,7 +250,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..efeb98bd2 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -47,11 +47,18 @@ 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
+(** 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 -> private_constant
 val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 569a58378..2eb2c040e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -26,8 +26,6 @@ module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
-let mk_pure_proof c = (c, Univ.ContextSet.empty), []
-
 let equal_eff e1 e2 =
   let open Entries in
   match e1, e2 with
@@ -39,13 +37,54 @@ let equal_eff e1 e2 =
           cl1 cl2
   | _ -> false
 
-let rec uniq_seff = function
-  | [] -> []
-  | x :: xs -> x :: uniq_seff (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))
+module SideEffects :
+sig
+  type t
+  val repr : t -> side_effect list
+  val empty : t
+  val add : side_effect -> t -> t
+  val concat : t -> t -> t
+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
+end
+
+module SeffSet = Set.Make(SeffOrd)
+
+type t = { seff : side_effect list; elts : SeffSet.t }
+(** Invariant: [seff] is a permutation of the elements of [elts] *)
+
+let repr eff = eff.seff
+let empty = { seff = []; elts = SeffSet.empty }
+let add x es =
+  if SeffSet.mem x es.elts then es
+  else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
+let concat xes yes =
+  List.fold_right add xes.seff yes
+
+end
+
+type side_effects = SideEffects.t
+
+let uniq_seff_rev = SideEffects.repr
+let uniq_seff l = List.rev (SideEffects.repr l)
+
+let empty_seff = SideEffects.empty
+let add_seff = SideEffects.add
+let concat_seff = SideEffects.concat
+
+let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
 
 let inline_side_effects env body ctx side_eff =
   let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
@@ -98,7 +137,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 *)
@@ -380,7 +419,7 @@ let constant_entry_of_side_effect cb u =
     | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
     | _ -> assert false in
   DefinitionEntry {
-    const_entry_body = Future.from_val (pt, []);
+    const_entry_body = Future.from_val (pt, empty_seff);
     const_entry_secctx = None;
     const_entry_feedback = None;
     const_entry_type =
@@ -414,7 +453,7 @@ let export_side_effects mb env ce =
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
         const_entry_body = Future.chain ~pure:true body
-          (fun (b_ctx, _) -> b_ctx, []) } in
+          (fun (b_ctx, _) -> b_ctx, empty_seff) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
         with Not_found -> true in 
@@ -426,7 +465,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, _ ->
@@ -498,7 +537,7 @@ let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
-      (body, ctx'), []);
+      (body, ctx'), empty_seff);
 }
 
 let inline_side_effects env body side_eff =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 89b5fc40e..075389ea5 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,15 @@ 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
+(** [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
+(** Return the list of individual side-effects in the order of their
+    creation. *)
+
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :