structure Std.Queue (α : Type u) : 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?).

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

O(1). The empty queue.

Equations

• Std.Queue.empty = { }

instance Std.Queue.instEmptyCollection {α : Type u} : EmptyCollection (Queue α)

Equations

• Std.Queue.instEmptyCollection = { emptyCollection := Std.Queue.empty }

instance Std.Queue.instInhabited {α : Type u} : Inhabited (Queue α)

Equations

• Std.Queue.instInhabited = { default := ∅ }

def Std.Queue.isEmpty {α : Type u} (q : Queue α) : Bool

O(1). Is the queue empty?

Equations

• q.isEmpty = (q.dList.isEmpty && q.eList.isEmpty)

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

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

Equations

• Std.Queue.enqueue v q = { eList := v :: q.eList, dList := q.dList }

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

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

Equations

• Std.Queue.enqueueAll vs q = { eList := vs ++ q.eList, dList := q.dList }

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

• q.dequeue? = match q.dList with | d :: ds => some (d, { eList := q.eList, dList := ds }) | [] => match q.eList.reverse with | [] => none | d :: ds => some (d, { dList := ds })

def Std.Queue.toArray {α : Type u} (q : Queue α) : Array α

Equations

• q.toArray = q.dList.toArray ++ q.eList.toArray.reverse