structure Batteries.BinaryHeap (α : Type u_1) (lt : α → α → Bool) : Type u_1

A max-heap data structure.

• arr : Array α

  O(1). Get data array for a BinaryHeap.

@[irreducible]

def Batteries.BinaryHeap.heapifyDown {α : Type u_1} {sz : Nat} (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) : Vector α sz

Core operation for binary heaps, expressed directly on arrays. Given an array which is a max-heap, push item i down to restore the max-heap property.

def Batteries.BinaryHeap.mkHeap {α : Type u_1} {sz : Nat} (lt : α → α → Bool) (a : Vector α sz) : Vector α sz

Core operation for binary heaps, expressed directly on arrays. Construct a heap from an unsorted array, by heapifying all the elements.

def Batteries.BinaryHeap.mkHeap.loop {α : Type u_1} {sz : Nat} (lt : α → α → Bool) (i : Nat) (a : Vector α sz) : i ≤ sz → Vector α sz

Inner loop for mkHeap.

@[irreducible]

def Batteries.BinaryHeap.heapifyUp {α : Type u_1} {sz : Nat} (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) : Vector α sz

Core operation for binary heaps, expressed directly on arrays. Given an array which is a max-heap, push item i up to restore the max-heap property.

def Batteries.BinaryHeap.empty {α : Type u_1} (lt : α → α → Bool) : BinaryHeap α lt

O(1). Build a new empty heap.

instance Batteries.BinaryHeap.instInhabited {α : Type u_1} (lt : α → α → Bool) : Inhabited (BinaryHeap α lt)

instance Batteries.BinaryHeap.instEmptyCollection {α : Type u_1} (lt : α → α → Bool) : EmptyCollection (BinaryHeap α lt)

def Batteries.BinaryHeap.singleton {α : Type u_1} (lt : α → α → Bool) (x : α) : BinaryHeap α lt

O(1). Build a one-element heap.

def Batteries.BinaryHeap.size {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) : Nat

O(1). Get the number of elements in a BinaryHeap.

def Batteries.BinaryHeap.vector {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) : Vector α self.size

O(1). Get data vector of a BinaryHeap.

def Batteries.BinaryHeap.get {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (i : Fin self.size) : α

O(1). Get an element in the heap by index.

def Batteries.BinaryHeap.insert {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt

O(log n). Insert an element into a BinaryHeap, preserving the max-heap property.

@[simp]

theorem Batteries.BinaryHeap.size_insert {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (x : α) : (self.insert x).size = self.size + 1

def Batteries.BinaryHeap.max {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) : Option α

O(1). Get the maximum element in a BinaryHeap.

def Batteries.BinaryHeap.popMax {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) : BinaryHeap α lt

O(log n). Remove the maximum element from a BinaryHeap. Call max first to actually retrieve the maximum element.

@[simp]

theorem Batteries.BinaryHeap.size_popMax {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) : self.popMax.size = self.size - 1

def Batteries.BinaryHeap.extractMax {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) : Option α × BinaryHeap α lt

O(log n). Return and remove the maximum element from a BinaryHeap.

theorem Batteries.BinaryHeap.size_pos_of_max {α : Type u_1} {lt : α → α → Bool} {x : α} {self : BinaryHeap α lt} (h : self.max = some x) : 0 < self.size

def Batteries.BinaryHeap.insertExtractMax {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt

O(log n). Equivalent to extractMax (self.insert x), except that extraction cannot fail.

def Batteries.BinaryHeap.replaceMax {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α lt

O(log n). Equivalent to (self.max, self.popMax.insert x).

def Batteries.BinaryHeap.decreaseKey {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt

O(log n). Replace the value at index i by x. Assumes that x ≤ self.get i.

def Batteries.BinaryHeap.increaseKey {α : Type u_1} {lt : α → α → Bool} (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt

O(log n). Replace the value at index i by x. Assumes that self.get i ≤ x.

def Batteries.Vector.toBinaryHeap {α : Type u_1} {n : Nat} (lt : α → α → Bool) (v : Vector α n) : BinaryHeap α lt

O(n). Convert an unsorted vector to a BinaryHeap.

def Array.toBinaryHeap {α : Type u_1} (lt : α → α → Bool) (a : Array α) : Batteries.BinaryHeap α lt

O(n). Convert an unsorted array to a BinaryHeap.

@[specialize #[]]

def Array.heapSort {α : Type u_1} (a : Array α) (lt : α → α → Bool) : Array α

O(n log n). Sort an array using a BinaryHeap.

@[irreducible]

def Array.heapSort.loop {α : Type u_1} (lt : α → α → Bool) (a : Batteries.BinaryHeap α (flip lt)) (out : Array α) : Array α

Inner loop for heapSort.