State Transaction Machine

The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).

The observe id function runs the transactions necessary to reach to the
state id.  Transaction being on a merged branch are not executed but
stored into a future.

The finish function calls observe on the tip of the current branch.

Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.

This is the work described in the Coq Workshop 2012 paper.

Coq is compile with thread support from now on.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 355 insertions, 124 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index bb29b9645..4c2f22199 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -42,11 +42,7 @@ type my_global_reference =
   | IndRef of inductive
   | ConstructRef of constructor
 
-let cache = (Hashtbl.create 13 : (my_global_reference, constr) Hashtbl.t)
-
-let clear_cooking_sharing () = Hashtbl.clear cache
-
-let share r (cstl,knl) =
+let share cache r (cstl,knl) =
   try Hashtbl.find cache r
   with Not_found ->
   let f,l =
@@ -59,13 +55,12 @@ let share r (cstl,knl) =
 	mkConst (pop_con cst), Cmap.find cst cstl in
   let c = mkApp (f, Array.map mkVar l) in
   Hashtbl.add cache r c;
-  (* has raised Not_found if not in work_list *)
   c
 
-let update_case_info ci modlist =
+let update_case_info cache ci modlist =
   try
     let ind, n =
-      match kind_of_term (share (IndRef ci.ci_ind) modlist) with
+      match kind_of_term (share cache (IndRef ci.ci_ind) modlist) with
       | App (f,l) -> (destInd f, Array.length l)
       | Ind ind -> ind, 0
       | _ -> assert false in
@@ -78,7 +73,9 @@ let empty_modlist = (Cmap.empty, Mindmap.empty)
 let is_empty_modlist (cm, mm) =
   Cmap.is_empty cm && Mindmap.is_empty mm
 
-let expmod_constr modlist c =
+let expmod_constr cache modlist c =
+  let share = share cache in
+  let update_case_info = update_case_info cache in
   let rec substrec c =
     match kind_of_term c with
       | Case (ci,p,t,br) ->
@@ -122,25 +119,27 @@ type recipe = {
 type inline = bool
 
 type result =
-  constant_def * constant_type * Univ.constraints * inline
+  constant_def * constant_type * constant_constraints * inline
     * Context.section_context option
 
 let on_body f = function
-  | Undef inl -> Undef inl
+  | Undef _ as x -> x
   | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
   | OpaqueDef lc ->
-    OpaqueDef (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))
+    OpaqueDef (Future.chain ~id:"Cooking.on_body" ~pure:true lc (fun lc ->
+        (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))))
 
 let constr_of_def = function
   | Undef _ -> assert false
   | Def cs -> Lazyconstr.force cs
-  | OpaqueDef lc -> Lazyconstr.force_opaque lc
+  | OpaqueDef lc -> Lazyconstr.force_opaque (Future.force lc)
 
 let cook_constant env r =
+  let cache = Hashtbl.create 13 in
   let cb = r.d_from in
-  let hyps = Context.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
+  let hyps = Context.map_named_context (expmod_constr cache r.d_modlist) r.d_abstract in
   let body = on_body
-    (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps)
+    (fun c -> abstract_constant_body (expmod_constr cache r.d_modlist c) hyps)
     cb.const_body
   in
   let const_hyps =
@@ -149,12 +148,16 @@ let cook_constant env r =
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
     | NonPolymorphicType t ->
-	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
+	let typ =
+          abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in
 	NonPolymorphicType typ
     | PolymorphicArity (ctx,s) ->
 	let t = mkArity (ctx,Type s.poly_level) in
-	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
+	let typ =
+          abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in
 	let j = make_judge (constr_of_def body) typ in
 	Typeops.make_polymorphic_if_constant_for_ind env j
   in
   (body, typ, cb.const_constraints, cb.const_inline_code, Some const_hyps)
