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.

7 files changed, 43 insertions, 60 deletions

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|]))
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 5584b74b36..9f148ee248 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -43,6 +43,8 @@ let default_get_univ dp _ =
   CErrors.user_err (Pp.pr_sequence Pp.str [
     "Cannot access universe constraints of opaque proofs in library ";
     DirPath.to_string dp])
+let not_here () =
+  CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
 let get_opaque = ref default_get_opaque
 let get_univ = ref default_get_univ
@@ -102,7 +104,10 @@ let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
       let pt =
         if DirPath.equal dp odp
         then Future.chain (snd (Int.Map.find i prfs)) fst
-        else !get_opaque dp i in
+        else match !get_opaque dp i with
+        | None -> not_here ()
+        | Some v -> Future.from_val v
+      in
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
@@ -113,7 +118,7 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
       then snd (Future.force (snd (Int.Map.find i prfs)))
       else match !get_univ dp i with
         | None -> Univ.ContextSet.empty
-        | Some u -> Future.force u
+        | Some u -> u
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
@@ -121,22 +126,23 @@ let get_direct_constraints = function
 
 module FMap = Future.UUIDMap
 
-let a_constr = Future.from_val (mkRel 1)
-let a_univ = Future.from_val Univ.ContextSet.empty
-let a_discharge : cooking_info list = []
-
-let dump { opaque_val = otab; opaque_len = n; _ } =
-  let opaque_table = Array.make n a_constr in
-  let univ_table = Array.make n a_univ in
-  let disch_table = Array.make n a_discharge in
+let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
+  let opaque_table = Array.make n None in
+  let univ_table = Array.make n None in
+  let disch_table = Array.make n [] in
   let f2t_map = ref FMap.empty in
-  Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 cu in
-    Future.sink u;
-    Future.sink c;
-    opaque_table.(n) <- c;
-    univ_table.(n) <- u;
-    disch_table.(n) <- d;
-    f2t_map := FMap.add (Future.uuid cu) n !f2t_map)
-  otab;
+  let iter n (d, cu) =
+    let uid = Future.uuid cu in
+    let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
+    if Future.is_val cu then
+      let (c, u) = Future.force cu in
+      let () = univ_table.(n) <- Some u in
+      opaque_table.(n) <- Some c
+    else if Future.UUIDSet.mem uid except then
+      disch_table.(n) <- d
+    else
+      CErrors.anomaly
+        Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+  in
+  let () = Int.Map.iter iter otab in
   opaque_table, univ_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index b84aeaf35a..3b61ec71ef 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -59,9 +59,9 @@ val discharge_direct_opaque :
 
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
-val dump : opaquetab ->
-  Constr.t Future.computation array *
-  Univ.ContextSet.t Future.computation array *
+val dump : ?except:Future.UUIDSet.t -> opaquetab ->
+  Constr.t option array *
+  Univ.ContextSet.t option array *
   cooking_info list array *
   int Future.UUIDMap.t
 
@@ -73,7 +73,7 @@ val dump : opaquetab ->
 *)
 
 val set_indirect_opaque_accessor :
-  (DirPath.t -> int -> constr Future.computation) -> unit
+  (DirPath.t -> int -> constr option) -> unit
 val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit
+  (DirPath.t -> int -> Univ.ContextSet.t option) -> unit
 
diff --git a/library/library.ml b/library/library.ml
index 9f4eb531ed..3bc2e84054 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,7 +315,7 @@ 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 () =
@@ -328,9 +328,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 +590,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 +603,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..d2b0c4f202 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 *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 9e9d23ba93..30cf8a0622 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1846,13 +1846,8 @@ end = struct (* {{{ *)
         let pr = map (Option.get (Global.body_of_constant_body c)) in
         let pr = discharge pr in
         let pr = Constr.hcons pr in
-        let return c =
-          let fc = Future.from_val c in
-          let _ = Future.join fc in
-          fc
-        in
-        u.(bucket) <- return uc;
-        p.(bucket) <- return pr;
+        u.(bucket) <- Some uc;
+        p.(bucket) <- Some pr;
         u, Univ.ContextSet.union cst uc, false
 
   let check_task name l i =