New compilation mode -vi2vo

To obtain a.vo one can now:
1) coqtop -quick -compile a
2) coqtop -vi2vo a.vi

To make that possible the .vo structure has been complicated.  It is now
made of 5 segments.

               |  vo  | vi  | vi2vo | contents
 --------------+------+-----+-------+------------------------------------
 lib           | Yes  | Yes | Yes   | libstack (modules, notations,...)
 opauqe_univs  | No   | Yes | Yes   | constraints coming from opaque proofs
 discharge     | No   | Yes | No    | data needed to close sections
 tasks         | No   | Yes | No    | STM tasks to produce proof terms
 opaque_proofs | Yes  | Yes | Yes   | proof terms
 --------------+------+-----+-------+------------------------------------

This means one can load only the strictly necessay parts.  Usually one
does not load the tasks segment of a .vi nor the opaque_proof segment of
a .vo, unless one is turning a .vi into a .vo, in which case he load
all the segments.

Optional segments are marshalled as None.  But for lib, all segments
are Array.t of:

               | type
 --------------+---------------------------------------------------------
 lib           | a list of Libobject.obj (n'importe quoi)
 opauqe_univs  | Univ.consraints Future.computation
 discharge     | what Cooking.cook_constr needs
 tasks         | Stm.tasks (a task is system_state * vernacexpr list)
 opaque_proofs | Term.constr Future.computation
 --------------+------+-----+-------+------------------------------------

Invariant: all Future.computation in a vo file (obtained by a vi2vo
compilation or not) have been terminated with Future.join (or
Future.sink).  This means they are values (inside a box).
This invariant does not hold for vi files.  E.g. opauqe_proofs can be
dangling Future.computation (i.e. NotHere exception).  The vi2vo
compilation step will replace them by true values.

Rationale for opaque_univs: in the vi2vo transformation we want to reuse
the lib segment.  Hence the missing pieces have to be put on the side,
not inside.  Opaque proof terms are already in a separte segment.
Universe constraints are not, hence the new opauqe_univs segment.  Such
segment, if present in a .vo file, is always loaded, and
Declare.open_constant will add to the environment the constraints stored
there.  For regular constants this is not necessay since the constraints
are already in their enclosing module (and also in the constant_body).
With vi2vo the constraints coming from the proof are not in the
constant_body (hence not in the enclosing module) but there and are
added to the environment explicitly by Declare.open_constant.

Rationale for discharge: vi2vo produces a proof term in its original
context (in the middle of a section).  Then it has to discharge the
object.  This segment contains the data that is needed in order to do
so.  It is morally the input that Lib.close_section passes to Cooking
(via the insane rewinding of libstack, GlobalRecipe, etc chain).

Checksums: the checksum of .vi and a .vo obtain from it is the same.
This means that if if b.vo has been compiled using a.vi, and then
a.vi is compiled into a.vo, Require Import b works (and recursively
loads a.vo).

5 files changed, 182 insertions, 57 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 3bd4cdd3f..477e96bd8 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -117,7 +117,13 @@ let open_constant i ((sp,kn), obj) =
   if obj.cst_locl then ()
   else
     let con = Global.constant_of_delta_kn kn in
-    Nametab.push (Nametab.Exactly i) sp (ConstRef con)
+    Nametab.push (Nametab.Exactly i) sp (ConstRef con);
+    match (Global.lookup_constant con).const_body with
+    | (Def _ | Undef _) -> ()
+    | OpaqueDef lc ->
+        match Lazyconstr.get_opaque_future_constraints lc with
+        | Some f when Future.is_val f -> Global.add_constraints (Future.force f)
+        | _ -> ()
 
 let exists_name id =
   variable_exists id || Global.exists_objlabel (Label.of_id id)
@@ -144,12 +150,12 @@ let discharged_hyps kn sechyps =
 
 let discharge_constant ((sp, kn), obj) =
   let con = constant_of_kn kn in
-  let cb = Global.lookup_constant con in
-  let repl = replacement_context () in
-  let sechyps = section_segment_of_constant con in
-  let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in
-  let new_hyps = (discharged_hyps kn sechyps) @ obj.cst_hyps in
-  let new_decl = GlobalRecipe recipe in
+  let from = Global.lookup_constant con in
+  let modlist = replacement_context () in
+  let hyps = section_segment_of_constant con in
+  let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
+  let abstract = named_of_variable_context hyps in
+  let new_decl = GlobalRecipe{ from; info = { Lazyconstr.modlist; abstract }} in
   Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -192,8 +198,7 @@ let declare_sideff se =
   let pt_opaque_of cb =
     match cb with
     | { const_body = Def sc } -> Lazyconstr.force sc, false
-    | { const_body = OpaqueDef fc } ->
-          Lazyconstr.force_opaque (Future.force fc), true
+    | { const_body = OpaqueDef fc } -> Lazyconstr.force_opaque fc, true
     | { const_body = Undef _ } -> anomaly(str"Undefined side effect")
   in
   let ty_of cb =
diff --git a/library/lib.ml b/library/lib.ml
index eef8171cc..ee89bb997 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -385,7 +385,7 @@ type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap
 
 let sectab =
   Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
-		        Cooking.work_list * abstr_list) list)
+		        Lazyconstr.work_list * abstr_list) list)
     ~name:"section-context"
 
 let add_section () =
