diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-12-20 12:23:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-04 17:07:15 +0100 |
| commit | a5ebab4f0cd762904055a69b20e6217d08f46637 (patch) | |
| tree | 1aac871466202fb00a7fefd36b16b78ecf76d7a9 /lib/future.mli | |
| parent | 0582c9363fa981798811ff11ef0e8c76c38255f7 (diff) | |
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.
Diffstat (limited to 'lib/future.mli')
| -rw-r--r-- | lib/future.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/future.mli b/lib/future.mli index 1a1648ff1..4f27767ba 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 |