feat: library suggestion engine for local theorems (#11030)

This PR adds a library suggestion engine for local theorems. To be
useful, I still need to write more combinators to re-rank and combine
suggestions from multiple engines.

This is stacked on top of #11029.

Author: kim-em

src/Lean/LibrarySuggestions/Basic.lean

@@ -286,6 +286,22 @@ def random (gen : StdGen := ⟨37, 59⟩) : Selector := fun _ cfg => do
       suggestions := suggestions.push { name := name, score := 1.0 / consts.size.toFloat }
   return suggestions
 
+/-- A library suggestion engine that returns locally defined theorems (those in the current file). -/
+def currentFile : Selector := fun _ cfg => do
+  let env ← getEnv
+  let max := cfg.maxSuggestions
+  -- Use map₂ from the staged map, which contains locally defined constants
+  let mut suggestions := #[]
+  for (name, ci) in env.constants.map₂.toList do
+    if suggestions.size >= max then
+      break
+    if isDeniedPremise env name then
+      continue
+    match ci with
+    | .thmInfo _ => suggestions := suggestions.push { name := name, score := 1.0 }
+    | _ => continue
+  return suggestions
+
 builtin_initialize librarySuggestionsExt : EnvExtension (Option Selector) ←
   registerEnvExtension (pure none)
 

tests/lean/run/library_suggestions_local.lean

@@ -0,0 +1,39 @@
+import Lean.LibrarySuggestions.Basic
+
+-- Define some initial local constants
+def myLocalDef : Nat := 42
+
+theorem myLocalTheorem : myLocalDef = 42 := rfl
+
+-- Add a theorem in the Lean namespace (should be filtered by isDeniedPremise)
+namespace Lean
+theorem shouldBeFiltered : True := trivial
+end Lean
+
+-- Test the currentFile selector (should only show theorems, not definitions)
+set_library_suggestions Lean.LibrarySuggestions.currentFile
+
+-- First test: should show only myLocalTheorem
+-- (not myLocalDef since it's a def, not Lean.shouldBeFiltered since it's in Lean namespace)
+/--
+info: Library suggestions: [myLocalTheorem]
+-/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial
+
+-- Add more local constants (mix of theorems and definitions)
+theorem anotherTheorem : True := trivial
+
+def myFunction (x : Nat) : Nat := x + 1
+
+-- Second test: should show only the two theorems (not myFunction)
+/--
+info: Library suggestions: [anotherTheorem, myLocalTheorem]
+-/
+#guard_msgs in
+example : False → True := by
+  suggestions
+  intro h
+  trivial