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 ≤ m
m < 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
.