Equations
- Std.HashMapBucket α β = { b // Array.size b > 0 }
def
Std.HashMapBucket.update
{α : Type u}
{β : Type v}
(data : Std.HashMapBucket α β)
(i : USize)
(d : Std.AssocList α β)
(h : USize.toNat i < Array.size data.val)
:
Equations
- Std.HashMapBucket.update data i d h = { val := Array.uset data.val i d h, property := (_ : Array.size (Array.uset data.val i d h) > 0) }
- size : Nat
- buckets : Std.HashMapBucket α β
Equations
- Std.mkHashMapImp capacity = let_fun nbuckets := Std.numBucketsForCapacity capacity; let n := if nbuckets = 0 then 8 else nbuckets; { size := 0, buckets := { val := mkArray n Std.AssocList.nil, property := (_ : Array.size (mkArray n Std.AssocList.nil) > 0) } }
Equations
- Std.HashMapImp.mkIdx h u = { val := u % n, property := (_ : USize.toNat (u % n) < n) }
@[inline]
def
Std.HashMapImp.reinsertAux
{α : Type u}
{β : Type v}
(hashFn : α → UInt64)
(data : Std.HashMapBucket α β)
(a : α)
(b : β)
:
Equations
- Std.HashMapImp.reinsertAux hashFn data a b = let x := Std.HashMapImp.mkIdx (_ : Array.size data.val > 0) (UInt64.toUSize (hashFn a)); match x with | { val := i, property := h } => Std.HashMapBucket.update data i (Std.AssocList.cons a b (Array.uget data.val i h)) h
@[inline]
def
Std.HashMapImp.foldBucketsM
{α : Type u}
{β : Type v}
{δ : Type w}
{m : Type w → Type w}
[inst : Monad m]
(data : Std.HashMapBucket α β)
(d : δ)
(f : δ → α → β → m δ)
:
m δ
Equations
- Std.HashMapImp.foldBucketsM data d f = Array.foldlM (fun d b => Std.AssocList.foldlM f d b) d data.val 0 (Array.size data.val)
@[inline]
def
Std.HashMapImp.foldBuckets
{α : Type u}
{β : Type v}
{δ : Type w}
(data : Std.HashMapBucket α β)
(d : δ)
(f : δ → α → β → δ)
:
δ
Equations
- Std.HashMapImp.foldBuckets data d f = Id.run (Std.HashMapImp.foldBucketsM data d f)
@[inline]
def
Std.HashMapImp.foldM
{α : Type u}
{β : Type v}
{δ : Type w}
{m : Type w → Type w}
[inst : Monad m]
(f : δ → α → β → m δ)
(d : δ)
(h : Std.HashMapImp α β)
:
m δ
Equations
- Std.HashMapImp.foldM f d h = Std.HashMapImp.foldBucketsM h.buckets d f
@[inline]
def
Std.HashMapImp.fold
{α : Type u}
{β : Type v}
{δ : Type w}
(f : δ → α → β → δ)
(d : δ)
(m : Std.HashMapImp α β)
:
δ
Equations
- Std.HashMapImp.fold f d m = Std.HashMapImp.foldBuckets m.buckets d f
@[inline]
def
Std.HashMapImp.forBucketsM
{α : Type u}
{β : Type v}
{m : Type w → Type w}
[inst : Monad m]
(data : Std.HashMapBucket α β)
(f : α → β → m PUnit)
:
m PUnit
Equations
- Std.HashMapImp.forBucketsM data f = Array.forM (fun b => Std.AssocList.forM f b) data.val 0 (Array.size data.val)
@[inline]
def
Std.HashMapImp.forM
{α : Type u}
{β : Type v}
{m : Type w → Type w}
[inst : Monad m]
(f : α → β → m PUnit)
(h : Std.HashMapImp α β)
:
m PUnit
Equations
- Std.HashMapImp.forM f h = Std.HashMapImp.forBucketsM h.buckets f
def
Std.HashMapImp.findEntry?
{α : Type u}
{β : Type v}
[inst : BEq α]
[inst : Hashable α]
(m : Std.HashMapImp α β)
(a : α)
:
Equations
- Std.HashMapImp.findEntry? m a = match m with | { size := x, buckets := buckets } => let x := Std.HashMapImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => Std.AssocList.findEntry? a (Array.uget buckets.val i h)
def
Std.HashMapImp.find?
{α : Type u}
{β : Type v}
[inst : BEq α]
[inst : Hashable α]
(m : Std.HashMapImp α β)
(a : α)
:
Option β
Equations
- Std.HashMapImp.find? m a = match m with | { size := x, buckets := buckets } => let x := Std.HashMapImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => Std.AssocList.find? a (Array.uget buckets.val i h)
def
Std.HashMapImp.contains
{α : Type u}
{β : Type v}
[inst : BEq α]
[inst : Hashable α]
(m : Std.HashMapImp α β)
(a : α)
:
Equations
- Std.HashMapImp.contains m a = match m with | { size := x, buckets := buckets } => let x := Std.HashMapImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => Std.AssocList.contains a (Array.uget buckets.val i h)
partial def
Std.HashMapImp.moveEntries
{α : Type u}
{β : Type v}
[inst : Hashable α]
(i : Nat)
(source : Array (Std.AssocList α β))
(target : Std.HashMapBucket α β)
:
def
Std.HashMapImp.expand
{α : Type u}
{β : Type v}
[inst : Hashable α]
(size : Nat)
(buckets : Std.HashMapBucket α β)
:
Std.HashMapImp α β
Equations
- Std.HashMapImp.expand size buckets = let nbuckets := Array.size buckets.val * 2; let_fun this := (_ : Array.size buckets.val * 2 > 0); let new_buckets := { val := mkArray nbuckets Std.AssocList.nil, property := (_ : Array.size (mkArray nbuckets Std.AssocList.nil) > 0) }; { size := size, buckets := Std.HashMapImp.moveEntries 0 buckets.val new_buckets }
@[inline]
def
Std.HashMapImp.insert
{α : Type u}
{β : Type v}
[inst : BEq α]
[inst : Hashable α]
(m : Std.HashMapImp α β)
(a : α)
(b : β)
:
Std.HashMapImp α β × Bool
Equations
- Std.HashMapImp.insert m a b = match m with | { size := size, buckets := buckets } => let x := Std.HashMapImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => let bkt := Array.uget buckets.val i h; if Std.AssocList.contains a bkt = true then ({ size := size, buckets := Std.HashMapBucket.update buckets i (Std.AssocList.replace a b bkt) h }, true) else let size' := size + 1; let buckets' := Std.HashMapBucket.update buckets i (Std.AssocList.cons a b bkt) h; if Std.numBucketsForCapacity size' ≤ Array.size buckets.val then ({ size := size', buckets := buckets' }, false) else (Std.HashMapImp.expand size' buckets', false)
def
Std.HashMapImp.erase
{α : Type u}
{β : Type v}
[inst : BEq α]
[inst : Hashable α]
(m : Std.HashMapImp α β)
(a : α)
:
Std.HashMapImp α β
Equations
- Std.HashMapImp.erase m a = match m with | { size := size, buckets := buckets } => let x := Std.HashMapImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => let bkt := Array.uget buckets.val i h; if Std.AssocList.contains a bkt = true then { size := size - 1, buckets := Std.HashMapBucket.update buckets i (Std.AssocList.erase a bkt) h } else m
inductive
Std.HashMapImp.WellFormed
{α : Type u}
{β : Type v}
[inst : BEq α]
[inst : Hashable α]
:
Std.HashMapImp α β → Prop
- mkWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (n : Nat), Std.HashMapImp.WellFormed (Std.mkHashMapImp n)
- insertWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.HashMapImp α β) (a : α) (b : β), Std.HashMapImp.WellFormed m → Std.HashMapImp.WellFormed (Std.HashMapImp.insert m a b).fst
- eraseWff: ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.HashMapImp α β) (a : α), Std.HashMapImp.WellFormed m → Std.HashMapImp.WellFormed (Std.HashMapImp.erase m a)
noncomputable def
Std.HashMap
(α : Type u)
(β : Type v)
[inst : BEq α]
[inst : Hashable α]
:
Type (max 0 u v)
Equations
- Std.HashMap α β = { m // Std.HashMapImp.WellFormed m }
def
Std.mkHashMap
{α : Type u}
{β : Type v}
[inst : BEq α]
[inst : Hashable α]
(capacity : optParam Nat 0)
:
Std.HashMap α β
Equations
- Std.mkHashMap capacity = { val := Std.mkHashMapImp capacity, property := (_ : Std.HashMapImp.WellFormed (Std.mkHashMapImp capacity)) }
instance
Std.HashMap.instInhabitedHashMap
{α : Type u_1}
{β : Type u_2}
[inst : BEq α]
[inst : Hashable α]
:
Inhabited (Std.HashMap α β)
Equations
- Std.HashMap.instInhabitedHashMap = { default := Std.mkHashMap }
instance
Std.HashMap.instEmptyCollectionHashMap
{α : Type u_1}
{β : Type u_2}
[inst : BEq α]
[inst : Hashable α]
:
EmptyCollection (Std.HashMap α β)
Equations
- Std.HashMap.instEmptyCollectionHashMap = { emptyCollection := Std.mkHashMap }
@[inline]
def
Std.HashMap.empty
{α : Type u_1}
{β : Type u_2}
[inst : BEq α]
[inst : Hashable α]
:
Std.HashMap α β
Equations
- Std.HashMap.empty = Std.mkHashMap
def
Std.HashMap.insert
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → Std.HashMap α β
Equations
- Std.HashMap.insert m a b = match m with | { val := m, property := hw } => match Std.HashMapImp.insert m a b, (_ : Std.HashMapImp.insert m a b = Std.HashMapImp.insert m a b) with | (m', x), h => { val := m', property := (_ : Std.HashMapImp.WellFormed (m', x).fst) }
def
Std.HashMap.insert'
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → Std.HashMap α β × Bool
Equations
- Std.HashMap.insert' m a b = match m with | { val := m, property := hw } => match Std.HashMapImp.insert m a b, (_ : Std.HashMapImp.insert m a b = Std.HashMapImp.insert m a b) with | (m', replaced), h => ({ val := m', property := (_ : Std.HashMapImp.WellFormed (m', replaced).fst) }, replaced)
@[inline]
def
Std.HashMap.erase
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Std.HashMap α β
Equations
- Std.HashMap.erase m a = match m with | { val := m, property := hw } => { val := Std.HashMapImp.erase m a, property := (_ : Std.HashMapImp.WellFormed (Std.HashMapImp.erase m a)) }
@[inline]
def
Std.HashMap.findEntry?
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Option (α × β)
Equations
- Std.HashMap.findEntry? m a = match m with | { val := m, property := x } => Std.HashMapImp.findEntry? m a
@[inline]
def
Std.HashMap.find?
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Option β
Equations
- Std.HashMap.find? m a = match m with | { val := m, property := x } => Std.HashMapImp.find? m a
@[inline]
def
Std.HashMap.findD
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → β
Equations
- Std.HashMap.findD m a b₀ = Option.getD (Std.HashMap.find? m a) b₀
@[inline]
def
Std.HashMap.find!
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Std.HashMap α β → α → β
Equations
- Std.HashMap.find! m a = match Std.HashMap.find? m a with | some b => b | none => panicWithPosWithDecl "Std.Data.HashMap" "Std.HashMap.find!" 177 14 "key is not in the map"
@[inline]
def
Std.HashMap.getOp
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Option β
Equations
- Std.HashMap.getOp self idx = Std.HashMap.find? self idx
@[inline]
def
Std.HashMap.contains
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Bool
Equations
- Std.HashMap.contains m a = match m with | { val := m, property := x } => Std.HashMapImp.contains m a
@[inline]
def
Std.HashMap.foldM
{α : Type u}
{β : Type v}
:
{x : BEq α} →
{x_1 : Hashable α} →
{δ : Type w} → {m : Type w → Type w} → [inst : Monad m] → (δ → α → β → m δ) → δ → Std.HashMap α β → m δ
Equations
- Std.HashMap.foldM f init h = match h with | { val := h, property := x } => Std.HashMapImp.foldM f init h
@[inline]
def
Std.HashMap.fold
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → (δ → α → β → δ) → δ → Std.HashMap α β → δ
Equations
- Std.HashMap.fold f init m = match m with | { val := m, property := x } => Std.HashMapImp.fold f init m
@[inline]
Equations
- Std.HashMap.forM f h = match h with | { val := h, property := x } => Std.HashMapImp.forM f h
@[inline]
def
Std.HashMap.size
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Nat
Equations
- Std.HashMap.size m = match m with | { val := { size := sz, buckets := x }, property := x_1 } => sz
@[inline]
def
Std.HashMap.isEmpty
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Bool
Equations
- Std.HashMap.isEmpty m = decide (Std.HashMap.size m = 0)
def
Std.HashMap.toList
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → List (α × β)
Equations
- Std.HashMap.toList m = Std.HashMap.fold (fun r k v => (k, v) :: r) [] m
def
Std.HashMap.toArray
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Array (α × β)
Equations
- Std.HashMap.toArray m = Std.HashMap.fold (fun r k v => Array.push r (k, v)) #[] m
def
Std.HashMap.numBuckets
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Nat
Equations
- Std.HashMap.numBuckets m = Array.size m.val.buckets.val
def
Std.HashMap.ofList
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → List (α × β) → Std.HashMap α β
Equations
- Std.HashMap.ofList l = List.foldl (fun m p => Std.HashMap.insert m p.fst p.snd) Std.HashMap.empty l
def
Std.HashMap.ofListWith
{α : Type u}
{β : Type v}
:
{x : BEq α} → {x_1 : Hashable α} → List (α × β) → (β → β → β) → Std.HashMap α β
Equations
- Std.HashMap.ofListWith l f = List.foldl (fun m p => match Std.HashMap.find? m p.fst with | none => Std.HashMap.insert m p.fst p.snd | some v => Std.HashMap.insert m p.fst (f v p.snd)) Std.HashMap.empty l