Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.

Reviewed-by: gares

4 files changed, 79 insertions, 99 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b88a2e6194..fae06f7163 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -239,7 +239,7 @@ let cook_constant { from = cb; info } =
   | Undef _ as x -> x
   | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
   | OpaqueDef o ->
-    OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
+    OpaqueDef (Opaqueproof.discharge_opaque info o)
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
   let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f0ffd2e073..f0b706e4f5 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -24,7 +24,7 @@ type 'a delayed_universes =
 | PrivateMonomorphic of 'a
 | PrivatePolymorphic of int * Univ.ContextSet.t
 
-type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option
+type opaque_proofterm = (Constr.t * unit delayed_universes) option
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> opaque_proofterm;
@@ -38,10 +38,10 @@ let drop_mono = function
 type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
 
 type opaque =
-  | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
-  | Direct of cooking_info list * proofterm
+| Indirect of substitution list * cooking_info list * DirPath.t * int (* subst, discharge, lib, index *)
+
 type opaquetab = {
-  opaque_val : (cooking_info list * proofterm) Int.Map.t;
+  opaque_val : proofterm Int.Map.t;
   (** Actual proof terms *)
   opaque_len : int;
   (** Size of the above map *)
@@ -56,44 +56,33 @@ let empty_opaquetab = {
 let not_here () =
   CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
-let create cu = Direct ([],cu)
-
-let turn_indirect dp o tab = match o with
-  | Indirect (_,_,i) ->
-      if not (Int.Map.mem i tab.opaque_val)
-      then CErrors.anomaly (Pp.str "Indirect in a different table.")
-      else CErrors.anomaly (Pp.str "Already an indirect opaque.")
-  | Direct (d, cu) ->
-    (* Invariant: direct opaques only exist inside sections, we turn them
-      indirect as soon as we are at toplevel. At this moment, we perform
-      hashconsing of their contents, potentially as a future. *)
-      let hcons (c, u) =
-        let c = Constr.hcons c in
-        let u = match u with
-        | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
-        | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u)
-        in
-        (c, u)
-      in
-      let cu = Future.chain cu hcons in
-      let id = tab.opaque_len in
-      let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
-      let opaque_dir =
-        if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
-        else if DirPath.equal tab.opaque_dir DirPath.initial then dp
-        else CErrors.anomaly
-          (Pp.str "Using the same opaque table for multiple dirpaths.") in
-      let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in
-      Indirect ([],dp,id), ntab
+let create dp cu tab =
+  let hcons (c, u) =
+    let c = Constr.hcons c in
+    let u = match u with
+    | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
+    | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u)
+    in
+    (c, u)
+  in
+  let cu = Future.chain cu hcons in
+  let id = tab.opaque_len in
+  let opaque_val = Int.Map.add id cu tab.opaque_val in
+  let opaque_dir =
+    if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
+    else if DirPath.equal tab.opaque_dir DirPath.initial then dp
+    else CErrors.anomaly
+      (Pp.str "Using the same opaque table for multiple dirpaths.") in
+  let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in
+  Indirect ([], [], dp, id), ntab
 
 let subst_opaque sub = function
-  | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
-  | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
+| Indirect (s, ci, dp, i) -> Indirect (sub :: s, ci, dp, i)
 
-let discharge_direct_opaque ci = function
-  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-  | Direct (d, cu) ->
-      Direct (ci :: d, cu)
+let discharge_opaque info = function
+| Indirect (s, ci, dp, i) ->
+  assert (CList.is_empty s);
+  Indirect ([], info :: ci, dp, i)
 
 let join except cu = match except with
 | None -> ignore (Future.join cu)
@@ -102,25 +91,21 @@ let join except cu = match except with
   else ignore (Future.join cu)
 
 let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> join except cu
-  | Indirect (_,dp,i) ->
-      if DirPath.equal dp odp then
-        let (_, fp) = Int.Map.find i prfs in
-        join except fp
+| Indirect (_,_,dp,i) ->
+    if DirPath.equal dp odp then
+      let fp = Int.Map.find i prfs in
+      join except fp
 
 let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (d, cu) ->
-    let (c, u) = Future.force cu in
-    access.access_discharge d (c, drop_mono u)
-  | Indirect (l,dp,i) ->
+  | Indirect (l,d,dp,i) ->
       let c, u =
         if DirPath.equal dp odp
         then
-          let (d, cu) = Int.Map.find i prfs in
+          let cu = Int.Map.find i prfs in
           let (c, u) = Future.force cu in
           access.access_discharge d (c, drop_mono u)
         else
-          let (d, cu) = access.access_proof dp i in
+          let cu = access.access_proof dp i in
           match cu with
           | None -> not_here ()
           | Some (c, u) -> access.access_discharge d (c, u)
@@ -133,21 +118,19 @@ let get_mono (_, u) = match u with
 | PrivatePolymorphic _ -> Univ.ContextSet.empty
 
 let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) ->
-    get_mono (Future.force cu)
-  | Indirect (_,dp,i) ->
+| Indirect (_,_,dp,i) ->
       if DirPath.equal dp odp
       then
-        let ( _, cu) = Int.Map.find i prfs in
+        let cu = Int.Map.find i prfs in
         get_mono (Future.force cu)
       else Univ.ContextSet.empty
 
 module FMap = Future.UUIDMap
 
 let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
-  let opaque_table = Array.make n ([], None) in
+  let opaque_table = Array.make n None in
   let f2t_map = ref FMap.empty in
-  let iter n (d, cu) =
+  let iter n cu =
     let uid = Future.uuid cu in
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
     let c =
@@ -160,7 +143,7 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
         CErrors.anomaly
           Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
     in
