Documentation

Std.Data.PersistentArray

inductive Std.PersistentArrayNode (α : Type u) :

Type u

node: {α : Type u} → Array (Std.PersistentArrayNode α) → Std.PersistentArrayNode α
leaf: {α : Type u} → Array α → Std.PersistentArrayNode α

instance Std.instInhabitedPersistentArrayNode:

{a : Type u_1} → Inhabited (Std.PersistentArrayNode a)

Equations

Std.instInhabitedPersistentArrayNode = { default := Std.PersistentArrayNode.node default }

def Std.PersistentArrayNode.isNode {α : Type u_1} :

Std.PersistentArrayNode α → Bool

Equations

Std.PersistentArrayNode.isNode _fun_discr = match _fun_discr with | Std.PersistentArrayNode.node cs => true | Std.PersistentArrayNode.leaf vs => false

@[inline]

abbrev Std.PersistentArray.initShift:

Equations

Std.PersistentArray.initShift = 5

@[inline]

abbrev Std.PersistentArray.branching:

Equations

Std.PersistentArray.branching = USize.ofNat (2 ^ USize.toNat Std.PersistentArray.initShift)

structure Std.PersistentArray (α : Type u) :

Type u

root : Std.PersistentArrayNode α
tail : Array α
size : Nat
shift : USize
tailOff : Nat

instance Std.instInhabitedPersistentArray:

{a : Type u_1} → Inhabited (Std.PersistentArray a)

Equations

Std.instInhabitedPersistentArray = { default := { root := default, tail := default, size := default, shift := default, tailOff := default } }

@[inline]

abbrev Std.PArray (α : Type u) :

Type u

Equations

Std.PArray α = Std.PersistentArray α

def Std.PersistentArray.empty {α : Type u} :

Std.PersistentArray α

Equations

One or more equations did not get rendered due to their size.

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

Equations

Std.PersistentArray.isEmpty a = (a.size == 0)

def Std.PersistentArray.mkEmptyArray {α : Type u} :

Equations

Std.PersistentArray.mkEmptyArray = Array.mkEmpty (USize.toNat Std.PersistentArray.branching)

@[inline]

abbrev Std.PersistentArray.mul2Shift (i : USize) (shift : USize) :

Equations

Std.PersistentArray.mul2Shift i shift = USize.shiftLeft i shift

@[inline]

abbrev Std.PersistentArray.div2Shift (i : USize) (shift : USize) :

Equations

Std.PersistentArray.div2Shift i shift = USize.shiftRight i shift

@[inline]

abbrev Std.PersistentArray.mod2Shift (i : USize) (shift : USize) :

Equations

Std.PersistentArray.mod2Shift i shift = USize.land i (USize.shiftLeft 1 shift - 1)

partial def Std.PersistentArray.getAux {α : Type u} [inst : Inhabited α] :

Std.PersistentArrayNode α → USize → USize → α

def Std.PersistentArray.get! {α : Type u} [inst : Inhabited α] (t : Std.PersistentArray α) (i : Nat) :

α

Equations

Std.PersistentArray.get! t i = if i ≥ t.tailOff then Array.get! t.tail (i - t.tailOff) else Std.PersistentArray.getAux t.root (USize.ofNat i) t.shift

def Std.PersistentArray.getOp {α : Type u} [inst : Inhabited α] (self : Std.PersistentArray α) (idx : Nat) :

α

Equations

Std.PersistentArray.getOp self idx = Std.PersistentArray.get! self idx

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

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

def Std.PersistentArray.set {α : Type u} (t : Std.PersistentArray α) (i : Nat) (a : α) :

Std.PersistentArray α

Equations

One or more equations did not get rendered due to their size.

@[specialize]

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

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

@[specialize]

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

Std.PersistentArray α

Equations

One or more equations did not get rendered due to their size.

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

Std.PersistentArrayNode α

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

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

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

Std.PersistentArray α

Equations

One or more equations did not get rendered due to their size.

def Std.PersistentArray.tooBig:

Equations

Std.PersistentArray.tooBig = USize.size / 8

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

Std.PersistentArray α

Equations

One or more equations did not get rendered due to their size.

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

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

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

Std.PersistentArray α

Equations

One or more equations did not get rendered due to their size.

@[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

One or more equations did not get rendered due to their size.

@[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

@[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 β)

@[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

One or more equations did not get rendered due to their size.

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 }

@[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 β)

@[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)

@[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 β)

@[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)

@[specialize]

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

Std.PersistentArrayNode α → m PUnit

@[specialize]

def Std.PersistentArray.forM {α : Type u} {m : Type v → Type w} [inst : Monad m] (t : Std.PersistentArray α) (f : α → 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)

@[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)

@[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)

@[inline]

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

Std.PersistentArray α

Equations

One or more equations did not get rendered due to their size.

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

Equations

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

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₁

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

Append (Std.PersistentArray α)

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

@[specialize]

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

Std.PersistentArrayNode α → m Bool

@[specialize]

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

Equations

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

@[inline]

def Std.PersistentArray.allM {α : Type u} {m : Type → Type w} [inst : Monad m] (a : Std.PersistentArray α) (p : α → 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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[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 β)

@[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

One or more equations did not get rendered due to their size.

@[inline]

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

Std.PersistentArray β

Equations

Std.PersistentArray.map f t = Id.run (Std.PersistentArray.mapM f t)

structure Std.PersistentArray.Stats:

Type

numNodes : Nat
depth : Nat
tailSize : Nat

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

Std.PersistentArrayNode α → Std.PersistentArray.Stats → Nat → Std.PersistentArray.Stats

def Std.PersistentArray.stats {α : Type u} (r : Std.PersistentArray α) :

Std.PersistentArray.Stats

Equations

Std.PersistentArray.stats r = Std.PersistentArray.collectStats r.root { numNodes := 0, depth := 0, tailSize := Array.size r.tail } 0

def Std.PersistentArray.Stats.toString (s : Std.PersistentArray.Stats) :

Equations

One or more equations did not get rendered due to their size.

instance Std.PersistentArray.instToStringStats:

ToString Std.PersistentArray.Stats

Equations

Std.PersistentArray.instToStringStats = { toString := Std.PersistentArray.Stats.toString }

def Std.mkPersistentArray {α : Type u} (n : Nat) (v : α) :

Equations

Std.mkPersistentArray n v = Nat.fold (fun x p => Std.PersistentArray.push p v) n Std.PersistentArray.empty

@[inline]

def Std.mkPArray {α : Type u} (n : Nat) (v : α) :

Equations

Std.mkPArray n v = Std.mkPersistentArray n v

def List.toPersistentArrayAux {α : Type u} :

List α → Std.PersistentArray α → Std.PersistentArray α

Equations

List.toPersistentArrayAux [] _fun_discr = _fun_discr
List.toPersistentArrayAux (x :: xs) _fun_discr = List.toPersistentArrayAux xs (Std.PersistentArray.push _fun_discr x)

def List.toPersistentArray {α : Type u} (xs : List α) :

Std.PersistentArray α

Equations

One or more equations did not get rendered due to their size.

def Array.toPersistentArray {α : Type u} (xs : Array α) :

Std.PersistentArray α

Equations

Array.toPersistentArray xs = Array.foldl (fun p x => Std.PersistentArray.push p x) Std.PersistentArray.empty xs 0 (Array.size xs)

@[inline]

def Array.toPArray {α : Type u} (xs : Array α) :

Std.PersistentArray α

Equations

Array.toPArray xs = Array.toPersistentArray xs