sorting
diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 76d475f..472c73f 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean
@@ -120,18 +120,6 @@ (a : α) (fallback : β a) : β a := Raw₀.getD ⟨m.1, m.2.size_buckets_pos⟩ a fallback -@[inline, inherit_doc Raw.getKey?] def getKey? (m : DHashMap α β) (a : α) : Option α := - Raw₀.getKey? ⟨m.1, m.2.size_buckets_pos⟩ a - -@[inline, inherit_doc Raw.getKey] def getKey (m : DHashMap α β) (a : α) (h : a ∈ m) : α := - Raw₀.getKey ⟨m.1, m.2.size_buckets_pos⟩ a h - -@[inline, inherit_doc Raw.getKey!] def getKey! [Inhabited α] (m : DHashMap α β) (a : α) : α := - Raw₀.getKey! ⟨m.1, m.2.size_buckets_pos⟩ a - -@[inline, inherit_doc Raw.getKeyD] def getKeyD (m : DHashMap α β) (a : α) (fallback : α) : α := - Raw₀.getKeyD ⟨m.1, m.2.size_buckets_pos⟩ a fallback - @[inline, inherit_doc Raw.erase] def erase (m : DHashMap α β) (a : α) : DHashMap α β := ⟨Raw₀.erase ⟨m.1, m.2.size_buckets_pos⟩ a, .erase₀ m.2⟩ @@ -164,6 +152,18 @@ end +@[inline, inherit_doc Raw.getKey?] def getKey? (m : DHashMap α β) (a : α) : Option α := + Raw₀.getKey? ⟨m.1, m.2.size_buckets_pos⟩ a + +@[inline, inherit_doc Raw.getKey] def getKey (m : DHashMap α β) (a : α) (h : a ∈ m) : α := + Raw₀.getKey ⟨m.1, m.2.size_buckets_pos⟩ a h + +@[inline, inherit_doc Raw.getKey!] def getKey! [Inhabited α] (m : DHashMap α β) (a : α) : α := + Raw₀.getKey! ⟨m.1, m.2.size_buckets_pos⟩ a + +@[inline, inherit_doc Raw.getKeyD] def getKeyD (m : DHashMap α β) (a : α) (fallback : α) : α := + Raw₀.getKeyD ⟨m.1, m.2.size_buckets_pos⟩ a fallback + @[inline, inherit_doc Raw.size] def size (m : DHashMap α β) : Nat := m.1.size
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean index 3646666..8cc0c22 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean
@@ -88,11 +88,6 @@ else es.getCast? a /-- Internal implementation detail of the hash map -/ -def getKey? [BEq α] (a : α) : AssocList α β → Option α - | nil => none - | cons k _ es => if k == a then some k else es.getKey? a - -/-- Internal implementation detail of the hash map -/ def contains [BEq α] (a : α) : AssocList α β → Bool | nil => false | cons k _ l => k == a || l.contains a @@ -118,6 +113,11 @@ | cons k v es => if h : k == a then cast (congrArg β (eq_of_beq h)) v else es.getCast! a /-- Internal implementation detail of the hash map -/ +def getKey? [BEq α] (a : α) : AssocList α β → Option α + | nil => none + | cons k _ es => if k == a then some k else es.getKey? a + +/-- Internal implementation detail of the hash map -/ def get! {β : Type v} [BEq α] [Inhabited β] (a : α) : AssocList α (fun _ => β) → β | nil => panic! "key is not present in hash table" | cons k v es => bif k == a then v else es.get! a
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index a4f52c3..866208b 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
@@ -58,11 +58,6 @@ induction l <;> simp_all [getCast?, List.getValueCast?] @[simp] -theorem getKey?_eq [BEq α] {l : AssocList α β} {a : α} : - l.getKey? a = List.getKey? a l.toList := by - induction l <;> simp_all [getKey?] - -@[simp] theorem contains_eq [BEq α] {l : AssocList α β} {a : α} : l.contains a = containsKey a l.toList := by induction l <;> simp_all [contains, List.containsKey] @@ -118,6 +113,11 @@ Bool.apply_cond Option.get!] @[simp] +theorem getKey?_eq [BEq α] {l : AssocList α β} {a : α} : + l.getKey? a = List.getKey? a l.toList := by + induction l <;> simp_all [getKey?] + +@[simp] theorem getKey_eq [BEq α] {l : AssocList α β} {a : α} {h} : l.getKey a h = List.getKey a l.toList (contains_eq.symm.trans h) := by induction l
diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index 40d48e3..6d2fc80 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean
@@ -313,30 +313,6 @@ buckets[idx.1].getCast! a /-- Internal implementation detail of the hash map -/ -@[inline] def getKey? [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option α := - let ⟨⟨_, buckets⟩, h⟩ := m - let ⟨i, h⟩ := mkIdx buckets.size h (hash a) - buckets[i].getKey? a - -/-- Internal implementation detail of the hash map -/ -@[inline] def getKey [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (hma : m.contains a) : α := - let ⟨⟨_, buckets⟩, h⟩ := m - let idx := mkIdx buckets.size h (hash a) - buckets[idx.1].getKey a hma - -/-- Internal implementation detail of the hash map -/ -@[inline] def getKeyD [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : α) : α := - let ⟨⟨_, buckets⟩, h⟩ := m - let idx := mkIdx buckets.size h (hash a) - buckets[idx.1].getKeyD a fallback - -/-- Internal implementation detail of the hash map -/ -@[inline] def getKey! [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) : α := - let ⟨⟨_, buckets⟩, h⟩ := m - let idx := mkIdx buckets.size h (hash a) - buckets[idx.1].getKey! a - -/-- Internal implementation detail of the hash map -/ @[inline] def erase [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Raw₀ α β := let ⟨⟨size, buckets⟩, hb⟩ := m let ⟨i, h⟩ := mkIdx buckets.size hb (hash a) @@ -444,6 +420,30 @@ end +/-- Internal implementation detail of the hash map -/ +@[inline] def getKey? [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option α := + let ⟨⟨_, buckets⟩, h⟩ := m + let ⟨i, h⟩ := mkIdx buckets.size h (hash a) + buckets[i].getKey? a + +/-- Internal implementation detail of the hash map -/ +@[inline] def getKey [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (hma : m.contains a) : α := + let ⟨⟨_, buckets⟩, h⟩ := m + let idx := mkIdx buckets.size h (hash a) + buckets[idx.1].getKey a hma + +/-- Internal implementation detail of the hash map -/ +@[inline] def getKeyD [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : α) : α := + let ⟨⟨_, buckets⟩, h⟩ := m + let idx := mkIdx buckets.size h (hash a) + buckets[idx.1].getKeyD a fallback + +/-- Internal implementation detail of the hash map -/ +@[inline] def getKey! [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) : α := + let ⟨⟨_, buckets⟩, h⟩ := m + let idx := mkIdx buckets.size h (hash a) + buckets[idx.1].getKey! a + end Raw₀ /-- Internal implementation detail of the hash map -/
diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index 8e254d1..9d0d96b 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean
@@ -130,15 +130,6 @@ else none -- will never happen for well-formed inputs /-- -Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`. -The result in the `some` case is guaranteed to be pointer equal to the key in the map. --/ -@[inline] def getKey? [BEq α] [Hashable α] (m : Raw α β) (a : α) : Option α := - if h : 0 < m.buckets.size then - Raw₀.getKey? ⟨m, h⟩ a - else none -- will never happen for well-formed inputs - -/-- Returns `true` if there is a mapping for the given key. There is also a `Prop`-valued version of this: `a ∈ m` is equivalent to `m.contains a = true`. @@ -188,32 +179,6 @@ Raw₀.get! ⟨m, h⟩ a else default -- will never happen for well-formed inputs -/-- -Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by -requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map. --/ -@[inline] def getKey [BEq α] [Hashable α] (m : Raw α β) (a : α) (h : a ∈ m) : α := - Raw₀.getKey ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a - (by change dite .. = true at h; split at h <;> simp_all) - -/-- -Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`. -If a mapping exists the result is guaranteed to be pointer equal to the key in the map. --/ -@[inline] def getKeyD [BEq α] [Hashable α] (m : Raw α β) (a : α) (fallback : α) : α := - if h : 0 < m.buckets.size then - Raw₀.getKeyD ⟨m, h⟩ a fallback - else fallback -- will never happen for well-formed inputs - -/-- -Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. -If no panic occurs the result is guaranteed to be pointer equal to the key in the map. --/ -@[inline] def getKey! [BEq α] [Hashable α] [Inhabited α] (m : Raw α β) (a : α) : α := - if h : 0 < m.buckets.size then - Raw₀.getKey! ⟨m, h⟩ a - else default -- will never happen for well-formed inputs - /-- Removes the mapping for the given key if it exists. -/ @[inline] def erase [BEq α] [Hashable α] (m : Raw α β) (a : α) : Raw α β := if h : 0 < m.buckets.size then @@ -273,6 +238,41 @@ end /-- +Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`. +The result in the `some` case is guaranteed to be pointer equal to the key in the map. +-/ +@[inline] def getKey? [BEq α] [Hashable α] (m : Raw α β) (a : α) : Option α := + if h : 0 < m.buckets.size then + Raw₀.getKey? ⟨m, h⟩ a + else none -- will never happen for well-formed inputs + +/-- +Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by +requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map. +-/ +@[inline] def getKey [BEq α] [Hashable α] (m : Raw α β) (a : α) (h : a ∈ m) : α := + Raw₀.getKey ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a + (by change dite .. = true at h; split at h <;> simp_all) + +/-- +Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`. +If a mapping exists the result is guaranteed to be pointer equal to the key in the map. +-/ +@[inline] def getKeyD [BEq α] [Hashable α] (m : Raw α β) (a : α) (fallback : α) : α := + if h : 0 < m.buckets.size then + Raw₀.getKeyD ⟨m, h⟩ a fallback + else fallback -- will never happen for well-formed inputs + +/-- +Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. +If no panic occurs the result is guaranteed to be pointer equal to the key in the map. +-/ +@[inline] def getKey! [BEq α] [Hashable α] [Inhabited α] (m : Raw α β) (a : α) : α := + if h : 0 < m.buckets.size then + Raw₀.getKey! ⟨m, h⟩ a + else default -- will never happen for well-formed inputs + +/-- Returns `true` if the hash map contains no mappings. Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index b8eb2fc..973889e 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean
@@ -116,9 +116,6 @@ def find? (m : HashMap α β) (a : α) : Option β := m.get? a -@[inline, inherit_doc DHashMap.getKey?] def getKey? (m : HashMap α β) (a : α) : Option α := - DHashMap.getKey? m.inner a - @[inline, inherit_doc DHashMap.contains] def contains (m : HashMap α β) (a : α) : Bool := m.inner.contains a @@ -163,6 +160,9 @@ getElem? m a := m.get? a getElem! m a := m.get! a +@[inline, inherit_doc DHashMap.getKey?] def getKey? (m : HashMap α β) (a : α) : Option α := + DHashMap.getKey? m.inner a + @[inline, inherit_doc DHashMap.getKey] def getKey (m : HashMap α β) (a : α) (h : a ∈ m) : α := DHashMap.getKey m.inner a h
diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 31b02dd..afaf810 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean
@@ -103,10 +103,6 @@ @[inline] def get? [beq : BEq α] [Hashable α] (m : Raw α β) (a : α) : Option β := DHashMap.Raw.Const.get? m.inner a -@[inline, inherit_doc DHashMap.Raw.getKey?] def getKey? [BEq α] [Hashable α] (m : Raw α β) (a : α) : - Option α := - DHashMap.Raw.getKey? m.inner a - @[inline, inherit_doc DHashMap.Raw.contains] def contains [BEq α] [Hashable α] (m : Raw α β) (a : α) : Bool := m.inner.contains a @@ -142,6 +138,10 @@ getElem? m a := m.get? a getElem! m a := m.get! a +@[inline, inherit_doc DHashMap.Raw.getKey?] def getKey? [BEq α] [Hashable α] (m : Raw α β) (a : α) : + Option α := + DHashMap.Raw.getKey? m.inner a + @[inline, inherit_doc DHashMap.Raw.getKey] def getKey [BEq α] [Hashable α] (m : Raw α β) (a : α) (h : a ∈ m) : α := DHashMap.Raw.getKey m.inner a h
diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index 30119ca..a065598 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean
@@ -89,13 +89,6 @@ ⟨replaced, ⟨r⟩⟩ /-- -Checks if given key is contained and returns the key if it is, otherwise `none`. -The result in the `some` case is guaranteed to be pointer equal to the key in the set. --/ -@[inline] def get? (m : HashSet α) (a : α) : Option α := - m.inner.getKey? a - -/-- Returns `true` if the given key is present in the set. There is also a `Prop`-valued version of this: `a ∈ m` is equivalent to `m.contains a = true`. @@ -111,6 +104,21 @@ instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m) := inferInstanceAs (Decidable (a ∈ m.inner)) +/-- Removes the element if it exists. -/ +@[inline] def erase (m : HashSet α) (a : α) : HashSet α := + ⟨m.inner.erase a⟩ + +/-- The number of elements present in the set -/ +@[inline] def size (m : HashSet α) : Nat := + m.inner.size + +/-- +Checks if given key is contained and returns the key if it is, otherwise `none`. +The result in the `some` case is guaranteed to be pointer equal to the key in the set. +-/ +@[inline] def get? (m : HashSet α) (a : α) : Option α := + m.inner.getKey? a + /-- Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set. @@ -132,14 +140,6 @@ @[inline] def get! [BEq α] [Hashable α] [Inhabited α] (m : HashSet α) (a : α) : α := m.inner.getKey! a -/-- Removes the element if it exists. -/ -@[inline] def erase (m : HashSet α) (a : α) : HashSet α := - ⟨m.inner.erase a⟩ - -/-- The number of elements present in the set -/ -@[inline] def size (m : HashSet α) : Nat := - m.inner.size - /-- Returns `true` if the hash set contains no elements.
diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean index fa54d5e..88cab2e 100644 --- a/src/Std/Data/HashSet/Raw.lean +++ b/src/Std/Data/HashSet/Raw.lean
@@ -90,13 +90,6 @@ ⟨replaced, ⟨r⟩⟩ /-- -Checks if given key is contained and returns the key if it is, otherwise `none`. -The result in the `some` case is guaranteed to be pointer equal to the key in the map. --/ -@[inline] def get? [BEq α] [Hashable α] (m : Raw α) (a : α) : Option α := - m.inner.getKey? a - -/-- Returns `true` if the given element is present in the set. There is also a `Prop`-valued version of this: `a ∈ m` is equivalent to `m.contains a = true`. @@ -112,6 +105,21 @@ instance [BEq α] [Hashable α] {m : Raw α} {a : α} : Decidable (a ∈ m) := inferInstanceAs (Decidable (a ∈ m.inner)) +/-- Removes the element if it exists. -/ +@[inline] def erase [BEq α] [Hashable α] (m : Raw α) (a : α) : Raw α := + ⟨m.inner.erase a⟩ + +/-- The number of elements present in the set -/ +@[inline] def size (m : Raw α) : Nat := + m.inner.size + +/-- +Checks if given key is contained and returns the key if it is, otherwise `none`. +The result in the `some` case is guaranteed to be pointer equal to the key in the map. +-/ +@[inline] def get? [BEq α] [Hashable α] (m : Raw α) (a : α) : Option α := + m.inner.getKey? a + /-- Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set. @@ -133,14 +141,6 @@ @[inline] def get! [BEq α] [Hashable α] [Inhabited α] (m : Raw α) (a : α) : α := m.inner.getKey! a -/-- Removes the element if it exists. -/ -@[inline] def erase [BEq α] [Hashable α] (m : Raw α) (a : α) : Raw α := - ⟨m.inner.erase a⟩ - -/-- The number of elements present in the set -/ -@[inline] def size (m : Raw α) : Nat := - m.inner.size - /-- Returns `true` if the hash set contains no elements.