Data.Queue

Immutable FIFO Queues

Definitions

record Queue : Type -> Type

  An immutable first-in first-out structure with amortized
  O(1) enqueue and dequeue operations.

Totality: total
Visibility: export
Constructor: 

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

Projections:

.back : Queue a -> SnocList a

.front : Queue a -> List a

Hints:

Eq a => Eq (Queue a)

Foldable Queue

Functor Queue

Monoid (Queue a)

Semigroup (Queue a)

Show a => Show (Queue a)

Traversable Queue

empty : Queue a

  The empty `Queue`. O(1)

Totality: total
Visibility: export

fromList : List a -> Queue a

  Converts a list to a `Queue`, keeping the order of
  elements. O(1)

Totality: total
Visibility: export

fromSnocList : SnocList a -> Queue a

  Converts a `SnocList` to a `Queue`, keeping the order of
  elements. O(1)

Totality: total
Visibility: export

toSnocList : Queue a -> SnocList a

  Converts a `Queue` to a `SnocList`, keeping the order
  of elements. O(n)

Totality: total
Visibility: export

enqueue : Queue a -> a -> Queue a

  Append a value at the back of the `Queue`. O(1)

Totality: total
Visibility: export

enqueueAll : Queue a -> List a -> Queue a

  Append a list of values at the back of the `Queue`. O(1)

Totality: total
Visibility: export

dequeue : Queue a -> Maybe (a, Queue a)

  Take a value from the front of the `Queue`.
  
  In case of the front being empty, this transfers
  the back to the front, which runs in O(n). However,
  every element in the `Queue` is thus shifted at most
  once before being dequeued, so this runs in amortized
  O(1).

Totality: total
Visibility: export

prepend : a -> Queue a -> Queue a

  We can prepend an element to our `Queue`, making it the new
  "oldest" element. O(1)
  
  This is against the typical use case for a FIFO data
  structure, but it allows us to conveniently implement
  `peekOldest`.

Totality: total
Visibility: export

peekOldest : Queue a -> Maybe (a, Queue a)

  Return the last element of the `Queue`, plus the unmodified
  `Queue`.
  
  Note: `peekOldest` might involve a rearrangement of the elements
        just like `dequeue`. In order to keep our amortized O(1)
        runtime behavior, the newly arranged `Queue` should be used
        henceforth.

Totality: total
Visibility: export

(++) : Queue a -> Queue a -> Queue a

  Appends two `Queue`s. O(m + n)

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

length : Queue a -> Nat

  Returns the length of the `Queue`. O(n).

Totality: total
Visibility: export

filter : (a -> Bool) -> Queue a -> Queue a

  Keeps only those values in a queue for which the given predicate
  returns `True`.

Totality: total
Visibility: export

mapMaybe : (a -> Maybe b) -> Queue a -> Queue b

  Maps the values in a queue, keeping only those for which the given
  function returns a `Just`.

Totality: total
Visibility: export