Future: allow custom action when a delegated future is forced

The default action is to raise NotReady, but one may want to
make the action "blocking" but successful.  Using this device
all delayed proofs can be "delegated".  If there are slaves, they
will eventually pick up the task.  If there are no slaves, then
the future can behave like a regular, non delegated, lazy computation.

2 files changed, 29 insertions, 23 deletions

diff --git a/lib/future.ml b/lib/future.ml
index 8c40f0edb7..391f5a65c7 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -29,21 +29,23 @@ let _ = Errors.register_handler (function
 type fix_exn = exn -> exn
 let id x = prerr_endline "no fix_exn"; x
 
+type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
+
 (* Val is not necessarily a final state, so the
    computation restarts from the state stocked into Val *)
-type 'a comp =
-  | Delegated
+and 'a comp =
+  | Delegated of (unit -> 'a assignement)
       (* 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 =
+and 'a comput =
   | Ongoing of (fix_exn * 'a comp ref) Ephemeron.key
   | Finished of 'a
 
-type 'a computation = 'a comput ref
+and 'a computation = 'a comput ref
 
 let create f x = ref (Ongoing (Ephemeron.create (f, Pervasives.ref x)))
 let get x =
@@ -57,41 +59,42 @@ type 'a value = [ `Val of 'a | `Exn of exn ]
 
 let is_over kx = let _, x = get kx in match !x with
   | Val _ | Exn _ -> true
-  | Closure _ | Delegated -> false
+  | Closure _ | Delegated _ -> false
 
 let is_val kx = let _, x = get kx in match !x with
   | Val _ -> true
-  | Exn _ | Closure _ | Delegated -> false
+  | Exn _ | Closure _ | Delegated _ -> false
 
 let is_exn kx = let _, x = get kx in match !x with
   | Exn _ -> true
-  | Val _ | Closure _ | Delegated -> false
+  | Val _ | Closure _ | Delegated _ -> false
 
 let peek_val kx = let _, x = get kx in match !x with
   | Val (v, _) -> Some v
-  | Exn _ | Closure _ | Delegated -> None
+  | Exn _ | Closure _ | Delegated _ -> None
 
 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 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
+let default_force () = raise NotReady
+let assignement ck = fun v ->
+  let fix_exn, c = get ck in
+  assert (match !c with Delegated _ -> true | _ -> false);
+  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
+let create_delegate ?(force=default_force) fix_exn =
+  let ck = create fix_exn (Delegated force) in
+  ck, assignement ck
 
 (* TODO: get rid of try/catch to be stackless *)
-let compute ~pure ck : 'a value =
+let rec 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
+  | Delegated f -> assignement ck (f ()); compute ~pure ck
   | Closure f ->
       try
         let data = f () in
@@ -111,7 +114,7 @@ let force ~pure x = match compute ~pure x with
 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))
+  | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck))
   | Exn _ as x -> x
   | Val (v, None) when pure -> Closure (fun () -> f v)
   | Val (v, Some _) when pure -> Closure (fun () -> f v)
diff --git a/lib/future.mli b/lib/future.mli
index 1a1648ff1f..4f27767ba4 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -74,9 +74,12 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
    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 *)
+(* Run remotely, returns the function to assign.  Optionally tekes a function
+   that is called when forced.  The default one is to raise NotReady *)
 type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
-val create_delegate : fix_exn -> 'a computation * ('a assignement -> unit)
+val create_delegate :
+  ?force:(unit -> 'a assignement) ->
+  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