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

8 files changed, 47 insertions, 97 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index e4638f5e4..b01e24196 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -236,7 +236,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
           else (s, acc)
       else (s, acc)
     in
-      match Declareops.body_of_constant cb with
+      match Global.body_of_constant_body cb with
       | None -> do_type (Axiom kn)
       | Some body -> do_constr body s acc
 
diff --git a/library/declare.ml b/library/declare.ml
index 1c9e10a19..4ec81c49f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -116,7 +116,7 @@ let open_constant i ((sp,kn), obj) =
     match (Global.lookup_constant con).const_body with
     | (Def _ | Undef _) -> ()
     | OpaqueDef lc ->
-        match Opaqueproof.get_constraints lc with
+        match Opaqueproof.get_constraints (Global.opaque_tables ())lc with
         | Some f when Future.is_val f -> Global.push_context_set (Future.force f)
         | _ -> ()
 
@@ -208,7 +208,8 @@ let declare_sideff env fix_exn se =
     match cb with
     | { const_body = Def sc } -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false
     | { const_body = OpaqueDef fc } -> 
-      (Opaqueproof.force_proof fc, Opaqueproof.force_constraints fc), true
+      (Opaqueproof.force_proof (Environ.opaque_tables env) fc,
+       Opaqueproof.force_constraints (Environ.opaque_tables env) fc), true
     | { const_body = Undef _ } -> anomaly(str"Undefined side effect")
   in
   let ty_of cb =
diff --git a/library/global.ml b/library/global.ml
index 80238d8e2..49f78e495 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -113,6 +113,14 @@ let lookup_modtype kn = lookup_modtype kn (env())
 
 let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
+let opaque_tables () = Environ.opaque_tables (env ())
+let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb
+let body_of_constant cst = body_of_constant_body (lookup_constant cst)
+let constraints_of_constant_body cb =
+  Declareops.constraints_of_constant (opaque_tables ()) cb
+let universes_of_constant_body cb =
+  Declareops.universes_of_constant (opaque_tables ()) cb
+
 (** Operations on kernel names *)
 
 let constant_of_delta_kn kn =
@@ -153,7 +161,9 @@ let type_of_global_unsafe r =
   | VarRef id -> Environ.named_type id env
   | ConstRef c -> 
      let cb = Environ.lookup_constant c env in 
-     let univs = Declareops.universes_of_polymorphic_constant cb in
+     let univs =
+       Declareops.universes_of_polymorphic_constant
+         (Environ.opaque_tables env) cb in
      let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
        Vars.subst_instance_constr (Univ.UContext.instance univs) ty
   | IndRef ind ->
@@ -175,7 +185,9 @@ let type_of_global_in_context env r =
   | VarRef id -> Environ.named_type id env, Univ.UContext.empty
   | ConstRef c -> 
      let cb = Environ.lookup_constant c env in 
-     let univs = Declareops.universes_of_polymorphic_constant cb in
+     let univs =
+       Declareops.universes_of_polymorphic_constant
+         (Environ.opaque_tables env) cb in
        Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
@@ -198,7 +210,8 @@ let universes_of_global env r =
     | VarRef id -> Univ.UContext.empty
     | ConstRef c -> 
       let cb = Environ.lookup_constant c env in 
-	Declareops.universes_of_polymorphic_constant cb
+	Declareops.universes_of_polymorphic_constant
+          (Environ.opaque_tables env) cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
 	Univ.instantiate_univ_context mib.mind_universes 
diff --git a/library/global.mli b/library/global.mli
index 7dcfdbd3a..8ae77a9e4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,6 +87,14 @@ val exists_objlabel  : Label.t -> bool
 val constant_of_delta_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
 
+val opaque_tables : unit -> Opaqueproof.opaquetab
+val body_of_constant : constant -> Term.constr option
+val body_of_constant_body : Declarations.constant_body -> Term.constr option
+val constraints_of_constant_body :
+  Declarations.constant_body -> Univ.constraints
+val universes_of_constant_body :
+  Declarations.constant_body -> Univ.universe_context
+
 (** {6 Compiled libraries } *)
 
 val start_library : DirPath.t -> module_path
diff --git a/library/heads.ml b/library/heads.ml
index 8b28f0500..94ce11731 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -123,7 +123,7 @@ let compute_head = function
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
      if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
-     then Declareops.body_of_constant cb else None 
+     then Declareops.body_of_constant (Environ.opaque_tables env) cb else None 
    in
      (match body with
      | None -> RigidHead (RigidParameter cst)
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 = {
diff --git a/library/library.mli b/library/library.mli
index 5154c25e4..c92b9d623 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -43,8 +43,8 @@ val import_module : bool -> qualid located -> unit
 val start_library : string -> DirPath.t * string
 
 (** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : ?todo:((Future.UUID.t * int) list -> 'tasks) ->
-  DirPath.t -> string -> unit
+val save_library_to : ?todo:(int Future.UUIDMap.t -> 'tasks) ->
+  DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :
   string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
diff --git a/library/universes.ml b/library/universes.ml
index cc0153311..708324aed 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -310,7 +310,10 @@ let unsafe_instance_from ctx =
 let fresh_constant_instance env c inst =
   let cb = lookup_constant c env in
     if cb.Declarations.const_polymorphic then
-      let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in
+      let inst, ctx =
+        fresh_instance_from
+          (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst
+      in
 	((c, inst), ctx)
     else ((c,Instance.empty), ContextSet.empty)
 
@@ -331,7 +334,8 @@ let fresh_constructor_instance env (ind,i) inst =
 let unsafe_constant_instance env c =
   let cb = lookup_constant c env in
     if cb.Declarations.const_polymorphic then
-      let inst, ctx = unsafe_instance_from (Declareops.universes_of_constant cb) in
+      let inst, ctx = unsafe_instance_from
+        (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in
 	((c, inst), ctx)
     else ((c,Instance.empty), UContext.empty)
 
@@ -441,7 +445,7 @@ let type_of_reference env r =
      let cb = Environ.lookup_constant c env in
      let ty = Typeops.type_of_constant_type env cb.const_type in
        if cb.const_polymorphic then
-	 let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) None in
+	 let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in
 	   Vars.subst_instance_constr inst ty, ctx
        else ty, ContextSet.empty