feat: add nolint options for function arguments and pattern variables

src/Lean/Linter/Basic.lean

@@ -12,8 +12,18 @@ register_builtin_option linter.unusedVariables : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter"
 }
+register_builtin_option linter.unusedVariables.funArgs : Bool := {
+  defValue := true,
+  descr := "enable the 'unused variables' linter to mark unused function arguments"
+}
+register_builtin_option linter.unusedVariables.patternVars : Bool := {
+  defValue := true,
+  descr := "enable the 'unused variables' linter to mark unused pattern variables"
+}
 
 def getLinterUnusedVariables (o : Options) : Bool := o.get linter.unusedVariables.name (getLinterAll o)
+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
   let some stxRange := stx.getRange?
@@ -71,21 +81,33 @@ def unusedVariables : Linter := fun stx => do
     if !stxRange.contains range.start then
       continue
 
-    if !getLinterUnusedVariables decl.ci.options then
+    let opts := decl.ci.options
+    if !getLinterUnusedVariables opts then
       continue
 
-    let some stack := findSyntaxStack? stx declStx
-      | continue
-    let ignoredPatternFns := [
+    let mut ignoredPatternFns := #[
       isTopLevelDecl constDecls,
       matchesUnusedPattern,
       isVariable,
-      isInStructure,
-      isInLetDeclaration,
-      isInDeclarationSignature,
-      isInFun,
+      isInCtorOrStructBinder,
+      isInConstantOrAxiom,
+      isInDefWithForeignDefinition,
       isInDepArrow
     ]
+    if !getLinterUnusedVariablesFunArgs opts then
+      ignoredPatternFns := ignoredPatternFns.append #[
+        isInLetDeclaration,
+        isInDeclarationSignature,
+        isInStructure,
+        isInFun
+      ]
+    if !getLinterUnusedVariablesPatternVars opts then
+      ignoredPatternFns := ignoredPatternFns.append #[
+        isPatternVar
+      ]
+
+    let some stack := findSyntaxStack? stx declStx
+      | continue
     if ignoredPatternFns.any (· declStx stack) then
       continue
 
