chore: update stage0

src/Lean/Elab/Tactic/Grind.lean

@@ -21,20 +21,23 @@ open Command Term in
 @[builtin_command_elab Lean.Parser.Command.grindPattern]
 def elabGrindPattern : CommandElab := fun stx => do
   match stx with
-  | `(grind_pattern $thmName:ident => $terms,*) => do
-    liftTermElabM do
-      let declName ← resolveGlobalConstNoOverload thmName
-      discard <| addTermInfo thmName (← mkConstWithLevelParams declName)
-      let info ← getConstInfo declName
-      forallTelescope info.type fun xs _ => do
-        let patterns ← terms.getElems.mapM fun term => do
-          let pattern ← Term.elabTerm term none
-          synthesizeSyntheticMVarsUsingDefault
-          let pattern ← instantiateMVars pattern
-          let pattern ← Grind.preprocessPattern pattern
-          return pattern.abstract xs
-        Grind.addEMatchTheorem declName xs.size patterns.toList .user
+  | `(grind_pattern $thmName:ident => $terms,*) => go thmName terms .global
+  | `(scoped grind_pattern $thmName:ident => $terms,*) => go thmName terms .scoped
+  | `(local grind_pattern $thmName:ident => $terms,*) => go thmName terms .local
   | _ => throwUnsupportedSyntax
+where
+  go (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term ",") (kind : AttributeKind) : CommandElabM Unit := liftTermElabM do
+    let declName ← resolveGlobalConstNoOverload thmName
+    discard <| addTermInfo thmName (← mkConstWithLevelParams declName)
+    let info ← getConstInfo declName
+    forallTelescope info.type fun xs _ => do
+      let patterns ← terms.getElems.mapM fun term => do
+        let pattern ← Term.elabTerm term none
+        synthesizeSyntheticMVarsUsingDefault
+        let pattern ← instantiateMVars pattern
+        let pattern ← Grind.preprocessPattern pattern
+        return pattern.abstract xs
+      Grind.addEMatchTheorem declName xs.size patterns.toList .user kind
 
 open Command in
 @[builtin_command_elab Lean.Parser.resetGrindAttrs]

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

@@ -935,8 +935,8 @@ def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Boo
 Adds an E-matching theorem to the environment.
 See `mkEMatchTheorem`.
 -/
-def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) : MetaM Unit := do
-  ematchTheoremsExt.add (← mkEMatchTheorem declName numParams patterns kind)
+def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) (attrKind := AttributeKind.global) : MetaM Unit := do
+  ematchTheoremsExt.add (← mkEMatchTheorem declName numParams patterns kind) attrKind
 
 /--
 Adds an E-matching equality theorem to the environment.

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

@@ -11,7 +11,7 @@ namespace Lean.Parser.Command
 Builtin parsers for `grind` related commands
 -/
 @[builtin_command_parser] def grindPattern := leading_parser
-  "grind_pattern " >>  ident >> darrow >> sepBy1 termParser ","
+  Term.attrKind >> "grind_pattern " >>  ident >> darrow >> sepBy1 termParser ","
 
 @[builtin_command_parser] def initGrindNorm := leading_parser
   "init_grind_norm " >> many ident >> "| " >> many ident

tests/lean/run/grind_pattern3.lean

@@ -0,0 +1,61 @@
+reset_grind_attrs%
+def Set (α : Type) := α → Bool
+
+def insertElem [DecidableEq α] (s : Set α) (a : α) : Set α :=
+  fun x => a = x || s x
+
+def contains (s : Set α) (a : α) : Bool :=
+  s a
+
+namespace Set
+
+theorem contains_insert [DecidableEq α] (s : Set α) (a : α) : contains (insertElem s a) a := by
+  simp [contains, insertElem]
+
+scoped grind_pattern contains_insert => contains (insertElem s a) a
+
+end Set
+
+example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
+        s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by
+  fail_if_success grind -- should fail
+  open Set in grind -- scoped pattern was activated, it should work now
+
+example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
+        s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by
+  fail_if_success grind -- should fail
+  intros; subst s₂ a₁; apply Set.contains_insert
+
+open Set in
+example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
+        s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by
+  grind -- should work
+
+example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
+        s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by
+  fail_if_success grind -- should fail
+  intros; subst s₂ a₁; apply Set.contains_insert
+
+
+-- TheoremPattern activation test
+
+def a := 10
+def b := 20
+def foo (x : List Nat) (y : List Nat) := x ++ y ++ x
+
+theorem fooThm : foo x [a, b] = x ++ [a, b] ++ x := rfl
+
+section
+local grind_pattern fooThm => foo x [a, b]
+
+/-- trace: [grind.ematch.instance] fooThm: foo x [a, b] = x ++ [a, b] ++ x -/
+#guard_msgs in
+set_option trace.grind.ematch.instance true in
+example : xs = [a, b] → foo x xs = x ++ [a, b] ++ x := by
+  grind
+
+end
+
+example : xs = [a, b] → foo x xs = x ++ [a, b] ++ x := by
+  fail_if_success grind -- should fail, `local grind_pattern` is not active anymore
+  intro; subst xs; apply fooThm