Future: ported to Ephemeron + exception enhancing

A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.

A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost.  This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).

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

1 files changed, 27 insertions, 21 deletions

diff --git a/lib/future.mli b/lib/future.mli
index a1535b13d..4ba601976 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -6,48 +6,51 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Futures: for now lazy computations with some purity enforcing *)
-(* TODO: it may be worth separating in the type pure and inpure computations *)
+(* Futures: asynchronous computations with some purity enforcing *)
 
 exception NotReady
 
 type 'a computation
 type 'a value = [ `Val of 'a | `Exn of exn ]
+type fix_exn = exn -> exn
 
-(* Build a computation *)
-val create : (unit -> 'a) -> 'a computation
-val from_val : 'a -> 'a computation
+(* Build a computation.  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. *)
+val create : fix_exn -> (unit -> 'a) -> 'a computation
+
+(* Usually from_val is used to create "fake" futures, to use the same API
+   as if a real asynchronous computations was there.  In this case fixing
+   the exception is not needed, but *if* the future is chained, the fix_exn
+   argument should really be given *)
+val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
+
+(* Like from_val, but also takes a snapshot of the global state.  Morally
+   the value is not just the 'a but also the global system state *)
+val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
 
 (* Run remotely, returns the function to assign *)
 type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
-val create_delegate : unit -> 'a computation * ('a assignement -> unit)
+val create_delegate : fix_exn -> 'a computation * ('a assignement -> unit)
 
 (* Given a computation that is_exn, replace it by another one *)
 val replace : 'a computation -> 'a computation -> unit
 
-(* Variants to stock a copy of the current environment *)
-val create_here : (unit -> 'a) -> 'a computation
-val from_here : 'a -> 'a computation
-
 (* Inspect a computation *)
 val is_over : 'a computation -> bool
 val is_val : 'a computation -> bool
 val is_exn : 'a computation -> bool
 val peek_val : 'a computation -> 'a option
 
-(* Chain computations.
-   Note that in [chain c f], f will execute in an environment modified by c
-   unless ~pure:true *)
-val chain :
-  ?id:string -> ?pure:bool -> 'a computation -> ('a -> 'b) -> 'b computation
+(* Chain computations.  *)
+val chain : 'a computation -> ('a -> 'b) -> 'b computation
 
 (* Forcing a computation *)
 val force : 'a computation -> 'a
 val compute : 'a computation -> 'a value
 
-val drop : 'a computation -> 'a computation
-
-(* Final call, no more impure chain allowed since the state is lost *)
+(* Final call, no more chain allowed since the state is lost *)
 val join : 'a computation -> 'a
 
 (* Utility *)
@@ -58,11 +61,14 @@ val map2 :
   ('a computation -> 'b -> 'c) ->
      'a list computation -> 'b list -> 'c list
 
-(* These functions are needed to get rid of side effects *)
-val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
-
 (* Once set_freeze is called we can purify a computation *)
 val purify : ('a -> 'b) -> 'a -> 'b
 (* And also let a function alter the state but backtrack if it raises exn *)
 val transactify : ('a -> 'b) -> 'a -> 'b
 
+(* These functions are needed to get rid of side effects.
+   Thy are set for the outermos layer of the system, since they have to
+   deal with the whole system state. *)
+val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+
+