@[inline]
def
Array.qpartition
{α : Type}
[inst : Inhabited α]
(as : Array α)
(lt : α → α → Bool)
(lo : Nat)
(hi : Nat)
:
Equations
- Array.qpartition as lt lo hi = let mid := (lo + hi) / 2; let as := if lt (Array.get! as mid) (Array.get! as lo) = true then Array.swap! as lo mid else as; let as := if lt (Array.get! as hi) (Array.get! as lo) = true then Array.swap! as lo hi else as; let as := if lt (Array.get! as mid) (Array.get! as hi) = true then Array.swap! as mid hi else as; let pivot := Array.get! as hi; (fun loop => loop as lo lo) (Array.qpartition.loop lt hi pivot)
def
Array.qpartition.loop
{α : Type}
[inst : Inhabited α]
(lt : α → α → Bool)
(hi : Nat)
(pivot : α)
(as : Array α)
(i : Nat)
(j : Nat)
:
Equations
- Array.qpartition.loop lt hi pivot as i j = if h : j < hi then if lt (Array.get! as j) pivot = true then let as := Array.swap! as i j; Array.qpartition.loop lt hi pivot as (i + 1) (j + 1) else Array.qpartition.loop lt hi pivot as i (j + 1) else let as := Array.swap! as i hi; (i, as)
@[inline]
def
Array.qsort
{α : Type}
[inst : Inhabited α]
(as : Array α)
(lt : α → α → Bool)
(low : optParam Nat 0)
(high : optParam Nat (Array.size as - 1))
:
Array α
Equations
- Array.qsort as lt low high = (fun sort => sort as low high) (Array.qsort.sort lt)