+
+let expmod_constr modlist c = expmod_constr (Hashtbl.create 13) modlist c
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 8d046a12e..2d6e53407 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -24,17 +24,12 @@ type recipe = {
 type inline = bool
 
 type result =
-  constant_def * constant_type * constraints * inline
+  constant_def * constant_type * constant_constraints * inline
     * Context.section_context option
 
 val cook_constant : env -> recipe -> result
 
-
 (** {6 Utility functions used in module [Discharge]. } *)
 
 val expmod_constr : work_list -> constr -> constr
 
-val clear_cooking_sharing : unit -> unit
-
-
-
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 43b908e1f..5cb406ffa 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -38,7 +38,7 @@ type inline = int option
 type constant_def =
   | Undef of inline
   | Def of Lazyconstr.constr_substituted
-  | OpaqueDef of Lazyconstr.lazy_constr
+  | OpaqueDef of Lazyconstr.lazy_constr Future.computation
 
 (** Linking information for the native compiler. The boolean flag indicates if
   the term is protected by a lazy tag *)
@@ -48,15 +48,19 @@ type native_name =
   | LinkedInteractive of string * bool
   | NotLinked
 
+type constant_constraints = Univ.constraints Future.computation
+
 type constant_body = {
     const_hyps : Context.section_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted;
-    const_constraints : Univ.constraints;
+    const_constraints : constant_constraints;
     const_native_name : native_name ref;
     const_inline_code : bool }
 
+type side_effect = NewConstant of constant * constant_body
+    
 (** {6 Representation of mutual inductive types in the kernel } *)
 
 type recarg =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 64496033a..e597ea9a9 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,7 +19,7 @@ open Util
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
   | Def c -> Some (Lazyconstr.force c)
-  | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc)
+  | OpaqueDef lc -> Some (Lazyconstr.force_opaque (Future.force lc))
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
@@ -50,7 +50,8 @@ let subst_const_type sub arity =
 let subst_const_def sub = function
   | Undef inl -> Undef inl
   | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+  | OpaqueDef lc ->
+      OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
 
 let subst_const_body sub cb = {
   const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
@@ -84,14 +85,24 @@ let hcons_const_type = function
 
 let hcons_const_def = function
   | Undef inl -> Undef inl
-  | Def cs -> Def (from_val (Term.hcons_constr (Lazyconstr.force cs)))
-  | OpaqueDef lc -> OpaqueDef (Lazyconstr.hcons_lazy_constr lc)
+  | Def l_constr ->
+    let constr = force l_constr in
+    Def (from_val (Term.hcons_constr constr))
+  | OpaqueDef lc ->
+    if Future.is_val lc then
+      let constr = force_opaque (Future.force lc) in
+      OpaqueDef (Future.from_val (opaque_from_val (Term.hcons_constr constr)))
+    else OpaqueDef lc
 
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = hcons_const_type cb.const_type;
-    const_constraints = Univ.hcons_constraints cb.const_constraints }
+    const_constraints =
+      if Future.is_val cb.const_constraints then
+        Future.from_val
+          (Univ.hcons_constraints (Future.force cb.const_constraints))
+      else cb.const_constraints }
 
 (** Inductive types *)
 
@@ -193,3 +204,21 @@ let hcons_mind mib =
     mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_constraints = Univ.hcons_constraints mib.mind_constraints }
+
+let join_constant_body cb =
+  ignore(Future.join cb.const_constraints);
+  match cb.const_body with
+  | OpaqueDef d -> ignore(Future.join d)
+  | _ -> ()
+
+let string_of_side_effect = function
+  | NewConstant (c,_) -> Names.string_of_con c
+type side_effects = side_effect list
+let no_seff = ([] : side_effects)
+let iter_side_effects f l = List.iter f l
+let fold_side_effects f a l = List.fold_left f a l
+let uniquize_side_effects l = List.uniquize l
+let union_side_effects l1 l2 = l1 @ l2
+let flatten_side_effects l = List.flatten l
+let side_effects_of_list l = l
+let cons_side_effects x l = x :: l
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index c4d67ba52..635b8c47a 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -28,6 +28,19 @@ val body_of_constant : constant_body -> Term.constr option
 
 val is_opaque : constant_body -> bool
 
+(** Side effects *)
+
+val string_of_side_effect : side_effect -> string
+
+type side_effects
+val no_seff : side_effects
+val iter_side_effects : (side_effect -> unit) -> side_effects -> unit
+val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a
+val uniquize_side_effects : side_effects -> side_effects
+val union_side_effects : side_effects -> side_effects -> side_effects
+val flatten_side_effects : side_effects list -> side_effects
+val side_effects_of_list : side_effect list -> side_effects
+val cons_side_effects : side_effect -> side_effects -> side_effects
 
 (** {6 Inductive types} *)
 
