From 70aff92f8fd901dc9e19eb3a12e02fbe5d21778d Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Wed, 6 Jul 2022 17:58:06 +0200
Subject: [PATCH] fix: short-circuit ignore functions in unused variables
 linter

---
 src/Lean/Linter/Basic.lean | 46 ++++++++++++++++++--------------------
 1 file changed, 22 insertions(+), 24 deletions(-)

diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index b2d0655552..0944d4fa52 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -25,12 +25,12 @@ def getLinterUnusedVariables (o : Options) : Bool := o.get linter.unusedVariable
 def getLinterUnusedVariablesFunArgs (o : Options) : Bool := o.get linter.unusedVariables.funArgs.name (getLinterUnusedVariables o)
 def getLinterUnusedVariablesPatternVars (o : Options) : Bool := o.get linter.unusedVariables.patternVars.name (getLinterUnusedVariables o)
 
-def unusedVariables : Linter := fun stx => do
+def unusedVariables : Linter := fun cmdStx => do
   -- NOTE: `messages` is local to the current command
   if (← get).messages.hasErrors then
     return
 
-  let some stxRange := stx.getRange?
+  let some cmdStxRange := cmdStx.getRange?
     | pure ()
 
   let infoTrees := (← get).infoState.trees.toArray
@@ -83,7 +83,7 @@ def unusedVariables : Linter := fun stx => do
       | continue
     let some localDecl := decl.info.lctx.find? id
       | continue
-    if !stxRange.contains range.start || localDecl.userName.hasMacroScopes then
+    if !cmdStxRange.contains range.start || localDecl.userName.hasMacroScopes then
       continue
 
     -- check linter options
@@ -92,7 +92,7 @@ def unusedVariables : Linter := fun stx => do
       continue
 
     -- collect ignore functions
-    let mut ignoredPatternFns := #[
+    let mut ignoreFns := #[
       isTopLevelDecl constDecls,
       matchesUnusedPattern,
       isVariable,
@@ -104,36 +104,34 @@ def unusedVariables : Linter := fun stx => do
       isInDepArrow
     ]
     if !getLinterUnusedVariablesFunArgs opts then
-      ignoredPatternFns := ignoredPatternFns.append #[
+      ignoreFns := ignoreFns.append #[
         isInLetDeclaration,
         isInDeclarationSignature,
         isInFun
       ]
     if !getLinterUnusedVariablesPatternVars opts then
-      ignoredPatternFns := ignoredPatternFns.append #[
+      ignoreFns := ignoreFns.append #[
         isPatternVar
       ]
 
-    -- collect syntax versions from macro expansions
-    let mut stxVersions := #[stx]
-    for tree in infoTrees do
+    -- evaluate ignore functions on original syntax
+    if let some stack := findSyntaxStack? cmdStx declStx then
+      if ignoreFns.any (· declStx stack) then
+        continue
+    else
+      continue
+
+    -- evaluate ignore functions on macro expansion outputs
+    if ← infoTrees.anyM fun tree => do
       if let some macroExpansions ← collectMacroExpansions? range tree then
-        for exp in macroExpansions do
-          stxVersions := stxVersions.push exp.output
-
-    -- apply ignore functions to syntax stacks
-    let continue? ← stxVersions.foldlM (init := none) (fun (result : Option Bool ) stx => do
-      if result matches some true then
-        return true
-
-      let some stack := findSyntaxStack? stx declStx
-        | return result
-
-      if ignoredPatternFns.any (· declStx stack) then
-        return true
+        return macroExpansions.reverse.any fun expansion =>
+          if let some stack := findSyntaxStack? expansion.output declStx then
+            ignoreFns.any (· declStx stack)
+          else
+            false
       else
-        return false)
-    if continue? matches some true || continue? matches none then
+        return false
+    then
       continue
 
     -- publish warning if variable is unused