Module Why3findUtils.FibersSource

The time of computations that produces an 'a.

return v computation that immediately returns v.

Monadic bind a f operator binds result v of a to a new computation f v. See Monad.let* operator.

Monadic apply a f operator binds result v of a to computation return (f v). See Monad.let+ operator.

Same as apply with reversed arguments.

Combines two computations into a parallel computation of both.

See Monad.and*, and Monad.@* operators.

Monadic and Applicative operators.

Iterable Queues.

any ks synchronizes on the first computation in ks that terminates.

seq ks waits all continuations in sequence and returns their result.

all ks waits all continuations in parallel and returns their result one they _all_ have terminated.

find f ks runs all continuations in parallel and returns the _first_ result that satisfies the filter f, if any.

Inter tasks communication.

Creates a new channel for signaling.

Register a hook on the signal.

Un-register a hook on the signal.

Register a hook that automatically disconnect itself on first emit.

At most one hook is connected to the signal.

Remove all hooks on the signal.

Remove all registered hooks.

Broadcast a value on all registered hooks.

Creates a delated fiber.

peek x returns the value assigned to variable x, if any.

set x v stores value v into fiber x and signals all computations that are waiting on x.

Successive calls to set x _ will be ignored.

find x returns the value assigned to variable x or raise Not_found.

• raises Not_found

defined x returns true is the variable x has been assigned.

A limited set of resources to be shared on different tasks.

mutex n creates a pool of n resources.

sync m f x synchronize task f x as soon as there is one available resource in mutex m. The resource is released when the computation terminates.

async f register a new asynchronous task. Each time the global queue is yield, f () is invoked until it returns Some v which terminates the continuation with value v.

Ping all pending asynchronous tasks for termination. Enabled continuations are executed and dequeued.

Number of asynchronous tasks still waiting.

Waits for all pending tasks to terminate. The default ~polling interval is 10 milliseconds.

sleep ms asynchronously waits for (at least) ms milliseconds.

finally ~callback f starts computation f, eventually passing its result to callback, while immediately returning f for chaining.

Default ~callback is ignore.

background f k starts computation f and immediately returns. Result of computation will be eventually passed to continuation k.

Default ~callback is ignore. This is the same as ignore @@ finally ?callback f.

monitor ~signal ~handler f starts computation f and returns f immediately for chaining. When both are provided, the handler is connected to signal until computation f is terminated.

await f waits until the end of computation f, yielding periodically until termination.

Default ~polling interval is 10 milliseconds.