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

9 files changed, 93 insertions, 38 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index dbe83a856..0a1d713c4 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 3083c1738..8eae2aed8 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 3132d45e3..35da705ef 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 987621619..b2b6df392 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);
 }
diff --git a/lib/future.ml b/lib/future.ml
index b93d33640..e9a2be989 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -109,14 +109,23 @@ let force ~pure x = match compute ~pure x with
   | `Val v -> v
   | `Exn e -> raise e
 
-let chain ?(pure=false) ck f =
+let chain ~pure ck f =
   let fix_exn, c = get ck in
   create fix_exn (match !c with
   | Closure _ | Delegated -> Closure (fun () -> f (force ~pure ck))
   | Exn _ as x -> x
-  | Val (v, None) -> Closure (fun () -> f v)
+  | Val (v, None) when pure -> Closure (fun () -> f v)
   | Val (v, Some _) when pure -> Closure (fun () -> f v)
-  | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v))
+  | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
+  | Val (v, None) ->
+      match !ck with
+      | Finished _ -> Errors.anomaly(Pp.str
+          "Future.chain ~pure:false call on an already joined computation")
+      | Ongoing _ -> Errors.anomaly(Pp.strbrk(
+          "Future.chain ~pure:false call on a pure computation. "^
+          "This can happen if the computation was initial created with "^
+          "Future.from_val or if it was Future.chain ~pure:true with a "^
+          "function and later forced.")))
 
 let create fix_exn f = create fix_exn (Closure f)
 
@@ -149,20 +158,13 @@ let join kx =
   v
 
 let split2 x =
-  chain ~pure:false x (fun x -> fst x),
-  chain ~pure:false x (fun x -> snd x)
-
-let split3 x =
-  chain ~pure:false x (fun x -> Util.pi1 x),
-  chain ~pure:false x (fun x -> Util.pi2 x),
-  chain ~pure:false x (fun x -> Util.pi3 x)
+  chain ~pure:true x (fun x -> fst x),
+  chain ~pure:true x (fun x -> snd x)
 
 let map2 f x l =
   CList.map_i (fun i y ->
-    let xi = chain ~pure:false x (fun x ->
+    let xi = chain ~pure:true x (fun x ->
         try List.nth x i
         with Failure _ | Invalid_argument _ ->
           Errors.anomaly (Pp.str "Future.map2 length mismatch")) in
     f xi y) 0 l
-
-let chain f g = chain f g
diff --git a/lib/future.mli b/lib/future.mli
index 4ba601976..f1a68f3b3 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -6,7 +6,49 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Futures: asynchronous computations with some purity enforcing *)
+(* Futures: asynchronous computations with some purity enforcing
+ *
+ * A Future.computation is like a lazy_t but with some extra bells and whistles
+ * to deal with imperative code and eventual delegation to a slave process.
+ *
+ * Example of a simple scenario taken into account:
+ *
+ *   let f = Future.from_here (number_of_constants (Global.env())) in
+ *   let g = Future.chain ~pure:false f (fun n ->
+ *             n = number_of_constants (Global.env())) in
+ *   ...
+ *   Lemmas.save_named ...;
+ *   ...
+ *   let b = Future.force g in
+ *
+ * The Future.computation f holds a (immediate, no lazy here) value.
+ * We then chain to obtain g that (will) hold false if (when it will be
+ * run) the global environment has a different number of constants, true
+ * if nothing changed.
+ * Before forcing g, we add to the global environment one more constant.
+ * When finally we force g.  Its value is going to be *true*.
+ * This because Future.from_here stores in the computation not only the initial
+ * value but the entire system state.  When g is forced the state is restored,
+ * hence Global.env() returns the environment that was actual when f was
+ * created.
+ * Last, forcing g is run protecting the system state, hence when g finishes,
+ * the actual system state is restored.
+ *
+ * If you compare this with lazy_t, you see that the value returned is *false*,
+ * that is counter intuitive and error prone.
+ *
+ * Still not all computations are impure and acess/alter the system state.
+ * This class can be optimized by using ~pure:true, but there is no way to
+ * statically check if this flag is misused, hence use it with care.
+ *
+ * Other differences with lazy_t is that a future computation that produces
+ * and exception can be substituted for another computation of the same type.
+ * Moreover a future computation can be delegated to another execution entity
+ * that will be allowed to set the result.  Finally future computations can
+ * always be marshalled: if they were joined before marshalling, they will
+ * hold the computed value (assuming it is itself marshallable), otherwise
+ * they will become invalid and accessing them raises a private exception.
+ *)
 
 exception NotReady
 
