fix: grind error messages

This PR ensures `grind` error messages use `{.ofConstName declName}`
when referencing declaration names.

src/Lean/Elab/Tactic/Grind.lean

@@ -101,7 +101,7 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
         let thms := s.find (.decl declName)
         let thms := thms.filter fun thm => thm.kind == .user
         if thms.isEmpty then
-          throwErrorAt p "invalid use of `usr` modifier, `{declName}` does not have patterns specified with the command `grind_pattern`"
+          throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`"
         for thm in thms do
           params := { params with extra := params.extra.push thm }
       | .ematch kind =>
@@ -114,7 +114,7 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
           for ctor in info.ctors do
             params ← withRef p <| addEMatchTheorem params ctor (.default false)
         else
-          throwError "invalid use of `intro` modifier, `{declName}` is not an inductive predicate"
+          throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
       | .ext =>
         throwError "`[grind ext]` cannot be set using parameters"
       | .infer =>
@@ -151,14 +151,14 @@ where
         return { params with extra := params.extra.push thm }
     | .defn =>
       if (← isReducible declName) then
-        throwError "`{declName}` is a reducible definition, `grind` automatically unfolds them"
+        throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them"
       if !kind.isEqLhs && !kind.isDefault then
-        throwError "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='"
+        throwError "invalid `grind` parameter, `{.ofConstName declName}` is a definition, the only acceptable (and redundant) modifier is '='"
       let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
-        | throwError "failed to generate equation theorems for `{declName}`"
+        | throwError "failed to generate equation theorems for `{.ofConstName declName}`"
       return { params with extra := params.extra ++ thms.toPArray' }
     | _ =>
-      throwError "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type"
+      throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type"
 
 def mkGrindParams (config : Grind.Config) (only : Bool) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
   let params ← Grind.mkParams config

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean

@@ -20,7 +20,7 @@ private def reportMissingToIntAdapter (type : Expr) (instType : Expr) : MetaM Un
   trace[grind.debug.cutsat.debug] "`ToInt` initialization failure, failed to synthesize{indentExpr instType}\nfor type{indentExpr type}"
 
 private def throwMissingDecl (declName : Name) : MetaM Unit :=
-  throwError "`grind cutsat`, unexpected missing declaration {declName}"
+  throwError "`grind cutsat`, unexpected missing declaration {.ofConstName declName}"
 
 private def checkDecl (declName : Name) : MetaM Unit := do
   unless (← getEnv).contains declName do

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

@@ -98,7 +98,7 @@ private def registerGrindAttr (showInfo : Bool) : IO Unit :=
           for ctor in info.ctors do
             addEMatchAttr ctor attrKind (.default false) (← getGlobalSymbolPriorities) (showInfo := showInfo)
         else
-          throwError "invalid `[grind intro]`, `{declName}` is not an inductive predicate"
+          throwError "invalid `[grind intro]`, `{.ofConstName declName}` is not an inductive predicate"
       | .ext => addExtAttr declName attrKind
       | .infer =>
         if let some declName ← isCasesAttrCandidate? declName false then

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

@@ -89,9 +89,9 @@ def isCasesAttrPredicateCandidate? (declName : Name) (eager : Bool) : MetaM (Opt
 def validateCasesAttr (declName : Name) (eager : Bool) : CoreM Unit := do
   unless (← isCasesAttrCandidate declName eager) do
     if eager then
-      throwError "invalid `[grind cases eager]`, `{declName}` is not a non-recursive inductive datatype or an alias for one"
+      throwError "invalid `[grind cases eager]`, `{.ofConstName declName}` is not a non-recursive inductive datatype or an alias for one"
     else
-      throwError "invalid `[grind cases]`, `{declName}` is not an inductive datatype or an alias for one"
+      throwError "invalid `[grind cases]`, `{.ofConstName declName}` is not an inductive datatype or an alias for one"
 
 def addCasesAttr (declName : Name) (eager : Bool) (attrKind : AttributeKind) : CoreM Unit := do
   validateCasesAttr declName eager
@@ -101,11 +101,11 @@ def CasesTypes.eraseDecl (s : CasesTypes) (declName : Name) : CoreM CasesTypes :
   if s.contains declName then
     return s.erase declName
   else
-    throwError "`{declName}` is not marked with the `[grind]` attribute"
+    throwError "`{.ofConstName declName}` is not marked with the `[grind]` attribute"
 
 def ensureNotBuiltinCases (declName : Name) : CoreM Unit := do
   if isBuiltinEagerCases declName then
-    throwError "`{declName}` is marked as a built-in case-split for `grind` and cannot be erased"
+    throwError "`{.ofConstName declName}` is marked as a built-in case-split for `grind` and cannot be erased"
 
 def eraseCasesAttr (declName : Name) : CoreM Unit := do
   ensureNotBuiltinCases declName

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

@@ -593,7 +593,7 @@ private def isCandidateSymbol (declName : Name) (root : Bool) : M Bool := do
   if prio == 0 then return false
   -- Remark: uncomment the following code to fix bootstrapping issues
   -- if declName ∈ badForPatterns then
-  --  throwError "INSERT `import Init.Grind.Tactics`, otherwise a pattern containing `{declName}` will be used, prio: {prio}"
+  --  throwError "INSERT `import Init.Grind.Tactics`, otherwise a pattern containing `{.ofConstName declName}` will be used, prio: {prio}"
   -- If it is the root symbol, then we check whether `prio ≥ minPrio`
   if root then
     return prio ≥ ctx.minPrio
@@ -897,7 +897,7 @@ private def getProofFor (declName : Name) : MetaM Expr := do
   -- For theorems, `isProp` has already been checked at declaration time
   unless wasOriginallyTheorem (← getEnv) declName do
     unless (← isProp info.type) do
-      throwError "invalid E-matching theorem `{declName}`, type is not a proposition"
+      throwError "invalid E-matching theorem `{.ofConstName declName}`, type is not a proposition"
   let us := info.levelParams.map mkLevelParam
   return mkConst declName us
 
@@ -1286,7 +1286,7 @@ where
 
 def mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) (showInfo := false) : MetaM EMatchTheorem := do
   let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind prios (showInfo := showInfo)
-    | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
+    | throwError "`@{thmKind.toAttribute} theorem {.ofConstName declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
   return thm
 
 def mkEMatchEqTheoremsForDef? (declName : Name) (showInfo := false) : MetaM (Option (Array EMatchTheorem)) := do
@@ -1299,14 +1299,14 @@ private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind
     ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs) (gen := thmKind.gen) (showInfo := showInfo)) attrKind
   else if let some thms ← mkEMatchEqTheoremsForDef? declName (showInfo := showInfo) then
     unless useLhs do
