chore: add isDebugEnabled to grind

This PR adds `isDebugEnabled` for checking whether `grind.debug` is
set to `true` when `grind` was initialized.

src/Lean/Meta/Tactic/Grind/AC/Eq.lean

@@ -228,7 +228,7 @@ private def EqCnstr.superposeWithAC (c₁ : EqCnstr) : ACM Unit := do
     if lhs₁.sharesVar lhs₂ then
       assert! lhs₁ != lhs₂
       let some (r₁, c, r₂) := lhs₁.superposeAC? lhs₂ | unreachable!
-      if grind.debug.get (← getOptions) then
+      if (← isDebugEnabled) then
         assert! lhs₁ == r₁.union c
         assert! lhs₂ == r₂.union c
       let c ← mkEqCnstr (c₁.rhs.union r₂) (c₂.rhs.union r₁) (.superpose_ac r₁ c r₂ c₁ c₂)
@@ -239,7 +239,7 @@ private def EqCnstr.superposeA (c₁ c₂ : EqCnstr) : ACM Unit := do
   let lhs₂ := c₂.lhs
   assert! lhs₁ != lhs₂
   if let some (p, c, s) := lhs₁.superpose? lhs₂ then
-    if grind.debug.get (← getOptions) then
+    if (← isDebugEnabled) then
       assert! lhs₁ == p ++ c
       assert! lhs₂ == c ++ s
     let c ← mkEqCnstr (c₁.rhs ++ s) (p ++ c₂.rhs) (.superpose p c s c₁ c₂)

src/Lean/Meta/Tactic/Grind/AC/Inv.lean

@@ -53,7 +53,7 @@ def checkStructInvs : ACM Unit := do
   checkDiseqs
 
 public def checkInvariants : GoalM Unit := do
-  unless grind.debug.get (← getOptions) do return ()
+  if (← isDebugEnabled) then
   for opId in *...(← get').structs.size do
     ACM.run opId checkStructInvs
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean

@@ -49,7 +49,7 @@ private def checkRingInvs : RingM Unit := do
   checkDiseqs
 
 def checkInvariants : GoalM Unit := do
-  unless grind.debug.get (← getOptions) do return ()
+  if (← isDebugEnabled) then
   for ringId in *...(← get').rings.size do
     RingM.run ringId do
       assert! (← getRingId) == ringId

src/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.lean

@@ -97,7 +97,7 @@ def checkStructInvs : LinearM Unit := do
   checkDiseqCnstrs
 
 public def checkInvariants : GoalM Unit := do
-  unless grind.debug.get (← getOptions) do return ()
+  if (← isDebugEnabled) then
   for structId in *...(← get').structs.size do
     LinearM.run structId do
       assert! (← getStructId) == structId

src/Lean/Meta/Tactic/Grind/Inv.lean

@@ -119,7 +119,7 @@ def checkProofs : GoalM Unit := do
 
 /-- Checks invariants if `grind.debug` is enabled. -/
 public def checkInvariants (expensive := false) : GoalM Unit := do
-  if grind.debug.get (← getOptions) then
+  if (← isDebugEnabled) then
     for e in (← getExprs) do
       let node ← getENode e
       checkParents node.self

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -119,9 +119,11 @@ def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTacti
   let symPrios := params.symPrios
   let extensions := params.extensions
   let anchorRefs? := params.anchorRefs?
+  let debug := grind.debug.get (← getOptions)
   x (← mkMethods evalTactic?).toMethodsRef
     { config, anchorRefs?, simpMethods, simp, extensions, symPrios
-      trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr }
+      trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr
+      debug }
     |>.run' { scState }
 
 private def mkCleanState (mvarId : MVarId) : GrindM Clean.State := mvarId.withContext do

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -206,7 +206,7 @@ where
 def internalizeCnstr (e : Expr) (kind : CnstrKind) (lhs rhs : Expr) : OrderM Unit := do
   let some c ← mkCnstr? e kind lhs rhs | return ()
   trace[grind.order.internalize] "{c.u}, {c.v}, {c.k}"
-  if grind.debug.get (← getOptions) then
+  if (← isDebugEnabled) then
     if let some h := c.h? then check h
   let u ← mkNode c.u
   let v ← mkNode c.v

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

@@ -167,6 +167,7 @@ structure Context where
   bfalseExpr   : Expr
   ordEqExpr    : Expr -- `Ordering.eq`
   intExpr      : Expr -- `Int`
+  debug        : Bool -- Cached `grind.debug (← getOptions)`
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -252,6 +253,10 @@ abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 @[inline] def mapGrindM [MonadControlT GrindM m] [Monad m] (f : {α : Type} → GrindM α → GrindM α) {α} (x : m α) : m α :=
   controlAt GrindM fun runInBase => f <| runInBase x
 
+/-- Returns `true` if `grind.debug` is set -/
+@[inline] def isDebugEnabled : GrindM Bool :=
+  return (← readThe Context).debug
+
 /--
 Backtrackable state for the `GrindM` monad.
 -/
@@ -1072,7 +1077,7 @@ def markTheoremInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool :=
 
 /-- Adds a new fact `prop` with proof `proof` to the queue for preprocessing and the assertion. -/
 def addNewRawFact (proof : Expr) (prop : Expr) (generation : Nat) (splitSource : SplitSource) : GoalM Unit := do
-  if grind.debug.get (← getOptions) then
+  if (← isDebugEnabled) then
     unless (← withGTransparency <| isDefEq (← inferType proof) prop) do
       throwError "`grind` internal error, trying to assert{indentExpr prop}\n\
         with proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\n\
@@ -1231,7 +1236,7 @@ If `isHEq` is `false`, it pushes `lhs = rhs` with `proof` to `newEqs`.
 Otherwise, it pushes `lhs ≍ rhs`.
 -/
 def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
-  if grind.debug.get (← getOptions) then
+  if (← isDebugEnabled) then
     unless (← alreadyInternalized lhs) do
       throwError "`grind` internal error, lhs of new equality has not been internalized{indentExpr lhs}"
     unless (← alreadyInternalized rhs) do