library/opaqueTables: enable their use in interactive mode

Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).

With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
  1) directly (before the constant is discharged)
  2) indirectly, via an int, that is mapped by the opaque table to
     the proof term.
This is now consistent in batch/interactive mode

This is step 0 to make an interactive coqtop able to dump a .vo/.vi

1 files changed, 9 insertions, 85 deletions

diff --git a/library/library.ml b/library/library.ml
index 7bff05cda..7f5ca5af6 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -351,87 +351,15 @@ let access_opaque_table dp i =
     (fetch_table "opaque proofs")
     add_opaque_table !opaque_tables dp i
 let access_univ_table dp i =
-  access_table
-    (fetch_table "universe contexts of opaque proofs")
-    add_univ_table !univ_tables dp i
-
-(** Table of opaque terms from the library currently being compiled *)
-
-module OpaqueTables = struct
-
- let a_constr = Future.from_val (Term.mkRel 1)
- let a_univ = Future.from_val Univ.ContextSet.empty
- let a_discharge : Opaqueproof.cooking_info list = []
-
- let local_opaque_table = ref (Array.make 100 a_constr)
- let local_univ_table = ref (Array.make 100 a_univ)
- let local_discharge_table = ref (Array.make 100 a_discharge)
- let local_index = ref 0
-
- module FMap = Map.Make(Future.UUID)
- let f2t = ref FMap.empty
-
- let get_opaque dp i =
-   if DirPath.equal dp (Lib.library_dp ())
-   then (!local_opaque_table).(i)
-   else access_opaque_table dp i
- 
- let join_local_opaque dp i =
-   if DirPath.equal dp (Lib.library_dp ()) then
-    ignore(Future.force (!local_opaque_table).(i))
-
- let join_local_univ dp i =
-   if DirPath.equal dp (Lib.library_dp ()) then
-    ignore(Future.join (!local_univ_table).(i))
-
- let get_univ dp i =
-   if DirPath.equal dp (Lib.library_dp ())
-   then Some (!local_univ_table).(i)
-   else try Some (access_univ_table dp i) with Not_found -> None
-
- let store (d,cu) =
-  let n = !local_index in
-  incr local_index;
-  if Int.equal n (Array.length !local_opaque_table) then begin
-    let t = Array.make (2*n) a_constr in
-    Array.blit !local_opaque_table 0 t 0 n;
-    local_opaque_table := t;
-    let t = Array.make (2*n) a_univ in
-    Array.blit !local_univ_table 0 t 0 n;
-    local_univ_table := t;
-    let t = Array.make (2*n) a_discharge in
-    Array.blit !local_discharge_table 0 t 0 n;
-    local_discharge_table := t
-  end;
-  let c, u = Future.split2 ~greedy:true cu in
-  Future.sink u;
-  Future.sink c;
-  (!local_opaque_table).(n) <- c;
-  (!local_univ_table).(n) <- u;
-  (!local_discharge_table).(n) <- d;
-  f2t := FMap.add (Future.uuid cu) n !f2t;
-  Some (Lib.library_dp (), n)
-
- let dump () =
-   Array.sub !local_opaque_table 0 !local_index,
-   Array.sub !local_univ_table 0 !local_index,
-   Array.sub !local_discharge_table 0 !local_index,
-   FMap.bindings !f2t
-
- let reset () =
-   local_discharge_table := Array.make 100 a_discharge;
-   local_univ_table := Array.make 100 a_univ;
-   local_opaque_table := Array.make 100 a_constr;
-   f2t := FMap.empty;
-   local_index := 0
-
-end
+  try
+    Some (access_table 
+            (fetch_table "universe contexts of opaque proofs")
+            add_univ_table !univ_tables dp i)
+  with Not_found -> None
 
 let () =
-  Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque;
-  Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ;
-  Opaqueproof.set_join_indirect_local_opaque OpaqueTables.join_local_opaque;
-  Opaqueproof.set_join_indirect_local_univ OpaqueTables.join_local_univ
+  Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
+  Opaqueproof.set_indirect_univ_accessor access_univ_table
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -694,8 +622,6 @@ let start_library f =
   check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
-  OpaqueTables.reset ();
-  Opaqueproof.set_indirect_creator OpaqueTables.store;
   Declaremods.start_library ldir;
   ldir,longf
 
@@ -743,7 +669,7 @@ let error_recursively_dependent_library dir =
 (* Security weakness: file might have been changed on disk between
    writing the content and computing the checksum... *)
 
-let save_library_to ?todo dir f =
+let save_library_to ?todo dir f otab =
   let f, todo, utab, dtab =
     match todo with
     | None ->
@@ -753,10 +679,8 @@ let save_library_to ?todo dir f =
         assert(!Flags.compilation_mode = Flags.BuildVi);
         f ^ "i", (fun x -> Some (d x)),
           (fun x -> Some (x,Univ.ContextSet.empty,false)), (fun x -> Some x) in
-  Opaqueproof.reset_indirect_creator ();
   let cenv, seg, ast = Declaremods.end_library dir in
-  let opaque_table, univ_table, disch_table, f2t_map =
-    OpaqueTables.dump () in
+  let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
   assert(!Flags.compilation_mode = Flags.BuildVi ||
          Array.for_all Future.is_val opaque_table);
   let md = {