-      throwError "`{declName}` is a definition, you must only use the left-hand side for extracting patterns"
+      throwError "`{.ofConstName declName}` is a definition, you must only use the left-hand side for extracting patterns"
     thms.forM (ematchTheoremsExt.add · attrKind)
   else
     throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions"
 
 def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems := do
   let throwErr {α} : MetaM α :=
-    throwError "`{declName}` is not marked with the `[grind]` attribute"
+    throwError "`{.ofConstName declName}` is not marked with the `[grind]` attribute"
   if !wasOriginallyTheorem (← getEnv) declName then
     if let some eqns ← getEqnsFor? declName then
        let s := ematchTheoremsExt.getState (← getEnv)

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

@@ -25,7 +25,7 @@ builtin_initialize extTheoremsExt : SimpleScopedEnvExtension Name ExtTheorems
 def validateExtAttr (declName : Name) : CoreM Unit := do
   if !(← Ext.isExtTheorem declName) then
   if !(isStructure (← getEnv) declName) then
-    throwError "invalid `[grind ext]`, `{declName}` is neither tagged with `[ext]` nor is a structure"
+    throwError "invalid `[grind ext]`, `{.ofConstName declName}` is neither tagged with `[ext]` nor is a structure"
 
 def addExtAttr (declName : Name) (attrKind : AttributeKind) : CoreM Unit := do
   validateExtAttr declName
@@ -35,7 +35,7 @@ private def eraseDecl (s : ExtTheorems) (declName : Name) : CoreM ExtTheorems :=
   if s.contains declName then
     return s.erase declName
   else
-    throwError "`{declName}` is not marked with the `[grind ext]` attribute"
+    throwError "`{.ofConstName declName}` is not marked with the `[grind ext]` attribute"
 
 def eraseExtAttr (declName : Name) : CoreM Unit := do
   let s := extTheoremsExt.getState (← getEnv)

tests/lean/run/grind_ematch1.lean

@@ -78,7 +78,7 @@ namespace using_grind_fwd
 opaque S : Nat → Nat → Prop
 
 /--
-error: `@[grind →] theorem using_grind_fwd.StransBad` failed to find patterns in the antecedents of the theorem, consider using different options or the `grind_pattern` command
+error: `@[grind →] theorem StransBad` failed to find patterns in the antecedents of the theorem, consider using different options or the `grind_pattern` command
 -/
 #guard_msgs (error) in
 @[grind→] theorem StransBad (a b c d : Nat) : S a b ∨ R a b → S b c → S a c ∧ S b d := sorry
@@ -143,7 +143,7 @@ opaque Q : Nat → Prop
 opaque f : Nat → Nat → Nat
 
 /--
-error: `@[grind →] theorem using_grind_fwd2.pqfBad` failed to find patterns in the antecedents of the theorem, consider using different options or the `grind_pattern` command
+error: `@[grind →] theorem pqfBad` failed to find patterns in the antecedents of the theorem, consider using different options or the `grind_pattern` command
 -/
 #guard_msgs (error) in
 @[grind→] theorem pqfBad : Q x → P (f x y) := sorry
@@ -172,13 +172,13 @@ opaque P : Nat → Nat → Prop
 opaque Q : Nat → Nat → Prop
 
 /--
-error: `@[grind →] theorem using_grind_mixed.pqBad1` failed to find patterns in the antecedents of the theorem, consider using different options or the `grind_pattern` command
+error: `@[grind →] theorem pqBad1` failed to find patterns in the antecedents of the theorem, consider using different options or the `grind_pattern` command
 -/
 #guard_msgs (error) in
 @[grind→] theorem pqBad1 : P x y → Q x z := sorry
 
 /--
-error: `@[grind ←] theorem using_grind_mixed.pqBad2` failed to find patterns in the theorem's conclusion, consider using different options or the `grind_pattern` command
+error: `@[grind ←] theorem pqBad2` failed to find patterns in the theorem's conclusion, consider using different options or the `grind_pattern` command
 -/
 #guard_msgs (error) in
 @[grind←] theorem pqBad2 : P x y → Q x z := sorry

tests/lean/run/grind_ematch_patterns.lean

@@ -1,5 +1,4 @@
 module
-public section -- TODO: Fix error messages with private names.
 def replicate : (n : Nat) → (a : α) → List α
   | 0,   _ => []
   | n+1, a => a :: replicate n a

tests/lean/run/grind_ite.lean

@@ -1,7 +1,7 @@
 module
 public import Std.Data.HashMap
 public import Std.Data.TreeMap
-public section -- TODO: Workaround for private declaration issue
+public section -- TODO: Workaround for private declaration + dot-notation issue
 /-!
 # If normalization