Lean4
/-- Evaluates an expression `e` into a normalized representation as a polynomial.
This is a variant of `Mathlib.Tactic.Ring.eval`, the main driver of the `ring` tactic.
It differs in
* operating on `Expr` (input) and `Simp.Result` (output), rather than typed `Qq` versions of these;
* throwing an error if the expression `e` is an atom for the `ring` tactic.
-/
def evalExpr (e : Expr) : AtomM Simp.Result := do
let e ← withReducible <| whnf e
guard e.isApp
let ⟨u, α, e⟩ ← inferTypeQ' e
let sα ← synthInstanceQ q(CommSemiring $α)
let c ← mkCache sα
let ⟨a, _, pa⟩ ←
match ← isAtomOrDerivable q($sα) c q($e) with
| none =>
eval sα c e
| some none =>
failure
| some (some r) =>
pure r
pure { expr := a, proof? := pa }
