From 15909f209fbf90c7fc16a837865e5600ca253d2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Sep 2022 20:51:37 -0700 Subject: [PATCH] feat: inline small declarations not tagged with `[noinline]` --- src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean | 7 +++++-- src/Lean/Compiler/LCNF/Simp/SimpM.lean | 8 ++++---- tests/lean/linterUnusedVariables.lean.expected.out | 2 +- 3 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean index 6e6abeb8f8..ef3388ce7e 100644 --- a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean +++ b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean @@ -40,10 +40,13 @@ def inlineCandidate? (e : Expr) : SimpM (Option InlineCandidateInfo) := do let numArgs := e.getAppNumArgs let f := e.getAppFn if let .const declName us ← findExpr f then - let inlineIfReduce := hasInlineIfReduceAttribute (← getEnv) declName - unless mustInline || hasInlineAttribute (← getEnv) declName || inlineIfReduce do return none let some decl ← getDecl? declName | return none + let inlineIfReduce := hasInlineIfReduceAttribute (← getEnv) declName if !inlineIfReduce && decl.recursive then return none + let small ← isSmall decl.value + let env ← getEnv + unless mustInline || hasInlineAttribute env declName || inlineIfReduce || (small && !hasNoInlineAttribute env declName) do + return none let arity := decl.getArity let inlinePartial := (← read).config.inlinePartial if !mustInline && !inlinePartial && numArgs < arity then return none diff --git a/src/Lean/Compiler/LCNF/Simp/SimpM.lean b/src/Lean/Compiler/LCNF/Simp/SimpM.lean index 4468c44b24..57324d00bf 100644 --- a/src/Lean/Compiler/LCNF/Simp/SimpM.lean +++ b/src/Lean/Compiler/LCNF/Simp/SimpM.lean @@ -229,10 +229,10 @@ def isOnceOrMustInline (fvarId : FVarId) : SimpM Bool := do | _ => return false /-- -Return `true` if the given local function declaration is considered "small". +Return `true` if the given code is considered "small". -/ -def isSmall (decl : FunDecl) : SimpM Bool := - return decl.value.sizeLe (← getConfig).smallThreshold +def isSmall (code : Code) : SimpM Bool := + return code.sizeLe (← getConfig).smallThreshold /-- Return `true` if the given local function declaration should be inlined. @@ -241,7 +241,7 @@ def shouldInlineLocal (decl : FunDecl) : SimpM Bool := do if (← isOnceOrMustInline decl.fvarId) then return true else - isSmall decl + isSmall decl.value /-- LCNF "Beta-reduce". The equivalent of `(fun params => code) args`. diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out index 2872589237..0f69453305 100644 --- a/tests/lean/linterUnusedVariables.lean.expected.out +++ b/tests/lean/linterUnusedVariables.lean.expected.out @@ -3,8 +3,8 @@ linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unuse linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:29:2-29:3: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:34:5-34:6: warning: unused variable `x` [linter.unusedVariables] -linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables] linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables] +linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables] linterUnusedVariables.lean:42:7-42:8: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:45:8-45:9: warning: unused variable `x` [linter.unusedVariables] linterUnusedVariables.lean:49:9-49:10: warning: unused variable `z` [linter.unusedVariables]