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, 26 insertions, 28 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 55901bce9..f059ea1ae 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -28,15 +28,21 @@ let prerr_endline =
   if debug then prerr_endline else fun _ -> ()
 
 let constrain_type env j cst1 = function
-  | None ->
+  | `None ->
       make_polymorphic_if_constant_for_ind env j, cst1
-  | Some t ->
+  | `Some t ->
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
       assert (eq_constr t tj.utj_val);
       let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
       NonPolymorphicType t, cstrs
+  | `SomeWJ (t, tj, cst2) ->
+      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
+      assert (eq_constr t tj.utj_val);
+      let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
+      NonPolymorphicType t, cstrs
 
+let map_option_typ = function None -> `None | Some x -> `Some x
 
 let translate_local_assum env t =
   let (j,cst) = infer env t in
@@ -68,7 +74,7 @@ let handle_side_effects env body side_eff =
           let t = sub c 1 (Vars.lift 1 t) in
           mkLetIn (cname c, b, b_ty, t)
       | OpaqueDef b -> 
-          let b = Lazyconstr.force_opaque (Future.join b) in
+          let b = Lazyconstr.force_opaque b in
           let b_ty = Typeops.type_of_constant_type env cb.const_type in
           let t = sub c 1 (Vars.lift 1 t) in
           mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
@@ -84,28 +90,27 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Interface.Complete)
   
-(* what is used for debugging only *)
-let infer_declaration ?(what="UNKNOWN") env dcl =
+let infer_declaration env dcl =
   match dcl with
   | ParameterEntry (ctx,t,nl) ->
       let j, cst = infer env t in
       let t = hcons_constr (Typeops.assumption_of_judgment env j) in
-      Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx
+      Undef nl, NonPolymorphicType t, cst, false, ctx
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true } as c) ->
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
-      let body_cst =
+      let tyj, tycst = infer_type env typ in
+      let proofterm =
         Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) ->
           let body = handle_side_effects env body side_eff in
           let j, cst = infer env body in
           let j = hcons_j j in
-          let _typ, cst = constrain_type env j cst (Some typ) in
+          let _typ, cst = constrain_type env j cst (`SomeWJ (typ,tyj,tycst)) in
           feedback_completion_typecheck feedback_id;
-          Lazyconstr.opaque_from_val j.uj_val, cst) in
-      let body, cst = Future.split2 ~greedy:true body_cst in
-      let def = OpaqueDef body in
+          j.uj_val, cst) in
+      let def = OpaqueDef (Lazyconstr.opaque_from_val proofterm) in
       let typ = NonPolymorphicType typ in
-      def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
+      def, typ, tycst, c.const_entry_inline_code, c.const_entry_secctx
   | DefinitionEntry c ->
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
@@ -113,10 +118,9 @@ let infer_declaration ?(what="UNKNOWN") env dcl =
       let body = handle_side_effects env body side_eff in
       let j, cst = infer env body in
       let j = hcons_j j in
-      let typ, cst = constrain_type env j cst typ in
+      let typ, cst = constrain_type env j cst (map_option_typ typ) in
       feedback_completion_typecheck feedback_id;
       let def = Def (Lazyconstr.from_val j.uj_val) in
-      let cst = Future.from_val cst in
       def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
 
 let global_vars_set_constant_type env = function
@@ -127,7 +131,6 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-
 let record_aux env s1 s2 =
   let v =
     String.concat " "
@@ -157,16 +160,13 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
         let ids_def = match def with
         | Undef _ -> Idset.empty
         | Def cs -> global_vars_set env (Lazyconstr.force cs)
-        | OpaqueDef lc -> 
-            (* we force so that cst are added to the env immediately after *)
-            ignore(Future.join cst);
-            let vars =
-              global_vars_set env (Lazyconstr.force_opaque (Future.join lc)) in
+        | OpaqueDef lc ->
+            let vars = global_vars_set env (Lazyconstr.force_opaque lc) in
             !suggest_proof_using kn env vars ids_typ context_ids;
             if !Flags.compilation_mode = Flags.BuildVo then
               record_aux env ids_typ vars;
             vars
-            in
+        in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.compilation_mode = Flags.BuildVo then
@@ -184,12 +184,11 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
-            OpaqueDef (Future.chain ~greedy:true ~pure:true lc (fun lc ->
+            OpaqueDef (Lazyconstr.iter_direct_lazy_constr (fun c ->
               let ids_typ = global_vars_set_constant_type env typ in
-              let ids_def =
-                global_vars_set env (Lazyconstr.force_opaque lc) in
+              let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
-              check declared inferred; lc)) in
+              check declared inferred) lc) in
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
@@ -200,8 +199,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
 (*s Global and local constant declaration. *)
 
 let translate_constant env kn ce =
-  build_constant_declaration kn env 
-    (infer_declaration ~what:(string_of_con kn) env ce)
+  build_constant_declaration kn env (infer_declaration env ce)
 
 let translate_recipe env kn r =
   let def,typ,cst,inline_code,hyps = Cooking.cook_constant env r in
@@ -209,7 +207,7 @@ let translate_recipe env kn r =
 
 let translate_local_def env id centry =
   let def,typ,cst,inline_code,ctx =
-    infer_declaration ~what:(string_of_id id) env (DefinitionEntry centry) in
+    infer_declaration env (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   def, typ, cst