From 130e2d93a53f79f8728c204db35b3db475dd07e2 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 17 Apr 2025 13:47:40 -0700 Subject: [PATCH] fix: change inlining heuristics to match old code generator (#8006) This PR changes the inlining heuristics of the new code generator to match the old one, which ensures that monadic folds get sufficiently inlined for their tail recursion to be exposed to the code generator. --- src/Lean/Compiler/LCNF/Simp.lean | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean index 9808b65858..d3ed81f153 100644 --- a/src/Lean/Compiler/LCNF/Simp.lean +++ b/src/Lean/Compiler/LCNF/Simp.lean @@ -42,30 +42,13 @@ def Decl.simp? (decl : Decl) : SimpM (Option Decl) := do partial def Decl.simp (decl : Decl) (config : Config) : CompilerM Decl := do let mut config := config if (← isTemplateLike decl) then - let mut inlineDefs := config.inlineDefs - /- - At the base phase, we don't inline definitions occurring in instances. - Reason: we eagerly lambda lift local functions occurring at instances before saving their code at the end of the base - phase. The goal is to make them cheap to inline in actual code. By inlining definitions we would be just generating extra - work for the lambda lifter. - - There is an exception: inlineable instances. This is important for auxiliary instances such as - ``` - @[always_inline] - instance : Monad TermElabM := let i := inferInstanceAs (Monad TermElabM); { pure := i.pure, bind := i.bind } - ``` - by keeping `inlineDefs := true`, we can pre-compute the `pure` and `bind` methods for `TermElabM`. - -/ - if (← inBasePhase <&&> Meta.isInstance decl.name) then - unless decl.inlineable do - inlineDefs := false /- We do not eta-expand or inline partial applications in template like code. Recall we don't want to generate code for them. Remark: by eta-expanding partial applications in instances, we also make the simplifier work harder when inlining instance projections. -/ - config := { config with etaPoly := false, inlinePartial := false, inlineDefs } + config := { config with etaPoly := false, inlinePartial := false } go decl config where go (decl : Decl) (config : Config) : CompilerM Decl := do