From 85528a41b90a5be3b0309e59299bafda137713a9 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 9 Nov 2024 21:51:46 +0000 Subject: [PATCH 1/2] perf: optimize `Key.hash` at `DiscrTree` for the `.const` constructor --- src/Lean/Meta/DiscrTreeTypes.lean | 2 +- src/Lean/Meta/LazyDiscrTree.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean index d0e96aa62506..559257bce29e 100644 --- a/src/Lean/Meta/DiscrTreeTypes.lean +++ b/src/Lean/Meta/DiscrTreeTypes.lean @@ -26,7 +26,7 @@ inductive Key where deriving Inhabited, BEq, Repr protected def Key.hash : Key → UInt64 - | .const n a => mixHash 5237 $ mixHash (hash n) (hash a) + | .const n a => mixHash (hash n) (hash a) | .fvar n a => mixHash 3541 $ mixHash (hash n) (hash a) | .lit v => mixHash 1879 $ hash v | .star => 7883 diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean index 29a37cdd8218..3b2c5ddddcb8 100644 --- a/src/Lean/Meta/LazyDiscrTree.lean +++ b/src/Lean/Meta/LazyDiscrTree.lean @@ -42,7 +42,7 @@ namespace Key /-- Hash function -/ protected def hash : Key → UInt64 - | .const n a => mixHash 5237 $ mixHash n.hash (hash a) + | .const n a => mixHash (hash n) (hash a) | .fvar n a => mixHash 3541 $ mixHash (hash n) (hash a) | .lit v => mixHash 1879 $ hash v | .star => 7883 From ea98113575fba9babc5a73bcba382364061abeff Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Sat, 9 Nov 2024 23:02:51 +0000 Subject: [PATCH 2/2] that's weird, why did the build fail? --- src/Lean/Meta/DiscrTreeTypes.lean | 2 +- src/Lean/Meta/LazyDiscrTree.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean index 559257bce29e..c7c6b48cec35 100644 --- a/src/Lean/Meta/DiscrTreeTypes.lean +++ b/src/Lean/Meta/DiscrTreeTypes.lean @@ -32,7 +32,7 @@ protected def Key.hash : Key → UInt64 | .star => 7883 | .other => 2411 | .arrow => 17 - | .proj s i a => mixHash (hash a) $ mixHash (hash s) (hash i) + | .proj s i a => mixHash 5237 $ mixHash (hash a) $ mixHash (hash s) (hash i) instance : Hashable Key := ⟨Key.hash⟩ diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean index 3b2c5ddddcb8..22b69959cf95 100644 --- a/src/Lean/Meta/LazyDiscrTree.lean +++ b/src/Lean/Meta/LazyDiscrTree.lean @@ -48,7 +48,7 @@ protected def hash : Key → UInt64 | .star => 7883 | .other => 2411 | .arrow => 17 - | .proj s i a => mixHash (hash a) $ mixHash (hash s) (hash i) + | .proj s i a => mixHash 5237 $ mixHash (hash a) $ mixHash (hash s) (hash i) instance : Hashable Key := ⟨Key.hash⟩