IO.Async.Loop

Utilities for working with work loops.

Reexports

Definitions

record FbrState : Type -> Type

  Internal state of a running fiber.

Totality: total
Visibility: export
Constructor: 

FST : FiberImpl resErrs resType -> Nat -> Async e curErrs curType -> Stack e curErrs resErrs curType resType -> FbrState e

Projections:

.comp : ({rec:0} : FbrState e) -> Async e (curErrs {rec:0}) (curType {rec:0})

0 .curErrs : FbrState e -> List Type

0 .curType : FbrState e -> Type

.fiber : ({rec:0} : FbrState e) -> FiberImpl (resErrs {rec:0}) (resType {rec:0})

.mask : FbrState e -> Nat

0 .resErrs : FbrState e -> List Type

0 .resType : FbrState e -> Type

.stack : ({rec:0} : FbrState e) -> Stack e (curErrs {rec:0}) (resErrs {rec:0}) (curType {rec:0}) (resType {rec:0})

data RunRes : Type -> Type

  Result of (partially) evaluate a fiber.

Totality: total
Visibility: public export
Constructors:

Done : RunRes e

  The fiber has terminated with an `Outcome`, or we arrived at
  an asynchronous boundary (`Asnc` data constructor) and the
  fiber should be parked until a result is ready.

Cont : FbrState e -> RunRes e

  Evaluation of the fiber is not yet finished, but should be
  rescheduled by moving the fiber at the end of the event loop's
  work queue. This happens a) after a certain number of evaluation
  steps, or b) when `cede` is encountered.

interface EventLoop : Type -> Type

  A context for submitting and running work packages asynchronously.
  
  The basic functionality of an event loop is to allow us to spawn
  new work packages, all of which will then be run concurrently (but not
  necessarily in parallel), and to `cede` a running computation, so that
  it will be processed later while allowing other work packages to be
  processed first.
  
  In addition, an event loop can support arbitrary additional effects, for
  instance, the ability to setup timers, signal handlers, and asynchronous
  `IO` actions. These additional capabilities are represented by type
  parameter `e`, representing the event loop currently processing a work
  package.

Parameters: e
Constructor: 

EL

Methods:

spawn : e -> FbrState e -> IO1 ()

  Submits a fiber to be run by event loop `el`

limit : Nat

  Number of evaluation steps before a fiber should be rescheduled.

Implementation: 

EventLoop SyncST

spawn : EventLoop e => e -> FbrState e -> IO1 ()

  Submits a fiber to be run by event loop `el`

Totality: total
Visibility: public export

limit : EventLoop e => Nat

  Number of evaluation steps before a fiber should be rescheduled.

Totality: total
Visibility: public export

runFbr : EventLoop e => e -> FbrState e -> IO1 (RunRes e)

Totality: total
Visibility: export

runAsyncWith : EventLoop e => e -> Async e es a -> (Outcome es a -> IO ()) -> IO ()

Totality: total
Visibility: export

runAsync : EventLoop e => e -> Async e es a -> IO ()

Totality: total
Visibility: export