feat: add SolverExtension.action and Solvers.mkAction (#10836)

This PR implements support for `Action` in the `grind` solver extensions
(`SolverExtension`). It also provides the `Solvers.mkAction` function
that constructs an `Action` using all registered solvers. The generated
action is "fair," that is, a solver cannot prevent other solvers from
making progress.

Author: leodemoura

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

@@ -37,8 +37,8 @@ builtin_initialize
     (internalize := AC.internalize)
     (newEq       := AC.processNewEq)
     (newDiseq    := AC.processNewDiseq)
+    (action      := Action.ac)
     (check       := AC.check')
     (checkInv    := AC.checkInvariants)
-    (mkTactic?   := return some (← `(grind| ac)))
 
 end Lean.Meta.Grind.AC

src/Lean/Meta/Tactic/Grind/AC/Eq.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.AC.Util
-public import Lean.Meta.Tactic.Grind.CheckResult
 import Lean.Meta.Tactic.Grind.AC.DenoteExpr
 import Lean.Meta.Tactic.Grind.AC.Proof
 import Lean.Meta.Tactic.Grind.AC.Seq

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

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.CheckResult
 public section
 namespace Lean.Meta.Grind
 /-!
@@ -69,42 +68,20 @@ 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 TGrind)
-  | /--
-    The action could not make further progress.
-    `gs` are subgoals that could not be closed. They are used for producing error messages.
-    -/
-    stuck (gs : List Goal)
-
 def ActionResult.toMessageData : ActionResult → MessageData
   | .closed seq => m!"closed {seq}"
   | .stuck goals => m!"stuck {goals.map (·.mvarId)}"
 
 instance : ToMessageData ActionResult where
   toMessageData := ActionResult.toMessageData
 
-abbrev ActionCont : Type :=
-  Goal → GrindM ActionResult
-
-abbrev Action : Type :=
-  Goal → (kna : ActionCont) → (kp : ActionCont) → GrindM ActionResult
-
 namespace Action
 
 def skip : Action := fun goal _ kp =>
   kp goal
 
-def notApplicable : Action := fun goal kna _ =>
-  kna goal
-
 /--
 If the `goal` is already inconsistent, returns `.closed []`. Otherwise, executes
 then not applicable continuation.

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -53,8 +53,8 @@ builtin_initialize
     (internalize := CommRing.internalize)
     (newEq       := CommRing.processNewEq)
     (newDiseq    := CommRing.processNewDiseq)
+    (action      := Action.ring)
     (check       := CommRing.check')
     (checkInv    := CommRing.checkInvariants)
-    (mkTactic?   := return some (← `(grind| ring)))
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-public import Lean.Meta.Tactic.Grind.CheckResult
 import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.Util

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

@@ -49,9 +49,9 @@ builtin_initialize
     (internalize := Cutsat.internalize)
     (newEq       := Cutsat.processNewEq)
     (newDiseq    := Cutsat.processNewDiseq)
+    (action      := Action.lia)
     (check       := Cutsat.check)
     (checkInv    := Cutsat.checkInvariants)
     (mbtc        := Cutsat.mbtc)
-    (mkTactic?   := return some (← `(grind| lia)))
 
 end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Linear.lean

@@ -48,9 +48,9 @@ builtin_initialize
     (internalize := Linear.internalize)
     (newEq       := Linear.processNewEq)
     (newDiseq    := Linear.processNewDiseq)
+    (action      := Action.linarith)
     (check       := Linear.check)
     (checkInv    := Linear.checkInvariants)
     (mbtc        := Linear.mbtc)
-    (mkTactic?   := return some (← `(grind| linarith)))
 
 end Lean.Meta.Grind.Arith.Linear

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Init.Data.Repr
 public section
 namespace Lean.Meta.Grind
 /--

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

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Simp.Types
 public import Lean.Meta.Tactic.Grind.AlphaShareCommon
 public import Lean.Meta.Tactic.Grind.Attr
+public import Lean.Meta.Tactic.Grind.CheckResult
 public import Init.Data.Queue
 import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.HeadIndex
@@ -1493,6 +1494,38 @@ def withoutModifyingState (x : GoalM α) : GoalM α := do
 @[extern "lean_grind_canon"] -- Forward definition
 opaque canon (e : Expr) : GoalM Expr
 
+/-!
+`Action` is the *control interface* for `grind`’s search steps. It is defined in
+Continuation-Passing Style (CPS).
+See `Grind/Action.lean` for additional details.
+-/
+
+abbrev TGrind := TSyntax `grind
+
+/-- 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 TGrind)
+  | /--
+    The action could not make further progress.
+    `gs` are subgoals that could not be closed. They are used for producing error messages.
+    -/
+    stuck (gs : List Goal)
+
+abbrev ActionCont : Type :=
+  Goal → GrindM ActionResult
+
+abbrev Action : Type :=
+  Goal → (kna : ActionCont) → (kp : ActionCont) → GrindM ActionResult
+
+@[expose] def Action.notApplicable : Action := fun goal kna _ =>
+  kna goal
+
+instance : Inhabited Action where
+  default := Action.notApplicable
+
 /-!
 Solver Extensions
 -/
@@ -1508,9 +1541,9 @@ structure SolverExtension (σ : Type) where private mk ::
   newEq       : Expr → Expr → GoalM Unit
   newDiseq    : Expr → Expr → GoalM Unit
   mbtc        : GoalM Bool
-  check       : GoalM Bool
+  action      : Action
+  check       : GoalM Bool -- **TODO**: Consider deleting `check` in the future.
   checkInv    : GoalM Unit
-  mkTactic?   : CoreM (Option (TSyntax `grind))
   deriving Inhabited
 
 private builtin_initialize solverExtensionsRef : IO.Ref (Array (SolverExtension SolverExtensionState)) ← IO.mkRef #[]
