Abstract away the API for side-effect certificates.

1 files changed, 41 insertions, 15 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d1631e8cb0..1f97497d60 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -249,8 +249,36 @@ let check_engagement env expected_impredicative_set =
 
 (** {6 Stm machinery } *)
 
+module Certificate :
+sig
+  type t
+
+  val make : safe_environment -> t
+
+  (** Checks whether [dst] is a valid extension of [src] *)
+  val check : src:t -> dst:t -> bool
+end =
+struct
+
+type t = {
+  certif_struc : Declarations.structure_body;
+}
+
+let make senv = {
+  certif_struc = senv.revstruct;
+}
+
+let is_suffix l suf = match l with
+| [] -> false
+| _ :: l -> l == suf
+
+let check ~src ~dst =
+  is_suffix dst.certif_struc src.certif_struc
+
+end
+
 type side_effect = {
-  from_env : Declarations.structure_body CEphemeron.key;
+  seff_certif : Certificate.t CEphemeron.key;
   seff_constant : Constant.t;
   seff_body : Constr.t Declarations.constant_body;
 }
@@ -609,7 +637,7 @@ let inline_side_effects env body side_eff =
   let filter e =
     let cb = (e.seff_constant, e.seff_body) in
     if Environ.mem_constant e.seff_constant env then None
-    else Some (cb, e.from_env)
+    else Some (cb, e.seff_certif)
   in
   (* CAVEAT: we assure that most recent effects come first *)
   let side_eff = List.map_filter filter (SideEffects.repr side_eff) in
@@ -678,21 +706,18 @@ let inline_private_constants env ((body, ctx), side_eff) =
   let ctx' = Univ.ContextSet.union ctx ctx' in
   (body, ctx')
 
-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 check_signatures senv sl =
+  let curmb = Certificate.make senv in
   let is_direct_ancestor accu mb =
     match accu with
     | None -> None
     | Some curmb ->
         try
           let mb = CEphemeron.get mb in
-          if is_suffix mb curmb
+          if Certificate.check ~src:curmb ~dst:mb
           then Some mb
           else None
         with CEphemeron.InvalidKey -> None in
@@ -759,13 +784,14 @@ let translate_direct_opaque env kn ce =
   let () = assert (is_empty_private u) in
   { cb with const_body = OpaqueDef c }
 
-let export_side_effects mb env eff =
+let export_side_effects senv eff =
+  let env = senv.env in
       let not_exists e = not (Environ.mem_constant e.seff_constant env) in
       let aux (acc,sl) e =
         if not (not_exists e) then acc, sl
-        else e :: acc, e.from_env :: sl in
+        else e :: acc, e.seff_certif :: sl in
       let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in
-      let trusted = check_signatures mb signatures in
+      let trusted = check_signatures senv signatures in
       let push_seff env eff =
         let { seff_constant = kn; seff_body = cb ; _ } = eff in
         let env = Environ.add_constant kn (lift_constant cb) env in
@@ -803,7 +829,7 @@ let push_opaque_proof pf senv =
   senv, o
 
 let export_private_constants eff senv =
-  let exported = export_side_effects senv.revstruct senv.env eff in
+  let exported = export_side_effects senv eff in
   let map senv (kn, c) = match c.const_body with
   | OpaqueDef p ->
     let local = empty_private c.const_universes in
@@ -825,7 +851,7 @@ let add_constant l decl senv =
       | OpaqueEntry ce ->
         let handle env body eff =
           let body, uctx, signatures = inline_side_effects env body eff in
-          let trusted = check_signatures senv.revstruct signatures in
+          let trusted = check_signatures senv signatures in
           let trusted = if trusted then List.length signatures else 0 in
           body, uctx, trusted
         in
@@ -888,9 +914,9 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e
   in
   let senv = add_constant_aux senv (kn, dcb) in
   let eff =
-    let from_env = CEphemeron.create senv.revstruct in
+    let from_env = CEphemeron.create (Certificate.make senv) in
     let eff = {
-      from_env = from_env;
+      seff_certif = from_env;
       seff_constant = kn;
       seff_body = cb;
     } in