Data.BoundedQueue.Unsized

Bounded Queues

Definitions

empty : Nat -> BoundedQueue a

  The empty `BoundedQueue`. O(1)

Totality: total
Visibility: export

null : BoundedQueue a -> Bool

  Is the `BoundedQueue` empty? O(1)

Totality: total
Visibility: export

fromList : Nat -> List a -> BoundedQueue a

  Naively keeps the first `n` values of a list, and converts
  into a `BoundedQueue` (keeps the order of the elements). O(1)

Totality: total
Visibility: export

fromSnocList : Nat -> SnocList a -> BoundedQueue a

  Naively keeps the first `n` values of a `SnocList`, and converts
  into a `BoundedQueue` (keeps the order of the elements). O(1)

Totality: total
Visibility: export

toList : BoundedQueue a -> List a

  Converts a `BoundedQueue` to a `List`, keeping the order
  of elements. O(n)

Totality: total
Visibility: export

toSnocList : BoundedQueue a -> SnocList a

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

Totality: total
Visibility: export

enqueue : BoundedQueue a -> a -> BoundedQueue a

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

Totality: total
Visibility: export

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

  Take a value from the front of the `BoundedQueue`. O(1)

Totality: total
Visibility: export

prepend : a -> BoundedQueue a -> BoundedQueue a

  We can prepend an element to our `BoundedQueue`, 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 : BoundedQueue a -> Maybe (a, BoundedQueue a)

  Return the last element of the `BoundedQueue`, 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

(++) : BoundedQueue a -> BoundedQueue a -> BoundedQueue a

  Appends two `BoundedQueues`. O(m + n)

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

length : BoundedQueue a -> Nat

  Returns the length of the `BoundedQueue`. O(1).

Totality: total
Visibility: export