package why3find
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=435da830a513fd91ec5411c91126b763
sha512=fd8b04eb16d569c0dc9e5595a40b174d7858121b080c81d459b2f28fb3af1ebc32ef408859d5c1c5f45c61790625c027c2ecfc3d45e597943543de7212bab8d6
doc/why3find.utils/Why3findUtils/Fibers/index.html
Module Why3findUtils.FibersSource
Lightweight and Monadic Fibers Library.
Freely inspired from the Fiber dune package.
Basic Constructors
The time of computations that produces an 'a.
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.
Combines two computations into a parallel computation of both.
See Monad.and*, and Monad.@* operators.
List Combinators
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.
Signals
Inter tasks communication.
Register a hook that automatically disconnect itself on first emit.
Variables
Variables are simply fibers to be assigned later on.
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.
Mutual Exclusion
A limited set of resources to be shared on different tasks.
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 Tasks
The 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.
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.
Computation Results
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.