@@ -45,6 +58,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 
+val join_constant_body : constant_body -> unit
 
 (** {6 Hash-consing} *)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 392a2cd84..3b7a2fd19 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -47,7 +47,8 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list }
 
 (** {6 Constants (Definition/Axiom) } *)
-type const_entry_body = constr
+type proof_output = constr * Declareops.side_effects
+type const_entry_body = proof_output Future.computation
 
 type definition_entry = {
   const_entry_body   : const_entry_body;
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f7f3c2b77..67db4e806 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -97,16 +97,17 @@ and check_with_def env sign (idl,c) mp equiv =
 		    let (j,cst1) = Typeops.infer env' c in
 		    let typ = Typeops.type_of_constant_type env' cb.const_type in
 		    let cst2 = Reduction.conv_leq env' j.uj_type typ in
-		    let cst =
-		      union_constraints
-			(union_constraints cb.const_constraints cst1)
+		    let cst = union_constraints
+			(union_constraints
+                          (Future.force cb.const_constraints) cst1)
 			cst2
 		    in
 		    let def = Def (Lazyconstr.from_val j.uj_val) in
 		    def,cst
 		| Def cs ->
 		    let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
-		    let cst = union_constraints cb.const_constraints cst1 in
+		    let cst = union_constraints
+                      (Future.force cb.const_constraints) cst1 in
 		    let def = Def (Lazyconstr.from_val c) in
 		    def,cst
 	      in
@@ -115,7 +116,7 @@ and check_with_def env sign (idl,c) mp equiv =
 		  const_body = def;
 		  const_body_code =
 		    Cemitcodes.from_val (compile_constant_body env' def);
-		  const_constraints = cst }
+		  const_constraints = Future.from_val cst }
 	      in
 	      SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
       | _ ->
@@ -373,13 +374,14 @@ let rec add_struct_expr_constraints env = function
 	  (add_struct_expr_constraints env meb1)
 	  meb2)
   | SEBwith(meb,With_definition_body(_,cb))->
-      Environ.add_constraints cb.const_constraints
+      Environ.add_constraints (Future.force cb.const_constraints)
 	(add_struct_expr_constraints env meb)
   | SEBwith(meb,With_module_body(_,_))->
       add_struct_expr_constraints env meb
 		
 and add_struct_elem_constraints env = function 
-  | SFBconst cb -> Environ.add_constraints cb.const_constraints env
+  | SFBconst cb -> 
+      Environ.add_constraints (Future.force cb.const_constraints) env
   | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
   | SFBmodule mb -> add_module_constraints env mb
   | SFBmodtype mtb -> add_modtype_constraints env mtb
@@ -418,7 +420,7 @@ let rec struct_expr_constraints cst = function
 	meb2
   | SEBwith(meb,With_definition_body(_,cb))->
       struct_expr_constraints
-        (Univ.union_constraints cb.const_constraints cst) meb
+        (Univ.union_constraints (Future.force cb.const_constraints) cst) meb
   | SEBwith(meb,With_module_body(_,_))->
       struct_expr_constraints  cst meb	
 		
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 3b789016b..39e5514c9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -588,3 +588,32 @@ let clean_bounded_mod_expr = function
       let str_clean = collect_mbid [] str in 
 	if  str_clean == str then str else str_clean
   | str -> str
