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

2 files changed, 86 insertions, 70 deletions

diff --git a/lib/future.ml b/lib/future.ml
index c1fb176df..b93d33640 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* to avoid side effects *)
+(* To deal with side effects we have to save/restore the system state *)
 let freeze = ref (fun () -> assert false : unit -> Dyn.t)
 let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
 let set_freeze f g = freeze := f; unfreeze := g
@@ -26,59 +26,73 @@ let _ = Errors.register_handler (function
                 "asynchronous script processing.")
   | _ -> raise Errors.Unhandled)
 
+type fix_exn = exn -> exn
+let id x = prerr_endline "no fix_exn"; x
+
 (* Val is not necessarily a final state, so the
    computation restarts from the state stocked into Val *)
 type 'a comp =
   | Delegated
-  | Dropped
+      (* TODO in some cases one would like to block, sock here
+         a mutex and a condition to make this possible *)
   | Closure of (unit -> 'a)
   | Val of 'a * Dyn.t option
   | Exn of exn
+      (* Invariant: this exception is always "fixed" as in fix_exn *)
+
+type 'a comput =
+  | Ongoing of (fix_exn * 'a comp ref) Ephemeron.key
+  | Finished of 'a
 
-type 'a computation = 'a comp ref
+type 'a computation = 'a comput ref
+
+let create f x = ref (Ongoing (Ephemeron.create (f, Pervasives.ref x)))
+let get x =
+  match !x with
+  | Finished v -> (fun x -> x), ref( Val (v,None))
+  | Ongoing x ->
+      try Ephemeron.get x
+      with Ephemeron.InvalidKey -> (fun x -> x), ref (Exn NotHere)
 
 type 'a value = [ `Val of 'a | `Exn of exn ]
 
-let is_over x = match !x with
+let is_over kx = let _, x = get kx in match !x with
   | Val _ | Exn _ -> true
-  | Closure _ | Delegated | Dropped -> false
+  | Closure _ | Delegated -> false
 
-let is_val x = match !x with
+let is_val kx = let _, x = get kx in match !x with
   | Val _ -> true
-  | Exn _ | Closure _ | Delegated | Dropped -> false
+  | Exn _ | Closure _ | Delegated -> false
 
-let is_exn x = match !x with
+let is_exn kx = let _, x = get kx in match !x with
   | Exn _ -> true
-  | Val _ | Closure _ | Delegated | Dropped -> false
+  | Val _ | Closure _ | Delegated -> false
 
-let peek_val x = match !x with
+let peek_val kx = let _, x = get kx in match !x with
   | Val (v, _) -> Some v
-  | Exn _ | Closure _ | Delegated | Dropped -> None
-
-let from_val v = ref (Val (v, None))
-let from_here v = ref (Val (v, Some (!freeze ())))
-let proj = function
-  | `Val (x, _ ) -> `Val x
-  | `Exn e -> `Exn e
+  | Exn _ | Closure _ | Delegated -> None
 
-let create f = ref (Closure f)
+let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
+let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
 
 type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
-let create_delegate () =
-  let c = ref Delegated in
-  c, (fun v ->
-      assert (!c == Delegated);
-      match v with
-      | `Val v -> c := Val (v, None)
-      | `Exn e -> c := Exn e
-      | `Comp f -> c := !f)
-
-(* TODO: get rid of try/catch *)
-let compute ~pure c : 'a value = match !c with
+let create_delegate fix_exn =
+  let ck = create fix_exn Delegated in
+  ck, fun v ->
+        let fix_exn, c = get ck in
+        assert (!c == Delegated);
+        match v with
+        | `Val v -> c := Val (v, None)
+        | `Exn e -> c := Exn (fix_exn e)
+        | `Comp f -> let _, comp = get f in c := !comp
+
+(* TODO: get rid of try/catch to be stackless *)
+let compute ~pure ck : 'a value =
+  let fix_exn, c = get ck in
+  match !c with
   | Val (x, _) -> `Val x
   | Exn e -> `Exn e
   | Delegated -> `Exn NotReady
-  | Dropped -> `Exn NotHere
   | Closure f ->
       try
         let data = f () in
@@ -86,6 +100,7 @@ let compute ~pure c : 'a value = match !c with
         c := Val (data, state); `Val data
       with e ->
         let e = Errors.push e in
+        let e = fix_exn e in
         match e with
         | NotReady -> `Exn e
         | _ -> c := Exn e; `Exn e
@@ -94,20 +109,19 @@ let force ~pure x = match compute ~pure x with
   | `Val v -> v
   | `Exn e -> raise e
 
-let drop c = match !c with Closure _ | Val (_,Some _) -> ref Dropped | _ -> c
-
-let chain ?(id="none") ?(pure=false) c f = ref (match !c with
-  | Closure _ | Delegated | Dropped -> Closure (fun () -> f (force ~pure c))
+let chain ?(pure=false) 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, Some _) when pure -> Closure (fun () -> f v)
-  | Val (v, Some state) ->
-(*        prerr_endline ("Future: restarting (check if optimizable): " ^ id); *)
-       Closure (fun () -> !unfreeze state; f v))
+  | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v))
 
-let create_here f = chain ~pure:false (from_here ()) f
+let create fix_exn f = create fix_exn (Closure f)
 
-let replace x y =
+let replace kx y =
+  let _, x = get kx in
   match !x with
   | Exn _ -> x := Closure (fun () -> force ~pure:false y)
   | _ -> Errors.anomaly (Pp.str "Only Exn futures can be replaced")
@@ -125,19 +139,13 @@ let transactify f x =
   try f x
   with e -> let e = Errors.push e in !unfreeze state; raise e
 
-let purify_future f x =
-  match !x with
-  | Val _ | Exn _ | Delegated | Dropped -> f x
-  | Closure _ -> purify f x
-
+let purify_future f x = if is_over x then f x else purify f x
 let compute x = purify_future (compute ~pure:false) x
 let force x = purify_future (force ~pure:false) x
 
-let join x =
-  let v = force x in
-  (x := match !x with
-       | Val (x,_) -> Val (x, None)
-       | Exn _ | Delegated | Dropped | Closure _ -> assert false);
+let join kx =
+  let v = force kx in
+  kx := Finished v;
   v
 
 let split2 x =
@@ -156,3 +164,5 @@ let map2 f x l =
         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 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
+
+