Future: better doc + restore ~pure optimization

This optimization was undone because the kernel type checking was
not a pure functions (it was accessing the conv_oracle state imperatively).
Now that the conv_oracle state is part of env, the optimization can be
restored.  This was the cause of the increase in memory consumption, since
it was forcing to keep a copy of the system state for every proof, even the
ones that are not delayed/delegated to slaves.

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

4 files changed, 11 insertions, 10 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index dbe83a8565..0a1d713c4d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -126,7 +126,7 @@ let on_body f = function
   | Undef _ as x -> x
   | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
   | OpaqueDef lc ->
-    OpaqueDef (Future.chain lc (fun lc ->
+    OpaqueDef (Future.chain ~pure:true lc (fun lc ->
         (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))))
 
 let constr_of_def = function
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3083c17389..8eae2aed8e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -52,7 +52,8 @@ let subst_const_type sub arity = match arity with
 let subst_const_def sub def = match def with
   | Undef _ -> def
   | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc -> OpaqueDef (Future.chain lc (subst_lazy_constr sub))
+  | OpaqueDef lc ->
+      OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
 
 (* TODO : the native compiler seems to rely on a fresh (ref NotLinked)
    being created at each substitution. Quite ugly... For the moment,
@@ -99,7 +100,7 @@ let hcons_const_def = function
     Def (from_val (Term.hcons_constr constr))
   | OpaqueDef lc ->
     OpaqueDef
-      (Future.chain lc
+      (Future.chain ~pure:true lc
          (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc))))
 
 let hcons_const_body cb =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3132d45e37..35da705efb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -379,7 +379,7 @@ let add_constant dir l decl senv =
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
       { cb with const_body =
-           OpaqueDef (Future.chain lc Lazyconstr.turn_indirect) }
+           OpaqueDef (Future.chain ~pure:true lc Lazyconstr.turn_indirect) }
     | _ -> cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 987621619a..b2b6df3929 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,7 +68,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.force b) in
+          let b = Lazyconstr.force_opaque (Future.join 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
@@ -85,7 +85,7 @@ let infer_declaration ?(what="UNKNOWN") env dcl =
       let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
       if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then
         let body_cst =
-          Future.chain entry_body (fun (body, side_eff) ->
+          Future.chain ~pure:true entry_body (fun (body, side_eff) ->
             let body = handle_side_effects env body side_eff in
             let j, cst = infer env body in
             let j =
@@ -100,7 +100,7 @@ let infer_declaration ?(what="UNKNOWN") env dcl =
         | Some typ -> NonPolymorphicType typ in
         def, typ, cst, c.const_entry_inline_code, ctx
       else
-        let body, side_eff = Future.force entry_body in
+        let body, side_eff = Future.join entry_body in
         let body = handle_side_effects env body side_eff in
         let j, cst =
           try infer env body 
@@ -147,7 +147,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
         | 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
+            global_vars_set env (Lazyconstr.force_opaque (Future.join lc)) in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None -> [], def (* Empty section context: no need to check *)
     | Some declared ->
@@ -162,7 +162,7 @@ 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 lc (fun lc ->
+            OpaqueDef (Future.chain ~pure:true 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
@@ -197,7 +197,7 @@ let translate_local_def env id centry =
 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
+  const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun (body, side_eff) ->
        handle_side_effects env body side_eff, Declareops.no_seff);
 }