+
+let rec join_module_body mb =
+  Option.iter join_struct_expr_body mb.mod_expr;
+  Option.iter join_struct_expr_body mb.mod_type_alg;
+  join_struct_expr_body mb.mod_type
+and join_structure_body struc =
+  let join_body (l,body) = match body with
+    | SFBconst sb -> join_constant_body sb
+    | SFBmind _ -> ()
+    | SFBmodule m -> join_module_body m
+    | SFBmodtype m ->
+         join_struct_expr_body m.typ_expr;
+         Option.iter join_struct_expr_body m.typ_expr_alg in
+  List.iter join_body struc;
+and join_struct_expr_body = function
+  | SEBfunctor (_,t,e) ->
+      join_struct_expr_body t.typ_expr;
+      Option.iter join_struct_expr_body t.typ_expr_alg;
+      join_struct_expr_body e
+  | SEBident mp -> ()
+  | SEBstruct s -> join_structure_body s
+  | SEBapply (mexpr,marg,u) ->
+       join_struct_expr_body mexpr;
+       join_struct_expr_body marg
+  | SEBwith (seb,wdcl) ->
+       join_struct_expr_body seb;
+       match wdcl with
+       | With_module_body _ -> ()
+       | With_definition_body (_, sb) -> join_constant_body sb
diff --git a/kernel/modops.mli b/kernel/modops.mli
index c4d8ab349..30f9274d2 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -50,6 +50,10 @@ val subst_modtype_and_resolver : module_type_body -> module_path ->
 
 val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
 
+val join_module_body : module_body -> unit
+val join_structure_body : structure_body -> unit
+val join_struct_expr_body : struct_expr_body -> unit
+
 (** Errors *)
 
 type signature_mismatch_error =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 753b97a0c..13368aab9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -99,6 +99,7 @@ type safe_environment =
       objlabels : Label.Set.t;
       revstruct : structure_body;
       univ : Univ.constraints;
+      future_cst : Univ.constraints Future.computation list;
       engagement : engagement option;
       imports : library_info list;
       loads : (module_path * module_body) list;
@@ -107,6 +108,36 @@ type safe_environment =
 let exists_modlabel l senv = Label.Set.mem l senv.modlabels
 let exists_objlabel l senv = Label.Set.mem l senv.objlabels
 
+(* type to be maintained isomorphic to Entries.side_effects *)
+(* XXX ideally this function obtains a valid side effect that 
+ * can be pushed into another (safe) environment without re-typechecking *)
+type side_effect = NewConstant of constant * constant_body
+let sideff_of_con env c = 
+  Obj.magic (NewConstant (c, Environ.lookup_constant c env.env))
+
+let env_of_safe_env senv = senv.env
+let env_of_senv = env_of_safe_env
+
+type constraints_addition =
+  Now of Univ.constraints | Later of Univ.constraints Future.computation
+
+let add_constraints cst senv =
+  match cst with
+  | Later fc -> {senv with future_cst = fc :: senv.future_cst}
+  | Now cst ->
+  { senv with
+    env = Environ.add_constraints cst senv.env;
+    univ = Univ.union_constraints cst senv.univ }
+
+let is_curmod_library senv = 
+  match senv.modinfo.variant with LIBRARY _ -> true | _ -> false
+
+let rec join_safe_environment e =
+  join_structure_body e.revstruct;
+  List.fold_left 
+    (fun e fc -> add_constraints (Now (Future.join fc)) e)
+    {e with future_cst = []} e.future_cst
+
 let check_modlabel l senv =
   if exists_modlabel l senv then error_existing_label l
 let check_objlabel l senv =
@@ -141,25 +172,21 @@ let rec empty_environment =
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
     revstruct = [];
+    future_cst = [];
     univ = Univ.empty_constraint;
     engagement = None;
     imports = [];
     loads = [];
     local_retroknowledge = [] }
 
-let env_of_safe_env senv = senv.env
-let env_of_senv = env_of_safe_env
-
-let add_constraints cst senv =
-  { senv with
-    env = Environ.add_constraints cst senv.env;
-    univ = Univ.union_constraints cst senv.univ }
-
 let constraints_of_sfb = function
-  | SFBconst cb -> cb.const_constraints
-  | SFBmind mib -> mib.mind_constraints
-  | SFBmodtype mtb -> mtb.typ_constraints
-  | SFBmodule mb -> mb.mod_constraints
+  | 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
 
 (* A generic function for adding a new field in a same environment.
    It also performs the corresponding [add_constraints]. *)
@@ -246,14 +273,20 @@ let safe_push_named (id,_,_ as d) env =
   Environ.push_named d env
 
 let push_named_def (id,de) senv =
