Data.BoundedQueue1.Unsized

Linear Bounded Queues

Definitions

empty : Nat -> F1 s (BoundedQueue1 s a)

  The empty `BoundedQueue1`. O(1)

Totality: total
Visibility: export

null : BoundedQueue1 s a -> F1 s Bool

  Is the `BoundedQueuei1` empty? O(1)

Totality: total
Visibility: export

fromList : Nat -> List a -> F1 s (BoundedQueue1 s a)

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

Totality: total
Visibility: export

fromSnocList : Nat -> SnocList a -> F1 s (BoundedQueue1 s a)

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

Totality: total
Visibility: export

toList : BoundedQueue1 s a -> F1 s (List a)

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

Totality: total
Visibility: export

toSnocList : BoundedQueue1 s a -> F1 s (SnocList a)

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

Totality: total
Visibility: export

enqueue : BoundedQueue1 s a -> a -> F1 s Bool

  Append a value at the back of the `BoundedQueue1`.
  This function returns `True` if the value was enqueued,
  and `False` if the queue was full. O(1)

Totality: total
Visibility: export

dequeue : BoundedQueue1 s a -> F1 s (Maybe a)

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

Totality: total
Visibility: export

prepend : a -> BoundedQueue1 s a -> F1 s Bool

  We can prepend an element to our `BoundedQueue1`, making it the new
  "oldest" element. O(1)
  This function returns `True` is the value was pre-pended,
  and `False` if the queue was full. O(1)

Totality: total
Visibility: export

peekOldest : BoundedQueue1 s a -> F1 s (Maybe (a, BoundedQueue1 s a))

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

length : BoundedQueue1 s a -> F1 s Nat

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

Totality: total
Visibility: export