Std.Data.PersistentHashMap

source

inductive Std.PersistentHashMap.Entry (α : Type u) (β : Type v) (σ : Type w) :

Type (max (max u v) w)

entry: {α : Type u} → {β : Type v} → {σ : Type w} → α → β → Std.PersistentHashMap.Entry α β σ
ref: {α : Type u} → {β : Type v} → {σ : Type w} → σ → Std.PersistentHashMap.Entry α β σ
null: {α : Type u} → {β : Type v} → {σ : Type w} → Std.PersistentHashMap.Entry α β σ

source

instance Std.PersistentHashMap.instInhabitedEntry {α : Type u_1} {β : Type u_2} {σ : Type u_3} :

Inhabited (Std.PersistentHashMap.Entry α β σ)

Equations

Std.PersistentHashMap.instInhabitedEntry = { default := Std.PersistentHashMap.Entry.null }

source

inductive Std.PersistentHashMap.Node (α : Type u) (β : Type v) :

Type (max u v)

entries: {α : Type u} → {β : Type v} → Array (Std.PersistentHashMap.Entry α β (Std.PersistentHashMap.Node α β)) → Std.PersistentHashMap.Node α β
collision: {α : Type u} → {β : Type v} → (ks : Array α) → (vs : Array β) → Array.size ks = Array.size vs → Std.PersistentHashMap.Node α β

source

instance Std.PersistentHashMap.instInhabitedNode {α : Type u_1} {β : Type u_2} :

Inhabited (Std.PersistentHashMap.Node α β)

Equations

