chore: update stage0

src/Init/Tactics.lean

@@ -1425,6 +1425,16 @@ If there are several with the same priority, it is uses the "most recent one". E
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
 
+/--
+Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
+-/
+syntax (name := grind_norm) "grind_norm" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
+
+/--
+Simplification procedures tagged with the `grind_norm_proc` attribute are used by the `grind` tactic normalizer/pre-processor.
+-/
+syntax (name := grind_norm_proc) "grind_norm_proc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
 
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"

src/Lean/Meta/Tactic.lean

@@ -40,3 +40,4 @@ import Lean.Meta.Tactic.SolveByElim
 import Lean.Meta.Tactic.FunInd
 import Lean.Meta.Tactic.Rfl
 import Lean.Meta.Tactic.Rewrites
+import Lean.Meta.Tactic.Grind

src/Lean/Meta/Tactic/Grind.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Attr

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

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Simp.Attr
+import Lean.Meta.Tactic.Simp.Simproc
+
+namespace Lean.Meta.Grind
+open Simp
+
+builtin_initialize grindNormExt : SimpExtension ←
+  registerSimpAttr `grind_norm "simplification/normalization theorems for `grind`"
+
+builtin_initialize grindNormSimprocExt : SimprocExtension ←
+  registerSimprocAttr `grind_norm_proc "simplification/normalization procedured for `grind`" none
+
+
+#check simpAttrNameToSimprocAttrName
+
+/-
+  let str := id.getId.toString
+  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
+  let descr := quote ((doc.map (·.getDocString) |>.getD s!"simp set for {id.getId.toString}").removeLeadingSpaces)
+  let procId := mkIdentFrom id (simpAttrNameToSimprocAttrName id.getId)
+  let procStr := procId.getId.toString
+  let procIdParser := mkIdentFrom procId (`Parser.Attr ++ procId.getId)
+  let procDescr := quote s!"simproc set for {procId.getId.toString}"
+  -- TODO: better docDomment for simprocs
+  `($[$doc:docComment]? initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr $(quote id.getId)
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? (prio)? : attr
+    /-- Simplification procedure -/
+    initialize extProc : SimprocExtension ← registerSimprocAttr $(quote procId.getId) $procDescr none $(quote procId.getId)
+    /-- Simplification procedure -/
+    syntax (name := $procIdParser:ident) $(quote procStr):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? : attr)
+
+-/
+
+end Lean.Meta.Grind