max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf: quadratic behavior in whnfCore (#7630)

Browse source 
This PR fixes a performance issue in the `whnfCore` procedure.
This commit is contained in:
Leonardo de Moura 2025-03-21 15:29:21 -07:00 • committed by GitHub
parent b768e44ba7
commit eb0c015e7c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Lean/Meta/WHNF.lean
View file

@ -588,18 +588,30 @@ expand let-expressions, expand assigned meta-variables.
partial def whnfCore (e : Expr) : MetaM Expr :=
go e
where
expandLet (e : Expr) (vs : Array Expr) : Expr :=
if let .letE _ _ v b _ := e then
expandLet b (vs.push <| v.instantiateRev vs)
else if let some (#[], _, _, v, b) := e.letFunAppArgs? then
expandLet b (vs.push <| v.instantiateRev vs)
else
e.instantiateRev vs
go (e : Expr) : MetaM Expr :=
whnfEasyCases e fun e => do
trace[Meta.whnf] e
match e with
| .const .. => pure e
| .letE _ _ v b _ => if (← getConfig).zeta then go <| b.instantiate1 v else return e
| .letE _ _ v b _ =>
if (← getConfig).zeta then
go <| expandLet b #[v]
else
return e
| .app f .. =>
let cfg ← getConfig
if cfg.zeta then
if let some (args, _, _, v, b) := e.letFunAppArgs? then
-- When zeta reducing enabled, always reduce `letFun` no matter the current reducibility level
return (← go <| mkAppN (b.instantiate1 v) args)
return (← go <| mkAppN (expandLet b #[v]) args)
let f := f.getAppFn
let f' ← go f
/-