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

Std.Queue.empty = { eList := [], dList := [] }

instance Std.Queue.instEmptyCollection {α : Type u} :

EmptyCollection (Std.Queue α)

Equations

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

instance Std.Queue.instInhabited {α : Type u} :

Inhabited (Std.Queue α)

Equations

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

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

O(1). Is the queue empty?

Equations

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

def Std.Queue.enqueue {α : Type u} (v : α) (q : Std.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 : Std.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 : Std.Queue α) :

Option (α × Std.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

One or more equations did not get rendered due to their size.

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

Equations

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