diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 9f9b26ef73..8ddbfd8021 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -291,11 +291,11 @@ but will later become a primitive operation. ⟨(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 +@[inline, inherit_doc Raw.Const.insertManyIfNewUnit] def Const.insertManyIfNewUnit {ρ : Type w} [ForIn Id ρ α] (m : DHashMap α (fun _ => Unit)) (l : ρ) : DHashMap α (fun _ => Unit) := - ⟨(Raw₀.Const.insertManyUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1, - (Raw₀.Const.insertManyUnit ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insert₀ m.2⟩ + ⟨(Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1, + (Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insertIfNew₀ m.2⟩ @[inline, inherit_doc Raw.ofList] def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) : DHashMap α β := @@ -313,11 +313,11 @@ instance [BEq α] [Hashable α] : Union (DHashMap α β) := ⟨union⟩ @[inline, inherit_doc Raw.Const.unitOfList] def Const.unitOfList [BEq α] [Hashable α] (l : List α) : DHashMap α (fun _ => Unit) := - Const.insertManyUnit ∅ l + Const.insertManyIfNewUnit ∅ l @[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) : DHashMap α (fun _ => Unit) := - Const.insertManyUnit ∅ l + Const.insertManyIfNewUnit ∅ l @[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets (m : DHashMap α β) : Nat := diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index 85bda512af..e4a03ce53e 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean @@ -407,14 +407,14 @@ variable {β : Type v} return r /-- Internal implementation detail of the hash map -/ -@[inline] def Const.insertManyUnit {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α] +@[inline] def Const.insertManyIfNewUnit {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α] (m : Raw₀ α (fun _ => Unit)) (l : ρ) : { m' : Raw₀ α (fun _ => Unit) // ∀ (P : Raw₀ α (fun _ => Unit) → Prop), - (∀ {m'' a b}, P m'' → P (m''.insert a b)) → P m → P m' } := Id.run do + (∀ {m'' a b}, P m'' → P (m''.insertIfNew a b)) → P m → P m' } := Id.run do let mut r : { m' : Raw₀ α (fun _ => Unit) // ∀ (P : Raw₀ α (fun _ => Unit) → Prop), - (∀ {m'' a b}, P m'' → P (m''.insert a b)) → P m → P m' } := ⟨m, fun _ _ => id⟩ + (∀ {m'' a b}, P m'' → P (m''.insertIfNew a b)) → P m → P m' } := ⟨m, fun _ _ => id⟩ for a in l do - r := ⟨r.1.insert a (), fun _ h hm => h (r.2 _ h hm)⟩ + r := ⟨r.1.insertIfNew a (), fun _ h hm => h (r.2 _ h hm)⟩ return r end diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index d10b37a527..eb9740b82e 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -738,9 +738,9 @@ theorem Const.wfImp_insertMany {β : Type v} [BEq α] [Hashable α] [EquivBEq α {l : ρ} (h : Raw.WFImp m.1) : Raw.WFImp (Const.insertMany m l).1.1 := Raw.WF.out ((Const.insertMany m l).2 _ Raw.WF.insert₀ (.wf m.2 h)) -theorem Const.wfImp_insertManyUnit [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} +theorem Const.wfImp_insertManyIfNewUnit [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ α] {m : Raw₀ α (fun _ => Unit)} {l : ρ} (h : Raw.WFImp m.1) : - Raw.WFImp (Const.insertManyUnit m l).1.1 := - Raw.WF.out ((Const.insertManyUnit m l).2 _ Raw.WF.insert₀ (.wf m.2 h)) + Raw.WFImp (Const.insertManyIfNewUnit m l).1.1 := + Raw.WF.out ((Const.insertManyIfNewUnit m l).2 _ Raw.WF.insertIfNew₀ (.wf m.2 h)) end Raw₀ diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index 4e1bbd1a40..153cc4c652 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -58,7 +58,12 @@ instance : Inhabited (Raw α β) where default := ∅ /-- -Inserts the given mapping into the map, replacing an existing mapping for the key if there is one. +Inserts the given mapping into the map. If there is already a mapping for the given key, then both +key and value will be replaced. + +Note: this replacement behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`. +The `insert` function on `HashSet` and `HashSet.Raw` behaves differently: it will return the set +unchanged if a matching key is already present. -/ @[inline] def insert [BEq α] [Hashable α] (m : Raw α β) (a : α) (b : β a) : Raw α β := if h : 0 < m.buckets.size then @@ -373,6 +378,10 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where /-- Inserts multiple mappings into the hash map by iterating over the given collection and calling `insert`. If the same key appears multiple times, the last occurrence takes precedence. + +Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`. +The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first +appearance. -/ @[inline] def insertMany [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (m : Raw α β) (l : ρ) : Raw α β := @@ -388,15 +397,16 @@ Inserts multiple mappings into the hash map by iterating over the given collecti /-- Inserts multiple keys with the value `()` into the hash map by iterating over the given collection -and calling `insert`. If the same key appears multiple times, the last occurrence takes precedence. +and calling `insertIfNew`. If the same key appears multiple times, the first occurrence takes +precedence. This is mainly useful to implement `HashSet.insertMany`, so if you are considering using this, `HashSet` or `HashSet.Raw` might be a better fit for you. -/ -@[inline] def Const.insertManyUnit [BEq α] [Hashable α] {ρ : Type w} +@[inline] def Const.insertManyIfNewUnit [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α] (m : Raw α (fun _ => Unit)) (l : ρ) : Raw α (fun _ => Unit) := if h : 0 < m.buckets.size then - (Raw₀.Const.insertManyUnit ⟨m, h⟩ l).1 + (Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l).1 else m -- will never happen for well-formed inputs /-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last @@ -420,7 +430,7 @@ This is mainly useful to implement `HashSet.ofList`, so if you are considering u `HashSet` or `HashSet.Raw` might be a better fit for you. -/ @[inline] def Const.unitOfList [BEq α] [Hashable α] (l : List α) : Raw α (fun _ => Unit) := - Const.insertManyUnit ∅ l + Const.insertManyIfNewUnit ∅ l /-- Creates a hash map from an array of keys, associating the value `()` with each key. @@ -428,7 +438,7 @@ This is mainly useful to implement `HashSet.ofArray`, so if you are considering `HashSet` or `HashSet.Raw` might be a better fit for you. -/ @[inline] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) : Raw α (fun _ => Unit) := - Const.insertManyUnit ∅ l + Const.insertManyIfNewUnit ∅ l /-- Returns the number of buckets in the internal representation of the hash map. This function may be @@ -547,10 +557,10 @@ theorem WF.Const.insertMany {β : Type v} [BEq α] [Hashable α] {ρ : Type w} [ simpa [Raw.Const.insertMany, h.size_buckets_pos] using (Raw₀.Const.insertMany ⟨m, h.size_buckets_pos⟩ l).2 _ WF.insert₀ h -theorem WF.Const.insertManyUnit [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α] - {m : Raw α (fun _ => Unit)} {l : ρ} (h : m.WF) : (Const.insertManyUnit m l).WF := by - simpa [Raw.Const.insertManyUnit, h.size_buckets_pos] using - (Raw₀.Const.insertManyUnit ⟨m, h.size_buckets_pos⟩ l).2 _ WF.insert₀ h +theorem WF.Const.insertManyIfNewUnit [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α] + {m : Raw α (fun _ => Unit)} {l : ρ} (h : m.WF) : (Const.insertManyIfNewUnit m l).WF := by + simpa [Raw.Const.insertManyIfNewUnit, h.size_buckets_pos] using + (Raw₀.Const.insertManyIfNewUnit ⟨m, h.size_buckets_pos⟩ l).2 _ WF.insertIfNew₀ h theorem WF.ofList [BEq α] [Hashable α] {l : List ((a : α) × β a)} : (ofList l : Raw α β).WF := @@ -562,7 +572,7 @@ theorem WF.Const.ofList {β : Type v} [BEq α] [Hashable α] {l : List (α × β theorem WF.Const.unitOfList [BEq α] [Hashable α] {l : List α} : (Const.unitOfList l : Raw α (fun _ => Unit)).WF := - Const.insertManyUnit WF.empty + Const.insertManyIfNewUnit WF.empty end WF diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index 5fd777e386..0063ae3e48 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -265,9 +265,9 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β [ForIn Id ρ (α × β)] (m : HashMap α β) (l : ρ) : HashMap α β := ⟨DHashMap.Const.insertMany m.inner l⟩ -@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit +@[inline, inherit_doc DHashMap.Const.insertManyIfNewUnit] def insertManyIfNewUnit {ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit := - ⟨DHashMap.Const.insertManyUnit m.inner l⟩ + ⟨DHashMap.Const.insertManyIfNewUnit m.inner l⟩ @[inline, inherit_doc DHashMap.Const.ofList] def ofList [BEq α] [Hashable α] (l : List (α × β)) : HashMap α β := diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 07cfe66dbb..91718cb8f3 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -229,9 +229,9 @@ m.inner.values {ρ : Type w} [ForIn Id ρ (α × β)] (m : Raw α β) (l : ρ) : Raw α β := ⟨DHashMap.Raw.Const.insertMany m.inner l⟩ -@[inline, inherit_doc DHashMap.Raw.Const.insertManyUnit] def insertManyUnit [BEq α] [Hashable α] - {ρ : Type w} [ForIn Id ρ α] (m : Raw α Unit) (l : ρ) : Raw α Unit := - ⟨DHashMap.Raw.Const.insertManyUnit m.inner l⟩ +@[inline, inherit_doc DHashMap.Raw.Const.insertManyIfNewUnit] def insertManyIfNewUnit [BEq α] + [Hashable α] {ρ : Type w} [ForIn Id ρ α] (m : Raw α Unit) (l : ρ) : Raw α Unit := + ⟨DHashMap.Raw.Const.insertManyIfNewUnit m.inner l⟩ @[inline, inherit_doc DHashMap.Raw.Const.ofList] def ofList [BEq α] [Hashable α] (l : List (α × β)) : Raw α β := @@ -306,9 +306,9 @@ theorem WF.insertMany [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ (α × (h : m.WF) : (m.insertMany l).WF := ⟨DHashMap.Raw.WF.Const.insertMany h.out⟩ -theorem WF.insertManyUnit [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α] {m : Raw α Unit} {l : ρ} - (h : m.WF) : (m.insertManyUnit l).WF := - ⟨DHashMap.Raw.WF.Const.insertManyUnit h.out⟩ +theorem WF.insertManyIfNewUnit [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α] {m : Raw α Unit} + {l : ρ} (h : m.WF) : (m.insertManyIfNewUnit l).WF := + ⟨DHashMap.Raw.WF.Const.insertManyIfNewUnit h.out⟩ theorem WF.ofList [BEq α] [Hashable α] {l : List (α × β)} : (ofList l).WF := ⟨DHashMap.Raw.WF.Const.ofList⟩ diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index 55d529ec0a..bbbb3517b4 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean @@ -73,6 +73,10 @@ 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. + +Note: this non-replacement behavior is true for `HashSet` and `HashSet.Raw`. +The `insert` function on `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves +differently: it will overwrite an existing mapping. -/ @[inline] def insert (m : HashSet α) (a : α) : HashSet α := ⟨m.inner.insertIfNew a ()⟩ @@ -218,13 +222,16 @@ instance [BEq α] [Hashable α] {m : Type v → Type v} : ForIn m (HashSet α) m.inner.keysArray /-- -Inserts multiple elements into the hash set. Note that unlike repeatedly calling `insert`, if the -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. +Inserts multiple mappings into the hash set by iterating over the given collection and calling +`insert`. If the same key appears multiple times, the first occurrence takes precedence. + +Note: this precedence behavior is true for `HashSet` and `HashSet.Raw`. The `insertMany` function on +`HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves differently: it will prefer the last +appearance. -/ @[inline] def insertMany {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) : HashSet α := - ⟨m.inner.insertManyUnit l⟩ + ⟨m.inner.insertManyIfNewUnit l⟩ /-- Creates a hash set from a list of elements. Note that unlike repeatedly calling `insert`, if the diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean index c4f506ffdf..d0a7dd010f 100644 --- a/src/Std/Data/HashSet/Raw.lean +++ b/src/Std/Data/HashSet/Raw.lean @@ -74,6 +74,10 @@ instance : Inhabited (Raw α) 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. + +Note: this non-replacement behavior is true for `HashSet` and `HashSet.Raw`. +The `insert` function on `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves +differently: it will overwrite an existing mapping. -/ @[inline] def insert [BEq α] [Hashable α] (m : Raw α) (a : α) : Raw α := ⟨m.inner.insertIfNew a ()⟩ @@ -216,13 +220,16 @@ instance {m : Type v → Type v} : ForIn m (Raw α) α where m.inner.keysArray /-- -Inserts multiple elements into the hash set. Note that unlike repeatedly calling `insert`, if the -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. +Inserts multiple mappings into the hash set by iterating over the given collection and calling +`insert`. If the same key appears multiple times, the first occurrence takes precedence. + +Note: this precedence behavior is true for `HashSet` and `HashSet.Raw`. The `insertMany` function on +`HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves differently: it will prefer the last +appearance. -/ @[inline] def insertMany [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] (m : Raw α) (l : ρ) : Raw α := - ⟨m.inner.insertManyUnit l⟩ + ⟨m.inner.insertManyIfNewUnit l⟩ /-- Creates a hash set from a list of elements. Note that unlike repeatedly calling `insert`, if the @@ -290,7 +297,7 @@ theorem WF.filter [BEq α] [Hashable α] {m : Raw α} {f : α → Bool} (h : m.W theorem WF.insertMany [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] {m : Raw α} {l : ρ} (h : m.WF) : (m.insertMany l).WF := - ⟨HashMap.Raw.WF.insertManyUnit h.out⟩ + ⟨HashMap.Raw.WF.insertManyIfNewUnit h.out⟩ theorem WF.ofList [BEq α] [Hashable α] {l : List α} : (ofList l : Raw α).WF :=