test: constant pattern

src/Lean/Meta/Tactic/Grind.lean

@@ -71,5 +71,6 @@ builtin_initialize registerTraceClass `grind.debug.matchCond
 builtin_initialize registerTraceClass `grind.debug.matchCond.lambda
 builtin_initialize registerTraceClass `grind.debug.matchCond.proveFalse
 builtin_initialize registerTraceClass `grind.debug.mbtc
+builtin_initialize registerTraceClass `grind.debug.ematch
 
 end Lean

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

@@ -197,9 +197,22 @@ private partial def processOffset (c : Choice) (pArg : Expr) (k : Nat) (e : Expr
     curr ← getNext curr
     if isSameExpr curr e then break
 
+/--
+Retuns "applications" in the given goal that may match `p`.
+We say "applications," because we assume a constant is a zero-ary application.
+-/
+private def getAppsOf (p : Expr) : GoalM (Option (List Expr)) := do
+  if p.isConst then
+    if (← alreadyInternalized p) then
+      return some [p]
+    else
+      return none
+  else
+    return (← get).appMap.find? p.toHeadIndex
+
 /-- Processes `continue` contraint used to implement multi-patterns. -/
 private def processContinue (c : Choice) (p : Expr) : M Unit := do
-  let some apps := (← getThe Goal).appMap.find? p.toHeadIndex
+  let some apps ← getAppsOf p
     | return ()
   let maxGeneration ← getMaxGeneration
   for app in apps do
@@ -331,7 +344,7 @@ private def processChoices : M Unit := do
       | .continue p :: cnstrs => processContinue { c with cnstrs } p
 
 private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
-  let some apps := (← getThe Goal).appMap.find? p.toHeadIndex
+  let some apps ← getAppsOf p
     | return ()
   let numParams  := (← read).thm.numParams
   let assignment := .replicate numParams unassigned

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

@@ -333,7 +333,7 @@ private def saveBVar (idx : Nat) : M Unit := do
   modify fun s => { s with bvarsFound := s.bvarsFound.insert idx }
 
 private def getPatternFn? (pattern : Expr) : Option Expr :=
-  if !pattern.isApp then
+  if !pattern.isApp && !pattern.isConst then
     none
   else match pattern.getAppFn with
     | f@(.const declName _) => if isForbidden declName then none else some f

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

@@ -116,14 +116,19 @@ private def mkENode' (e : Expr) (generation : Nat) : GoalM Unit :=
 
 /-- Internalizes the nested ground terms in the given pattern. -/
 private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
-  if pattern.isBVar || isPatternDontCare pattern then
-    return pattern
-  else if let some e := groundPattern? pattern then
-    let e ← preprocessGroundPattern e
-    internalize e generation none
-    return mkGroundPattern e
-  else pattern.withApp fun f args => do
-    return mkAppN f (← args.mapM (internalizePattern · generation))
+  -- Recall that it is important to ensure patterns are maximally shared since
+  -- we assume that in functions such as `getAppsOf` in `EMatch.lean`
+  go (← shareCommon pattern)
+where
+  go (pattern : Expr) : GoalM Expr := do
+    if pattern.isBVar || isPatternDontCare pattern then
+      return pattern
+    else if let some e := groundPattern? pattern then
+      let e ← preprocessGroundPattern e
+      internalize e generation none
+      return mkGroundPattern e
+    else pattern.withApp fun f args => do
+      return mkAppN f (← args.mapM go)
 
 /-- Internalizes the `MatchCond` gadget. -/
 private def internalizeMatchCond (matchCond : Expr) (generation : Nat) : GoalM Unit := do
@@ -228,8 +233,11 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
         internalizeImpl b generation e
         registerParent e b
       propagateUp e
-  | .lit .. | .const .. =>
+  | .lit .. =>
     mkENode e generation
+  | .const declName _ =>
+    mkENode e generation
+    activateTheoremPatterns declName generation
   | .mvar .. =>
     reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
     mkENode' e generation

tests/lean/run/grind_const_pattern.lean

@@ -0,0 +1,76 @@
+set_option grind.warning false
+%reset_grind_attrs
+
+attribute [grind] List.map_append
+
+def a := 10
+
+example : a = 5 + 5 := by
+  grind [a]
+
+/--
+error: `grind` failed
+case grind
+h : ¬a = 10
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬a = 10
+  [eqc] False propositions
+    [prop] a = 10
+-/
+#guard_msgs (error) in
+example : a = 5 + 5 := by
+  grind
+
+section
+attribute [local grind] a
+
+example : a = 5 + 5 := by
+  grind
+end
+
+def f (x : Nat) := x + 1
+
+theorem fa : f a = 11 := rfl
+
+example : f a = 10 + 1 := by
+  grind [fa]
+
+/--
+error: `grind` failed
+case grind
+h : ¬f a = 11
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬f a = 11
+  [eqc] False propositions
+    [prop] f a = 11
+-/
+#guard_msgs (error) in
+example : f a = 10 + 1 := by
+  grind
+
+attribute [grind] fa
+
+example : f a = 10 + 1 := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+x : Nat
+h : ¬f x = 11
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬f x = 11
+  [eqc] False propositions
+    [prop] f x = 11
+  [ematch] E-matching patterns
+    [thm] fa: [f `[a]]
+-/
+#guard_msgs (error) in
+example : f x = 10 + 1 := by
+  grind