Std.Data.PersistentArray

Std.PersistentArray.set t i a = if i ≥ t.tailOff then { root := t.root, tail := Array.set! t.tail (i - t.tailOff) a, size := t.size, shift := t.shift, tailOff := t.tailOff } else { root := Std.PersistentArray.setAux t.root (USize.ofNat i) t.shift a, tail := t.tail, size := t.size, shift := t.shift, tailOff := t.tailOff }

source

@[specialize]

partial def Std.PersistentArray.modifyAux {α : Type u} [inst : Inhabited α] (f : α → α) :

Std.PersistentArrayNode α → USize → USize → Std.PersistentArrayNode α

source

@[specialize]

def Std.PersistentArray.modify {α : Type u} [inst : Inhabited α] (t : Std.PersistentArray α) (i : Nat) (f : α → α) :

Std.PersistentArray α

Equations

Std.PersistentArray.modify t i f = if i ≥ t.tailOff then { root := t.root, tail := Array.modify t.tail (i - t.tailOff) f, size := t.size, shift := t.shift, tailOff := t.tailOff } else { root := Std.PersistentArray.modifyAux f t.root (USize.ofNat i) t.shift, tail := t.tail, size := t.size, shift := t.shift, tailOff := t.tailOff }

source

partial def Std.PersistentArray.mkNewPath {α : Type u} (shift : USize) (a : Array α) :

Std.PersistentArrayNode α

source

partial def Std.PersistentArray.insertNewLeaf {α : Type u} :

Std.PersistentArrayNode α → USize → USize → Array α → Std.PersistentArrayNode α

source

def Std.PersistentArray.mkNewTail {α : Type u} (t : Std.PersistentArray α) :

Std.PersistentArray α

Equations

Std.PersistentArray.mkNewTail t = if t.size ≤ USize.toNat (Std.PersistentArray.mul2Shift 1 (t.shift + Std.PersistentArray.initShift)) then { root := Std.PersistentArray.insertNewLeaf t.root (USize.ofNat (t.size - 1)) t.shift t.tail, tail := Std.PersistentArray.mkEmptyArray, size := t.size, shift := t.shift, tailOff := t.size } else { root := let n := Array.push Std.PersistentArray.mkEmptyArray t.root; Std.PersistentArrayNode.node (Array.push n (Std.PersistentArray.mkNewPath t.shift t.tail)), tail := #[], size := t.size, shift := t.shift + Std.PersistentArray.initShift, tailOff := t.size }

source

def Std.PersistentArray.tooBig :

Nat

Equations

Std.PersistentArray.tooBig = USize.size / 8

source

def Std.PersistentArray.push {α : Type u} (t : Std.PersistentArray α) (a : α) :

Std.PersistentArray α

Equations

Std.PersistentArray.push t a = let r := { root := t.root, tail := Array.push t.tail a, size := t.size + 1, shift := t.shift, tailOff := t.tailOff }; if (decide (Array.size r.tail < USize.toNat Std.PersistentArray.branching) || decide (t.size ≥ Std.PersistentArray.tooBig)) = true then r else Std.PersistentArray.mkNewTail r

source

partial def Std.PersistentArray.popLeaf {α : Type u} :

Std.PersistentArrayNode α → Option (Array α) × Array (Std.PersistentArrayNode α)

source

def Std.PersistentArray.pop {α : Type u} (t : Std.PersistentArray α) :

Std.PersistentArray α

Equations

Std.PersistentArray.pop t = if Array.size t.tail > 0 then { root := t.root, tail := Array.pop t.tail, size := t.size - 1, shift := t.shift, tailOff := t.tailOff } else match Std.PersistentArray.popLeaf t.root with | (none, x) => t | (some last, newRoots) => let last := Array.pop last; let newSize := t.size - 1; let newTailOff := newSize - Array.size last; if (Array.size newRoots == 1 && Std.PersistentArrayNode.isNode (Array.get! newRoots 0)) = true then { root := Array.get! newRoots 0, tail := last, size := newSize, shift := t.shift - Std.PersistentArray.initShift, tailOff := newTailOff } else { root := Std.PersistentArrayNode.node newRoots, tail := last, size := newSize, shift := t.shift, tailOff := newTailOff }

source

@[specialize]

def Std.PersistentArray.foldlM {α : Type u} {m : Type v → Type w} [inst : Monad m] {β : Type v} (t : Std.PersistentArray α) (f : β → α → m β) (init : β) (start : optParam Nat 0) :

m β

Equations

Std.PersistentArray.foldlM t f init start = if (start == 0) = true then do let b ← Std.PersistentArray.foldlMAux f t.root init Array.foldlM f b t.tail 0 (Array.size t.tail) else if start ≥ t.tailOff then Array.foldlM f init t.tail (start - t.tailOff) (Array.size t.tail) else do let b ← Std.PersistentArray.foldlFromMAux f t.root (USize.ofNat start) t.shift init Array.foldlM f b t.tail 0 (Array.size t.tail)

source

@[specialize]

def Std.PersistentArray.foldrM {α : Type u} {m : Type v → Type w} {β : Type v} [inst : Monad m] (t : Std.PersistentArray α) (f : α → β → m β) (init : β) :

m β

Equations

Std.PersistentArray.foldrM t f init = do let a ← Array.foldrM f init t.tail (Array.size t.tail) Std.PersistentArray.foldrMAux f t.root a

source

@[specialize]

partial def Std.PersistentArray.forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] [inh : Inhabited β] (f : α → β → m (ForInStep β)) (n : Std.PersistentArrayNode α) (b : β) :