-    opaque_table.(n) <- (d, c)
+    opaque_table.(n) <- c
   in
   let () = Int.Map.iter iter otab in
   opaque_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 758a9f5107..1870241dcd 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -16,10 +16,7 @@ open Mod_subst
     Opaque proof terms are special since:
     - they can be lazily computed and substituted
     - they are stored in an optionally loaded segment of .vo files
-    An [opaque] proof terms holds the real data until fully discharged.
-    In this case it is called [direct].
-    When it is [turn_indirect] the data is relocated to an opaque table
-    and the [opaque] is turned into an index. *)
+    An [opaque] proof terms holds an index into an opaque table. *)
 
 type 'a delayed_universes =
 | PrivateMonomorphic of 'a
@@ -33,12 +30,7 @@ type opaque
 val empty_opaquetab : opaquetab
 
 (** From a [proofterm] to some [opaque]. *)
-val create : proofterm -> opaque
-
-(** Turn a direct [opaque] into an indirect one. It is your responsibility to
-  hashcons the inner term beforehand. The integer is an hint of the maximum id
-  used so far *)
-val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
+val create : DirPath.t -> proofterm -> opaquetab -> opaque * opaquetab
 
 type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
   (Univ.Instance.t * Id.t array) Mindmap.t
@@ -47,14 +39,14 @@ type cooking_info = {
   modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 
-type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option
+type opaque_proofterm = (Constr.t * unit delayed_universes) option
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> opaque_proofterm;
   access_discharge : cooking_info list ->
     (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
 }
-(** When stored indirectly, opaque terms are indexed by their library
+(** Opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
     this indirect storage, by telling how to retrieve terms.
 *)
@@ -66,7 +58,7 @@ val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.Context
 
 val subst_opaque : substitution -> opaque -> opaque
 
-val discharge_direct_opaque :
+val discharge_opaque :
   cooking_info -> opaque -> opaque
 
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1069d9a62c..9b4d2e69ac 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -591,17 +591,6 @@ let add_constant_aux ~in_section senv (kn, cb) =
   let l = Constant.label kn in
   (* This is the only place where we hashcons the contents of a constant body *)
   let cb = if in_section then cb else Declareops.hcons_const_body cb in
-  let cb, otab = match cb.const_body with
-    | OpaqueDef lc when not in_section ->
-      (* In coqc, opaque constants outside sections will be stored
-         indirectly in a specific table *)
-      let od, otab =
-        Opaqueproof.turn_indirect
-          (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in
-      { cb with const_body = OpaqueDef od }, otab
-    | _ -> cb, (Environ.opaque_tables senv.env)
-  in
-  let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
@@ -805,17 +794,25 @@ let export_side_effects mb env (b_ctx, eff) =
      in
        translate_seff trusted seff [] env
 
+let push_opaque_proof pf senv =
+  let o, otab = Opaqueproof.create (library_dp_of_senv senv) pf (Environ.opaque_tables senv.env) in
+  let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
+  senv, o
+
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map univs p =
-    let local = match univs with
+  let map senv (kn, c) = match c.const_body with
+  | OpaqueDef p ->
+    let local = match c.const_universes with
     | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
     | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
     in
-    Opaqueproof.create (Future.from_val (p, local))
+    let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in
+    senv, (kn, { c with const_body = OpaqueDef o })
+  | Def _ | Undef _ | Primitive _ as body ->
+    senv, (kn, { c with const_body = body })
   in
-  let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in
-  let bodies = List.map map exported in
+  let senv, bodies = List.fold_left_map map senv exported in
   let exported = List.map (fun (kn, _) -> kn) exported in
   (* No delayed constants to declare *)
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -836,20 +833,25 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let delayed_cst = match cb.const_body with
-    | OpaqueDef fc when not (Declareops.constant_is_polymorphic cb) ->
-      let map (_, u) = match u with
-      | Opaqueproof.PrivateMonomorphic ctx -> ctx
-      | Opaqueproof.PrivatePolymorphic _ -> assert false
+    let senv, cb, delayed_cst = match cb.const_body with
+    | OpaqueDef fc ->
+      let senv, o = push_opaque_proof fc senv in
+      let delayed_cst =
+        if not (Declareops.constant_is_polymorphic cb) then
+          let map (_, u) = match u with
+          | Opaqueproof.PrivateMonomorphic ctx -> ctx
+          | Opaqueproof.PrivatePolymorphic _ -> assert false
+          in
+          let fc = Future.chain fc map in
+          match Future.peek_val fc with
+          | None -> [Later fc]
+          | Some c -> [Now c]
+        else []
       in
-      let fc = Future.chain fc map in
-      begin match Future.peek_val fc with
-      | None -> [Later fc]
-      | Some c -> [Now c]
-      end
-    | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
+      senv, { cb with const_body = OpaqueDef o }, delayed_cst
+    | Undef _ | Def _ | Primitive _ as body ->
+      senv, { cb with const_body = body }, []
     in
-    let cb = map_constant (fun c -> Opaqueproof.create c) cb in
     let senv = add_constant_aux ~in_section senv (kn, cb) in
     add_constraints_list delayed_cst senv
   in
@@ -985,6 +987,9 @@ let close_section senv =
      that are going to be replayed. Those that are not forced are not readded
      by {!add_constant_aux}. *)
   let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in
+  (* Do not revert the opaque table, the discharged opaque constants are
+     referring to it. *)
+  let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in
   let senv = { senv with env; revstruct; sections; univ; objlabels; } in
   (* Second phase: replay the discharged section contents *)
   let senv = add_constraints (Now cstrs) senv in