feat: remove +premises from grind? output

Author: kim-em

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

@@ -201,6 +201,27 @@ def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `ta
 def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
+/-- Filter out `+premises` from the config syntax -/
+def filterPremisesFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : MetaM (TSyntax ``Lean.Parser.Tactic.optConfig) := do
+  let configItems := config.raw.getArgs
+  let filteredItems := configItems.filter fun item =>
+    -- The structure is: null node -> configItem node -> posConfigItem node
+    -- We need to check if this is a +premises config item
+    if let some configItem := item[0]? then
+      if let some innerItem := configItem[0]? then
+        if innerItem.getKind == ``Lean.Parser.Tactic.posConfigItem then
+          if let some ident := innerItem[1]? then
+            ident.getId != `premises
+          else
+            true
+        else
+          true
+      else
+        true
+    else
+      true
+  return ⟨config.raw.setArgs filteredItems⟩
+
 def mkGrindOnly
     (config : TSyntax ``Lean.Parser.Tactic.optConfig)
     (trace : Grind.Trace)
@@ -217,7 +238,8 @@ def mkGrindOnly
       else
         let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
-  let result ← `(tactic| grind $config:optConfig only)
+  let filteredConfig ← filterPremisesFromConfig config
+  let result ← `(tactic| grind $filteredConfig:optConfig only)
   return setGrindParams result params
 
 private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (interactive : Bool) : TacticM Grind.Config := do

tests/lean/run/grind_question_mark_premises.lean

@@ -0,0 +1,12 @@
+import Lean
+
+set_premise_selector Lean.PremiseSelection.sineQuaNonSelector
+
+-- Test that grind? +premises does NOT include +premises in its output
+/--
+info: Try this:
+  [apply] grind only
+-/
+#guard_msgs in
+example {x y : Nat} (h : x = y) : y = x := by
+  grind? +premises