def
Array.qpartition
{α : Type u_1}
{n : Nat}
(as : Vector α n)
(lt : α → α → Bool)
(lo hi : Nat)
(w : lo ≤ hi := by omega)
(hlo : lo < n := by omega)
(hhi : hi < n := by omega)
:
Internal implementation of Array.qsort.
qpartition as lt lo hi hlo hhi returns a pair (⟨m, h₁, h₂⟩, as') where
as' is a permutation of as and m is a number such that:
lo ≤ mm < n∀ i, lo ≤ i → i < m → lt as[i] as[m]∀ j, m < j → j < hi → !lt as[j] as[m]
It does so by first swapping the elements at indices lo, mid := (lo + hi) / 2, and hi
if necessary so that the middle (pivot) element is at index hi.
We then iterate from k = lo to k = hi, with a pointer i starting at lo, and
swapping each element which is less than the pivot to position i, and then incrementing i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
def
Array.qpartition.loop
{α : Type u_1}
{n : Nat}
(lt : α → α → Bool)
(lo hi : Nat)
(hhi : hi < n := by omega)
(pivot : α)
(as : Vector α n)
(i k : Nat)
(ilo : lo ≤ i := by omega)
(ik : i ≤ k := by omega)
(w : k ≤ hi := by omega)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Array.qsort
{α : Type u_1}
(as : Array α)
(lt : α → α → Bool := by exact (· < ·))
(lo : Nat := 0)
(hi : Nat := as.size - 1)
:
Array α
In-place quicksort.
qsort as lt lo hi sorts the subarray as[lo:hi+1] in-place using lt to compare elements.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[irreducible, specialize #[]]
def
Array.qsort.sort
{α : Type u_1}
(lt : α → α → Bool := by exact (· < ·))
{n : Nat}
(as : Vector α n)
(lo hi : Nat)
(w : lo ≤ hi := by omega)
(hlo : lo < n := by omega)
(hhi : hi < n := by omega)
:
Vector α n
Equations
- One or more equations did not get rendered due to their size.