-  let (c,typ,cst) = Term_typing.translate_local_def senv.env de in
-  let senv' = add_constraints cst senv in
+  let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
+  (* XXX for now we force *)
+  let c = match c with
+    | Def c -> Lazyconstr.force c
+    | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c)
+    | _ -> assert false in
+  let cst = Future.join cst 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''})
 
 let push_named_assum (id,t) senv =
   let (t,cst) = Term_typing.translate_local_assum senv.env t in
-  let senv' = add_constraints cst senv in
+  let senv' = add_constraints (Now cst) senv in
   let env'' = safe_push_named (id,None,t) senv'.env in
   (cst, {senv' with env=env''})
 
@@ -267,16 +300,17 @@ type global_declaration =
 let add_constant dir l decl senv =
   let kn = make_con senv.modinfo.modpath dir l in
   let cb = match decl with
-    | ConstantEntry ce -> Term_typing.translate_constant senv.env ce
+    | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
     | GlobalRecipe r ->
-      let cb = Term_typing.translate_recipe senv.env r in
+      let cb = Term_typing.translate_recipe senv.env kn r in 
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
   in
   let cb = match cb.const_body with
     | 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 (Lazyconstr.turn_indirect lc) }
+      { cb with const_body =
+           OpaqueDef (Future.chain lc Lazyconstr.turn_indirect) }
     | _ -> cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
@@ -317,7 +351,7 @@ let add_modtype l mte inl senv =
 
 (* full_add_module adds module with universes and constraints *)
 let full_add_module mb senv =
-  let senv = add_constraints mb.mod_constraints senv in
+  let senv = add_constraints (Now mb.mod_constraints) senv in
   { senv with env = Modops.add_module mb senv.env }
 
 (* Insertion of modules *)
@@ -350,6 +384,7 @@ let start_module l senv =
 	 objlabels = Label.Set.empty;
 	 revstruct = [];
          univ = Univ.empty_constraint;
+         future_cst = [];
          engagement = None;
 	 imports = senv.imports;
 	 loads = [];
@@ -435,6 +470,7 @@ let end_module l restype senv =
 		  objlabels = oldsenv.objlabels;
 		  revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
 		  univ = Univ.union_constraints senv'.univ oldsenv.univ;
+                  future_cst = senv'.future_cst @ oldsenv.future_cst;
 		  (* engagement is propagated to the upper level *)
 		  engagement = senv'.engagement;
 		  imports = senv'.imports;
@@ -457,14 +493,14 @@ let end_module l restype senv =
 	   senv.modinfo.modpath inl me in
        mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
    in
-   let senv = add_constraints cst senv in
+   let senv = add_constraints (Now cst) senv in
    let mp_sup = senv.modinfo.modpath in
      (* Include Self support  *)
    let rec compute_sign sign mb resolver senv = 
      match sign with
      | SEBfunctor(mbid,mtb,str) ->
 	 let cst_sub = check_subtypes senv.env mb mtb in
-	 let senv = add_constraints cst_sub senv in
+	 let senv = add_constraints (Now cst_sub) senv in
 	 let mpsup_delta =
 	   inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta
 	 in
@@ -533,6 +569,7 @@ let add_module_parameter mbid mte inl senv =
 		     objlabels = senv.objlabels;
 		     revstruct = [];
 		     univ = senv.univ;
+                     future_cst = senv.future_cst;
 		     engagement = senv.engagement;
 		     imports = senv.imports;
 		     loads = [];
@@ -557,6 +594,7 @@ let start_modtype l senv =
 	objlabels = Label.Set.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
+        future_cst = [];
         engagement = None;
 	imports = senv.imports;
 	loads = [] ;
@@ -609,6 +647,7 @@ let end_modtype l senv =
 	  objlabels = oldsenv.objlabels;
 	  revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
           univ = Univ.union_constraints senv.univ oldsenv.univ;
+          future_cst = senv.future_cst @ oldsenv.future_cst;
           engagement = senv.engagement;
 	  imports = senv.imports;
 	  loads = senv.loads@oldsenv.loads;
@@ -644,6 +683,8 @@ type compiled_library = {
 
 type native_library = Nativecode.global list
 
+let join_compiled_library l = join_module_body l.comp_mod
+
 (* We check that only initial state Require's were performed before
    [start_library] was called *)
 
@@ -674,12 +715,16 @@ let start_library dir senv =
 	objlabels = Label.Set.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
+        future_cst = [];
         engagement = None;
 	imports = senv.imports;
 	loads = [];
         local_retroknowledge = [] }
 
 let export senv dir =
+  let senv = 
+    try join_safe_environment senv
+    with e -> Errors.errorlabstrm "future" (Errors.print e) in
   let modinfo = senv.modinfo in
   begin
     match modinfo.variant with
@@ -763,7 +808,6 @@ let import lib digest senv =
   in
   mp, senv, lib.comp_natsymbs
 
-
 type judgment = unsafe_judgment
 
 let j_val j = j.uj_val
@@ -787,3 +831,6 @@ let register_inline kn senv =
   let new_globals = { env.Pre_env.env_globals with Pre_env.env_constants = new_constants } in
   let env = { env with Pre_env.env_globals = new_globals } in
   { senv with env = env_of_pre_env env }
+
+let add_constraints c = add_constraints (Now c)
+
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 7ca033383..210d601fb 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -26,6 +26,15 @@ type safe_environment
 
 val env_of_safe_env : safe_environment -> Environ.env
 
+val sideff_of_con : safe_environment -> constant -> side_effect 
+
+val is_curmod_library : safe_environment -> bool
+
+
+(* safe_environment has functional data affected by lazy computations,
+ * thus this function returns a new safe_environment *)
+val join_safe_environment : safe_environment -> safe_environment
+
 val empty_environment : safe_environment
 val is_empty : safe_environment -> bool
 
@@ -109,6 +118,8 @@ val export : safe_environment -> DirPath.t
 val import : compiled_library -> Digest.t -> safe_environment
       -> module_path * safe_environment * Nativecode.symbol array
 
+val join_compiled_library : compiled_library -> unit
+
 (** {6 Typing judgments } *)
 
 type judgment
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 33a4b55e8..fd31d782a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,6 +23,10 @@ open Environ
 open Entries
 open Typeops
 
+let debug = false
+let prerr_endline =
+  if debug then prerr_endline else fun _ -> ()
+
 let constrain_type env j cst1 = function
   | None ->
       make_polymorphic_if_constant_for_ind env j, cst1
@@ -33,19 +37,6 @@ let constrain_type env j cst1 = function
       let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
       NonPolymorphicType t, cstrs
 
-let local_constrain_type env j cst1 = function
-  | None ->
-      j.uj_type, cst1
-  | 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);
-      t, union_constraints (union_constraints cst1 cst2) cst3
-
-let translate_local_def env de =
-  let (j,cst) = infer env de.const_entry_body in
-  let (typ,cst) = local_constrain_type env j cst de.const_entry_type in
-    (j.uj_val,typ,cst)
 
 let translate_local_assum env t =
   let (j,cst) = infer env t in
