package why3find

  1. Overview
  2. Docs
A Why3 Package Manager

Install

dune-project
 Dependency

Authors

Maintainers

Sources

why3find-1.3.0.tar.gz
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

Sourcetype 'a t

The time of computations that produces an 'a.

Sourceval return : 'a -> 'a t

return v computation that immediately returns v.

Sourceval 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.

Sourceval 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.

Sourceval map : ('a -> 'b) -> 'a t -> 'b t

Same as apply with reversed arguments.

Sourceval par : 'a t -> 'b t -> ('a * 'b) t

Combines two computations into a parallel computation of both.

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

Sourcemodule Monad : sig ... end

Monadic and Applicative operators.

Sourcemodule Queue : sig ... end

Iterable Queues.

List Combinators

Sourceval any : 'a t list -> 'a t

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

Sourceval seq : 'a t list -> 'a list t

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

Sourceval all : 'a t list -> 'a list t

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

Sourceval 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.

Signals

Sourcetype 'a signal

Inter tasks communication.

Sourceval signal : unit -> 'a signal

Creates a new channel for signaling.

Sourceval on : 'a signal -> ('a -> unit) -> unit

Register a hook on the signal.

Sourceval off : 'a signal -> ('a -> unit) -> unit

Un-register a hook on the signal.

Sourceval once : 'a signal -> ('a -> unit) -> unit

Register a hook that automatically disconnect itself on first emit.

Sourceval connected : 'a signal -> bool

At most one hook is connected to the signal.

Sourceval disconnect : 'a signal -> unit

Remove all hooks on the signal.

Sourceval clear : 'a signal -> unit

Remove all registered hooks.

Sourceval emit : 'a signal -> 'a -> unit

Broadcast a value on all registered hooks.

Variables

Variables are simply fibers to be assigned later on.

Sourceval var : ?init:'a -> unit -> 'a t

Creates a delated fiber.

Sourceval get : 'a t -> 'a option

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

Sourceval set : 'a t -> 'a -> unit

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.

Sourceval find : 'a t -> 'a

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

Sourceval defined : 'a t -> bool

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

Mutual Exclusion

Sourcetype mutex

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

Sourceval mutex : int -> mutex

mutex n creates a pool of n resources.

Sourceval sync : mutex -> ('a -> 'b t) -> 'a -> 'b t

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.

Sourceval 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.

Sourceval yield : unit -> unit

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

Sourceval pending : unit -> int

Number of asynchronous tasks still waiting.

Sourceval flush : ?polling:int -> unit -> unit

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

Sourceval sleep : int -> unit t

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

Computation Results

Sourceval 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.

Sourceval background : ?callback:('a -> unit) -> 'a t -> unit

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.

Sourceval 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.

Sourceval 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.