feat: compact notation for inspecting grind state (#10828)

This PR implements a compact notation for inspecting the `grind` state
in interactive mode. Within a `grind` tactic block, each tactic may
optionally have a suffix of the form `| filter?`.

Examples:

```lean
instantiate | gen > 0  -- Displays terms in the `grind` state after executing `instantiate` with generation greater than zero
```

```lean
instantiate |  -- Displays the `grind` state after executing `instantiate`
```

Remark: If the user places the cursor one space before `|`, the state
*before* executing `instantiate` is displayed.
This PR removes the code that was silently displaying the `grind` state
after each tactic step, as it was too noisy.
It also updates the notation for the `first` combinator in the `grind`
tactic mode to avoid conflicts with the new syntax.

Author: leodemoura

src/Init/Grind/Interactive.lean

@@ -17,13 +17,32 @@ when selecting patterns.
 syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
 
 namespace Grind
+declare_syntax_cat grind_filter (behavior := both)
+
+syntax:max ident : grind_filter
+syntax:max &"gen" " < "  num  : grind_filter
+syntax:max &"gen" " = "  num  : grind_filter
+syntax:max &"gen" " != " num  : grind_filter
+syntax:max &"gen" " ≤ "  num  : grind_filter
+syntax:max &"gen" " <= " num  : grind_filter
+syntax:max &"gen" " > "  num  : grind_filter
+syntax:max &"gen" " ≥ "  num  : grind_filter
+syntax:max &"gen" " >= " num  : grind_filter
+syntax:max "(" grind_filter ")" : grind_filter
+syntax:35 grind_filter:35 " && " grind_filter:36 : grind_filter
+syntax:35 grind_filter:35 " || " grind_filter:36 : grind_filter
+syntax:max "!" grind_filter:40 : grind_filter
+
+syntax grindFilter := (colGt grind_filter)?
 
 /-- `grind` is the syntax category for a "grind interactive tactic".
 A `grind` tactic is a program which receives a `grind` goal. -/
 declare_syntax_cat grind (behavior := both)
 
-syntax grindSeq1Indented := sepBy1IndentSemicolon(grind)
-syntax grindSeqBracketed := "{" withoutPosition(sepByIndentSemicolon(grind)) "}"
+syntax grindStep := grind ("|" (colGt ppSpace grind_filter)?)?
+
+syntax grindSeq1Indented := sepBy1IndentSemicolon(grindStep)
+syntax grindSeqBracketed := "{" withoutPosition(sepByIndentSemicolon(grindStep)) "}"
 syntax grindSeq := grindSeqBracketed <|> grindSeq1Indented
 
 /-- `(grindSeq)` runs the `grindSeq` in sequence on the current list of targets.
@@ -50,24 +69,6 @@ syntax thm := anchor <|> grindLemma <|> grindLemmaMin
 /-- Instantiates theorems using E-matching. -/
 syntax (name := instantiate) "instantiate" (colGt thm),* : grind
 
-declare_syntax_cat grind_filter (behavior := both)
-
-syntax:max ident : grind_filter
-syntax:max &"gen" " < "  num  : grind_filter
-syntax:max &"gen" " = "  num  : grind_filter
-syntax:max &"gen" " != " num  : grind_filter
-syntax:max &"gen" " ≤ "  num  : grind_filter
-syntax:max &"gen" " <= " num  : grind_filter
-syntax:max &"gen" " > "  num  : grind_filter
-syntax:max &"gen" " ≥ "  num  : grind_filter
-syntax:max &"gen" " >= " num  : grind_filter
-syntax:max "(" grind_filter ")" : grind_filter
-syntax:35 grind_filter:35 " && " grind_filter:36 : grind_filter
-syntax:35 grind_filter:35 " || " grind_filter:36 : grind_filter
-syntax:max "!" grind_filter:40 : grind_filter
-
-syntax grindFilter := (colGt grind_filter)?
-
 -- **Note**: Should we rename the following tactics to `trace_`?
 /-- Shows asserted facts. -/
 syntax (name := showAsserted) "show_asserted" ppSpace grindFilter : grind
@@ -145,10 +146,10 @@ macro:1 x:grind tk:" <;> " y:grind:2 : grind => `(grind|
     all_goals $y:grind)
 
 /-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
-syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "| " grindSeq)+) : grind
+syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "(" grindSeq ")")+) : grind
 
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
-macro "try " t:grindSeq : grind => `(grind| first | $t | skip)
+macro "try " t:grindSeq : grind => `(grind| first ($t:grindSeq) (skip))
 
 /-- `fail_if_success t` fails if the tactic `t` succeeds. -/
 syntax (name := failIfSuccess) "fail_if_success " grindSeq : grind
@@ -168,7 +169,7 @@ The tactic `tac` should eventually fail, otherwise `repeat tac` will run indefin
 syntax "repeat " grindSeq : grind
 
 macro_rules
-  | `(grind| repeat $seq) => `(grind| first | ($seq); repeat $seq | skip)
+  | `(grind| repeat $seq:grindSeq) => `(grind| first (($seq); repeat $seq:grindSeq) (skip))
 
 /-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
 syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : grind

src/Lean/Elab/Tactic/Grind.lean

@@ -8,5 +8,5 @@ prelude
 public import Lean.Elab.Tactic.Grind.Main
 public import Lean.Elab.Tactic.Grind.Basic
 public import Lean.Elab.Tactic.Grind.BuiltinTactic
-public import Lean.Elab.Tactic.Grind.Show
+public import Lean.Elab.Tactic.Grind.ShowState
 public import Lean.Elab.Tactic.Grind.Have

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

@@ -87,19 +87,6 @@ def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx
 def mkInitialTacticInfo (stx : Syntax) : GrindTacticM (GrindTacticM Info) := do
   let mctxBefore  ← getMCtx
   let goalsBefore ← getUnsolvedGoalMVarIds
-  /-
-  **Note**: We only display the grind state if there is exactly one goal.
-  This is a hack because we currently use a silent info to display the grind state, and we cannot attach it after each goal.
-  We claim this is not a big deal since the user will probably use `next =>` to focus on subgoals.
-  -/
-  if let [goal]  ← getGoals then goal.withContext do
-    let config := (← read).params.config
-    let msg := MessageData.lazy fun ctx => do
-      let .ok msg ← EIO.toBaseIO <| ctx.runMetaM
-          <| Grind.goalDiagToMessageData goal config (header := "Grind state") (collapsedMain := false)
-        | return "Grind state could not be generated"
-      return msg
-    logAt (severity := .information) (isSilent := true) stx msg
   return mkTacticInfo mctxBefore goalsBefore stx
 
 @[inline] def withTacticInfoContext (stx : Syntax) (x : GrindTacticM α) : GrindTacticM α := do

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

@@ -24,12 +24,26 @@ import Lean.Meta.Tactic.ExposeNames
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.RenameInaccessibles
 import Lean.Elab.Tactic.Grind.Filter
+import Lean.Elab.Tactic.Grind.ShowState
 namespace Lean.Elab.Tactic.Grind
 
+def showStateAt (ref : Syntax) (filter : Filter) : GrindTacticM Unit := do
+  if let goalBefore :: _ := (← getGoals) then
+    withRef ref <| goalBefore.withContext <| showState filter (isSilent := true)
+  else
+    logAt ref (severity := .information) (isSilent := true) "no grind state"
+
 def evalSepTactics (stx : Syntax) : GrindTacticM Unit := do
   for arg in stx.getArgs, i in *...stx.getArgs.size do
     if i % 2 == 0 then
-      evalGrindTactic arg
+      match arg with
+      | `(Parser.Tactic.Grind.grindStep| $tac:grind) => evalGrindTactic tac
+      | `(Parser.Tactic.Grind.grindStep| $tac:grind | $[$filter?]?) =>
+        let filter ← elabFilter filter?
+        showStateAt arg filter
+        evalGrindTactic tac
+        showStateAt arg[1] filter
+      | _ => throwUnsupportedSyntax
     else
       saveTacticInfoForToken arg
 
@@ -371,15 +385,14 @@ public def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIden
   replaceMainGoal []
 
 @[builtin_grind_tactic «first»] partial def evalFirst : GrindTactic := fun stx => do
-  let tacs := stx[1].getArgs
-  if tacs.isEmpty then throwUnsupportedSyntax
-  loop tacs 0
+  let `(grind| first $[($s:grindSeq)]*) := stx | throwUnsupportedSyntax
+  loop s 0
 where
-  loop (tacs : Array Syntax) (i : Nat) :=
-    if i == tacs.size - 1 then
-      evalGrindTactic tacs[i]![1]
+  loop (s : Array (TSyntax ``Parser.Tactic.Grind.grindSeq)) (i : Nat) :=
+    if i == s.size - 1 then
+      evalGrindTactic s[i]!
     else
-      evalGrindTactic tacs[i]![1] <|> loop tacs (i+1)
+      evalGrindTactic s[i]! <|> loop s (i+1)
 
 @[builtin_grind_tactic failIfSuccess] def evalFailIfSuccess : GrindTactic := fun stx =>
   Term.withoutErrToSorry <| withoutRecover do

src/Lean/Elab/Tactic/Grind/Show.lean src/Lean/Elab/Tactic/Grind/ShowState.leansrc/Lean/Elab/Tactic/Grind/Show.lean renamed to src/Lean/Elab/Tactic/Grind/ShowState.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
-import Lean.Elab.Tactic.Grind.Filter
+public import Lean.Elab.Tactic.Grind.Filter
 import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Anchor
 import Lean.Meta.Tactic.Grind.Split
@@ -92,15 +92,18 @@ def ppEqcs? (filter : Filter) (collapsed := false) : GrindTacticM (Option Messag
 def pushIfSome (msgs : Array MessageData) (msg? : Option MessageData) : Array MessageData :=
   if let some msg := msg? then msgs.push msg else msgs
 
-@[builtin_grind_tactic showState] def evalShowState : GrindTactic := fun stx => withMainContext do
-  let `(grind| show_state $[$filter?]?) := stx | throwUnsupportedSyntax
-  let filter ← elabFilter filter?
+public def showState (filter : Filter) (isSilent := false) : GrindTacticM Unit := do
   let msgs := #[]
   let msgs := pushIfSome msgs (← ppAsserted? filter (collapsed := true))
   let msgs := pushIfSome msgs (← ppProps? filter true (collapsed := false))
   let msgs := pushIfSome msgs (← ppProps? filter false (collapsed := false))
   let msgs := pushIfSome msgs (← ppEqcs? filter (collapsed := false))
-  logInfo <| MessageData.trace { cls := `grind, collapsed := false } "Grind state" msgs
+  logAt (← getRef) (severity := .information) (isSilent := isSilent) <| MessageData.trace { cls := `grind, collapsed := false } "Grind state" msgs
+
+@[builtin_grind_tactic Parser.Tactic.Grind.showState] def evalShowState : GrindTactic := fun stx => withMainContext do
+  let `(grind| show_state $[$filter?]?) := stx | throwUnsupportedSyntax
+  let filter ← elabFilter filter?
+  showState filter
 
 @[builtin_grind_tactic showCases] def evalShowCases : GrindTactic := fun stx => withMainContext do
   let `(grind| show_cases $[$filter?]?) := stx | throwUnsupportedSyntax

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

@@ -68,12 +68,15 @@ use `callCC` here.
 
 -/
 
+abbrev TGrind := TSyntax `grind
+abbrev TGrindStep := TSyntax ``Parser.Tactic.Grind.grindStep
+
 /-- Result type for a `grind` Action -/
 inductive ActionResult where
   | /--
     The goal has been closed, and you can use `seq` to close the goal efficiently.
     -/
-    closed (seq : List (TSyntax `grind))
+    closed (seq : List TGrind)
   | /--
     The action could not make further progress.
     `gs` are subgoals that could not be closed. They are used for producing error messages.
@@ -151,8 +154,16 @@ Executes `x`, but behaves like a `skip` if it is not applicable.
 def skipIfNA (x : Action) : Action := fun goal _ kp =>
   x goal kp kp
 
-def mkGrindSeq (s : List (TSyntax `grind)) : TSyntax ``Parser.Tactic.Grind.grindSeq :=
-  let s := s.map (·.raw)
+/-- ``TSyntax `grind`` => ``TSyntax `Lean.Parser.Tactic.Grind.grindStep`` -/
+def mkGrindStep (t : TGrind) : TGrindStep :=
+  mkNode ``Parser.Tactic.Grind.grindStep #[ t, mkNullNode ]
+
+def TGrindStep.getTactic : TGrindStep → TGrind
+  | `(Parser.Tactic.Grind.grindStep| $tac:grind $[| $_]?) => tac
+  | _ => ⟨mkNullNode⟩
+
+def mkGrindSeq (s : List TGrind) : TSyntax ``Parser.Tactic.Grind.grindSeq :=
+  let s := s.map fun tac => (mkGrindStep tac).raw
   let s := s.intersperse (mkNullNode #[])
   mkNode ``Parser.Tactic.Grind.grindSeq #[
   mkNode ``Parser.Tactic.Grind.grindSeq1Indented #[
@@ -169,7 +180,7 @@ next =>
 ```
 If the list is empty, it returns `next => done`.
 -/
-def mkGrindNext (s : List (TSyntax `grind)) : CoreM (TSyntax `grind) := do
+def mkGrindNext (s : List TGrind) : CoreM TGrind := do
   let s ← if s == [] then pure [← `(grind| done)] else pure s
   let s := mkGrindSeq s
   `(grind| next => $s:grindSeq)
@@ -203,7 +214,7 @@ def ungroup : Action := fun goal _ kp => do
     match r with
     | .closed [tac] =>
       match tac with
-      | `(grind| next => $seq;*) => return .closed seq.getElems.toList
+      | `(grind| next => $seq;*) => return .closed <| seq.getElems.toList.map TGrindStep.getTactic
       | _ => return r
     | _ => return r
   else

tests/lean/run/grind_interactive.lean

@@ -239,13 +239,13 @@ example : h bs = 1 → h as ≠ 0 := by
     skip
     try fail
     fail_if_success fail
-    first | fail | done | skip
+    first (fail) (done) (skip)
     fail "Failed here"
     done
 
 example : h bs = 1 → h as ≠ 0 := by
   grind [h.eq_def] =>
-    instantiate
+    instantiate | as
     cases #ec88
     all_goals instantiate
 
@@ -268,6 +268,12 @@ example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p
     cases?
     sorry
 
+set_option trace.Meta.debug true in
+example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by
+  grind =>
+    cases?
+    sorry
+
 /--
 info: Try these:
   [apply] cases #7a08 for
@@ -395,7 +401,7 @@ example (as bs cs : Array α) (v₁ v₂ : α)
         (h₆ : j < as.size)
         : cs[j] = as[j] := by
   grind =>
-    instantiate Array.getElem_set
+    instantiate Array.getElem_set | gen > 0
     instantiate Array.getElem_set
 
 example (as bs cs : Array α) (v₁ v₂ : α)