Data.Linear.Deferred

A `Deferred s` value, is an observable, initially empty
reference that can be set exactly once. As such, it is an
important synchronization primitive.

As with other mutable references, `Deferred` values can be safely used
in pure code as long as they are used locally in state thread.

Reexports

Definitions

record Once : Type -> Type -> Type

  An atomic reference that can be set exactly once and observed
  by at most one observer. All operations on `Once` are thread-safe.
  
  There are many occasions when it is enough to be able to register
  only one observer. Use `Once` for these, and use `Deferred` in
  case you need to register many observers.

Totality: total
Visibility: export
Constructor: 

O : Ref s (ST1 s a) -> Once s a

Projection: 

.ref : Once s a -> Ref s (ST1 s a)

once1 : F1 s (Once s a)

  Creates a new, empty `Once`.

Totality: total
Visibility: export

onceOf1 : (0 a : Type) -> F1 s (Once s a)

  Convenience alias of `once1`, which takes the type of
  the value stored as an explicit argument.

Totality: total
Visibility: export

completedOnce1 : Once s a -> F1 s Bool

  Returns `True` if a value has been set at the given `Once`.

Totality: total
Visibility: export

peekOnce1 : Once s a -> F1 s (Maybe a)

  Reads the set value of a `Once`. Returns `Nothing`,
  if no value has been set yet.

Totality: total
Visibility: export

putOnce1 : Once s a -> a -> F1' s

  Atomically tries to write the given value to a `Once`.
  
  The value is written if and only if no other value has
  been set first. If an observer has been registered, it will be
  invoked immediately.

Totality: total
Visibility: export

observeOnce1 : Once s a -> (a -> F1' s) -> F1 s (F1' s)

  Observe a `Once` by installing a callback.
  
  The callback is invoked immediately in case the value has
  already been set.
  
  The action that is returned by this function can be used to
  unregister the observer.
  
  Note: `Once` values can only be observed
        by one observer. Use `Deferred` in case you need to install
        many observers. In case another observer has already been set,
        this is a no-op and the callback never invoked.

Totality: total
Visibility: export

record Deferred : Type -> Type -> Type

  An atomic reference that can be set exactly once and observed
  by an arbitrary number of observers. Any operations on a `Deferred`
  are thread-safe.

Totality: total
Visibility: export
Constructor: 

D : Ref s (ST s a) -> Deferred s a

Projection: 

.ref : Deferred s a -> Ref s (ST s a)

deferred1 : F1 s (Deferred s a)

  Creates a new, empty `Deferred s a`.

Totality: total
Visibility: export

deferredOf1 : (0 a : Type) -> F1 s (Deferred s a)

  Convenience alias of `deferred1`, which takes the type of
  the value stored as an explicit argument.

Totality: total
Visibility: export

completed1 : Deferred s a -> F1 s Bool

  Returns `True` if a value has been set at the given `Deferred`.

Totality: total
Visibility: export

peekDeferred1 : Deferred s a -> F1 s (Maybe a)

  Reads the set value of a `Deferred`. Returns `Nothing`,
  if no value has been set yet.

Totality: total
Visibility: export

putDeferred1 : Deferred s a -> a -> F1' s

  Atomically tries to write the given value to a `Deferred`.
  
  The value is written if and only if no other values has
  been set first. Any observers will be invoked immediately.

Totality: total
Visibility: export

observeDeferredAs1 : Deferred s a -> Token s -> (a -> F1' s) -> F1 s (F1' s)

  Observe a `Deferred` by installing a callback using the given
  token for identification.
  
  The callback is invoked immediately in case the value has
  already been set.
  
  The action that is returned by this function can be used to
  unregister the observer.

Totality: total
Visibility: export

observeDeferred1 : Deferred s a -> (a -> F1' s) -> F1 s (F1' s)

  Observe a `Deferred` by installing a callback.
  
  The callback is invoked immediately in case the value has
  already been set.
  
  The action that is returned by this function can be used to
  unregister the observer.

Totality: total
Visibility: export

once : Lift1 s f => f (Once s a)

  Lifted version of `once1`

Totality: total
Visibility: export

onceOf : Lift1 s f => (0 a : Type) -> f (Once s a)

  Lifted version of `onceOf`

Totality: total
Visibility: export

peekOnce : Lift1 s f => Once s a -> f (Maybe a)

  Lifted version of `peekOnce1`

Totality: total
Visibility: export

completedOnce : Lift1 s f => Once s a -> f Bool

  Lifted version of `completedOnce1`

Totality: total
Visibility: export

putOnce : Lift1 s f => Once s a -> a -> f ()

  Lifted version of `putOnce1`

Totality: total
Visibility: export

completed : Lift1 s f => Deferred s a -> f Bool

  Lifted version of `completed1`

Totality: total
Visibility: export

deferred : Lift1 s f => f (Deferred s a)

  Lifted version of `deferred1`

Totality: total
Visibility: export

deferredOf : Lift1 s f => (0 a : Type) -> f (Deferred s a)

  Lifted version of `deferredOf1`

Totality: total
Visibility: export

peekDeferred : Lift1 s f => Deferred s a -> f (Maybe a)

  Lifted version of `peekDeferred1`

Totality: total
Visibility: export

putDeferred : Lift1 s f => Deferred s a -> a -> f ()

  Lifted version of `putDeferred1`

Totality: total
Visibility: export