perf: Don't hash the key when searching in empty hash tables

Based on: rust-lang/hashbrown#305
hargoniX · Aug 29, 2023 · 43a80dc · 43a80dc
1 parent a5583d7
commit 43a80dc
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
@@ -64,18 +64,21 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
 
 def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
   match m with
+  | ⟨0, _⟩ => none
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].findEntry? a
 
 def find? [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
   match m with
+  | ⟨0, _⟩ => none
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].find? a
 
 def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
   match m with
+  | ⟨0, _⟩ => false
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].contains a

diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
@@ -60,12 +60,14 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
 
 def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
   match m with
+  | ⟨0, _⟩ => none
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].find? (fun a' => a == a')
 
 def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
   match m with
+  | ⟨0, _⟩ => false
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].contains a