@@ -55,23 +46,89 @@ let translate_local_assum env t =
 
 (* Insertion of constants and parameters in environment. *)
 
-let infer_declaration env = function
+let handle_side_effects env body side_eff =
+  let handle_sideff t (NewConstant (c,cb)) =
+    let cname = 
+      let name = string_of_con c in
+      for i = 0 to String.length name - 1 do
+        if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done;
+      Name (id_of_string name) in
+    let rec sub i x = match kind_of_term x with
+      | Const c' when eq_constant c c' -> mkRel i
+      | _ -> map_constr_with_binders ((+) 1) sub i x in
+    match cb.const_body with
+    | Undef _ -> assert false
+    | Def b ->
+        let b = Lazyconstr.force b in
+        let b_ty = Typeops.type_of_constant_type env cb.const_type in
+        let t = sub 1 (Vars.lift 1 t) in
+        mkLetIn (cname, b, b_ty, t)
+    | OpaqueDef b -> 
+        let b = Lazyconstr.force_opaque (Future.force b) in
+        let b_ty = Typeops.type_of_constant_type env cb.const_type in
+        let t = sub 1 (Vars.lift 1 t) in
+        mkApp (mkLambda (cname, b_ty, t), [|b|])
+  in
+  (* CAVEAT: we assure a proper order *)
+  Declareops.fold_side_effects handle_sideff body
+    (Declareops.uniquize_side_effects side_eff)
+
+(* what is used for debugging only *)
+let infer_declaration ?(what="UNKNOWN") env dcl =
+  match dcl with
   | DefinitionEntry c ->
