Lean4
/-- Runs a tactic in the `AtomM.RecurseM` monad, given initial data:
* `s`: a reference to the mutable `AtomM` state, for persisting across calls.
This ensures that atom ordering is used consistently.
* `cfg`: the configuration options
* `eval`: a normalization operation which will be run recursively, potentially dependent on a known
atom ordering
* `simp`: a cleanup operation which will be used to post-process expressions
* `x`: the tactic to run
-/
partial def run {α : Type} (s : IO.Ref State) (cfg : Recurse.Config) (eval : Expr → AtomM Simp.Result)
(simp : Simp.Result → MetaM Simp.Result) (x : RecurseM α) : MetaM α := do
let ctx ←
Simp.mkContext { zetaDelta := cfg.zetaDelta, singlePass := true } (simpTheorems :=
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) { }]) (congrTheorems := ← getSimpCongrTheorems)
let nctx := { ctx, simp }
let rec /-- The recursive context. -/
rctx := { red := cfg.red, evalAtom }, /-- The atom evaluator calls `AtomM.onSubexpressions` recursively. -/
evalAtom e := onSubexpressions eval e false nctx rctx s
withConfig ({ · with zetaDelta := cfg.zetaDelta }) <| x nctx rctx s
