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))
 

Tactics/BvOmegaBench.lean

@@ -10,48 +10,105 @@ 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
 
+
+-- Adapted mkSimpContext:
+-- from https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Simp.lean#L287
+def bvOmegaSimpCtx : MetaM (Simp.Context ×  Array Simp.Simprocs) := do
+  let mut simprocs := #[]
+  let mut simpTheorems := #[]
+
+  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,
 with the goal state that is being run, and the time elapsed to solve the goal is written.
+
+Code adapted from: 
+- https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Simp.lean#L406
+- https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Omega/Frontend.lean#L685
 -/
-def run : TacticM Unit := do
+def run (g : MVarId) : MetaM Unit := do
   let minMs ← getBvOmegaBenchMinMs
-  let goal ← getMainGoal
-  let goalStr ← ppGoal goal
+  let goalStr ← ppGoal g
   let startTime ← IO.monoMsNow
+  let filePath ← getBvOmegaBenchFilePath
+  if (← getBvOmegaBenchIsEnabled) then do
+    IO.FS.withFile filePath IO.FS.Mode.append fun h => do
+        h.putStrLn "\n---\n"
+        h.putStrLn s!"goal"
+        h.putStrLn goalStr.pretty
+        h.putStrLn s!"endgoal"
   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"
+      g.withContext do
+        let (bvToNatSimpCtx, bvToNatSimprocs) ← bvOmegaSimpCtx
+        let nonDepHyps ← g.getNondepPropHyps
+        let mut g := g
+
+        try
+          let (result?, _stats) ← 
+            simpGoal g bvToNatSimpCtx bvToNatSimprocs
+              (simplifyTarget := true) (discharge? := .none) nonDepHyps
+          let .some (_, g') := result? | return ()
+          g := g'
+        catch e => 
+          trace[simp_mem.info] "in BvOmega, ran `simp only [bv_toNat]` and got error: {indentD e.toMessageData}"
+          throw e
+
+        g.withContext do 
+          let some g ← g.falseOrByContra | return ()
+          g.withContext do
+            let hyps := (← getLocalHyps).toList
+            omega hyps g {}
+            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 s!"time"
+                h.putStrLn s!"{delta}"
   catch e =>
+    let endTime ← IO.monoMsNow
+    let delta := endTime - startTime
+    IO.FS.withFile filePath IO.FS.Mode.append fun h => do
+      if delta >= minMs then
+        h.putStrLn s!"time"
+        h.putStrLn s!"{delta}"
+        h.putStrLn s!"error"
+        h.putStrLn s!"{← e.toMessageData.toString}"
     throw e
   return ()
 
+
 end BvOmegaBench
 
 syntax (name := bvOmegaBenchTac) "bv_omega_bench" : tactic
 
 @[tactic bvOmegaBenchTac]
 def bvOmegaBenchImpl : Tactic
 | `(tactic| bv_omega_bench) =>
-   BvOmegaBench.run
+    liftMetaFinishingTactic fun g => do
+      BvOmegaBench.run g
 | _ => throwUnsupportedSyntax