From 2405fd605e97e35fa3778e36a503d2826660423a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 27 Mar 2024 09:35:22 +0100 Subject: [PATCH] feat: trace non-easy whnf invocations (#3774) --- src/Lean/Meta/WHNF.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index c855ad0222..1a5287901c 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -936,21 +936,22 @@ private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do @[export lean_whnf] partial def whnfImp (e : Expr) : MetaM Expr := withIncRecDepth <| whnfEasyCases e fun e => do - checkSystem "whnf" let useCache ← useWHNFCache e match (← cached? useCache e) with | some e' => pure e' | none => - let e' ← whnfCore e - match (← reduceNat? e') with - | some v => cache useCache e v - | none => - match (← reduceNative? e') with + withTraceNode `Meta.whnf (fun _ => return m!"Non-easy whnf: {e}") do + checkSystem "whnf" + let e' ← whnfCore e + match (← reduceNat? e') with | some v => cache useCache e v | none => - match (← unfoldDefinition? e') with - | some e'' => cache useCache e (← whnfImp e'') - | none => cache useCache e e' + match (← reduceNative? e') with + | some v => cache useCache e v + | none => + match (← unfoldDefinition? e') with + | some e'' => cache useCache e (← whnfImp e'') + | none => cache useCache e e' /-- If `e` is a projection function that satisfies `p`, then reduce it -/ def reduceProjOf? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do