@@ -1530,10 +1563,10 @@ def registerSolverExtension {σ : Type} (mkInitial : IO σ) : IO (SolverExtensio
     internalize := fun _ _ => return ()
     newEq := fun _ _ => return ()
     newDiseq := fun _ _ => return ()
+    action := Action.notApplicable
     check := fun _ _ => return false
     checkInv := fun _ _ => return ()
     mbtc := fun _ _ => return false
-    mkTactic? := return none
   }
   solverExtensionsRef.modify fun exts => exts.push (unsafe unsafeCast ext)
   return ext
@@ -1548,16 +1581,16 @@ def SolverExtension.setMethods (ext : SolverExtension σ)
     (newEq       : Expr → Expr → GoalM Unit := fun _ _ => return ())
     (newDiseq    : Expr → Expr → GoalM Unit := fun _ _ => return ())
     (mbtc        : GoalM Bool := return false)
+    (action      : Action := Action.notApplicable)
     (check       : GoalM Bool := return false)
     (checkInv    : GoalM Unit := return ())
-    (mkTactic?   : CoreM (Option (TSyntax `grind)) := return none)
     : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register `grind` solver, extensions can only be registered during initialization")
   unless ext.id < (← solverExtensionsRef.get).size do
     throw (IO.userError "failed to register `grind` solver methods, invalid solver id")
   solverExtensionsRef.modify fun exts => exts.modify ext.id fun s => { s with
-    internalize, newEq, newDiseq, mbtc, check, checkInv, mkTactic?
+    internalize, newEq, newDiseq, mbtc, action, check, checkInv
   }
 
 /-- Returns initial state for registered solvers. -/
@@ -1621,6 +1654,31 @@ def Solvers.mbtc : GoalM Bool := do
       result := true
   return result
 
+/--
+Sequential conjunction: executes both `x` and `y`.
+
+- Runs `x` and always runs `y` afterward, regardless of whether `x` made progress.
+- It is not applicable only if both `x` and `y` are not applicable.
+-/
+def Action.andAlso (x y : Action) : Action := fun goal kna kp => do
+  x goal (fun goal => y goal kna kp) (fun goal => y goal kp kp)
+
+/-
+Creates an action that tries all solver extensions. It uses the `Action.andAlso`
+to combine them.
+-/
+def Solvers.mkAction : IO Action := do
+  let exts ← solverExtensionsRef.get
+  let rec go (i : Nat) (acc : Action) : Action :=
+    if h : i < exts.size then
+      go (i+1) (acc.andAlso exts[i].action)
+    else
+      acc
+  if h : 0 < exts.size then
+    return go 1 exts[0].action
+  else
+    return Action.notApplicable
+
 /--
 Given a new disequality `lhs ≠ rhs`, propagates it to relevant theories.
 -/