@@ -109,8 +131,40 @@ where
     stx.getId.toString.startsWith "_"
   isVariable (_ : Syntax) (stack : SyntaxStack) :=
     stackMatches stack [`null, none, `null, `Lean.Parser.Command.variable]
-  isInStructure (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, `Lean.Parser.Command.structure]
+  isInCtorOrStructBinder (_ : Syntax) (stack : SyntaxStack) :=
+    stackMatches stack [`null, none, `null, `Lean.Parser.Command.optDeclSig, none] &&
+    (stack.get? 4 |>.any fun (stx, _) =>
+      [`Lean.Parser.Command.ctor, `Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·))
+  isInConstantOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
+    stackMatches stack [`null, none, `null, `Lean.Parser.Command.declSig, none] &&
+    (stack.get? 4 |>.any fun (stx, _) =>
+      [`Lean.Parser.Command.constant, `Lean.Parser.Command.axiom].any (stx.isOfKind ·))
+  isInDefWithForeignDefinition (_ : Syntax) (stack : SyntaxStack) :=
+    stackMatches stack [`null, none, `null, none, none, `Lean.Parser.Command.declaration] &&
+    (stack.get? 3 |>.any fun (stx, _) =>
+      stx.isOfKind `Lean.Parser.Command.optDeclSig ||
+      stx.isOfKind `Lean.Parser.Command.declSig) &&
+    (stack.get? 5 |>.any fun (stx, _) => Id.run <| do
+      let declModifiers := stx[0]
+      if !declModifiers.isOfKind `Lean.Parser.Command.declModifiers then
+        return false
+      let termAttributes := declModifiers[1][0]
+      if !termAttributes.isOfKind `Lean.Parser.Term.attributes then
+        return false
+      let termAttrInstance := termAttributes[1][0]
+      if !termAttrInstance.isOfKind `Lean.Parser.Term.attrInstance then
+        return false
+
+      let attr := termAttrInstance[1]
+      if attr.isOfKind `Lean.Parser.Attr.extern then
+        return true
+      else if attr.isOfKind `Lean.Parser.Attr.simple then
+        return attr[0].getId == `implementedBy
+      else
+        return false)
+  isInDepArrow (_ : Syntax) (stack : SyntaxStack) :=
+    stackMatches stack [`null, `Lean.Parser.Term.explicitBinder, `Lean.Parser.Term.depArrow]
+
   isInLetDeclaration (_ : Syntax) (stack : SyntaxStack) :=
     stackMatches stack [`null, none, `null, `Lean.Parser.Term.letIdDecl, none] &&
     (stack.get? 3 |>.any fun (_, pos) => pos == 1) &&
@@ -120,10 +174,14 @@ where
     (stack.get? 3 |>.any fun (stx, pos) =>
       pos == 0 &&
       [`Lean.Parser.Command.optDeclSig, `Lean.Parser.Command.declSig].any (stx.isOfKind ·))
+  isInStructure (_ : Syntax) (stack : SyntaxStack) :=
+    stackMatches stack [`null, none, `null, `Lean.Parser.Command.structure]
   isInFun (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, `Lean.Parser.Term.basicFun]
-  isInDepArrow (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, `Lean.Parser.Term.explicitBinder, `Lean.Parser.Term.depArrow]
+    stackMatches stack [`null, `Lean.Parser.Term.basicFun] ||
+    stackMatches stack [`null, `Lean.Parser.Term.paren, `null, `Lean.Parser.Term.basicFun]
+
+  isPatternVar (_ : Syntax) (stack : SyntaxStack) :=
+    stack.any fun (stx, pos) => stx.isOfKind `Lean.Parser.Term.matchAlt && pos == 1
 
 builtin_initialize addLinter unusedVariables
 

tests/lean/linterUnusedVariables.lean

@@ -40,6 +40,9 @@ where
 def unusedFunctionArgument : Nat :=
   (fun x => 3) (x := 2)
 
+def unusedTypedFunctionArgument : Nat :=
+  (fun (x : Nat) => 3) 2
+
 def pattern (x y : Option Nat) : Nat :=
   match x with
   | some z =>
@@ -48,6 +51,18 @@ def pattern (x y : Option Nat) : Nat :=
     | none => 0
   | none => 0
 
+def patternLet (x : Option Nat) : Nat :=
+  if let some y := x then
+    0
+  else
+    1
+
+def patternMatches (x : Option Nat) : Nat :=
+  if x matches some y then
+    0
+  else
+    1
+
 def implicitVariables {α : Type} [inst : ToString α] : Nat := 4
 
 def autoImplicitVariable [Inhabited α] := 5
@@ -94,6 +109,22 @@ def lintUnusedVariables (x : Nat) : Nat :=
   3
 
 
+set_option linter.unusedVariables.funArgs false in
+def nolintFunArgs (w : Nat) : Nat :=
+  let a := 5
+  let f (x : Nat) := 3
+  let g := fun (y : Nat) => 3
+  f <| g <| h <| 2
+where
+  h (z : Nat) := 3
+
+set_option linter.unusedVariables.patternVars false in
+def nolintPatternVars (x : Option (Option Nat)) : Nat :=
+  match x with
+  | some (some y) => (fun z => 1) 2
+  | _ => 0
+
+
 inductive Foo (α : Type)
   | foo (x : Nat) (y : Nat)
 
@@ -147,3 +178,21 @@ constant foo' (x : Nat) : Nat :=
 variable (bar)
 variable (bar' : (x : Nat) → Nat)
 variable {α β} [inst : ToString α]
+
+@[specialize]
+def specializeDef (x : Nat) : Nat := 3
+
+@[implementedBy specializeDef]
+def implementedByDef (x : Nat) : Nat :=
+  let y := 3
+  5
+
+@[extern "test"]
+def externDef (x : Nat) : Nat :=
+  let y := 3
+  5
+
+@[extern "test"]
+constant externConst (x : Nat) : Nat :=
+  let y := 3
+  5

tests/lean/linterUnusedVariables.lean.expected.out

@@ -1,11 +1,30 @@
 linterUnusedVariables.lean:16:6-16:7: warning: unused variable `y`
+linterUnusedVariables.lean:15:21-15:22: warning: unused variable `x`
 linterUnusedVariables.lean:21:8-21:9: warning: unused variable `x`
 linterUnusedVariables.lean:28:2-28:3: warning: unused variable `x`
+linterUnusedVariables.lean:33:5-33:6: warning: unused variable `x`
 linterUnusedVariables.lean:38:2-38:3: warning: unused variable `f`
-linterUnusedVariables.lean:45:9-45:10: warning: unused variable `z`
-linterUnusedVariables.lean:47:11-47:12: warning: unused variable `z`
-linterUnusedVariables.lean:93:6-93:7: warning: unused variable `y`
-linterUnusedVariables.lean:107:8-107:9: warning: unused variable `y`
-linterUnusedVariables.lean:111:7-111:8: warning: unused variable `x`
-linterUnusedVariables.lean:121:6-121:7: warning: unused variable `s`
-linterUnusedVariables.lean:145:6-145:7: warning: unused variable `y`
+linterUnusedVariables.lean:38:5-38:6: warning: unused variable `x`
+linterUnusedVariables.lean:41:7-41:8: warning: unused variable `x`
+linterUnusedVariables.lean:44:8-44:9: warning: unused variable `x`
+linterUnusedVariables.lean:48:9-48:10: warning: unused variable `z`
+linterUnusedVariables.lean:50:11-50:12: warning: unused variable `z`
+linterUnusedVariables.lean:55:14-55:15: warning: unused variable `y`
+linterUnusedVariables.lean:61:20-61:21: warning: unused variable `y`
+linterUnusedVariables.lean:66:34-66:38: warning: unused variable `inst`
+linterUnusedVariables.lean:107:25-107:26: warning: unused variable `x`
+linterUnusedVariables.lean:108:6-108:7: warning: unused variable `y`
+linterUnusedVariables.lean:114:6-114:7: warning: unused variable `a`
+linterUnusedVariables.lean:124:26-124:27: warning: unused variable `z`
+linterUnusedVariables.lean:128:15-128:16: warning: unused variable `α`
+linterUnusedVariables.lean:131:15-131:16: warning: unused variable `α`
+linterUnusedVariables.lean:138:8-138:9: warning: unused variable `y`
+linterUnusedVariables.lean:142:7-142:8: warning: unused variable `x`
+linterUnusedVariables.lean:141:20-141:21: warning: unused variable `β`
+linterUnusedVariables.lean:152:6-152:7: warning: unused variable `s`
+linterUnusedVariables.lean:159:13-159:14: warning: unused variable `s`
+linterUnusedVariables.lean:176:6-176:7: warning: unused variable `y`
+linterUnusedVariables.lean:183:19-183:20: warning: unused variable `x`
+linterUnusedVariables.lean:187:6-187:7: warning: unused variable `y`
+linterUnusedVariables.lean:192:6-192:7: warning: unused variable `y`
+linterUnusedVariables.lean:197:6-197:7: warning: unused variable `y`