From 489c87a7a0f2d2a2f5d13a1d2bc3d78afca939c4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 7 Nov 2024 14:55:36 +0100
Subject: [PATCH] perf: optimize unfolding constant lookup
---
src/Lean/Meta/WHNF.lean | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 55db7b40d459..e3eb695a7606 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -831,10 +831,12 @@ mutual
else
unfoldDefault ()
| .const declName lvls => do
+ let some cinfo ← getUnfoldableConstNoEx? declName | pure none
+ -- check smart unfolding only after `getUnfoldableConstNoEx?` because smart unfoldings have a
+ -- significant chance of not existing and `Environment.contains` misses are more costly
if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
return none
else
- let some cinfo ← getUnfoldableConstNoEx? declName | pure none
unless cinfo.hasValue do return none
deltaDefinition cinfo lvls
(fun _ => pure none)