m (ForInStep β)

source

@[specialize]

def Std.PersistentArray.forIn {α : Type u} {m : Type v → Type w} [inst : Monad m] {β : Type v} (t : Std.PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) :

m β

Equations

Std.PersistentArray.forIn t init f = do let a ← Std.PersistentArray.forInAux f t.root init match a with | ForInStep.done b => pure b | ForInStep.yield b => let b := b; do let r ← let col := t.tail; forIn col { fst := none, snd := b } fun v r => let r := r.snd; let b := r; do let a ← f v b match a with | ForInStep.done r => pure (ForInStep.done { fst := some r, snd := b }) | ForInStep.yield bNew => let b := bNew; do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := b }) let x : β := r.snd let b : β := x let _do_jp : PUnit → m β := fun y => pure b match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

instance Std.PersistentArray.instForInPersistentArray {α : Type u} {m : Type v → Type w} :

ForIn m (Std.PersistentArray α) α

Equations

Std.PersistentArray.instForInPersistentArray = { forIn := fun {β} [Monad m] => Std.PersistentArray.forIn }

source

@[specialize]

partial def Std.PersistentArray.findSomeMAux {α : Type u} {m : Type v → Type w} [inst : Monad m] {β : Type v} (f : α → m (Option β)) :

Std.PersistentArrayNode α → m (Option β)

source

@[specialize]

def Std.PersistentArray.findSomeM? {α : Type u} {m : Type v → Type w} [inst : Monad m] {β : Type v} (t : Std.PersistentArray α) (f : α → m (Option β)) :

m (Option β)

Equations

Std.PersistentArray.findSomeM? t f = do let a ← Std.PersistentArray.findSomeMAux f t.root match a with | none => Array.findSomeM? t.tail f | some b => pure (some b)

source

@[specialize]

partial def Std.PersistentArray.findSomeRevMAux {α : Type u} {m : Type v → Type w} [inst : Monad m] {β : Type v} (f : α → m (Option β)) :

Std.PersistentArrayNode α → m (Option β)

source

@[specialize]

def Std.PersistentArray.findSomeRevM? {α : Type u} {m : Type v → Type w} [inst : Monad m] {β : Type v} (t : Std.PersistentArray α) (f : α → m (Option β)) :

m (Option β)

Equations

Std.PersistentArray.findSomeRevM? t f = do let a ← Array.findSomeRevM? t.tail f match a with | none => Std.PersistentArray.findSomeRevMAux f t.root | some b => pure (some b)

source

@[specialize]

partial def Std.PersistentArray.forMAux {α : Type u} {m : Type v → Type w} [inst : Monad m] (f : α → m PUnit) :

Std.PersistentArrayNode α → m PUnit

source

@[specialize]

def Std.PersistentArray.forM {α : Type u} {m : Type v → Type w} [inst : Monad m] (t : Std.PersistentArray α) (f : α → m PUnit) :

m PUnit

Equations

Std.PersistentArray.forM t f = SeqRight.seqRight (Std.PersistentArray.forMAux f t.root) fun x => Array.forM f t.tail 0 (Array.size t.tail)

source

@[inline]

def Std.PersistentArray.foldl {α : Type u} {β : Type u_1} (t : Std.PersistentArray α) (f : β → α → β) (init : β) (start : optParam Nat 0) :

β

Equations

Std.PersistentArray.foldl t f init start = Id.run (Std.PersistentArray.foldlM t f init start)