Std.PersistentHashMap.instInhabitedNode = { default := Std.PersistentHashMap.Node.entries #[] }

source

@[inline]

abbrev Std.PersistentHashMap.shift :

USize

Equations

Std.PersistentHashMap.shift = 5

source

@[inline]

abbrev Std.PersistentHashMap.branching :

USize

Equations

Std.PersistentHashMap.branching = USize.ofNat (2 ^ USize.toNat Std.PersistentHashMap.shift)

source

@[inline]

abbrev Std.PersistentHashMap.maxDepth :

USize

Equations

Std.PersistentHashMap.maxDepth = 7

source

@[inline]

abbrev Std.PersistentHashMap.maxCollisions :

Nat

Equations

Std.PersistentHashMap.maxCollisions = 4

source

def Std.PersistentHashMap.mkEmptyEntriesArray {α : Type u_1} {β : Type u_2} :

Array (Std.PersistentHashMap.Entry α β (Std.PersistentHashMap.Node α β))

Equations

Std.PersistentHashMap.mkEmptyEntriesArray = mkArray (USize.toNat Std.PersistentHashMap.branching) Std.PersistentHashMap.Entry.null

source

structure Std.PersistentHashMap (α : Type u) (β : Type v) [inst : BEq α] [inst : Hashable α] :

Type (max u v)

root : Std.PersistentHashMap.Node α β
size : Nat

source

@[inline]

abbrev Std.PHashMap (α : Type u) (β : Type v) [inst : BEq α] [inst : Hashable α] :

Type (max u v)

Equations

Std.PHashMap α β = Std.PersistentHashMap α β

source

def Std.PersistentHashMap.empty {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] :

Std.PersistentHashMap α β

Equations

Std.PersistentHashMap.empty = { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }

source

def Std.PersistentHashMap.isEmpty {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (m : Std.PersistentHashMap α β) :

Bool

Equations

Std.PersistentHashMap.isEmpty m = (m.size == 0)

source

instance Std.PersistentHashMap.instInhabitedPersistentHashMap {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] :

Inhabited (Std.PersistentHashMap α β)

Equations

Std.PersistentHashMap.instInhabitedPersistentHashMap = { default := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }

source

def Std.PersistentHashMap.mkEmptyEntries {α : Type u_1} {β : Type u_2} :

Std.PersistentHashMap.Node α β

Equations

Std.PersistentHashMap.mkEmptyEntries = Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray

source

@[inline]

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

USize

Equations

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

source

@[inline]

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

USize

Equations

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

source

@[inline]

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

USize

Equations

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

source

inductive Std.PersistentHashMap.IsCollisionNode {α : Type u_1} {β : Type u_2} :

Std.PersistentHashMap.Node α β → Prop

mk: ∀ {α : Type u_1} {β : Type u_2} (keys : Array α) (vals : Array β) (h : Array.size keys = Array.size vals), Std.PersistentHashMap.IsCollisionNode (Std.PersistentHashMap.Node.collision keys vals h)

source

@[inline]

abbrev Std.PersistentHashMap.CollisionNode (α : Type u_1) (β : Type u_2) :

Type (max 0 u_1 u_2)

Equations

Std.PersistentHashMap.CollisionNode α β = { n // Std.PersistentHashMap.IsCollisionNode n }

source

inductive Std.PersistentHashMap.IsEntriesNode {α : Type u_1} {β : Type u_2} :

Std.PersistentHashMap.Node α β → Prop

mk: ∀ {α : Type u_1} {β : Type u_2} (entries : Array (Std.PersistentHashMap.Entry α β (Std.PersistentHashMap.Node α β))), Std.PersistentHashMap.IsEntriesNode (Std.PersistentHashMap.Node.entries entries)

source

@[inline]

abbrev Std.PersistentHashMap.EntriesNode (α : Type u_1) (β : Type u_2) :

Type (max 0 u_1 u_2)

Equations

Std.PersistentHashMap.EntriesNode α β = { n // Std.PersistentHashMap.IsEntriesNode n }

source

partial def Std.PersistentHashMap.insertAtCollisionNodeAux {α : Type u_1} {β : Type u_2} [inst : BEq α] :

Std.PersistentHashMap.CollisionNode α β → Nat → α → β → Std.PersistentHashMap.CollisionNode α β

source

def Std.PersistentHashMap.insertAtCollisionNode {α : Type u_1} {β : Type u_2} [inst : BEq α] :

Std.PersistentHashMap.CollisionNode α β → α → β → Std.PersistentHashMap.CollisionNode α β

Equations

Std.PersistentHashMap.insertAtCollisionNode n k v = Std.PersistentHashMap.insertAtCollisionNodeAux n 0 k v

source

def Std.PersistentHashMap.getCollisionNodeSize {α : Type u_1} {β : Type u_2} :

Std.PersistentHashMap.CollisionNode α β → Nat

Equations

Std.PersistentHashMap.getCollisionNodeSize x = match x with | { val := Std.PersistentHashMap.Node.collision keys x x_1, property := x_2 } => Array.size keys | { val := Std.PersistentHashMap.Node.entries x, property := h } => False.elim (_ : False)

source

def Std.PersistentHashMap.mkCollisionNode {α : Type u_1} {β : Type u_2} (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) :

Std.PersistentHashMap.Node α β

Equations

Std.PersistentHashMap.mkCollisionNode k₁ v₁ k₂ v₂ = let ks := Array.mkEmpty Std.PersistentHashMap.maxCollisions; let ks := Array.push (Array.push ks k₁) k₂; let vs := Array.mkEmpty Std.PersistentHashMap.maxCollisions; let vs := Array.push (Array.push vs v₁) v₂; Std.PersistentHashMap.Node.collision ks vs (_ : Array.size (Array.push (Array.push (Array.mkEmpty Std.PersistentHashMap.maxCollisions) k₁) k₂) = Array.size (Array.push (Array.push (Array.mkEmpty Std.PersistentHashMap.maxCollisions) k₁) k₂))

source

partial def Std.PersistentHashMap.insertAux {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] :

Std.PersistentHashMap.Node α β → USize → USize → α → β → Std.PersistentHashMap.Node α β

source

partial def Std.PersistentHashMap.insertAux.traverse {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] (depth : USize) (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (entries : Std.PersistentHashMap.Node α β) :

Std.PersistentHashMap.Node α β

source

def Std.PersistentHashMap.insert {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → α → β → Std.PersistentHashMap α β

Equations

Std.PersistentHashMap.insert x x x = match x, x, x with | { root := n, size := sz }, k, v => { root := Std.PersistentHashMap.insertAux n (UInt64.toUSize (hash k)) 1 k v, size := sz + 1 }

source

partial def Std.PersistentHashMap.findAtAux {α : Type u_1} {β : Type u_2} [inst : BEq α] (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (k : α) :

Option β

source

partial def Std.PersistentHashMap.findAux {α : Type u_1} {β : Type u_2} [inst : BEq α] :

Std.PersistentHashMap.Node α β → USize → α → Option β

source

def Std.PersistentHashMap.find? {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → α → Option β

Equations

Std.PersistentHashMap.find? x x = match x, x with | { root := n, size := x }, k => Std.PersistentHashMap.findAux n (UInt64.toUSize (hash k)) k

source

@[inline]

def Std.PersistentHashMap.getOp {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → α → Option β

Equations

Std.PersistentHashMap.getOp self idx = Std.PersistentHashMap.find? self idx

source

@[inline]

def Std.PersistentHashMap.findD {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → α → β → β

Equations

Std.PersistentHashMap.findD m a b₀ = Option.getD (Std.PersistentHashMap.find? m a) b₀

source

@[inline]

def Std.PersistentHashMap.find! {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Std.PersistentHashMap α β → α → β

Equations

Std.PersistentHashMap.find! m a = match Std.PersistentHashMap.find? m a with | some b => b | none => panicWithPosWithDecl "Std.Data.PersistentHashMap" "Std.PersistentHashMap.find!" 158 14 "key is not in the map"

source

partial def Std.PersistentHashMap.findEntryAtAux {α : Type u_1} {β : Type u_2} [inst : BEq α] (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (k : α) :

Option (α × β)

source

partial def Std.PersistentHashMap.findEntryAux {α : Type u_1} {β : Type u_2} [inst : BEq α] :

Std.PersistentHashMap.Node α β → USize → α → Option (α × β)

source

def Std.PersistentHashMap.findEntry? {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → α → Option (α × β)

Equations

Std.PersistentHashMap.findEntry? x x = match x, x with | { root := n, size := x }, k => Std.PersistentHashMap.findEntryAux n (UInt64.toUSize (hash k)) k

source

partial def Std.PersistentHashMap.containsAtAux {α : Type u_1} {β : Type u_2} [inst : BEq α] (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (k : α) :

Bool

source

partial def Std.PersistentHashMap.containsAux {α : Type u_1} {β : Type u_2} [inst : BEq α] :

Std.PersistentHashMap.Node α β → USize → α → Bool

source

def Std.PersistentHashMap.contains {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst : Hashable α] :

Std.PersistentHashMap α β → α → Bool

Equations

Std.PersistentHashMap.contains x x = match x, x with | { root := n, size := x }, k => Std.PersistentHashMap.containsAux n (UInt64.toUSize (hash k)) k

source

partial def Std.PersistentHashMap.isUnaryEntries {α : Type u_1} {β : Type u_2} (a : Array (Std.PersistentHashMap.Entry α β (Std.PersistentHashMap.Node α β))) (i : Nat) (acc : Option (α × β)) :

Option (α × β)

source

def Std.PersistentHashMap.isUnaryNode {α : Type u_1} {β : Type u_2} :

Std.PersistentHashMap.Node α β → Option (α × β)

Equations

Std.PersistentHashMap.isUnaryNode x = match x with | Std.PersistentHashMap.Node.entries entries => Std.PersistentHashMap.isUnaryEntries entries 0 none | Std.PersistentHashMap.Node.collision keys vals heq => if h : 1 = Array.size keys then let_fun this := (_ : 0 < Array.size keys); some (Array.get keys { val := 0, isLt := this }, Array.get vals { val := 0, isLt := (_ : 0 < Array.size vals) }) else none

source

partial def Std.PersistentHashMap.eraseAux {α : Type u_1} {β : Type u_2} [inst : BEq α] :

Std.PersistentHashMap.Node α β → USize → α → Std.PersistentHashMap.Node α β × Bool

source

def Std.PersistentHashMap.erase {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → α → Std.PersistentHashMap α β

Equations

Std.PersistentHashMap.erase x x = match x, x with | { root := n, size := sz }, k => let h := UInt64.toUSize (hash k); let x := Std.PersistentHashMap.eraseAux n h k; match x with | (n, del) => { root := n, size := if del = true then sz - 1 else sz }

source

@[specialize]

partial def Std.PersistentHashMap.foldlMAux {m : Type w → Type w'} [inst : Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} (f : σ → α → β → m σ) :

Std.PersistentHashMap.Node α β → σ → m σ

source

partial def Std.PersistentHashMap.foldlMAux.traverse {m : Type w → Type w'} [inst : Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} (f : σ → α → β → m σ) (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (acc : σ) :

m σ

source

@[specialize]

def Std.PersistentHashMap.foldlM {m : Type w → Type w'} [inst : Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → (σ → α → β → m σ) → σ → m σ

Equations

Std.PersistentHashMap.foldlM map f init = Std.PersistentHashMap.foldlMAux f map.root init

source

@[specialize]

def Std.PersistentHashMap.forM {m : Type w → Type w'} [inst : Monad m] {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → (α → β → m PUnit) → m PUnit

Equations

Std.PersistentHashMap.forM map f = Std.PersistentHashMap.foldlM map (fun x => f) PUnit.unit

source

@[specialize]

def Std.PersistentHashMap.foldl {σ : Type w} {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → (σ → α → β → σ) → σ → σ

Equations

Std.PersistentHashMap.foldl map f init = Id.run (Std.PersistentHashMap.foldlM map f init)

source

def Std.PersistentHashMap.toList {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → List (α × β)

Equations

Std.PersistentHashMap.toList m = Std.PersistentHashMap.foldl m (fun ps k v => (k, v) :: ps) []

source

structure Std.PersistentHashMap.Stats :

Type

numNodes : Nat
numNull : Nat
numCollisions : Nat
maxDepth : Nat

source

partial def Std.PersistentHashMap.collectStats {α : Type u_1} {β : Type u_2} :

Std.PersistentHashMap.Node α β → Std.PersistentHashMap.Stats → Nat → Std.PersistentHashMap.Stats

source

def Std.PersistentHashMap.stats {α : Type u_1} {β : Type u_2} :

{x : BEq α} → {x_1 : Hashable α} → Std.PersistentHashMap α β → Std.PersistentHashMap.Stats

Equations

Std.PersistentHashMap.stats m = Std.PersistentHashMap.collectStats m.root { numNodes := 0, numNull := 0, numCollisions := 0, maxDepth := 0 } 1

source

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

String

Equations

Std.PersistentHashMap.Stats.toString s = toString "{ nodes := " ++ toString s.numNodes ++ toString ", null := " ++ toString s.numNull ++ toString ", collisions := " ++ toString s.numCollisions ++ toString ", depth := " ++ toString s.maxDepth ++ toString "}"

source

instance Std.PersistentHashMap.instToStringStats :

ToString Std.PersistentHashMap.Stats

Equations

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