perf: fix linearity issue in insertIfNew (#3881)

This fixes a linearity isssue in `insertIfNew`. As `insertIfNew` is used
in `Lean.finalizeImport` we expect this to improve performance.
This commit is contained in:
Henrik Böving 2024-04-11 17:12:10 +02:00 committed by GitHub
parent 36f1398aaa
commit 3ed2d9b3ad
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -122,7 +122,7 @@ def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapI
let ⟨i, h⟩ := mkIdx (hash a) buckets.property
let bkt := buckets.val[i]
if let some b := bkt.find? a then
(m, some b)
(⟨size, buckets⟩, some b)
else
let size' := size + 1
let buckets' := buckets.update i (AssocList.cons a b bkt) h