@[inline]
def
Array.binSearch
{α : Type}
[inst : Inhabited α]
(as : Array α)
(k : α)
(lt : α → α → Bool)
(lo : optParam Nat 0)
(hi : optParam Nat (Array.size as - 1))
:
Option α
Equations
- Array.binSearch as k lt lo hi = if lo < Array.size as then let hi := if hi < Array.size as then hi else Array.size as - 1; Array.binSearchAux lt id as k lo hi else none
@[inline]
def
Array.binSearchContains
{α : Type}
[inst : Inhabited α]
(as : Array α)
(k : α)
(lt : α → α → Bool)
(lo : optParam Nat 0)
(hi : optParam Nat (Array.size as - 1))
:
Equations
- Array.binSearchContains as k lt lo hi = if lo < Array.size as then let hi := if hi < Array.size as then hi else Array.size as - 1; Array.binSearchAux lt Option.isSome as k lo hi else false
@[specialize]
def
Array.binInsertM
{α : Type u}
{m : Type u → Type v}
[inst : Monad m]
[inst : Inhabited α]
(lt : α → α → Bool)
(merge : α → m α)
(add : Unit → m α)
(as : Array α)
(k : α)
:
m (Array α)
Equations
- Array.binInsertM lt merge add as k = if Array.isEmpty as = true then do let v ← add () pure (Array.push as v) else if lt k (Array.get! as 0) = true then do let v ← add () pure (Array.insertAt as 0 v) else if (!lt (Array.get! as 0) k) = true then Array.modifyM as 0 merge else if lt (Array.back as) k = true then do let v ← add () pure (Array.push as v) else if (!lt k (Array.back as)) = true then Array.modifyM as (Array.size as - 1) merge else Array.binInsertAux lt merge add as k 0 (Array.size as - 1)
@[inline]
def
Array.binInsert
{α : Type u}
[inst : Inhabited α]
(lt : α → α → Bool)
(as : Array α)
(k : α)
:
Array α
Equations
- Array.binInsert lt as k = Id.run (Array.binInsertM lt (fun x => k) (fun x => k) as k)