feat: finishTrace

Author: leodemoura

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

@@ -6,11 +6,37 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
+import Init.Grind.Interactive
+import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Tactic.Grind.Action
+import Lean.Meta.Tactic.Grind.EMatchAction
+import Lean.Meta.Tactic.Grind.Split
 namespace Lean.Elab.Tactic.Grind
 open Meta
 open Meta.Grind
 
+def withTracing (x : GrindTacticM α) : GrindTacticM α := do
+  withReader (fun ctx => { ctx with ctx.config.trace := true }) x
 
+def mkFinish (maxIterations : Nat) : IO Action := do
+  let solvers ← Solvers.mkAction
+  return Action.checkTactic >> (Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext).loop maxIterations
+
+def maxIterations := 1000 -- **TODO**: Add option
+
+@[builtin_grind_tactic finishTrace] def evalFinishTrace : GrindTactic := fun stx => do
+  let a ← mkFinish maxIterations
+  let goal ← getMainGoal
+  withTracing do
+  match (← liftGrindM <| a.run goal) with
+  | .closed seq =>
+    replaceMainGoal []
+    let seq := Action.mkGrindSeq seq
+    Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax seq }
+  | .stuck gs =>
+    let goal :: _ := gs | throwError "`finish?` failed, but resulting goal is not available"
+    let params := (← read).params
+    let result ← liftGrindM do mkResult params (some goal)
+    throwError "`finish?` failed\n{← result.toMessageData}"
 
 end Lean.Elab.Tactic.Grind

src/Lean/Meta/Tactic/Grind.lean

@@ -24,7 +24,6 @@ public import Lean.Meta.Tactic.Grind.Ctor
 public import Lean.Meta.Tactic.Grind.Parser
 public import Lean.Meta.Tactic.Grind.EMatchTheorem
 public import Lean.Meta.Tactic.Grind.EMatch
-public import Lean.Meta.Tactic.Grind.EMatchAction
 public import Lean.Meta.Tactic.Grind.Main
 public import Lean.Meta.Tactic.Grind.CasesMatch
 public import Lean.Meta.Tactic.Grind.Arith
@@ -44,9 +43,8 @@ public import Lean.Meta.Tactic.Grind.PropagateInj
 public import Lean.Meta.Tactic.Grind.Order
 public import Lean.Meta.Tactic.Grind.Anchor
 public import Lean.Meta.Tactic.Grind.Action
-
+public import Lean.Meta.Tactic.Grind.EMatchAction
 public section
-
 namespace Lean
 
 /-! Trace options for `grind` users -/

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

@@ -6,15 +6,20 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Action
+public import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
+public section
 namespace Lean.Meta.Grind.Action
 
-def Action.instantiate : Action := fun goal kna kp => do
+def instantiate' : Action := fun goal kna kp => do
   let (progress, goal') ← GoalM.run goal ematch
   -- **TODO**: filter relevant instances
   if progress then
     concatTactic (← kp goal') `(grind| instantiate)
   else
     kna goal
 
+def instantiate : Action :=
+  instantiate' >> assertAll
+
 end Lean.Meta.Grind.Action