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).

1 files changed, 79 insertions, 21 deletions

diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml
index 21aba6348a..23d6d559d9 100644
--- a/kernel/lazyconstr.ml
+++ b/kernel/lazyconstr.ml
@@ -10,6 +10,9 @@ open Names
 open Term
 open Mod_subst
 
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context } 
+
 (** [constr_substituted] are [constr] with possibly pending
     substitutions of kernel names. *)
 
@@ -29,48 +32,103 @@ let subst_constr_subst = subst_substituted
     should end in a .vo, this is checked by coqchk.
 *)
 
+type proofterm = (constr * Univ.constraints) Future.computation
 type lazy_constr =
-  | Indirect of substitution list * DirPath.t * int (* lib,index *)
-  | Direct of constr_substituted (* opaque in section or interactive session *)
+  (* subst, lib, index *)
+  | Indirect of substitution list * DirPath.t * int
+  (* opaque in section or interactive session *)
+  | Direct of cooking_info list * (constr_substituted * Univ.constraints) Future.computation
 
 (* TODO : this hcons function could probably be improved (for instance
    hash the dir_path in the Indirect case) *)
 
-let hcons_lazy_constr = function
-  | Direct c -> Direct (from_val (hcons_constr (force c)))
-  | Indirect _ as lc -> lc
-
 let subst_lazy_constr sub = function
-  | Direct cs -> Direct (subst_constr_subst sub cs)
+  | Direct ([],cu) ->
+      Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
+        subst_constr_subst sub c, u))
+  | Direct _ -> Errors.anomaly (Pp.str"still direct but not discharged")
   | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
 
+let iter_direct_lazy_constr f = function
+  | Indirect _ -> Errors.anomaly (Pp.str "iter_direct_lazy_constr")
+  | Direct (d,cu) ->
+      Direct (d, Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> f (force c); c, u))
+
+let discharge_direct_lazy_constr modlist abstract  f = function
+  | Indirect _ -> Errors.anomaly (Pp.str "discharge_direct_lazy_constr")
+  | Direct (d,cu) ->
+      Direct ({ modlist; abstract }::d,
+        Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
+          from_val (f (force c)), u))
+
 let default_get_opaque dp _ =
   Errors.error
-    ("Cannot access an opaque term in library " ^ DirPath.to_string dp)
+    ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
+let default_get_univ dp _ =
+  Errors.error
+    ("Cannot access universe constraints of opaque proofs in library " ^
+    DirPath.to_string dp)
 
-let default_mk_opaque _ = None
+let default_mk_indirect _ = None
+
+let default_join_indirect_local_opaque _ _ = ()
+let default_join_indirect_local_univ _ _ = ()
 
 let get_opaque = ref default_get_opaque
-let mk_opaque = ref default_mk_opaque
+let get_univ = ref default_get_univ
+let join_indirect_local_opaque = ref default_join_indirect_local_opaque
+let join_indirect_local_univ = ref default_join_indirect_local_univ
+
+let mk_indirect = ref default_mk_indirect
 let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_opaque_creator f = (mk_opaque := f)
-let reset_indirect_opaque_creator () = (mk_opaque := default_mk_opaque)
+let set_indirect_univ_accessor f = (get_univ := f)
+let set_indirect_creator f = (mk_indirect := f)
+let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
+let set_join_indirect_local_univ f = join_indirect_local_univ := f
+
+let reset_indirect_creator () = mk_indirect := default_mk_indirect
 
 let force_lazy_constr = function
-  | Direct c -> c
+  | Direct (_,c) -> Future.force c
   | Indirect (l,dp,i) ->
-    List.fold_right subst_constr_subst l (from_val (!get_opaque dp i))
+      let c = Future.force (!get_opaque dp i) in
+      List.fold_right subst_constr_subst l (from_val c),
+      Future.force
+        (Option.default
+          (Future.from_val Univ.empty_constraint)
+          (!get_univ dp i))
+
+let join_lazy_constr = function
+  | Direct (_,c) -> ignore(Future.force c)
+  | Indirect (_,dp,i) ->
+      !join_indirect_local_opaque dp i;
+      !join_indirect_local_univ dp i
 
 let turn_indirect lc = match lc with
   | Indirect _ ->
     Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
-  | Direct c ->
-    (* this constr_substituted shouldn't have been substituted yet *)
-    assert (fst (Mod_subst.repr_substituted c) == None);
-    match !mk_opaque (force c) with
+  | Direct (d,cu) ->
+    let cu = Future.chain ~greedy:true ~pure:true cu (fun (c,u) ->
+      (* this constr_substituted shouldn't have been substituted yet *)
+      assert (fst (Mod_subst.repr_substituted c) == None);
+      hcons_constr (force c),u) in
+    match !mk_indirect (d,cu) with
       | None -> lc
       | Some (dp,i) -> Indirect ([],dp,i)
 
-let force_opaque lc = force (force_lazy_constr lc)
-
-let opaque_from_val c = Direct (from_val c)
+let force_opaque lc =
+  let c, _u = force_lazy_constr lc in force c
+let force_opaque_w_constraints lc =
+  let c, u = force_lazy_constr lc in force c, u
+let get_opaque_future_constraints lc = match lc with
+  | Indirect (_,dp,i) -> !get_univ dp i
+  | Direct (_,cu) -> Some(snd (Future.split2 ~greedy:true cu))
+let get_opaque_futures lc = match lc with
+  | Indirect _ -> assert false
+  | Direct (_,cu) ->
+      let cu =
+        Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> force c, u) in
+      Future.split2 ~greedy:true cu
+
+let opaque_from_val cu =
+  Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> from_val c, u))