-      let (j,cst) = infer env c.const_entry_body in
-      let j =
-        {uj_val = hcons_constr j.uj_val;
-         uj_type = hcons_constr j.uj_type} in
-      let (typ,cst) = constrain_type env j cst c.const_entry_type in
-      let def =
-	if c.const_entry_opaque
-	then OpaqueDef (Lazyconstr.opaque_from_val j.uj_val)
-	else Def (Lazyconstr.from_val j.uj_val)
-      in
-      def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
+      let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
+      if c.const_entry_opaque && c.const_entry_type <> None then
+        let _ = prerr_endline ("deferring typing of "^what) in
+        let body_cst = Future.chain ~id:("infer_declaration " ^ what)
+            entry_body (fun entry_body ->
+          let _ = prerr_endline ("forcing deferred typing of "^what) in
+          let body, side_eff = entry_body in
+          let _ = prerr_endline ("... got proof of "^what) in
+          let body = if side_eff = Declareops.no_seff then body else
+            let _ = prerr_endline ("    Handling the following side eff:") in
+            Declareops.iter_side_effects (fun e -> 
+              prerr_endline("     " ^ Declareops.string_of_side_effect e)) 
+              side_eff;
+            handle_side_effects env body side_eff in
+          let (j,cst) = infer env body in
+          let _ = prerr_endline ("... typed proof of "^what) in
+          let j =
+            {uj_val = hcons_constr j.uj_val;
+             uj_type = hcons_constr j.uj_type} in
+          let (_typ,cst) = constrain_type env j cst c.const_entry_type in
+          Lazyconstr.opaque_from_val j.uj_val, cst) in
+        let body, cst = Future.split2 body_cst in
+        let def = OpaqueDef body in
+        let typ = match c.const_entry_type with
+        | None -> assert false
+        | Some typ -> NonPolymorphicType typ in
+        (def, typ, cst, c.const_entry_inline_code, ctx)
+      else
+        let _ = prerr_endline ("typing now "^what) in
+        let body, side_eff = Future.force entry_body in
+        let body = if side_eff = Declareops.no_seff then body else
+          let _ = prerr_endline ("    Handling the following side eff:") in
+          Declareops.iter_side_effects (fun e -> 
+            prerr_endline("     " ^ Declareops.string_of_side_effect e))
+            side_eff;
+          handle_side_effects env body side_eff in
+        let (j,cst) =
+          try infer env body 
+          with Not_found as e -> 
+            prerr_endline ("infer not found " ^ what);
+            raise e in
+        let j =
+          {uj_val = hcons_constr j.uj_val;
+           uj_type = hcons_constr j.uj_type} in
+        let (typ,cst) = constrain_type env j cst c.const_entry_type in
+        let _ = prerr_endline ("...typed "^what) in
+        let def = Def (Lazyconstr.from_val j.uj_val) in
+        (def, typ, Future.from_val cst, c.const_entry_inline_code, ctx)
   | 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, cst, false, ctx
+      Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx
 
 let global_vars_set_constant_type env = function
   | NonPolymorphicType t -> global_vars_set env t
@@ -81,48 +138,78 @@ 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 check_declared_variables declared inferred =
-  let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
-  let undeclared_set = Id.Set.diff (mk_set inferred) (mk_set declared) in
-  if not (Id.Set.is_empty undeclared_set) then
-    error ("The following section variables are used but not declared:\n"^
-              (String.concat ", "
-                 (List.map Id.to_string (Id.Set.elements undeclared_set))))
-
-let build_constant_declaration env (def,typ,cst,inline_code,ctx) =
-  let hyps =
-    let inferred =
-      let ids_typ = global_vars_set_constant_type env typ in
-      let ids_def = match def with
-        | Undef _ -> Id.Set.empty
-        | Def cs -> global_vars_set env (Lazyconstr.force cs)
-        | OpaqueDef lc -> global_vars_set env (Lazyconstr.force_opaque lc)
-      in
-      keep_hyps env (Id.Set.union ids_typ ids_def)
-    in
+let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
+  let check declared inferred =
+    let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
+    let inferred_set, declared_set = mk_set inferred, mk_set declared in
+    if not (Id.Set.subset inferred_set declared_set) then
+      error ("The following section variable are used but not declared:\n"^
+        (String.concat ", " (List.map Id.to_string
+          (Id.Set.elements (Idset.diff inferred_set declared_set))))) in
+  (* We try to postpone the computation of used section variables *)
+  let hyps, def = 
     match ctx with
