feat: Switch bvOmegaBench to use MetaM

This allows us to gradually convert all our tactics to `MetaM`,
which provides the correct level to discipline to make sure
that bugs like #154 don't happen anymore.
Also, as a mild bonus, one hopes that eliminating `evalTactic` makes stuff a bit faster,
but I would not hold my breath on this.

Arm/Memory/Common.lean

@@ -290,6 +290,7 @@ def omega (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs
     TacticM.withTraceNode' m!"goal post `bv_toNat` reductions (Note: can be large)" do
       trace[simp_mem.info] "{goal}"
     -- @bollu: TODO: understand what precisely we are recovering from.
+    -- | TODO: replace with bvOmegaBench, and make THAT work in TacticM.
     withoutRecover do
       evalTactic (← `(tactic| bv_omega_bench))
 

Arm/Memory/SeparateAutomation.lean

@@ -123,7 +123,7 @@ def Context.init (cfg : SimpMemConfig) : MetaM Context := do
     LNSymSimpContext
       (config := {failIfUnchanged := false})
       (simp_attrs := #[`bv_toNat])
-      (useDefaultSimprocs := false)
+      (useDefaultSimprocs := true)
   return {cfg, bvToNatSimpCtx, bvToNatSimprocs}
 
 /-- The internal state for the `SimpMemM` monad, recording previously encountered atoms. -/

Tactics/BvOmegaBench.lean

@@ -10,10 +10,36 @@ and allows us to send bug reports to the Lean developers.
 -/
 import Tactics.Attr
 import Lean
-open Lean Elab Meta Tactic
+import Lean.Elab.Tactic.Omega.Frontend
+import Lean.Elab.Tactic.Omega
+import Tactics.Simp
+
+
+open Lean Elab Meta Tactic Omega
 
 namespace BvOmegaBench
 
+
+def bvOmegaSimpCtx : MetaM (Simp.Context ×  Array Simp.Simprocs) := do
+  let mut simprocs := #[] -- #[← Simp.getSimprocs]
+  let mut simpTheorems := #[] -- #[← getSimpTheorems]
+
+  let some ext ← (getSimpExtension? `bv_toNat) 
+    | throwError m!"[omega] Error: unable to find `bv_toNat"
+  simpTheorems := simpTheorems.push (← ext.getTheorems)
+
+  if let some ext ← (Simp.getSimprocExtension? `bv_toNat) then
+    let s ← ext.getSimprocs
+    simprocs := simprocs.push s
+
+  let congrTheorems ← Meta.getSimpCongrTheorems
+  let config : Simp.Config := { failIfUnchanged := false }
+  let ctx : Simp.Context := { config, simpTheorems, congrTheorems }
+  return (ctx, simprocs)
+
+
+
+
 /--
 Run bv_omega, gather the results, and then store them at the value that is given by the option.
 By default, it's stored at `pwd`, with filename `omega-bench`. The file is appended to,
@@ -25,23 +51,33 @@ def run : TacticM Unit := do
   let goalStr ← ppGoal goal
   let startTime ← IO.monoMsNow
   try
-    withMainContext do
-      withoutRecover do
-        evalTactic (← `(tactic| bv_omega))
-        if !(← getBvOmegaBenchIsEnabled) then
-          return ()
-        let endTime ← IO.monoMsNow
-        let delta := endTime - startTime
-        let filePath ← getBvOmegaBenchFilePath
-        IO.FS.withFile filePath IO.FS.Mode.append fun h => do
-          if delta >= minMs then
-            h.putStrLn "\n---\n"
-            h.putStrLn s!"time"
-            h.putStrLn s!"{delta}"
-            h.putStrLn s!"endtime"
-            h.putStrLn s!"goal"
-            h.putStrLn goalStr.pretty
-            h.putStrLn s!"endgoal"
+    liftMetaFinishingTactic fun g => do
+      let some g ← g.falseOrByContra | return ()
+      g.withContext do
+       let (bvToNatSimpCtx, bvToNatSimprocs) ← bvOmegaSimpCtx
+       let nonDepHyps ← g.getNondepPropHyps
+       let (result?, _stats) ← simpGoal g bvToNatSimpCtx bvToNatSimprocs (simplifyTarget := true) (discharge? := .none) nonDepHyps
+       let .some (_, g) := result? | return ()
+
+       g.withContext do
+         let hyps := (← getLocalHyps).toList
+         trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"
+         omega hyps g {}
+         -- evalTactic (← `(tactic| bv_omega))
+         if !(← getBvOmegaBenchIsEnabled) then
+           return ()
+         let endTime ← IO.monoMsNow
+         let delta := endTime - startTime
+         let filePath ← getBvOmegaBenchFilePath
+         IO.FS.withFile filePath IO.FS.Mode.append fun h => do
+           if delta >= minMs then
+             h.putStrLn "\n---\n"
+             h.putStrLn s!"time"
+             h.putStrLn s!"{delta}"
+             h.putStrLn s!"endtime"
+             h.putStrLn s!"goal"
+             h.putStrLn goalStr.pretty
+             h.putStrLn s!"endgoal"
   catch e =>
     throw e
   return ()

Tactics/Simp.lean

@@ -65,6 +65,7 @@ def LNSymSimpContext
     else pure #[]
   let mut all_simprocs := all_simprocs
 
+
   for a in simp_attrs do
     let some ext ← (getSimpExtension? a) |
                    throwError m!"[LNSymSimpContext] Error: {a} simp attribute not found!"
@@ -91,10 +92,12 @@ def LNSymSimpContext
       newThms ← newThms.mapM fixSimpTheoremKey
     const_simpTheorems := newThms.foldl addSimpTheoremEntry const_simpTheorems
 
-  let all_simpTheorems := (#[const_simpTheorems] ++ ext_simpTheorems)
+  let all_simpTheorems := (#[← getSimpTheorems, const_simpTheorems] ++ ext_simpTheorems)
   let (ctx : Simp.Context) := { config := config,
                                 simpTheorems := all_simpTheorems,
                                 congrTheorems := (← Meta.getSimpCongrTheorems) }
+
+
   for s in simprocs do
     all_simprocs ← Simp.SimprocsArray.add all_simprocs s false
   return (ctx, all_simprocs)