@@ -14,7 +56,9 @@ type 'a computation
 type 'a value = [ `Val of 'a | `Exn of exn ]
 type fix_exn = exn -> exn
 
-(* Build a computation.  fix_exn is used to enrich any exception raised
+(* Build a computation, no snapshot of the global state is taken.  If you need
+   to grab a copy of the state start with from_here () and then chain.
+   fix_exn is used to enrich any exception raised
    by forcing the computations or any computation that is chained after
    it. It is used by STM to attach errors to their corresponding states,
    and to communicate to the code catching the exception a valid state id. *)
@@ -43,20 +87,25 @@ val is_val : 'a computation -> bool
 val is_exn : 'a computation -> bool
 val peek_val : 'a computation -> 'a option
 
-(* Chain computations.  *)
-val chain : 'a computation -> ('a -> 'b) -> 'b computation
+(* Chain computations.  When pure:true, the computation will not keep a copy
+ * of the global state.
+ * [let c' = chain ~pure:true c f in let c'' = chain ~pure:false c' g in]
+ * is invalid.  It works if one forces [c''] since the whole computation will
+ * be executed in one go.  It will not work, and raise an anomaly, if one
+ * forces c' and then c''.
+ * [join c; chain ~pure:false c g] is invalid and fails at runtime.
+ * [force c; chain ~pure:false c g] is correct. *)
+val chain : pure:bool -> 'a computation -> ('a -> 'b) -> 'b computation
 
 (* Forcing a computation *)
 val force : 'a computation -> 'a
 val compute : 'a computation -> 'a value
 
-(* Final call, no more chain allowed since the state is lost *)
+(* Final call, no more *inpure* chain allowed since the state is lost *)
 val join : 'a computation -> 'a
 
-(* Utility *)
+(*** Utility functions ************************************************* ***)
 val split2 : ('a * 'b) computation -> 'a computation * 'b computation
-val split3 :
-  ('a * 'b * 'c) computation -> 'a computation * 'b computation * 'c computation
 val map2 :
   ('a computation -> 'b -> 'c) ->
      'a list computation -> 'b list -> 'c list
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7382f438b..807d83384 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -278,7 +278,7 @@ let close_proof ~now fpl =
     const_entry_inline_code = false;
     const_entry_opaque = true }) fpl initial_goals in
   if now then
-    List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries;
+    List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries;
   (pid, (entries, compute_guard, strength, hook))
 
 let return_proof () =
@@ -302,7 +302,7 @@ let return_proof () =
 
 let close_future_proof proof = close_proof ~now:false proof
 let close_proof fix_exn =
-  close_proof ~now:true (Future.from_here ~fix_exn (return_proof ()))
+  close_proof ~now:true (Future.from_val ~fix_exn (return_proof ()))
 
 (**********************************************************)
 (*                                                        *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 04a2661d7..e63ff1991 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -68,9 +68,11 @@ let red_constant_entry n ce = function
   | None -> ce
   | Some red ->
       let proof_out = ce.const_entry_body in
-      { ce with const_entry_body = Future.chain proof_out (fun (body,eff) ->
-          under_binders (Global.env()) 
-            (fst (reduction_of_red_expr (Global.env()) red)) n body,eff) }
+      let env = Global.env () in
+      { ce with const_entry_body = Future.chain ~pure:true proof_out
+        (fun (body,eff) ->
+           under_binders env
+             (fst (reduction_of_red_expr env red)) n body,eff) }
 
 let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 519112dfd..d6b868b00 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -48,8 +48,9 @@ let adjust_guardness_conditions const = function
   | [] -> const (* Not a recursive statement *)
   | possible_indexes ->
   (* Try all combinations... not optimal *)
+     let env = Global.env() in
      { const with const_entry_body =
-        Future.chain const.const_entry_body
+        Future.chain ~pure:true const.const_entry_body
         (fun (body, eff) ->
           match kind_of_term body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
@@ -59,7 +60,7 @@ let adjust_guardness_conditions const = function
 	  lemma_guard (Array.to_list fixdefs) in
 *)
               let indexes =
-	        search_guard Loc.ghost (Global.env())
+	        search_guard Loc.ghost env
                   possible_indexes fixdecls in
               mkFix ((indexes,0),fixdecls),  eff
           | _ -> body, eff) }