IO.Async.Loop.Queue

Definitions

inc : IORef Nat -> IO1 ()

Totality: total
Visibility: export

dec : IORef Nat -> IO1 Bool

Totality: total
Visibility: export

record Queue : Type -> Type

  A specialize queue implementation enabling fast enqueue, dequeue,
  and work stealing.

Totality: total
Visibility: export
Constructor: 

Q : Bool -> List a -> SnocList a -> Queue a

Projections:

.asleep : Queue a -> Bool

.head : Queue a -> List a

.tail : Queue a -> SnocList a

queueOf : (0 a : Type) -> Queue a

Totality: total
Visibility: export

isEmpty : Queue a -> Bool

Totality: total
Visibility: export

enq : IORef (Queue a) -> a -> IO1 Bool

Totality: total
Visibility: export

enqall : IORef (Queue a) -> List a -> IO1 Bool

Totality: total
Visibility: export

deq : IORef (Queue a) -> IO1 (Maybe a)

Totality: total
Visibility: export

deqAndSleep : IORef (Queue a) -> IO1 (Maybe a)

Totality: total
Visibility: export

steal : IORef (Queue a) -> IO1 (Maybe a)

  Steals up to `STEAL_MAX` tasks from a queue but not more than half
  the enqueued tasks (rounded up).

Totality: total
Visibility: export