feat: add %reset_grind_attrs (#6824)

This PR introduces the auxiliary command `%reset_grind_attrs` for
debugging purposes. It is particularly useful for writing self-contained
tests.

src/Init/Grind/Tactics.lean

@@ -6,8 +6,13 @@ Authors: Leonardo de Moura
 prelude
 import Init.Tactics
 
-namespace Lean.Parser.Attr
+namespace Lean.Parser
+/--
+Reset all `grind` attributes. This command is intended for testing purposes only and should not be used in applications.
+-/
+syntax (name := resetGrindAttrs) "%reset_grind_attrs" : command
 
+namespace Attr
 syntax grindEq     := "= "
 syntax grindEqBoth := atomic("_" "=" "_ ")
 syntax grindEqRhs  := atomic("=" "_ ")
@@ -17,12 +22,10 @@ syntax grindFwd    := "→ "
 syntax grindUsr    := &"usr "
 syntax grindCases  := &"cases "
 syntax grindCasesEager := atomic(&"cases" &"eager ")
-
 syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindUsr <|> grindCasesEager <|> grindCases
-
 syntax (name := grind) "grind" (grindMod)? : attr
-
-end Lean.Parser.Attr
+end Attr
+end Lean.Parser
 
 namespace Lean.Grind
 /--

src/Lean/Elab/Tactic/Grind.lean

@@ -35,6 +35,12 @@ def elabGrindPattern : CommandElab := fun stx => do
         Grind.addEMatchTheorem declName xs.size patterns.toList .user
   | _ => throwUnsupportedSyntax
 
+open Command in
+@[builtin_command_elab Lean.Parser.resetGrindAttrs]
+def elabResetGrindAttrs : CommandElab := fun _ => liftTermElabM do
+  Grind.resetCasesExt
+  Grind.resetEMatchTheoremsExt
+
 open Command Term in
 @[builtin_command_elab Lean.Parser.Command.initGrindNorm]
 def elabInitGrindNorm : CommandElab := fun stx =>

src/Lean/Meta/Tactic/Grind/Cases.lean

@@ -60,6 +60,9 @@ builtin_initialize casesExt : SimpleScopedEnvExtension CasesEntry CasesTypes ←
     addEntry       := fun s {declName, eager} => s.insert declName eager
   }
 
+def resetCasesExt : CoreM Unit := do
+  modifyEnv fun env => casesExt.modifyState env fun _ => {}
+
 def getCasesTypes : CoreM CasesTypes :=
   return casesExt.getState (← getEnv)
 

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -224,6 +224,9 @@ private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTh
     initial  := {}
   }
 
+def resetEMatchTheoremsExt : CoreM Unit := do
+  modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => {}
+
 /--
 Symbols with built-in support in `grind` are unsuitable as pattern candidates for E-matching.
 This is because `grind` performs normalization operations and uses specialized data structures

tests/lean/run/grind_trace.lean

@@ -1,3 +1,5 @@
+%reset_grind_attrs
+
 attribute [grind =] List.length_cons
 attribute [grind →] List.getElem?_eq_getElem
 attribute [grind =] List.length_replicate
@@ -92,3 +94,12 @@ error: `And` is marked as a built-in case-split for `grind` and cannot be erased
 #guard_msgs (error) in
 example : p ∧ q → p := by
   grind [-And]
+
+example : (List.replicate n a)[m]? = if m < n then some a else none := by
+  grind?
+
+%reset_grind_attrs
+
+example : (List.replicate n a)[m]? = if m < n then some a else none := by
+  fail_if_success grind?
+  sorry