Merge PR #10201: Remove access to indirect opaques in the kernel

Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes

4 files changed, 31 insertions, 26 deletions

diff --git a/library/global.ml b/library/global.ml
index 58e2380440..d5ffae7716 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -132,9 +132,20 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
 let opaque_tables () = Environ.opaque_tables (env ())
 
-let body_of_constant_body ce = body_of_constant_body (env ()) ce
-
-let body_of_constant cst = body_of_constant_body (lookup_constant cst)
+let body_of_constant_body access env cb =
+  let open Declarations in
+  let otab = Environ.opaque_tables env in
+  match cb.const_body with
+  | Undef _ | Primitive _ ->
+     None
+  | Def c ->
+     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+  | OpaqueDef o ->
+     Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
+
+let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
+
+let body_of_constant access cst = body_of_constant_body access (lookup_constant cst)
 
 (** Operations on kernel names *)
 
diff --git a/library/global.mli b/library/global.mli
index 984d8c666c..aa9fc18477 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -100,13 +100,13 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
 
 val opaque_tables : unit -> Opaqueproof.opaquetab
 
-val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option
 (** Returns the body of the constant if it has any, and the polymorphic context
     it lives in. For monomorphic constant, the latter is empty, and for
     polymorphic constants, the term contains De Bruijn universe variables that
     need to be instantiated. *)
 
-val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
 (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
 (** {6 Compiled libraries } *)
diff --git a/library/library.ml b/library/library.ml
index 9f4eb531ed..039124635e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -276,8 +276,8 @@ let in_import_library : DirPath.t list * bool -> obj =
 (** Delayed / available tables of opaque terms *)
 
 type 'a table_status =
-  | ToFetch of 'a Future.computation array delayed
-  | Fetched of 'a Future.computation array
+  | ToFetch of 'a option array delayed
+  | Fetched of 'a option array
 
 let opaque_tables =
   ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
@@ -315,12 +315,13 @@ let access_opaque_table dp i =
 let access_univ_table dp i =
   try
     let what = "universe contexts of opaque proofs" in
-    Some (access_table what univ_tables dp i)
+    access_table what univ_tables dp i
   with Not_found -> None
 
-let () =
-  Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
-  Opaqueproof.set_indirect_univ_accessor access_univ_table
+let indirect_accessor = {
+  Opaqueproof.access_proof = access_opaque_table;
+  Opaqueproof.access_constraints = access_univ_table;
+}
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -328,9 +329,9 @@ let () =
 type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
 
 let mk_library sd md digests univs =
   {
@@ -590,7 +591,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
-  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
+  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
   let tasks, utab, dtab =
     match todo with
     | None -> None, None, None
@@ -603,16 +604,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
         Some (tasks,rcbackup),
         Some (univ_table,Univ.ContextSet.empty,false),
         Some disch_table in
-  let except =
-    Future.UUIDSet.fold (fun uuid acc ->
-      try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc
-      with Not_found -> acc)
-      except Int.Set.empty in
-  let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
-  Array.iteri (fun i x ->
-    if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
-      Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
-    opaque_table;
   let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
diff --git a/library/library.mli b/library/library.mli
index f3186d847f..2c0673c3b1 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -34,9 +34,9 @@ val require_library_from_dirpath
 type seg_sum
 type seg_lib
 type seg_univ = (* cst, all_cst, finished? *)
-  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
+  Univ.ContextSet.t option array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
@@ -73,3 +73,6 @@ val overwrite_library_filenames : string -> unit
 
 (** {6 Native compiler. } *)
 val native_name_from_filename : string -> string
+
+(** {6 Opaque accessors} *)
+val indirect_accessor : Opaqueproof.indirect_accessor