feat: add seval

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -273,9 +273,23 @@ def rewritePost (rflOnly := false) : Simproc := fun e => do
   return .continue
 
 /--
-Try to unfold ground term when `Context.unfoldGround := true`.
+Discharge procedure for the ground/symbolic evaluator.
 -/
-def simpGround : Simproc := fun e => do
+def dischargeGround (e : Expr) : SimpM (Option Expr) := do
+  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
+  let r ← simp e
+  if r.expr.consumeMData.isConstOf ``True then
+    try
+      return some (← mkOfEqTrue (← r.getProof))
+    catch _ =>
+      return none
+  else
+    return none
+
+/--
+Try to unfold ground term in the ground/symbolic evaluator.
+-/
+def sevalGround : Simproc := fun e => do
   -- Ground term unfolding is disabled.
   unless (← getContext).unfoldGround do return .continue
   -- `e` is not a ground term.
@@ -308,7 +322,70 @@ def simpGround : Simproc := fun e => do
   trace[Meta.Tactic.simp.ground] "delta, {e} => {eNew}"
   return .visit { expr := eNew }
 
-partial def preDefault (s : SimprocsArray) : Simproc :=
+partial def preSEval (s : SimprocsArray) : Simproc :=
+  rewritePre >>
+  simpMatch >>
+  userPreSimprocs s
+
+def postSEval (s : SimprocsArray) : Simproc :=
+  rewritePost >>
+  userPostSimprocs s >>
+  sevalGround >>
+  simpCtorEq
+
+def mkSEvalMethods : CoreM Methods := do
+  let s ← getSEvalSimprocs
+  return {
+    pre        := preSEval #[s]
+    post       := postSEval #[s]
+    discharge? := dischargeGround
+  }
+
+def mkSEvalContext : CoreM Context := do
+  let s ← getSEvalTheorems
+  let c ← Meta.getSimpCongrTheorems
+  return { simpTheorems := #[s], congrTheorems := c, unfoldGround := true }
+
+/--
+Invoke ground/symbolic evaluator from `simp`.
+It uses the `seval` theorems and simprocs.
+-/
+def seval (e : Expr) : SimpM Result := do
+  let m ← mkSEvalMethods
+  let ctx ← mkSEvalContext
+  let cacheSaved := (← get).cache
+  let cacheGroundSaved := (← get).cacheGround
+  let usedTheoremsSaved := (← get).usedTheorems
+  try
+    withReader (fun _ => m.toMethodsRef) do
+    withTheReader Simp.Context (fun _ => ctx) do
+    modify fun s => { s with cache := {}, usedTheorems := {} }
+    simp e
+  finally
+    modify fun s => { s with cache := cacheSaved, cacheGround := cacheGroundSaved, usedTheorems := usedTheoremsSaved }
+
+/--
+Try to unfold ground term in the ground/symbolic evaluator.
+-/
+def simpGround : Simproc := fun e => do
+  -- Ground term unfolding is disabled.
+  unless (← getContext).unfoldGround do return .continue
+  -- `e` is not a ground term.
+  unless !e.hasExprMVar && !e.hasFVar do return .continue
+  -- Check whether `e` is a constant application
+  let f := e.getAppFn
+  let .const declName _ := f | return .continue
+  -- If declaration has been marked to not be unfolded, return none.
+  let ctx ← getContext
+  if ctx.simpTheorems.isErased (.decl declName) then return .continue
+  -- Matcher applications should have been reduced before we get here.
+  if (← isMatcher declName) then return .continue
+  trace[Meta.Tactic.Simp.ground] "seval: {e}"
+  let r ← seval e
+  trace[Meta.Tactic.Simp.ground] "seval result: {e} => {r.expr}"
+  return .done r
+
+def preDefault (s : SimprocsArray) : Simproc :=
   rewritePre >>
   simpMatch >>
   userPreSimprocs s >>

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

@@ -44,6 +44,9 @@ structure Context where
   - When `unfoldGround := true` and term is not ground, we set `unfoldGround := false` when visiting instance implicit
     arguments. Reason: We don't want to unfold instance implicit arguments of non-ground applications.
   - When `unfoldGround := true` and term is ground, we try to unfold it during post-visit.
+
+  TODO: try to remove this flag. It would be great if the `simpGround` method did not have to rely
+  on this flag. Possible solution: use `parent?` to decide whether to unfold or not.
   -/
   unfoldGround      : Bool := config.ground
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
@@ -64,7 +67,7 @@ abbrev UsedSimps := HashMap Origin Nat
 
 structure State where
   cache        : Cache := {}
-  /-- Cache for `unfoldGround := true` -/
+  /-- Cache for `unfoldGround := true`. If we manage to remove the `unfoldGround`, then we can also remove this field. -/
   cacheGround  : Cache := {}
   congrCache   : CongrCache := {}
   usedTheorems : UsedSimps := {}
@@ -222,11 +225,12 @@ def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
 
 @[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
   let cacheSaved := (← get).cache
+  let cacheGroundSaved := (← get).cacheGround
   modify fun s => { s with cache := {} }
   try
     withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
   finally
-    modify fun s => { s with cache := cacheSaved }
+    modify fun s => { s with cache := cacheSaved, cacheGround := cacheGroundSaved }
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
   modify fun s => if s.usedTheorems.contains thmId then s else