feat: user attribute at grind_pattern (#11770)

This PR implements support for user-defined attributes at
`grind_pattern`. Suppose we have declared the `grind` attribute

```lean
register_grind_attr my_grind
```

Then, we can now write

```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
axiom fg : g (f x) = x

grind_pattern [my_grind] fg => g (f x)
```

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

@@ -35,9 +35,9 @@ open Lean.Parser.Command.GrindCnstr in
 @[builtin_command_elab Lean.Parser.Command.grindPattern]
 def elabGrindPattern : CommandElab := fun stx => do
   match stx with
-  | `(grind_pattern $thmName:ident => $terms,* $[$cnstrs?:grindPatternCnstrs]?) => go thmName terms cnstrs? .global
-  | `(scoped grind_pattern $thmName:ident => $terms,* $[$cnstrs?:grindPatternCnstrs]?) => go thmName terms cnstrs? .scoped
-  | `(local grind_pattern $thmName:ident => $terms,* $[$cnstrs?:grindPatternCnstrs]?) => go thmName terms cnstrs? .local
+  | `(grind_pattern $[[ $attr?:ident ]]? $thmName:ident => $terms,* $[$cnstrs?:grindPatternCnstrs]?) => go attr? thmName terms cnstrs? .global
+  | `(scoped grind_pattern $[[ $attr?:ident ]]? $thmName:ident => $terms,* $[$cnstrs?:grindPatternCnstrs]?) => go attr? thmName terms cnstrs? .scoped
+  | `(local grind_pattern $[[ $attr?:ident ]]? $thmName:ident => $terms,* $[$cnstrs?:grindPatternCnstrs]?) => go attr? thmName terms cnstrs? .local
   | _ => throwUnsupportedSyntax
 where
   findLHS (xs : Array Expr) (lhs : Syntax) : TermElabM (LocalDecl × Nat) := do
@@ -132,9 +132,11 @@ where
       else
         throwErrorAt cnstr "unexpected constraint"
 
-  go (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term ",")
+  go (attrName? : Option (TSyntax `ident)) (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term ",")
       (cnstrs? : Option (TSyntax ``Parser.Command.grindPatternCnstrs))
       (kind : AttributeKind) : CommandElabM Unit := liftTermElabM do
+    let attrName := if let some attrName := attrName? then attrName.getId else `grind
+    let some ext ← Grind.getExtension? attrName | throwError "unknown `grind` attribute `{attrName}`"
     let declName ← realizeGlobalConstNoOverloadWithInfo thmName
     let info ← getConstVal declName
     forallTelescope info.type fun xs _ => do
@@ -145,7 +147,7 @@ where
         let pattern ← Grind.preprocessPattern pattern
         return pattern.abstract xs
       let cnstrs ← elabCnstrs xs cnstrs?
-      Grind.grindExt.addEMatchTheorem declName xs.size patterns.toList .user kind cnstrs (minIndexable := false)
+      ext.addEMatchTheorem declName xs.size patterns.toList .user kind cnstrs (minIndexable := false)
 
 open Command in
 @[builtin_command_elab Lean.Parser.resetGrindAttrs]

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

@@ -138,7 +138,7 @@ example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
 ```
 -/
 @[builtin_command_parser] def grindPattern := leading_parser
-  Term.attrKind >> "grind_pattern " >>  ident >> darrow >> sepBy1 termParser "," >> optional grindPatternCnstrs
+  Term.attrKind >> "grind_pattern " >>  optional ("[" >> ident >> "]") >> ident >> darrow >> sepBy1 termParser "," >> optional grindPatternCnstrs
 
 @[builtin_command_parser] def initGrindNorm := leading_parser
   "init_grind_norm " >> many ident >> "| " >> many ident

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {
@@ -11,7 +12,7 @@ options get_default_options() {
     opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with

tests/pkg/user_attr/UserAttr/Tst.lean

@@ -160,6 +160,8 @@ namespace GrindAttr
 
 opaque f : Nat → Nat
 opaque g : Nat → Nat
+opaque foo : Nat → Nat → Nat
+opaque boo : Nat → Nat → Nat
 
 @[my_grind] theorem fax : f (f x) = f x := sorry
 
@@ -173,4 +175,25 @@ opaque g : Nat → Nat
 
 @[my_grind!? .] theorem fax4 : f (f (f x)) = f x := sorry
 
+theorem fooAx : foo x (f x) = x := sorry
+
+grind_pattern fooAx => foo x (f x)
+
+example : foo x (f (f x)) = x := by
+  fail_if_success grind only [my_grind]
+  grind only [my_grind, usr fooAx]
+
+grind_pattern [my_grind] fooAx => foo x (f x)
+
+example : foo x (f (f x)) = x := by
+  grind only [my_grind]
+
+theorem booAx : boo (f x) (f x) = x := sorry
+
+grind_pattern [my_grind] booAx => boo (f x) (f x)
+
+example : boo (f (f (f x))) (f (f x)) = x := by
+  grind only [my_grind]
+
+
 end GrindAttr