fix: resolve instances for HashMap via unification (#4759)
This commit is contained in:
Markus Himmel
GitHub
parent
ba3565f441
commit
c1df7564ce
7 changed files with 157 additions and 84 deletions
|
|
@ -30,6 +30,8 @@ universe u v w
|
|||
|
||||
variable {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w} [Monad m]
|
||||
|
||||
variable {_ : BEq α} {_ : Hashable α}
|
||||
|
||||
namespace Std
|
||||
|
||||
open DHashMap.Internal DHashMap.Internal.List
|
||||
|
|
@ -66,34 +68,34 @@ instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where
|
|||
instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where
|
||||
default := ∅
|
||||
|
||||
@[inline, inherit_doc Raw.insert] def insert [BEq α] [Hashable α] (m : DHashMap α β) (a : α)
|
||||
@[inline, inherit_doc Raw.insert] def insert (m : DHashMap α β) (a : α)
|
||||
(b : β a) : DHashMap α β :=
|
||||
⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩
|
||||
|
||||
@[inline, inherit_doc Raw.insertIfNew] def insertIfNew [BEq α] [Hashable α] (m : DHashMap α β)
|
||||
@[inline, inherit_doc Raw.insertIfNew] def insertIfNew (m : DHashMap α β)
|
||||
(a : α) (b : β a) : DHashMap α β :=
|
||||
⟨Raw₀.insertIfNew ⟨m.1, m.2.size_buckets_pos⟩ a b, .insertIfNew₀ m.2⟩
|
||||
|
||||
@[inline, inherit_doc Raw.containsThenInsert] def containsThenInsert [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.containsThenInsert] def containsThenInsert
|
||||
(m : DHashMap α β) (a : α) (b : β a) : Bool × DHashMap α β :=
|
||||
let m' := Raw₀.containsThenInsert ⟨m.1, m.2.size_buckets_pos⟩ a b
|
||||
⟨m'.1, ⟨m'.2.1, .containsThenInsert₀ m.2⟩⟩
|
||||
|
||||
@[inline, inherit_doc Raw.containsThenInsertIfNew] def containsThenInsertIfNew [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.containsThenInsertIfNew] def containsThenInsertIfNew
|
||||
(m : DHashMap α β) (a : α) (b : β a) : Bool × DHashMap α β :=
|
||||
let m' := Raw₀.containsThenInsertIfNew ⟨m.1, m.2.size_buckets_pos⟩ a b
|
||||
⟨m'.1, ⟨m'.2.1, .containsThenInsertIfNew₀ m.2⟩⟩
|
||||
|
||||
@[inline, inherit_doc Raw.getThenInsertIfNew?] def getThenInsertIfNew? [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.getThenInsertIfNew?] def getThenInsertIfNew?
|
||||
[LawfulBEq α] (m : DHashMap α β) (a : α) (b : β a) : Option (β a) × DHashMap α β :=
|
||||
let m' := Raw₀.getThenInsertIfNew? ⟨m.1, m.2.size_buckets_pos⟩ a b
|
||||
⟨m'.1, ⟨m'.2.1, .getThenInsertIfNew?₀ m.2⟩⟩
|
||||
|
||||
@[inline, inherit_doc Raw.get?] def get? [BEq α] [LawfulBEq α] [Hashable α] (m : DHashMap α β)
|
||||
@[inline, inherit_doc Raw.get?] def get? [LawfulBEq α] (m : DHashMap α β)
|
||||
(a : α) : Option (β a) :=
|
||||
Raw₀.get? ⟨m.1, m.2.size_buckets_pos⟩ a
|
||||
|
||||
@[inline, inherit_doc Raw.contains] def contains [BEq α] [Hashable α] (m : DHashMap α β) (a : α) :
|
||||
@[inline, inherit_doc Raw.contains] def contains (m : DHashMap α β) (a : α) :
|
||||
Bool :=
|
||||
Raw₀.contains ⟨m.1, m.2.size_buckets_pos⟩ a
|
||||
|
||||
|
|
@ -103,19 +105,19 @@ instance [BEq α] [Hashable α] : Membership α (DHashMap α β) where
|
|||
instance [BEq α] [Hashable α] {m : DHashMap α β} {a : α} : Decidable (a ∈ m) :=
|
||||
show Decidable (m.contains a) from inferInstance
|
||||
|
||||
@[inline, inherit_doc Raw.get] def get [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β) (a : α)
|
||||
@[inline, inherit_doc Raw.get] def get [LawfulBEq α] (m : DHashMap α β) (a : α)
|
||||
(h : a ∈ m) : β a :=
|
||||
Raw₀.get ⟨m.1, m.2.size_buckets_pos⟩ a h
|
||||
|
||||
@[inline, inherit_doc Raw.get!] def get! [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β)
|
||||
@[inline, inherit_doc Raw.get!] def get! [LawfulBEq α] (m : DHashMap α β)
|
||||
(a : α) [Inhabited (β a)] : β a :=
|
||||
Raw₀.get! ⟨m.1, m.2.size_buckets_pos⟩ a
|
||||
|
||||
@[inline, inherit_doc Raw.getD] def getD [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β)
|
||||
@[inline, inherit_doc Raw.getD] def getD [LawfulBEq α] (m : DHashMap α β)
|
||||
(a : α) (fallback : β a) : β a :=
|
||||
Raw₀.getD ⟨m.1, m.2.size_buckets_pos⟩ a fallback
|
||||
|
||||
@[inline, inherit_doc Raw.erase] def erase [BEq α] [Hashable α] (m : DHashMap α β) (a : α) :
|
||||
@[inline, inherit_doc Raw.erase] def erase (m : DHashMap α β) (a : α) :
|
||||
DHashMap α β :=
|
||||
⟨Raw₀.erase ⟨m.1, m.2.size_buckets_pos⟩ a, .erase₀ m.2⟩
|
||||
|
||||
|
|
@ -123,57 +125,57 @@ section
|
|||
|
||||
variable {β : Type v}
|
||||
|
||||
@[inline, inherit_doc Raw.Const.get?] def Const.get? [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.Const.get?] def Const.get?
|
||||
(m : DHashMap α (fun _ => β)) (a : α) : Option β :=
|
||||
Raw₀.Const.get? ⟨m.1, m.2.size_buckets_pos⟩ a
|
||||
|
||||
@[inline, inherit_doc Raw.Const.get] def Const.get [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.Const.get] def Const.get
|
||||
(m : DHashMap α (fun _ => β)) (a : α) (h : a ∈ m) : β :=
|
||||
Raw₀.Const.get ⟨m.1, m.2.size_buckets_pos⟩ a h
|
||||
|
||||
@[inline, inherit_doc Raw.Const.getD] def Const.getD [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.Const.getD] def Const.getD
|
||||
(m : DHashMap α (fun _ => β)) (a : α) (fallback : β) : β :=
|
||||
Raw₀.Const.getD ⟨m.1, m.2.size_buckets_pos⟩ a fallback
|
||||
|
||||
@[inline, inherit_doc Raw.Const.get!] def Const.get! [BEq α] [Hashable α] [Inhabited β]
|
||||
@[inline, inherit_doc Raw.Const.get!] def Const.get! [Inhabited β]
|
||||
(m : DHashMap α (fun _ => β)) (a : α) : β :=
|
||||
Raw₀.Const.get! ⟨m.1, m.2.size_buckets_pos⟩ a
|
||||
|
||||
@[inline, inherit_doc Raw.Const.getThenInsertIfNew?] def Const.getThenInsertIfNew? [BEq α]
|
||||
[Hashable α] (m : DHashMap α (fun _ => β)) (a : α) (b : β) :
|
||||
@[inline, inherit_doc Raw.Const.getThenInsertIfNew?] def Const.getThenInsertIfNew?
|
||||
(m : DHashMap α (fun _ => β)) (a : α) (b : β) :
|
||||
Option β × DHashMap α (fun _ => β) :=
|
||||
let m' := Raw₀.Const.getThenInsertIfNew? ⟨m.1, m.2.size_buckets_pos⟩ a b
|
||||
⟨m'.1, ⟨m'.2.1, .constGetThenInsertIfNew?₀ m.2⟩⟩
|
||||
|
||||
end
|
||||
|
||||
@[inline, inherit_doc Raw.size] def size [BEq α] [Hashable α] (m : DHashMap α β) : Nat :=
|
||||
@[inline, inherit_doc Raw.size] def size (m : DHashMap α β) : Nat :=
|
||||
m.1.size
|
||||
|
||||
@[inline, inherit_doc Raw.isEmpty] def isEmpty [BEq α] [Hashable α] (m : DHashMap α β) : Bool :=
|
||||
@[inline, inherit_doc Raw.isEmpty] def isEmpty (m : DHashMap α β) : Bool :=
|
||||
m.1.isEmpty
|
||||
|
||||
section Unverified
|
||||
|
||||
/-! We currently do not provide lemmas for the functions below. -/
|
||||
|
||||
@[inline, inherit_doc Raw.filter] def filter [BEq α] [Hashable α] (f : (a : α) → β a → Bool)
|
||||
@[inline, inherit_doc Raw.filter] def filter (f : (a : α) → β a → Bool)
|
||||
(m : DHashMap α β) : DHashMap α β :=
|
||||
⟨Raw₀.filter f ⟨m.1, m.2.size_buckets_pos⟩, .filter₀ m.2⟩
|
||||
|
||||
@[inline, inherit_doc Raw.foldM] def foldM [BEq α] [Hashable α] (f : δ → (a : α) → β a → m δ)
|
||||
@[inline, inherit_doc Raw.foldM] def foldM (f : δ → (a : α) → β a → m δ)
|
||||
(init : δ) (b : DHashMap α β) : m δ :=
|
||||
b.1.foldM f init
|
||||
|
||||
@[inline, inherit_doc Raw.fold] def fold [BEq α] [Hashable α] (f : δ → (a : α) → β a → δ)
|
||||
@[inline, inherit_doc Raw.fold] def fold (f : δ → (a : α) → β a → δ)
|
||||
(init : δ) (b : DHashMap α β) : δ :=
|
||||
b.1.fold f init
|
||||
|
||||
@[inline, inherit_doc Raw.forM] def forM [BEq α] [Hashable α] (f : (a : α) → β a → m PUnit)
|
||||
@[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
|
||||
(b : DHashMap α β) : m PUnit :=
|
||||
b.1.forM f
|
||||
|
||||
@[inline, inherit_doc Raw.forIn] def forIn [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.forIn] def forIn
|
||||
(f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : DHashMap α β) : m δ :=
|
||||
b.1.forIn f init
|
||||
|
||||
|
|
@ -183,49 +185,49 @@ instance [BEq α] [Hashable α] : ForM m (DHashMap α β) ((a : α) × β a) whe
|
|||
instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) where
|
||||
forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
|
||||
|
||||
@[inline, inherit_doc Raw.toList] def toList [BEq α] [Hashable α] (m : DHashMap α β) :
|
||||
@[inline, inherit_doc Raw.toList] def toList (m : DHashMap α β) :
|
||||
List ((a : α) × β a) :=
|
||||
m.1.toList
|
||||
|
||||
@[inline, inherit_doc Raw.toArray] def toArray [BEq α] [Hashable α] (m : DHashMap α β) :
|
||||
@[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
|
||||
Array ((a : α) × β a) :=
|
||||
m.1.toArray
|
||||
|
||||
@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v} [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v}
|
||||
(m : DHashMap α (fun _ => β)) : List (α × β) :=
|
||||
Raw.Const.toList m.1
|
||||
|
||||
@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v} [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
|
||||
(m : DHashMap α (fun _ => β)) : Array (α × β) :=
|
||||
Raw.Const.toArray m.1
|
||||
|
||||
@[inline, inherit_doc Raw.keys] def keys [BEq α] [Hashable α] (m : DHashMap α β) : List α :=
|
||||
@[inline, inherit_doc Raw.keys] def keys (m : DHashMap α β) : List α :=
|
||||
m.1.keys
|
||||
|
||||
@[inline, inherit_doc Raw.keysArray] def keysArray [BEq α] [Hashable α] (m : DHashMap α β) :
|
||||
@[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
|
||||
Array α :=
|
||||
m.1.keysArray
|
||||
|
||||
@[inline, inherit_doc Raw.values] def values {β : Type v} [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.values] def values {β : Type v}
|
||||
(m : DHashMap α (fun _ => β)) : List β :=
|
||||
m.1.values
|
||||
|
||||
@[inline, inherit_doc Raw.valuesArray] def valuesArray {β : Type v} [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.valuesArray] def valuesArray {β : Type v}
|
||||
(m : DHashMap α (fun _ => β)) : Array β :=
|
||||
m.1.valuesArray
|
||||
|
||||
@[inline, inherit_doc Raw.insertMany] def insertMany [BEq α] [Hashable α] {ρ : Type w}
|
||||
@[inline, inherit_doc Raw.insertMany] def insertMany {ρ : Type w}
|
||||
[ForIn Id ρ ((a : α) × β a)] (m : DHashMap α β) (l : ρ) : DHashMap α β :=
|
||||
⟨(Raw₀.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).1,
|
||||
(Raw₀.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insert₀ m.2⟩
|
||||
|
||||
@[inline, inherit_doc Raw.Const.insertMany] def Const.insertMany {β : Type v} [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.Const.insertMany] def Const.insertMany {β : Type v}
|
||||
{ρ : Type w} [ForIn Id ρ (α × β)] (m : DHashMap α (fun _ => β)) (l : ρ) :
|
||||
DHashMap α (fun _ => β) :=
|
||||
⟨(Raw₀.Const.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).1,
|
||||
(Raw₀.Const.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insert₀ m.2⟩
|
||||
|
||||
@[inline, inherit_doc Raw.Const.insertManyUnit] def Const.insertManyUnit [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc Raw.Const.insertManyUnit] def Const.insertManyUnit
|
||||
{ρ : Type w} [ForIn Id ρ α] (m : DHashMap α (fun _ => Unit)) (l : ρ) :
|
||||
DHashMap α (fun _ => Unit) :=
|
||||
⟨(Raw₀.Const.insertManyUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1,
|
||||
|
|
@ -243,7 +245,7 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
|
|||
DHashMap α (fun _ => Unit) :=
|
||||
Const.insertManyUnit ∅ l
|
||||
|
||||
@[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets [BEq α] [Hashable α]
|
||||
@[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
|
||||
(m : DHashMap α β) : Nat :=
|
||||
Raw.Internal.numBuckets m.1
|
||||
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ set_option autoImplicit false
|
|||
|
||||
universe u v
|
||||
|
||||
variable {α : Type u} {β : α → Type v} [BEq α] [Hashable α]
|
||||
variable {α : Type u} {β : α → Type v} {_ : BEq α} {_ : Hashable α}
|
||||
|
||||
namespace Std.DHashMap
|
||||
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ nested inductive types.
|
|||
|
||||
universe u v w
|
||||
|
||||
variable {α : Type u} {β : Type v}
|
||||
variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
|
||||
|
||||
namespace Std
|
||||
|
||||
|
|
@ -69,21 +69,21 @@ instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where
|
|||
instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
|
||||
default := ∅
|
||||
|
||||
@[inline, inherit_doc DHashMap.insert] def insert [BEq α] [Hashable α] (m : HashMap α β) (a : α)
|
||||
@[inline, inherit_doc DHashMap.insert] def insert (m : HashMap α β) (a : α)
|
||||
(b : β) : HashMap α β :=
|
||||
⟨m.inner.insert a b⟩
|
||||
|
||||
@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew [BEq α] [Hashable α] (m : HashMap α β)
|
||||
@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew (m : HashMap α β)
|
||||
(a : α) (b : β) : HashMap α β :=
|
||||
⟨m.inner.insertIfNew a b⟩
|
||||
|
||||
@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert
|
||||
(m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
|
||||
let ⟨replaced, r⟩ := m.inner.containsThenInsert a b
|
||||
⟨replaced, ⟨r⟩⟩
|
||||
|
||||
@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew [BEq α]
|
||||
[Hashable α] (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
|
||||
@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew
|
||||
(m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
|
||||
let ⟨replaced, r⟩ := m.inner.containsThenInsertIfNew a b
|
||||
⟨replaced, ⟨r⟩⟩
|
||||
|
||||
|
|
@ -96,7 +96,7 @@ returned map has a new value inserted.
|
|||
|
||||
Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.
|
||||
-/
|
||||
@[inline] def getThenInsertIfNew? [BEq α] [Hashable α] (m : HashMap α β) (a : α) (b : β) :
|
||||
@[inline] def getThenInsertIfNew? (m : HashMap α β) (a : α) (b : β) :
|
||||
Option β × HashMap α β :=
|
||||
let ⟨previous, r⟩ := DHashMap.Const.getThenInsertIfNew? m.inner a b
|
||||
⟨previous, ⟨r⟩⟩
|
||||
|
|
@ -106,10 +106,10 @@ The notation `m[a]?` is preferred over calling this function directly.
|
|||
|
||||
Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
|
||||
-/
|
||||
@[inline] def get? [BEq α] [Hashable α] (m : HashMap α β) (a : α) : Option β :=
|
||||
@[inline] def get? (m : HashMap α β) (a : α) : Option β :=
|
||||
DHashMap.Const.get? m.inner a
|
||||
|
||||
@[inline, inherit_doc DHashMap.contains] def contains [BEq α] [Hashable α] (m : HashMap α β)
|
||||
@[inline, inherit_doc DHashMap.contains] def contains (m : HashMap α β)
|
||||
(a : α) : Bool :=
|
||||
m.inner.contains a
|
||||
|
||||
|
|
@ -125,10 +125,10 @@ The notation `m[a]` or `m[a]'h` is preferred over calling this function directly
|
|||
Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
|
||||
`a ∈ m`.
|
||||
-/
|
||||
@[inline] def get [BEq α] [Hashable α] (m : HashMap α β) (a : α) (h : a ∈ m) : β :=
|
||||
@[inline] def get (m : HashMap α β) (a : α) (h : a ∈ m) : β :=
|
||||
DHashMap.Const.get m.inner a h
|
||||
|
||||
@[inline, inherit_doc DHashMap.Const.getD] def getD [BEq α] [Hashable α] (m : HashMap α β) (a : α)
|
||||
@[inline, inherit_doc DHashMap.Const.getD] def getD (m : HashMap α β) (a : α)
|
||||
(fallback : β) : β :=
|
||||
DHashMap.Const.getD m.inner a fallback
|
||||
|
||||
|
|
@ -137,7 +137,7 @@ The notation `m[a]!` is preferred over calling this function directly.
|
|||
|
||||
Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
|
||||
-/
|
||||
@[inline] def get! [BEq α] [Hashable α] [Inhabited β] (m : HashMap α β) (a : α) : β :=
|
||||
@[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β :=
|
||||
DHashMap.Const.get! m.inner a
|
||||
|
||||
instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a ∈ m) where
|
||||
|
|
@ -145,37 +145,37 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a
|
|||
getElem? m a := m.get? a
|
||||
getElem! m a := m.get! a
|
||||
|
||||
@[inline, inherit_doc DHashMap.erase] def erase [BEq α] [Hashable α] (m : HashMap α β) (a : α) :
|
||||
@[inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) :
|
||||
HashMap α β :=
|
||||
⟨m.inner.erase a⟩
|
||||
|
||||
@[inline, inherit_doc DHashMap.size] def size [BEq α] [Hashable α] (m : HashMap α β) : Nat :=
|
||||
@[inline, inherit_doc DHashMap.size] def size (m : HashMap α β) : Nat :=
|
||||
m.inner.size
|
||||
|
||||
@[inline, inherit_doc DHashMap.isEmpty] def isEmpty [BEq α] [Hashable α] (m : HashMap α β) : Bool :=
|
||||
@[inline, inherit_doc DHashMap.isEmpty] def isEmpty (m : HashMap α β) : Bool :=
|
||||
m.inner.isEmpty
|
||||
|
||||
section Unverified
|
||||
|
||||
/-! We currently do not provide lemmas for the functions below. -/
|
||||
|
||||
@[inline, inherit_doc DHashMap.filter] def filter [BEq α] [Hashable α] (f : α → β → Bool)
|
||||
@[inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool)
|
||||
(m : HashMap α β) : HashMap α β :=
|
||||
⟨m.inner.filter f⟩
|
||||
|
||||
@[inline, inherit_doc DHashMap.foldM] def foldM [BEq α] [Hashable α] {m : Type w → Type w}
|
||||
@[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
|
||||
[Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
|
||||
b.inner.foldM f init
|
||||
|
||||
@[inline, inherit_doc DHashMap.fold] def fold [BEq α] [Hashable α] {γ : Type w}
|
||||
@[inline, inherit_doc DHashMap.fold] def fold {γ : Type w}
|
||||
(f : γ → α → β → γ) (init : γ) (b : HashMap α β) : γ :=
|
||||
b.inner.fold f init
|
||||
|
||||
@[inline, inherit_doc DHashMap.forM] def forM [BEq α] [Hashable α] {m : Type w → Type w} [Monad m]
|
||||
@[inline, inherit_doc DHashMap.forM] def forM {m : Type w → Type w} [Monad m]
|
||||
(f : (a : α) → β → m PUnit) (b : HashMap α β) : m PUnit :=
|
||||
b.inner.forM f
|
||||
|
||||
@[inline, inherit_doc DHashMap.forIn] def forIn [BEq α] [Hashable α] {m : Type w → Type w} [Monad m]
|
||||
@[inline, inherit_doc DHashMap.forIn] def forIn {m : Type w → Type w} [Monad m]
|
||||
{γ : Type w} (f : (a : α) → β → γ → m (ForInStep γ)) (init : γ) (b : HashMap α β) : m γ :=
|
||||
b.inner.forIn f init
|
||||
|
||||
|
|
@ -185,33 +185,33 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForM m (HashMap α β)
|
|||
instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β) (α × β) where
|
||||
forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
|
||||
|
||||
@[inline, inherit_doc DHashMap.Const.toList] def toList [BEq α] [Hashable α] (m : HashMap α β) :
|
||||
@[inline, inherit_doc DHashMap.Const.toList] def toList (m : HashMap α β) :
|
||||
List (α × β) :=
|
||||
DHashMap.Const.toList m.inner
|
||||
|
||||
@[inline, inherit_doc DHashMap.Const.toArray] def toArray [BEq α] [Hashable α] (m : HashMap α β) :
|
||||
@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
|
||||
Array (α × β) :=
|
||||
DHashMap.Const.toArray m.inner
|
||||
|
||||
@[inline, inherit_doc DHashMap.keys] def keys [BEq α] [Hashable α] (m : HashMap α β) : List α :=
|
||||
@[inline, inherit_doc DHashMap.keys] def keys (m : HashMap α β) : List α :=
|
||||
m.inner.keys
|
||||
|
||||
@[inline, inherit_doc DHashMap.keysArray] def keysArray [BEq α] [Hashable α] (m : HashMap α β) :
|
||||
@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
|
||||
Array α :=
|
||||
m.inner.keysArray
|
||||
|
||||
@[inline, inherit_doc DHashMap.values] def values [BEq α] [Hashable α] (m : HashMap α β) : List β :=
|
||||
@[inline, inherit_doc DHashMap.values] def values (m : HashMap α β) : List β :=
|
||||
m.inner.values
|
||||
|
||||
@[inline, inherit_doc DHashMap.valuesArray] def valuesArray [BEq α] [Hashable α] (m : HashMap α β) :
|
||||
@[inline, inherit_doc DHashMap.valuesArray] def valuesArray (m : HashMap α β) :
|
||||
Array β :=
|
||||
m.inner.valuesArray
|
||||
|
||||
@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany [BEq α] [Hashable α] {ρ : Type w}
|
||||
@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany {ρ : Type w}
|
||||
[ForIn Id ρ (α × β)] (m : HashMap α β) (l : ρ) : HashMap α β :=
|
||||
⟨DHashMap.Const.insertMany m.inner l⟩
|
||||
|
||||
@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit
|
||||
{ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit :=
|
||||
⟨DHashMap.Const.insertManyUnit m.inner l⟩
|
||||
|
||||
|
|
@ -223,7 +223,7 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
|
|||
HashMap α Unit :=
|
||||
⟨DHashMap.Const.unitOfList l⟩
|
||||
|
||||
@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets [BEq α] [Hashable α]
|
||||
@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
|
||||
(m : HashMap α β) : Nat :=
|
||||
DHashMap.Internal.numBuckets m.inner
|
||||
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ set_option autoImplicit false
|
|||
|
||||
universe u v
|
||||
|
||||
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
|
||||
variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
|
||||
|
||||
namespace Std.HashMap
|
||||
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ set_option autoImplicit false
|
|||
|
||||
universe u v
|
||||
|
||||
variable {α : Type u}
|
||||
variable {α : Type u} {_ : BEq α} {_ : Hashable α}
|
||||
|
||||
namespace Std
|
||||
|
||||
|
|
@ -71,7 +71,7 @@ instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
|
|||
Inserts the given element into the set. If the hash set already contains an element that is
|
||||
equal (with regard to `==`) to the given element, then the hash set is returned unchanged.
|
||||
-/
|
||||
@[inline] def insert [BEq α] [Hashable α] (m : HashSet α) (a : α) : HashSet α :=
|
||||
@[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
|
||||
⟨m.inner.insertIfNew a ()⟩
|
||||
|
||||
/--
|
||||
|
|
@ -81,7 +81,7 @@ element, then the hash set is returned unchanged.
|
|||
|
||||
Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
|
||||
-/
|
||||
@[inline] def containsThenInsert [BEq α] [Hashable α] (m : HashSet α) (a : α) : Bool × HashSet α :=
|
||||
@[inline] def containsThenInsert (m : HashSet α) (a : α) : Bool × HashSet α :=
|
||||
let ⟨replaced, r⟩ := m.inner.containsThenInsertIfNew a ()
|
||||
⟨replaced, ⟨r⟩⟩
|
||||
|
||||
|
|
@ -92,7 +92,7 @@ this: `a ∈ m` is equivalent to `m.contains a = true`.
|
|||
Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` use
|
||||
`==` for comparisons, while for hash sets, both use `==`.
|
||||
-/
|
||||
@[inline] def contains [BEq α] [Hashable α] (m : HashSet α) (a : α) : Bool :=
|
||||
@[inline] def contains (m : HashSet α) (a : α) : Bool :=
|
||||
m.inner.contains a
|
||||
|
||||
instance [BEq α] [Hashable α] : Membership α (HashSet α) where
|
||||
|
|
@ -102,11 +102,11 @@ instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m)
|
|||
inferInstanceAs (Decidable (a ∈ m.inner))
|
||||
|
||||
/-- Removes the element if it exists. -/
|
||||
@[inline] def erase [BEq α] [Hashable α] (m : HashSet α) (a : α) : HashSet α :=
|
||||
@[inline] def erase (m : HashSet α) (a : α) : HashSet α :=
|
||||
⟨m.inner.erase a⟩
|
||||
|
||||
/-- The number of elements present in the set -/
|
||||
@[inline] def size [BEq α] [Hashable α] (m : HashSet α) : Nat :=
|
||||
@[inline] def size (m : HashSet α) : Nat :=
|
||||
m.inner.size
|
||||
|
||||
/--
|
||||
|
|
@ -116,7 +116,7 @@ Note that if your `BEq` instance is not reflexive or your `Hashable` instance is
|
|||
lawful, then it is possible that this function returns `false` even though `m.contains a = false`
|
||||
for all `a`.
|
||||
-/
|
||||
@[inline] def isEmpty [BEq α] [Hashable α] (m : HashSet α) : Bool :=
|
||||
@[inline] def isEmpty (m : HashSet α) : Bool :=
|
||||
m.inner.isEmpty
|
||||
|
||||
section Unverified
|
||||
|
|
@ -124,29 +124,29 @@ section Unverified
|
|||
/-! We currently do not provide lemmas for the functions below. -/
|
||||
|
||||
/-- Removes all elements from the hash set for which the given function returns `false`. -/
|
||||
@[inline] def filter [BEq α] [Hashable α] (f : α → Bool) (m : HashSet α) : HashSet α :=
|
||||
@[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α :=
|
||||
⟨m.inner.filter fun a _ => f a⟩
|
||||
|
||||
/--
|
||||
Monadically computes a value by folding the given function over the elements in the hash set in some
|
||||
order.
|
||||
-/
|
||||
@[inline] def foldM [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] {β : Type v}
|
||||
@[inline] def foldM {m : Type v → Type v} [Monad m] {β : Type v}
|
||||
(f : β → α → m β) (init : β) (b : HashSet α) : m β :=
|
||||
b.inner.foldM (fun b a _ => f b a) init
|
||||
|
||||
/-- Folds the given function over the elements of the hash set in some order. -/
|
||||
@[inline] def fold [BEq α] [Hashable α] {β : Type v} (f : β → α → β) (init : β) (m : HashSet α) :
|
||||
@[inline] def fold {β : Type v} (f : β → α → β) (init : β) (m : HashSet α) :
|
||||
β :=
|
||||
m.inner.fold (fun b a _ => f b a) init
|
||||
|
||||
/-- Carries out a monadic action on each element in the hash set in some order. -/
|
||||
@[inline] def forM [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] (f : α → m PUnit)
|
||||
@[inline] def forM {m : Type v → Type v} [Monad m] (f : α → m PUnit)
|
||||
(b : HashSet α) : m PUnit :=
|
||||
b.inner.forM (fun a _ => f a)
|
||||
|
||||
/-- Support for the `for` loop construct in `do` blocks. -/
|
||||
@[inline] def forIn [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] {β : Type v}
|
||||
@[inline] def forIn {m : Type v → Type v} [Monad m] {β : Type v}
|
||||
(f : α → β → m (ForInStep β)) (init : β) (b : HashSet α) : m β :=
|
||||
b.inner.forIn (fun a _ acc => f a acc) init
|
||||
|
||||
|
|
@ -157,11 +157,11 @@ instance [BEq α] [Hashable α] {m : Type v → Type v} : ForIn m (HashSet α)
|
|||
forIn m init f := m.forIn f init
|
||||
|
||||
/-- Transforms the hash set into a list of elements in some order. -/
|
||||
@[inline] def toList [BEq α] [Hashable α] (m : HashSet α) : List α :=
|
||||
@[inline] def toList (m : HashSet α) : List α :=
|
||||
m.inner.keys
|
||||
|
||||
/-- Transforms the hash set into an array of elements in some order. -/
|
||||
@[inline] def toArray [BEq α] [Hashable α] (m : HashSet α) : Array α :=
|
||||
@[inline] def toArray (m : HashSet α) : Array α :=
|
||||
m.inner.keysArray
|
||||
|
||||
/--
|
||||
|
|
@ -169,7 +169,7 @@ Inserts multiple elements into the hash set. Note that unlike repeatedly calling
|
|||
collection contains multiple elements that are equal (with regard to `==`), then the last element
|
||||
in the collection will be present in the returned hash set.
|
||||
-/
|
||||
@[inline] def insertMany [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) :
|
||||
@[inline] def insertMany {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) :
|
||||
HashSet α :=
|
||||
⟨m.inner.insertManyUnit l⟩
|
||||
|
||||
|
|
@ -186,7 +186,7 @@ Returns the number of buckets in the internal representation of the hash set. Th
|
|||
be useful for things like monitoring system health, but it should be considered an internal
|
||||
implementation detail.
|
||||
-/
|
||||
def Internal.numBuckets [BEq α] [Hashable α] (m : HashSet α) : Nat :=
|
||||
def Internal.numBuckets (m : HashSet α) : Nat :=
|
||||
HashMap.Internal.numBuckets m.inner
|
||||
|
||||
instance [BEq α] [Hashable α] [Repr α] : Repr (HashSet α) where
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ set_option autoImplicit false
|
|||
|
||||
universe u v
|
||||
|
||||
variable {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
|
||||
variable {α : Type u} {_ : BEq α} {_ : Hashable α} [EquivBEq α] [LawfulHashable α]
|
||||
|
||||
namespace Std.HashSet
|
||||
|
||||
|
|
|
|||
71
tests/lean/run/hashmap-implicits.lean
Normal file
71
tests/lean/run/hashmap-implicits.lean
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
import Std.Data.HashMap
|
||||
import Std.Data.HashSet
|
||||
import Std.Data.DHashMap
|
||||
|
||||
open Std (DHashMap HashMap HashSet)
|
||||
|
||||
/-! (Non-exhaustive) tests that `BEq` and `Hashable` arguments to query operations and lemmas are
|
||||
correctly solved by unification. -/
|
||||
|
||||
namespace DHashMap
|
||||
|
||||
structure A (α) extends BEq α, Hashable α where
|
||||
foo : DHashMap α (fun _ => Nat)
|
||||
|
||||
def A.add (xs : A α) (x : α) : A α :=
|
||||
{xs with foo := xs.foo.insert x 5}
|
||||
|
||||
example (xs : A α) (x : α) : ¬x ∈ @DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5 :=
|
||||
DHashMap.not_mem_empty
|
||||
|
||||
example (xs : A α) (x : α) : (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5).contains x = false := by
|
||||
rw [DHashMap.contains_empty]
|
||||
|
||||
example (xs : A α) (x : α) : DHashMap.Const.get? (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5) x = none := by
|
||||
rw [DHashMap.Const.get?_empty]
|
||||
|
||||
example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size :=
|
||||
DHashMap.size_le_size_insert
|
||||
|
||||
end DHashMap
|
||||
|
||||
namespace HashMap
|
||||
|
||||
structure A (α) extends BEq α, Hashable α where
|
||||
foo : HashMap α Nat
|
||||
|
||||
def A.add (xs : A α) (x : α) : A α :=
|
||||
{xs with foo := xs.foo.insert x 5}
|
||||
|
||||
example (xs : A α) (x : α) : ¬x ∈ @HashMap.empty _ Nat xs.toBEq xs.toHashable 5 :=
|
||||
HashMap.not_mem_empty
|
||||
|
||||
example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5).contains x = false := by
|
||||
rw [HashMap.contains_empty]
|
||||
|
||||
example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5)[x]? = none := by
|
||||
rw [HashMap.getElem?_empty]
|
||||
|
||||
example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size :=
|
||||
HashMap.size_le_size_insert
|
||||
|
||||
end HashMap
|
||||
|
||||
namespace HashSet
|
||||
|
||||
structure A (α) extends BEq α, Hashable α where
|
||||
foo : HashSet α
|
||||
|
||||
def A.add (xs : A α) (x : α) : A α :=
|
||||
{xs with foo := xs.foo.insert x}
|
||||
|
||||
example (xs : A α) (x : α) : ¬x ∈ @HashSet.empty _ xs.toBEq xs.toHashable 5 :=
|
||||
DHashMap.not_mem_empty
|
||||
|
||||
example (xs : A α) (x : α) : (@HashSet.empty _ xs.toBEq xs.toHashable 5).contains x = false := by
|
||||
rw [HashSet.contains_empty]
|
||||
|
||||
example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x).size :=
|
||||
HashSet.size_le_size_insert
|
||||
|
||||
end HashSet
|
||||
Loading…
Add table
Reference in a new issue