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, 22 insertions, 16 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3e9b646c1..a93415f92 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -282,11 +282,11 @@ let safe_push_named (id,_,_ as d) env =
 
 let push_named_def (id,de) senv =
   let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
-  let c = match c with
-    | Def c -> Lazyconstr.force c
-    | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c)
+  let c,cst' = match c with
+    | Def c -> Lazyconstr.force c, Univ.empty_constraint
+    | OpaqueDef c -> Lazyconstr.force_opaque_w_constraints c
     | _ -> assert false in
-  let cst = Future.join cst in
+  let senv = add_constraints (Now cst') senv in
   let senv' = add_constraints (Now cst) senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
   (cst, {senv' with env=env''})
@@ -314,13 +314,19 @@ let labels_of_mib mib =
   get ()
 
 let constraints_of_sfb = function
-  | SFBmind mib -> Now mib.mind_constraints
-  | SFBmodtype mtb -> Now mtb.typ_constraints
-  | SFBmodule mb -> Now mb.mod_constraints
-  | SFBconst cb ->
-      match Future.peek_val cb.const_constraints with
-      | Some c -> Now c
-      | None -> Later cb.const_constraints
+  | SFBmind mib -> [Now mib.mind_constraints]
+  | SFBmodtype mtb -> [Now mtb.typ_constraints]
+  | SFBmodule mb -> [Now mb.mod_constraints]
+  | SFBconst cb -> [Now cb.const_constraints] @
+      match cb.const_body with
+      | (Undef _ | Def _) -> []
+      | OpaqueDef lc ->
+          match Lazyconstr.get_opaque_future_constraints lc with
+          | None -> []
+          | Some fc ->
+              match Future.peek_val fc with
+              | None -> [Later fc]
+              | Some c -> [Now c]
 
 (** A generic function for adding a new field in a same environment.
     It also performs the corresponding [add_constraints]. *)
@@ -341,7 +347,7 @@ let add_field ((l,sfb) as field) gn senv =
     | SFBmodule _ | SFBmodtype _ ->
       check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
   in
-  let senv = add_constraints (constraints_of_sfb sfb) senv in
+  let senv = List.fold_right add_constraints (constraints_of_sfb sfb) senv in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
     | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
@@ -377,8 +383,7 @@ let add_constant dir l decl senv =
     | OpaqueDef lc when DirPath.is_empty dir ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
-      { cb with const_body =
-           OpaqueDef (Future.chain ~greedy:true ~pure:true lc Lazyconstr.turn_indirect) }
+      { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) }
     | _ -> cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
@@ -660,10 +665,11 @@ let start_library dir senv =
 let export compilation_mode senv dir =
   let senv =
     try
-      if compilation_mode = Flags.BuildVi then senv (* FIXME: cleanup future*)
+      if compilation_mode = Flags.BuildVi then { senv with future_cst = [] }
       else join_safe_environment senv
-    with e -> Errors.errorlabstrm "future" (Errors.print e)
+    with e -> Errors.errorlabstrm "export" (Errors.print e)
   in
+  assert(senv.future_cst = []);
   let () = check_current_library dir senv in
   let mp = senv.modpath in
   let str = NoFunctor (List.rev senv.revstruct) in