From b245a6c46bc3ef70142e8a165f6cde54265b941e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 11:51:31 +0200
Subject: Statically ensure the content of delayed proofs in vio file.

Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.

This also enhances debug printing, as the latter is unable to properly
print futures.
---
 checker/check.ml  |  2 +-
 checker/values.ml | 12 ++----------
 2 files changed, 3 insertions(+), 11 deletions(-)

(limited to 'checker')

diff --git a/checker/check.ml b/checker/check.ml
index a2c8a0f25d..cc5ad0af4c 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;
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|]))
-- 
cgit v1.2.3


From 2fa3dc389a58ca4a390b99995d82e6c089add163 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 May 2019 19:00:28 +0200
Subject: Move body_of_constant_body to Global and specialize its uses.

This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.

The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
---
 checker/mod_checking.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1dd16f1630..a3f151ef86 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -29,10 +29,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 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 -> ()
-- 
cgit v1.2.3


From d3c931cd8c84d1b7d9d5763e20221d51700f0709 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 May 2019 19:22:30 +0200
Subject: Remove the indirect opaque accessor hooks from Opaqueproof.

We simply pass them as arguments, now that they are not called by the
kernel anymore.

The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
---
 checker/check.ml         | 11 +----------
 checker/mod_checking.ml  | 10 +++++++++-
 checker/mod_checking.mli |  2 ++
 3 files changed, 12 insertions(+), 11 deletions(-)

(limited to 'checker')

diff --git a/checker/check.ml b/checker/check.ml
index cc5ad0af4c..76f40dbac2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -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 a3f151ef86..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 *)
@@ -33,7 +41,7 @@ let check_constant_declaration env kn cb =
   let body = match cb.const_body with
   | Undef _ | Primitive _ -> None
   | Def c -> Some (Mod_subst.force_constr c)
-  | OpaqueDef o -> Some (Opaqueproof.force_proof otab o)
+  | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o)
   in
   let () =
     match body with
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
-- 
cgit v1.2.3