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, 22 insertions, 23 deletions

diff --git a/checker/check.ml b/checker/check.ml
index a2c8a0f25d..76f40dbac2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -50,7 +50,7 @@ let pr_path sp =
 
 type compilation_unit_name = DirPath.t
 
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
 
 type library_t = {
   library_name : compilation_unit_name;
@@ -100,16 +100,7 @@ let access_opaque_table dp i =
   assert (i < Array.length t);
   t.(i)
 
-let access_opaque_univ_table dp i =
-  try
-    let t = LibraryMap.find dp !opaque_univ_tables in
-    assert (i < Array.length t);
-    Some t.(i)
-  with Not_found -> None
-
-let () =
-  Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
-  Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table
+let () = Mod_checking.set_indirect_accessor access_opaque_table
 
 let check_one_lib admit senv (dir,m) =
   let md = m.library_compiled in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1dd16f1630..1cf07e7cc7 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,6 +8,14 @@ open Environ
 
 (** {6 Checking constants } *)
 
+let get_proof = ref (fun _ _ -> assert false)
+let set_indirect_accessor f = get_proof := f
+
+let indirect_accessor = {
+  Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
+  Opaqueproof.access_constraints = (fun _ _ -> assert false);
+}
+
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   (* Locally set the oracle for further typechecking *)
@@ -29,10 +37,16 @@ let check_constant_declaration env kn cb =
   in
   let ty = cb.const_type in
   let _ = infer_type env' ty in
+  let otab = Environ.opaque_tables env in
+  let body = match cb.const_body with
+  | Undef _ | Primitive _ -> None
+  | Def c -> Some (Mod_subst.force_constr c)
+  | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o)
+  in
   let () =
-    match Environ.body_of_constant_body env cb with
+    match body with
     | Some bd ->
-      let j = infer env' (fst bd) in
+      let j = infer env' bd in
       (try conv_leq env' j.uj_type ty
        with NotConvertible -> Type_errors.error_actual_type env j ty)
     | None -> ()
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 6cff3e6b8c..dbc81c8507 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -8,4 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit
+
 val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 5cbf0ff298..4b651cafb6 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -53,7 +53,6 @@ let v_enum name n = Sum(name,n,[||])
 let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
 let v_bool = v_enum "bool" 2
 let v_unit = v_enum "unit" 1
-let v_ref v = v_tuple "ref" [|v|]
 
 let v_set v =
   let rec s = Sum ("Set.t",1,
@@ -70,13 +69,6 @@ let v_hmap vk vd = v_map Int (v_map vk vd)
 
 let v_pred v = v_pair v_bool (v_set v)
 
-(* lib/future *)
-let v_computation f =
-  Annot ("Future.computation",
-  v_ref
-    (v_sum "Future.comput" 0
-      [| [| Fail "Future.ongoing" |]; [| f |] |]))
-
 (** kernel/names *)
 
 let v_id = String
@@ -391,6 +383,6 @@ let v_libsum =
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
 
-let v_opaques = Array (v_computation v_constr)
+let v_opaques = Array (Opt v_constr)
 let v_univopaques =
-  Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
+  Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|]))