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

2 files changed, 72 insertions, 21 deletions

diff --git a/lib/future.ml b/lib/future.ml
index b93d33640a..e9a2be989d 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 4ba6019762..f1a68f3b38 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