feat: find declaration name inside of linters

Author: Wojciech Rozowski

src/Lean/Linter/Util.lean

@@ -74,3 +74,17 @@ def getNewDecls (t : InfoTree) : List Name :=
       else
         acc
     | _ => acc
+
+open Elab in
+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)

tests/pkg/module_linter/ModLinter.lean

@@ -3,3 +3,14 @@ import ModLinter.Def
 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

tests/pkg/module_linter/ModLinter/Def.lean

@@ -1,4 +1,5 @@
 import Lean.Elab.Command
+import Lean.Linter.Util
 
 open Lean Elab Command
 
@@ -7,4 +8,10 @@ def dummyModuleLinter : ModuleLinter where
     let ref := cmds[0]?.getD .missing
     logWarningAt ref m!"cmds: {cmds}"
 
+def myLinter : Linter where
+  run stx := do
+    if let some decl := (← Linter.findMatchingDecl? stx) then
+      logInfoAt stx m!"best match is: {decl}"
+
 initialize addModuleLinter dummyModuleLinter
+initialize addLinter myLinter