Std.Data.HashMap

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)

source

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

source

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

source

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

source

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

source

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

source

def Std.HashMapImp.findEntry? {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) :

Option (α × β)

Equations

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

source

def Std.HashMapImp.find? {α : Type u} {β : Type v} [beq : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) :

Option β

Equations

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

source

def Std.HashMapImp.contains {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) :

Bool

Equations

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

source

def Std.HashMapImp.moveEntries {α : Type u} {β : Type v} [inst : Hashable α] (i : Nat) (source : Array (Std.AssocList α β)) (target : Std.HashMapBucket α β) :

Std.HashMapBucket α β

Equations

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

source

def Std.HashMapImp.expand {α : Type u} {β : Type v} [inst : Hashable α] (size : Nat) (buckets : Std.HashMapBucket α β) :

Std.HashMapImp α β

Equations

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

source

@[inline]

def Std.HashMapImp.insert {α : Type u} {β : Type v} [beq : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) (b : β) :

Std.HashMapImp α β × Bool

Equations

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

source

def Std.HashMapImp.erase {α : Type u} {β : Type v} [inst : BEq α] [inst : Hashable α] (m : Std.HashMapImp α β) (a : α) :

Std.HashMapImp α β

Equations

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

source

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)

source

def Std.HashMap (α : Type u) (β : Type v) [inst : BEq α] [inst : Hashable α] :

Type (max 0 u v)

source

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)) }

source

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

Inhabited (Std.HashMap α β)

Equations

Std.HashMap.instInhabitedHashMap = { default := Std.mkHashMap }

source

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

EmptyCollection (Std.HashMap α β)

Equations

Std.HashMap.instEmptyCollectionHashMap = { emptyCollection := Std.mkHashMap }

source

@[inline]

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

Std.HashMap α β

Equations

Std.HashMap.empty = Std.mkHashMap

source

def Std.HashMap.insert {α : Type u} {β : Type v} :

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

Equations

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

source

def Std.HashMap.insert' {α : Type u} {β : Type v} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → Std.HashMap α β × Bool

Similar to insert, but also returns a Boolean flad indicating whether an existing entry has been replaced with a -> b.

Equations

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

source

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

source

@[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 := property } => Std.HashMapImp.findEntry? m a

source

@[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 := property } => Std.HashMapImp.find? m a

source

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

source

@[inline]

def Std.HashMap.find! {α : Type u} {β : Type v} :

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

Equations

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

source

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

source

@[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 := property } => Std.HashMapImp.contains m a

source

@[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 := property } => Std.HashMapImp.foldM f init h

source

@[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 := property } => Std.HashMapImp.fold f init m

source

@[inline]

def Std.HashMap.forM {α : Type u} {β : Type v} :

{x : BEq α} → {x_1 : Hashable α} → {m : Type w → Type w} → [inst : Monad m] → (α → β → m PUnit) → Std.HashMap α β → m PUnit

Equations

Std.HashMap.forM f h = match h with | { val := h, property := property } => Std.HashMapImp.forM f h

source

@[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 := buckets }, property := property } => sz

source

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

source

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

source

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

source

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

source

def Std.HashMap.ofList {α : Type u} {β : Type v} :

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

Builds a HashMap from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences.

Equations

Std.HashMap.ofList l = List.foldl (fun m p => Std.HashMap.insert m p.fst p.snd) Std.HashMap.empty l

source

def Std.HashMap.ofListWith {α : Type u} {β : Type v} :

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

Variant of ofList which accepts a function that combines values of duplicated keys.

Equations

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