Module Why3findUtils.Fibers Source Lightweight and Monadic Fibers Library.
Freely inspired from the Fiber dune package.
Basic ConstructorsThe time of computations that produces an 'a.
return v computation that immediately returns v.
Source val bind : 'a t -> ('a -> 'b t ) -> 'b t Monadic bind a f operator binds result v of a to a new computation f v. See Monad.let* operator.
Source val apply : 'a t -> ('a -> 'b ) -> 'b t Monadic apply a f operator binds result v of a to computation return (f v). See Monad.let+ operator.
Source val map : ('a -> 'b ) -> 'a t -> 'b t 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.
List Combinatorsany 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.
Source val first : ('a -> 'b option ) -> 'a t list -> 'b option t find f ks runs all continuations in parallel and returns the _first_ result that satisfies the filter f, if any.
SignalsInter 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.
VariablesVariables are simply fibers to be assigned later on.
Source val var : ?init :'a -> unit -> 'a t 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.
defined x returns true is the variable x has been assigned.
Mutual ExclusionA 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.
Asynchronous TasksThe Fibers library maintains a global pool of asynchronous tasks. Cooperative threads must repeatedly invoke yield to ping pending tasks. Eventually, the list of pending tasks can be wait to terminate by polling with flush .
Source val async : (unit -> 'a option ) -> 'a t 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.
Source val yield : unit -> unitPing all pending asynchronous tasks for termination. Enabled continuations are executed and dequeued.
Source val pending : unit -> intNumber of asynchronous tasks still waiting.
Source val flush : ?polling :int -> unit -> unitWaits for all pending tasks to terminate. The default ~polling interval is 10 milliseconds.
sleep ms asynchronously waits for (at least) ms milliseconds.
Computation ResultsSource val finally : ?callback :('a -> unit) -> 'a t -> 'a t finally ~callback f starts computation f, eventually passing its result to callback, while immediately returning f for chaining.
Default ~callback is ignore.
Source val background : ?callback :('a -> unit) -> 'a t -> unitbackground 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.
Source val monitor : ?signal :'a signal -> ?handler :('a -> unit) -> 'b t -> 'b t 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.
Source val await : ?polling :int -> 'a t -> 'a await f waits until the end of computation f, yielding periodically until termination.
Default ~polling interval is 10 milliseconds.