Documentation

Init.Data.Queue

structure Std.Queue (α : Type u) :

A functional queue data structure, using two back-to-back lists. If we think of the queue as having elements pushed on the front and popped from the back, then the queue itself is effectively eList ++ dList.reverse.

  • eList : List α

    The enqueue list, which stores elements that have just been pushed (with the most recently enqueued elements at the head).

  • dList : List α

    The dequeue list, which buffers elements ready to be dequeued (with the head being the next item to be yielded by dequeue?).

Instances For
    def Std.Queue.empty {α : Type u} :

    O(1). The empty queue.

    Equations
      Instances For
        Equations
          def Std.Queue.isEmpty {α : Type u} (q : Queue α) :

          O(1). Is the queue empty?

          Equations
            Instances For
              def Std.Queue.enqueue {α : Type u} (v : α) (q : Queue α) :

              O(1). Push an element on the front of the queue.

              Equations
                Instances For
                  def Std.Queue.enqueueAll {α : Type u} (vs : List α) (q : Queue α) :

                  O(|vs|). Push a list of elements vs on the front of the queue.

                  Equations
                    Instances For
                      def Std.Queue.dequeue? {α : Type u} (q : Queue α) :
                      Option (α × Queue α)

                      O(1) amortized, O(n) worst case. Pop an element from the back of the queue, returning the element and the new queue.

                      Equations
                        Instances For
                          def Std.Queue.toArray {α : Type u} (q : Queue α) :
                          Equations
                            Instances For
                              @[specialize #[]]
                              def Std.Queue.filterM {m : TypeType v} [Monad m] {α : Type} (p : αm Bool) (q : Queue α) :
                              m (Queue α)

                              O(n). Applies the monadic predicate p to every element in the queue, and returns the queue of elements for which p returns true. Note that there are currently no guarantees for the order that p is applied in.

                              Equations
                                Instances For