feat: add #grind_lint check in module <module> (#11167)

This PR implements support for `#grind_lint check in module <module>`.
Mathlib does not use namespaces, so we need to restrict the
`#grind_lint` search space using module (prefix) names. Example:

```lean
/--
info: instantiating `Array.filterMap_some` triggers more than 100 additional `grind` theorem instantiations
---
info: Array.filterMap_some
[thm] instances
  [thm] Array.filterMap_filterMap ↦ 94
  [thm] Array.size_filterMap_le ↦ 5
  [thm] Array.filterMap_some ↦ 1
---
info: instantiating `Array.range_succ` triggers 22 additional `grind` theorem instantiations
-/
#guard_msgs in
#grind_lint check (min := 20) in module Init.Data.Array
```

src/Init/Grind/Lint.lean

@@ -22,6 +22,7 @@ Usage examples:
 #grind_lint check
 #grind_lint check (min:=10) (detailed:=50)
 #grind_lint check in Foo Bar -- restrict analysis to these namespaces
+#grind_lint check in module Foo -- restrict analysis to theorems defined in module `Foo` or any of its submodules
 ```
 
 Options can include any valid `grind` configuration option, and `min` and `detailed`.
@@ -40,7 +41,7 @@ By default, `#grind_lint` uses the following `grind` configuration:
 ```
 Consider using `#grind_lint inspect <thm>` to focus on specific theorems.
 -/
-syntax (name := grindLintCheck) "#grind_lint" ppSpace &"check" (ppSpace configItem)* (ppSpace "in" ident+)? : command
+syntax (name := grindLintCheck) "#grind_lint" ppSpace &"check" (ppSpace configItem)* (ppSpace "in" (ppSpace &"module")? ident+)? : command
 
 /--
 `#grind_lint inspect thm₁ …` analyzes the specified theorem(s) individually.

src/Lean/Elab/Tactic/Grind/Lint.lean

@@ -138,34 +138,38 @@ def elabGrindLintInspect : CommandElab := fun stx => liftTermElabM <| withTheRea
         $(⟨stx⟩):command)
       Tactic.TryThis.addSuggestion (header := "Try this to display the actual theorem instances:") stx { suggestion := .tsyntax s }
 
-def getTheorems (prefixes? : Option (Array Name)) : CoreM (List Name) := do
+def getTheorems (prefixes? : Option (Array Name)) (inModule : Bool) : CoreM (List Name) := do
   let skip := skipExt.getState (← getEnv)
   let origins := (← getEMatchTheorems).getOrigins
-  return origins.filterMap fun
-    | .decl declName =>
-      if skip.contains declName then
-        none
-      else if let some prefixes := prefixes? then
-        let keep := prefixes.any fun pre =>
-          if pre == `_root_ then
-            declName.components.length == 1
-          else
-            pre.isPrefixOf declName
-        if keep then
-          some declName
-        else
-          none
+  let env ← getEnv
+  return origins.filterMap fun origin => Id.run do
+    let .decl declName := origin | return none
+    if skip.contains declName then return none
+    let some prefixes := prefixes? | return some declName
+    if inModule then
+      let some modIdx := env.getModuleIdxFor? declName | return none
+      let modName := env.header.moduleNames[modIdx]!
+      if prefixes.any fun pre => pre.isPrefixOf modName then
+        return some declName
       else
-        some declName
-    | _ => none
+        return none
+    else
+      let keep := prefixes.any fun pre =>
+        if pre == `_root_ then
+          declName.components.length == 1
+        else
+          pre.isPrefixOf declName
+      unless keep do return none
+      return some declName
 
 @[builtin_command_elab Lean.Grind.grindLintCheck]
 def elabGrindLintCheck : CommandElab := fun stx => liftTermElabM <| withTheReader Core.Context (fun c => { c with maxHeartbeats := 0 }) do
-  let `(#grind_lint check $[$items:configItem]* $[in $ids?:ident*]?) := stx | throwUnsupportedSyntax
+  let `(#grind_lint check $[$items:configItem]* $[in $[module%$m?]? $ids?:ident*]?) := stx | throwUnsupportedSyntax
   let config ← mkConfig items
   let params ← mkParams config
   let prefixes? := ids?.map (·.map (·.getId))
-  let decls ← getTheorems prefixes?
+  let inModule := m? matches some (some _)
+  let decls ← getTheorems prefixes? inModule
   let decls := decls.toArray.qsort Name.lt
   for declName in decls do
     try

tests/lean/run/grind_lint_1.lean

@@ -93,3 +93,17 @@ info: Try this to display the actual theorem instances:
 -/
 #guard_msgs in
 #grind_lint inspect Array.filterMap_some
+
+/--
+info: instantiating `Array.filterMap_some` triggers more than 100 additional `grind` theorem instantiations
+---
+info: Array.filterMap_some
+[thm] instances
+  [thm] Array.filterMap_filterMap ↦ 94
+  [thm] Array.size_filterMap_le ↦ 5
+  [thm] Array.filterMap_some ↦ 1
+---
+info: instantiating `Array.range_succ` triggers 22 additional `grind` theorem instantiations
+-/
+#guard_msgs in
+#grind_lint check (min := 20) in module Init.Data.Array