-      | None -> inferred
-      | Some declared ->
-        check_declared_variables declared inferred;
-        declared
-  in
-  let tps = Cemitcodes.from_val (compile_constant_body env def) in
+    | None when named_context env <> [] -> 
+        (* No declared section vars, and non-empty section context:
+           we must look at the body NOW, if any *)
+        let ids_typ = global_vars_set_constant_type env typ in
+        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);
+            global_vars_set env (Lazyconstr.force_opaque (Future.force lc)) in
+        keep_hyps env (Idset.union ids_typ ids_def), def
+    | None -> [], def (* Empty section context: no need to check *)
+    | Some declared ->
+        (* We use the declared set and chain a check of correctness *)
+        declared,
+        match def with
+        | Undef _ as x -> x (* nothing to check *)
+        | Def cs as x ->
+            let ids_typ = global_vars_set_constant_type env typ in
+            let ids_def = global_vars_set env (Lazyconstr.force cs) in
+            let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+            check declared inferred;
+            x
+        | OpaqueDef lc -> (* In this case we can postpone the check *)
+            OpaqueDef (Future.chain ~id:(string_of_con kn) lc (fun lc ->
+              let ids_typ = global_vars_set_constant_type env typ in
+              let ids_def =
+                global_vars_set env (Lazyconstr.force_opaque lc) in
+              let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+              check declared inferred; lc)) in
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
-    const_body_code = tps;
+    const_body_code = Cemitcodes.from_val (compile_constant_body env def);
     const_constraints = cst;
     const_native_name = ref NotLinked;
     const_inline_code = inline_code }
 
 (*s Global and local constant declaration. *)
 
-let translate_constant env ce =
-  build_constant_declaration env (infer_declaration env ce)
+let translate_constant env kn ce =
+  build_constant_declaration kn env 
+    (infer_declaration ~what:(string_of_con kn) env ce)
+
+let translate_recipe env kn r =
+  let def,typ,cst,inline_code,hyps = Cooking.cook_constant env r in
+  build_constant_declaration kn env (def,typ,cst,inline_code,hyps)
 
-let translate_recipe env r =
-  build_constant_declaration env (Cooking.cook_constant env 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
+  let typ = type_of_constant_type env typ in
+  def, typ, cst
 
 (* Insertion of inductive types. *)
 
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
+
+let handle_side_effects env ce = { ce with
+  const_entry_body = Future.chain ~id:"handle_side_effects" 
+    ce.const_entry_body (fun (body, side_eff) ->
+    handle_side_effects env body side_eff, Declareops.no_seff);
+}
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index c9bff84fc..59706bb83 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -13,20 +13,25 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : env -> definition_entry ->
-  constr * types * constraints
+val translate_local_def : env -> Id.t -> definition_entry ->
+  constant_def * types * constant_constraints
 
 val translate_local_assum : env -> types -> types * constraints
 
-val translate_constant : env -> constant_entry -> constant_body
+(* returns the same definition_entry but with side effects turned into
+ * let-ins or beta redexes. it is meant to get a term out of a not yet
+ * type checked proof *)
+val handle_side_effects : env -> definition_entry -> definition_entry
+
+val translate_constant : env -> constant -> constant_entry -> constant_body
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
 
-val translate_recipe : env -> Cooking.recipe -> constant_body
-
+val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : env -> constant_entry -> Cooking.result
-val build_constant_declaration : env -> Cooking.result -> constant_body
+val infer_declaration : ?what:string -> env -> constant_entry -> Cooking.result
+val build_constant_declaration :
+  constant -> env -> Cooking.result -> constant_body