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

3 files changed, 32 insertions, 21 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 36f2b14cb2..b0fea5916f 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -47,7 +47,7 @@ let retrieve_first_recthm = function
       (pi2 (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
-      (body_of_constant cb, is_opaque cb)
+      (Global.body_of_constant_body cb, is_opaque cb)
   | _ -> assert false
 
 let adjust_guardness_conditions const = function
diff --git a/stm/stm.ml b/stm/stm.ml
index 3e8181fe93..b68ef94969 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -805,8 +805,9 @@ module Task = struct
         List.iter (fun (_,se) -> Declareops.iter_side_effects (function
           | Declarations.SEsubproof(_,
              { Declarations.const_body = Declarations.OpaqueDef f;
-      	 const_universes = univs } ) ->
-              Opaqueproof.join_opaque f
+      	       const_universes = univs } ) ->
+              (* They are Direct *)
+              Opaqueproof.join_opaque Opaqueproof.empty_opaquetab f
           | _ -> ())
         se) (fst l);
         l, Unix.gettimeofday () -. wall_clock in
@@ -885,7 +886,8 @@ module Slaves : sig
   val slave_init_stdout : unit -> unit
 
   type tasks
-  val dump : (Future.UUID.t * int) list -> tasks
+  val dump_final : int Future.UUIDMap.t -> tasks
+  val dump_snapshot : int Future.UUIDMap.t -> tasks
   val check_task : string -> tasks -> int -> bool
   val info_tasks : tasks -> (string * float * int) list
   val finish_task :
@@ -953,21 +955,24 @@ end = struct
           Nametab.locate_constant
             (Libnames.qualid_of_ident po.Proof_global.id) in
         let c = Global.lookup_constant con in
-        match c.Declarations.const_body with
-        | Declarations.OpaqueDef lc ->
-            let uc = Option.get (Opaqueproof.get_constraints lc) in
-            let uc =
-              Future.chain
-                ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
-            let pr = Opaqueproof.get_proof lc in
-            let pr = Future.chain ~greedy:true ~pure:true pr discharge in
-            let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
-            Future.sink pr;
-            let extra = Future.join uc in
-            u.(bucket) <- uc;
-            p.(bucket) <- pr;
-            u, Univ.ContextSet.union cst extra, false
-        | _ -> assert false
+        let o = match c.Declarations.const_body with
+          | Declarations.OpaqueDef o -> o
+          | _ -> assert false in
+        let uc =
+          Option.get
+            (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+        let pr =
+          Future.from_val (Option.get (Global.body_of_constant_body c)) in
+        let uc =
+          Future.chain
+            ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
+        let pr = Future.chain ~greedy:true ~pure:true pr discharge in
+        let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+        Future.sink pr;
+        let extra = Future.join uc in
+        u.(bucket) <- uc;
+        p.(bucket) <- pr;
+        u, Univ.ContextSet.union cst extra, false
   
   let check_task name l i =
     match check_task_aux "" name l i with
@@ -1031,7 +1036,12 @@ end = struct
   let dump f2t_map =
     let tasks = TaskQueue.dump () in
     prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
-    List.map (function r -> { r with r_uuid = List.assoc r.r_uuid f2t_map })
+    List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map })
+      (CList.map_filter (Task.request_of_task `Fresh) tasks)
+  let dump_snapshot f2t_map =
+    let tasks = TaskQueue.snapshot () in
+    prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
+    List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map })
       (CList.map_filter (Task.request_of_task `Fresh) tasks)
 
 end
diff --git a/stm/stm.mli b/stm/stm.mli
index 75aa08e7b7..d77c19cfbe 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -48,7 +48,8 @@ val stop_worker : string -> unit
 val join : unit -> unit
 (* To save to disk an incomplete document *)
 type tasks
-val dump : (Future.UUID.t * int) list -> tasks
+val dump_final : int Future.UUIDMap.t -> tasks
+val dump_snapshot : int Future.UUIDMap.t -> tasks
 
 val check_task : string -> tasks -> int -> bool
 val info_tasks : tasks -> (string * float * int) list