feat: introduce findMatchingDecl? for code quality checks in Lean.Linter (#14880)

This PR adds `Lean.Linter.findMatchingDecl?`, which finds the
declaration a piece of syntax belongs to by searching the current
command's info trees for declarations whose declaration range contains
it, together with `Lean.Linter.findCodeQualitySource?` and
`Lean.Linter.findCodeQualitySource`, which turn that declaration into a
code-quality `Source` (the latter falling back to the current module
when no declaration matches). This gives linters a way to attribute
diagnostics and code-quality entries to the declaration being
elaborated.

The helpers are exercised by a new package test,
`tests/pkg/find_matching_decl`, which registers a linter reporting the
matched declaration and derived source for each command. It covers plain
definitions, inductives, mutual blocks, classes, instances, and commands
with no associated declaration.

Author: Wojciech Różowski

src/Lean/Linter/Util.lean

@@ -9,12 +9,13 @@ prelude
 public import Lean.Server.InfoUtils
 public import Lean.Linter.Init
 public import Lean.Elab.Term
+public import Lean.Linter.CodeQuality.Basic
 
 public section
 
 namespace Lean.Linter
 
-open Lean.Elab
+open Lean.Elab CodeQuality
 
 /-- Go upwards through the given `tree` starting from the smallest node that
 contains the given `range` and collect all `MacroExpansionInfo`s on the way up.
@@ -74,3 +75,38 @@ def getNewDecls (t : InfoTree) : List Name :=
       else
         acc
     | _ => acc
+
+/-- Find the declaration in the current file that `stx` belongs to.
+
+Searches the info trees of the current command for declarations (see `getNewDecls`) whose
+declaration range contains the range of `stx`, and returns the one whose range starts earliest.
+Returns `none` if `stx` has no position or no declaration's range contains it (e.g. for commands
+such as `#check` or `open`).
+-/
+def findMatchingDecl? [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m]
+    (stx : Syntax) : m (Option Name) := do
+  let some stxRange ← getDeclarationRange? stx | return none
+  let mut best? : Option (Name × DeclarationRange) := none
+  for t in ← getInfoTrees do
+    for declName in getNewDecls t do
+      let some ranges ← findDeclarationRangesCore? declName | continue
+      let r := ranges.range
+      unless !r.pos.lt stxRange.pos && !stxRange.endPos.lt r.endPos do continue
+      if best?.all fun (_, b) => r.pos.lt b.pos then
+        best? := some (declName, r)
+  return best?.map (·.1)
+
+/-- Build a code-quality `Source` attributing `stx` to the declaration it belongs to
+(see `findMatchingDecl?`), or `none` if no declaration matches. -/
+def findCodeQualitySource? [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m]
+    (stx : Syntax) : m (Option Source) := do
+  let some name ← findMatchingDecl? stx | return none
+  return some (.declaration (← getEnv).mainModule name)
+
+/-- Build a code-quality `Source` attributing `stx` to the declaration it belongs to
+(see `findMatchingDecl?`), falling back to the current module if no declaration matches. -/
+def findCodeQualitySource [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m]
+    (stx : Syntax) : m Source := do
+  match ← findMatchingDecl? stx with
+  | some name => return .declaration (← getEnv).mainModule name
+  | none      => return .module (← getEnv).mainModule

tests/pkg/find_matching_decl/FindMatchingDecl.lean

@@ -0,0 +1,29 @@
+import FindMatchingDecl.Linter
+
+/-! Declarations of various shapes for `Linter.findMatchingDecl?` to match: plain definitions,
+an inductive, a mutual block whose definitions are compiled via `partial_fixpoint`, a class,
+and an anonymous instance. -/
+
+def a := 1
+def b := 2
+def c := 3
+
+inductive Foo where
+  | mk : Foo
+
+mutual
+  def hello2 : Option Nat := hello1
+    partial_fixpoint
+
+  def hello1 : Option Nat := hello2
+    partial_fixpoint
+end
+
+class Magma (carrier : Type u) where
+  op : carrier → carrier → carrier
+
+instance : Magma Nat where
+  op := (· + ·)
+
+-- A command with no matching declaration: `findCodeQualitySource` falls back to the module.
+#check Nat

tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean

@@ -0,0 +1,19 @@
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+/-! A linter that reports the declaration `Linter.findMatchingDecl?` associates with each
+command it runs on, and the code-quality source derived from it by
+`Linter.findCodeQualitySource` and `Linter.findCodeQualitySource?`. -/
+
+open Lean Elab Command
+
+def matchingDeclLinter : Linter where
+  run stx := do
+    if let some decl := (← Linter.findMatchingDecl? stx) then
+      logInfoAt stx m!"best match is: {decl}"
+    let src ← Linter.findCodeQualitySource stx
+    let src? ← Linter.findCodeQualitySource? stx
+    -- `compress` keeps each message on one line so the test can grep for it
+    logInfoAt stx m!"source: {(toJson src).compress}; source?: {(toJson src?).compress}"
+
+initialize addLinter matchingDeclLinter

tests/pkg/find_matching_decl/lakefile.toml

@@ -0,0 +1,5 @@
+name = "find_matching_decl"
+defaultTargets = ["FindMatchingDecl"]
+
+[[lean_lib]]
+name = "FindMatchingDecl"

tests/pkg/find_matching_decl/lean-toolchain

@@ -0,0 +1 @@
+../../../build/release/stage1

tests/pkg/find_matching_decl/run_test.sh

@@ -0,0 +1,24 @@
+rm -rf .lake
+
+# Build the library; the linter registered in `FindMatchingDecl.Linter` runs on each
+# command of `FindMatchingDecl` and reports the declaration `findMatchingDecl?` picks.
+capture lake build
+
+check_out_contains "FindMatchingDecl.lean:7:0: best match is: a"
+check_out_contains "FindMatchingDecl.lean:8:0: best match is: b"
+check_out_contains "FindMatchingDecl.lean:9:0: best match is: c"
+check_out_contains "FindMatchingDecl.lean:11:0: best match is: Foo"
+# The whole `mutual` command resolves to the earliest declaration in the block.
+check_out_contains "FindMatchingDecl.lean:14:0: best match is: hello2"
+check_out_contains "FindMatchingDecl.lean:22:0: best match is: Magma"
+# An anonymous instance resolves to its generated name.
+check_out_contains "FindMatchingDecl.lean:25:0: best match is: instMagmaNat"
+
+# Commands inside a declaration yield a declaration source, in both variants.
+check_out_contains 'FindMatchingDecl.lean:7:0: source: {"declaration":{"module":"FindMatchingDecl","name":"a"}}; source?: {"declaration":{"module":"FindMatchingDecl","name":"a"}}'
+check_out_contains 'FindMatchingDecl.lean:14:0: source: {"declaration":{"module":"FindMatchingDecl","name":"hello2"}}'
+check_out_contains 'FindMatchingDecl.lean:25:0: source: {"declaration":{"module":"FindMatchingDecl","name":"instMagmaNat"}}'
+# The module docstring and `#check` match no declaration: the total variant falls back to the
+# module source while the optional variant returns `none`.
+check_out_contains 'FindMatchingDecl.lean:3:0: source: {"module":{"name":"FindMatchingDecl"}}; source?: null'
+check_out_contains 'FindMatchingDecl.lean:30:0: source: {"module":{"name":"FindMatchingDecl"}}; source?: null'