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

fix: more stable eager lambda lifting heuristic (#11010)

Browse source 
This PR makes the eager lambda lifting heuristic more predictable by
blocking it from lifting from
any kind of inlineable function, not just `@[inline]`. It also adapts
the doc-string to describe
what is actually going on.
This commit is contained in:
Henrik Böving 2025-10-29 14:58:23 +01:00 • committed by GitHub
parent a51822ead2
commit 1587d02dfb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Compiler/LCNF/LambdaLifting.lean
View file

@ -169,16 +169,17 @@ def lambdaLifting : Pass where
decls.foldlM (init := #[]) fun decls decl => return decls ++ (← decl.lambdaLifting false (suffix := `_lam))
/--
During eager lambda lifting, we lift
- All local function declarations from instances (motivation: make sure it is cheap to inline them later)
- Local function declarations that take local instances as parameters (motivation: ensure they are specialized)
During eager lambda lifting, we inspect declarations that are not inlineable or instances (doing it
everywhere can accidentally introduce mutual recursion which the compiler cannot handle well at the
moment). We then lift local function declarations that take local instances as parameters from
their body to ensure they are specialized.
-/
def eagerLambdaLifting : Pass where
phase := .base
name := `eagerLambdaLifting
run := fun decls => do
decls.foldlM (init := #[]) fun decls decl => do
if decl.inlineAttr || (← Meta.isInstance decl.name) then
if decl.inlineable || (← Meta.isInstance decl.name) then
return decls.push decl
else
return decls ++ (← decl.lambdaLifting (liftInstParamOnly := true) (suffix := `_elam))