@@ -455,6 +455,13 @@ let section_instance = function
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
+let full_replacement_context () = List.map pi2 !sectab
+let full_section_segment_of_constant con =
+  List.map (fun (vars,_,(x,_)) -> fun hyps ->
+    named_of_variable_context
+      (try Names.Cmap.find con x
+      with Not_found -> extract_hyps (vars, hyps))) !sectab
+
 (*************)
 (* Sections. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index fa3bd3f48..787dc969e 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -186,4 +186,9 @@ val discharge_con : Names.constant -> Names.constant
 val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
 
+(* discharging a constant in one go *)
+val full_replacement_context : unit -> Lazyconstr.work_list list
+val full_section_segment_of_constant :
+  Names.constant -> (Context.named_context -> Context.named_context) list
+
 
diff --git a/library/library.ml b/library/library.ml
index 1088bcb16..c40f9d204 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -299,12 +299,10 @@ exception Faulty
 (** Fetching a table of opaque terms at position [pos] in file [f],
     expecting to find first a copy of [digest]. *)
 
-let fetch_opaque_table dp (f,pos,digest) =
-  if !Flags.load_proofs == Flags.Dont then
-    error "Not accessing an opaque term due to option -dont-load-proofs.";
+let fetch_table what dp (f,pos,digest) =
   let dir_path = Names.DirPath.to_string dp in
   try
-    Pp.msg_info (Pp.str "Fetching opaque terms from disk for " ++ str dir_path);
+    msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
     let ch = System.with_magic_number_check raw_intern_library f in
     let () = seek_in ch pos in
     if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
@@ -316,64 +314,129 @@ let fetch_opaque_table dp (f,pos,digest) =
     table
   with e when Errors.noncritical e ->
     error
-      ("The file "^f^" (bound to " ^ dir_path ^ ") is inaccessible or corrupted,\n"
-       ^ "cannot load some opaque constant bodies in it.\n")
+      ("The file "^f^" (bound to " ^ dir_path ^
+      ") is inaccessible or corrupted,\n" ^
+      "cannot load some "^what^" in it.\n")
 
 (** Delayed / available tables of opaque terms *)
 
-type opaque_table_status =
+type 'a table_status =
   | ToFetch of string * int * Digest.t
-  | Fetched of Term.constr array
+  | Fetched of 'a Future.computation array
 
-let opaque_tables = ref (LibraryMap.empty : opaque_table_status LibraryMap.t)
+let opaque_tables =
+  ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t)
+let univ_tables =
+  ref (LibraryMap.empty : (Univ.constraints table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
+let add_univ_table dp st =
+  univ_tables := LibraryMap.add dp st !univ_tables
 
-let access_opaque_table dp i =
-  let t = match LibraryMap.find dp !opaque_tables with
+let access_table fetch_table add_table tables dp i =
+  let t = match LibraryMap.find dp tables with
     | Fetched t -> t
     | ToFetch (f,pos,digest) ->
-      let t = fetch_opaque_table dp (f,pos,digest) in
-      add_opaque_table dp (Fetched t);
+      let t = fetch_table dp (f,pos,digest) in
+      add_table dp (Fetched t);
       t
   in
   assert (i < Array.length t); t.(i)
 
+let access_opaque_table dp i =
+  if !Flags.load_proofs == Flags.Dont then
+    error "Not accessing an opaque term due to option -dont-load-proofs.";
+  access_table
+    (fetch_table "opaque proofs")
+    add_opaque_table !opaque_tables dp i
+let access_univ_table dp i =
+  access_table
+    (fetch_table "universe constraints 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 = Term.mkRel 1
+ let a_constr = Future.from_val (Term.mkRel 1)
+ let a_univ = Future.from_val Univ.empty_constraint
+ let a_discharge : Lazyconstr.cooking_info list = []
 
- let local_table = ref (Array.make 100 a_constr)
+ 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
 
- let get dp i =
+ module FMap = Map.Make(Future.UUID)
+ let f2t = ref FMap.empty
+
+ let get_opaque_nolib _ i = (!local_opaque_table).(i)
+
+ let get_opaque dp i =
    if DirPath.equal dp (Lib.library_dp ())
-   then (!local_table).(i)
+   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
+    Future.sink (!local_opaque_table).(i)
 
- let store c =
+ let join_local_univ dp i =
+   if DirPath.equal dp (Lib.library_dp ()) then
+    Future.sink (!local_univ_table).(i)
+
+ let get_univ_nolib _ i = Some (!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_table) then begin
+  if Int.equal n (Array.length !local_opaque_table) then begin
     let t = Array.make (2*n) a_constr in
-    Array.blit !local_table 0 t 0 n;
-    local_table := t
+    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;
-  (!local_table).(n) <- c;
+  let c, u = Future.split2 ~greedy:true cu in
+  if Future.is_val u then ignore(Future.join u);
+  if Future.is_val c then ignore(Future.join 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_table 0 !local_index
+ 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
 
 end
 
-let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get
+let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque
+let _ = Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ
+let _ = Lazyconstr.set_join_indirect_local_opaque OpaqueTables.join_local_opaque
+let _ = Lazyconstr.set_join_indirect_local_univ OpaqueTables.join_local_univ
 
 (************************************************************************)
 (* Internalise libraries *)
 
+type seg_lib = library_disk
+type seg_univ = Univ.constraints Future.computation array
+type seg_discharge = Lazyconstr.cooking_info list array
+type seg_proofs = Term.constr Future.computation array
+
 let mk_library md digest =
   {
     library_name     = md.md_name;
@@ -386,7 +449,10 @@ let mk_library md digest =
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
-  let lmd, _, digest_lmd = System.marshal_in_segment f ch in
+  let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
+  let (univs : seg_univ option), _, _ = System.marshal_in_segment f ch in
+  Option.iter (fun univs -> add_univ_table lmd.md_name (Fetched univs)) univs;
+  let _ = System.skip_in_segment f ch in
   let pos, digest = System.skip_in_segment f ch in
   register_library_filename lmd.md_name f;
   add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
@@ -394,18 +460,6 @@ let intern_from_file f =
   close_in ch;
   library
 
-let load_library_todo f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
-  let f = longf^"i" in
-  let ch = System.with_magic_number_check raw_intern_library f in
-  let _ = System.skip_in_segment f ch in
-  let tasks, _, _ = System.marshal_in_segment f ch in
-  match tasks with
-  | Some a -> a, longf
-  | None -> errorlabstrm "load_library_todo" (str"not a .vi file")
-
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
   try find_library dir, needed
@@ -604,10 +658,27 @@ let start_library f =
   let id = Id.of_string (Filename.basename f) in
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
-  Lazyconstr.set_indirect_opaque_creator OpaqueTables.store;
+  Lazyconstr.set_indirect_creator OpaqueTables.store;
   Declaremods.start_library ldir;
   ldir,longf
 
+let load_library_todo f =
+  let paths = Loadpath.get_paths () in
+  let _, longf =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let f = longf^"i" in
+  let ch = System.with_magic_number_check raw_intern_library f in
+  let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
+  let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
+  let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
+  let tasks, _, _ = System.marshal_in_segment f ch in
+  let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
+  close_in ch;
+  if tasks = None then errorlabstrm "restart" (str"not a .vi file");
+  if s2 = None then errorlabstrm "restart" (str"not a .vi file");
+  if s3 = None then errorlabstrm "restart" (str"not a .vi file");
+  longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
 
@@ -635,10 +706,25 @@ let error_recursively_dependent_library dir =
    writing the content and computing the checksum... *)
 
 let save_library_to ?todo dir f =
-  let f = if todo = None then f ^ "o" else f ^ "i" in
-  Lazyconstr.reset_indirect_opaque_creator ();
+  let f, todo, utab, dtab =
+    match todo with
+    | None ->
+        assert(!Flags.compilation_mode = Flags.BuildVo);
+        f ^ "o", (fun _ -> None), (fun _ -> None), (fun _ -> None)
+    | Some d ->
+        assert(!Flags.compilation_mode = Flags.BuildVi);
+        f ^ "i", (fun x -> Some (d x)), (fun x -> Some x), (fun x -> Some x) in
+  Lazyconstr.reset_indirect_creator ();
+  (* HACK: end_library resets Lib and then joins the safe env.  To join the
+   * env one needs to access the futures stored in the tables.  Standard
+   * accessors use Lib.  Hence *)
+  Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib;
+  Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ_nolib;
   let cenv, seg, ast = Declaremods.end_library dir in
-  let table = OpaqueTables.dump () in
+  let opaque_table, univ_table, disch_table, f2t_map =
+    OpaqueTables.dump () in
+  assert(!Flags.compilation_mode = Flags.BuildVi ||
+         Array.for_all Future.is_val opaque_table);
   let md = {
     md_name = dir;
     md_compiled = cenv;
@@ -651,9 +737,11 @@ let save_library_to ?todo dir f =
   let (f',ch) = raw_extern_library f in
   try
     (* Writing vo payload *)
-    System.marshal_out_segment f' ch md;    (* env + objs *)
-    System.marshal_out_segment f' ch todo;  (* STM tasks  *)
-    System.marshal_out_segment f' ch table; (* opaques    *)
+    System.marshal_out_segment f' ch (md               : seg_lib);
+    System.marshal_out_segment f' ch (utab univ_table  : seg_univ option);
+    System.marshal_out_segment f' ch (dtab disch_table : seg_discharge option);
+    System.marshal_out_segment f' ch (todo f2t_map     : 'tasks option);
+    System.marshal_out_segment f' ch (opaque_table     : seg_proofs);
     close_out ch;
     (* Writing native code files *)
     if not !Flags.no_native_compiler then
@@ -662,7 +750,7 @@ let save_library_to ?todo dir f =
       let lp = List.map map_path lp in
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Int.equal (Nativelibrary.compile_library dir ast lp fn) 0) then
-        msg_error (str "Could not compile the library to native code. Skipping.")
+        msg_error (str"Could not compile the library to native code. Skipping.")
    with reraise ->
     let reraise = Errors.push reraise in
     let () = msg_warning (str ("Removed file "^f')) in
@@ -670,6 +758,15 @@ let save_library_to ?todo dir f =
     let () = Sys.remove f' in
     raise reraise
 
+let save_library_raw f lib univs proofs =
+  let (f',ch) = raw_extern_library (f^"o") in
+  System.marshal_out_segment f' ch (lib        : seg_lib);
+  System.marshal_out_segment f' ch (Some univs : seg_univ option);
+  System.marshal_out_segment f' ch (None       : seg_discharge option);
+  System.marshal_out_segment f' ch (None       : 'tasks option);
+  System.marshal_out_segment f' ch (proofs     : seg_proofs);
+  close_out ch
+
 (************************************************************************)
 (*s Display the memory use of a library. *)
 
diff --git a/library/library.mli b/library/library.mli
index 647138483..ec39059e9 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -29,6 +29,13 @@ val require_library_from_file :
   Id.t option -> CUnix.physical_path -> bool option -> unit
 
 (** {6 ... } *)
+
+(** Segments of a library *)
+type seg_lib
+type seg_univ = Univ.constraints Future.computation array
+type seg_discharge = Lazyconstr.cooking_info list array
+type seg_proofs = Term.constr Future.computation array
+
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located -> unit
@@ -37,8 +44,12 @@ 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:'a -> DirPath.t -> string -> unit
-val load_library_todo : string -> 'a * string
+val save_library_to : ?todo:((Future.UUID.t * int) list -> 'tasks) ->
+  DirPath.t -> string -> unit
+
+val load_library_todo :
+  string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit
 
 (** {6 Interrogate the status of libraries } *)