source

@[inline]

def Std.PersistentArray.foldr {α : Type u} {β : Type u_1} (t : Std.PersistentArray α) (f : α → β → β) (init : β) :

β

Equations

Std.PersistentArray.foldr t f init = Id.run (Std.PersistentArray.foldrM t f init)

source

@[inline]

def Std.PersistentArray.filter {α : Type u} (as : Std.PersistentArray α) (p : α → Bool) :

Std.PersistentArray α

Equations

Std.PersistentArray.filter as p = Std.PersistentArray.foldl as (fun asNew a => if p a = true then Std.PersistentArray.push asNew a else asNew) { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 }

source

def Std.PersistentArray.toArray {α : Type u} (t : Std.PersistentArray α) :

Array α

Equations

Std.PersistentArray.toArray t = Std.PersistentArray.foldl t Array.push #[]

source

def Std.PersistentArray.append {α : Type u} (t₁ : Std.PersistentArray α) (t₂ : Std.PersistentArray α) :

Std.PersistentArray α

Equations

Std.PersistentArray.append t₁ t₂ = if Std.PersistentArray.isEmpty t₁ = true then t₂ else Std.PersistentArray.foldl t₂ Std.PersistentArray.push t₁

source

instance Std.PersistentArray.instAppendPersistentArray {α : Type u} :

Append (Std.PersistentArray α)

Equations

Std.PersistentArray.instAppendPersistentArray = { append := Std.PersistentArray.append }

source

@[inline]

def Std.PersistentArray.findSome? {α : Type u} {β : Type u_1} (t : Std.PersistentArray α) (f : α → Option β) :

Option β

Equations

Std.PersistentArray.findSome? t f = Id.run (Std.PersistentArray.findSomeM? t f)

source

@[inline]

def Std.PersistentArray.findSomeRev? {α : Type u} {β : Type u_1} (t : Std.PersistentArray α) (f : α → Option β) :

Option β

Equations

Std.PersistentArray.findSomeRev? t f = Id.run (Std.PersistentArray.findSomeRevM? t f)

source

def Std.PersistentArray.toList {α : Type u} (t : Std.PersistentArray α) :

List α

Equations

Std.PersistentArray.toList t = List.reverse (Std.PersistentArray.foldl t (fun xs x => x :: xs) [])

source

@[specialize]

partial def Std.PersistentArray.anyMAux {α : Type u} {m : Type → Type w} [inst : Monad m] (p : α → m Bool) :

Std.PersistentArrayNode α → m Bool

source

@[specialize]

def Std.PersistentArray.anyM {α : Type u} {m : Type → Type w} [inst : Monad m] (t : Std.PersistentArray α) (p : α → m Bool) :

m Bool

Equations

Std.PersistentArray.anyM t p = (Std.PersistentArray.anyMAux p t.root <||> Array.anyM p t.tail 0 (Array.size t.tail))

source

@[inline]

def Std.PersistentArray.allM {α : Type u} {m : Type → Type w} [inst : Monad m] (a : Std.PersistentArray α) (p : α → m Bool) :

m Bool

Equations

Std.PersistentArray.allM a p = do let b ← Std.PersistentArray.anyM a fun v => do let b ← p v pure !b pure !b

source

@[inline]

def Std.PersistentArray.any {α : Type u} (a : Std.PersistentArray α) (p : α → Bool) :

Bool

Equations

Std.PersistentArray.any a p = Id.run (Std.PersistentArray.anyM a p)

source

@[inline]

def Std.PersistentArray.all {α : Type u} (a : Std.PersistentArray α) (p : α → Bool) :

Bool

Equations

Std.PersistentArray.all a p = !Std.PersistentArray.any a fun v => !p v

source

@[specialize]

partial def Std.PersistentArray.mapMAux {α : Type u} {m : Type u → Type v} [inst : Monad m] {β : Type u} (f : α → m β) :

Std.PersistentArrayNode α → m (Std.PersistentArrayNode β)

source

@[specialize]

def Std.PersistentArray.mapM {α : Type u} {m : Type u → Type v} [inst : Monad m] {β : Type u} (f : α → m β) (t : Std.PersistentArray α) :

m (Std.PersistentArray β)

Equations

Std.PersistentArray.mapM f t = do let root ← Std.PersistentArray.mapMAux f t.root let tail ← Array.mapM f t.tail pure { root := root, tail := tail, size := t.size, shift := t.shift, tailOff := t.tailOff }