feat: "performance" counters for grind (#6834)

This PR adds "performance" counters (e.g., number of instances per
theorem) to `grind`. The counters are always reported on failures, and
on successes when `set_option diagnostics true`.

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

@@ -94,6 +94,29 @@ structure Result where
   issues   : List MessageData
   config   : Grind.Config
   trace    : Trace
+  counters : Counters
+
+private def countersToMessageData (header : String) (cls : Name) (data : Array (Name × Nat)) : MetaM MessageData := do
+  let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
+  let data ← data.mapM fun (declName, counter) =>
+    return .trace { cls } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
+  return .trace { cls } header data
+
+def Counters.toMessageData? (cs : Counters) : MetaM (Option MessageData) := do
+  let thms := cs.thm.toList.toArray.filterMap fun (origin, c) =>
+    match origin with
+    | .decl declName => some (declName, c)
+    | _ => none
+  let mut msgs := #[]
+  unless thms.isEmpty do
+    msgs := msgs.push <| (← countersToMessageData "E-Matching instances" `thm thms)
+  let cases := cs.case.toList.toArray
+  unless cases.isEmpty do
+    msgs := msgs.push <| (← countersToMessageData "Case splits" `cases cases)
+  if msgs.isEmpty then
+    return none
+  else
+    return some <| .trace { cls := `grind } "Counters" msgs
 
 def Result.hasFailures (r : Result) : Bool :=
   !r.failures.isEmpty
@@ -106,16 +129,24 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
     issues := .trace { cls := `issue } m #[] :: issues
   unless issues.isEmpty do
     msgs := msgs ++ [.trace { cls := `grind } "Issues" issues.reverse.toArray]
+  if let some msg ← result.counters.toMessageData? then
+    msgs := msgs ++ [msg]
   return MessageData.joinSep msgs m!"\n"
 
 def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM Result := do
   let go : GrindM Result := do
     let goals ← initCore mvarId params
     let (failures, skipped) ← solve goals fallback
     trace[grind.debug.final] "{← ppGoals goals}"
-    let issues := (← get).issues
-    let trace := (← get).trace
-    return { failures, skipped, issues, config := params.config, trace }
+    let issues   := (← get).issues
+    let trace    := (← get).trace
+    let counters := (← get).counters
+    if failures.isEmpty then
+      -- If there are no failures and diagnostics are enabled, we still report the performance counters.
+      if (← isDiagnosticsEnabled) then
+        if let some msg ← counters.toMessageData? then
+          logInfo msg
+    return { failures, skipped, issues, config := params.config, trace, counters }
   go.run mainDeclName params fallback
 
 end Lean.Meta.Grind

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

@@ -105,15 +105,15 @@ private def ppEqcs : M Unit := do
      pushMsg <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
 
 private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
-  let m := m!"{← thm.origin.pp}:\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
+  let m := m!"{← thm.origin.pp}: {thm.patterns.map ppPattern}"
   return .trace { cls := `thm } m #[]
 
 private def ppActiveTheorems : M Unit := do
   let goal ← read
   let m ← goal.thms.toArray.mapM fun thm => ppEMatchTheorem thm
   let m := m ++ (← goal.newThms.toArray.mapM fun thm => ppEMatchTheorem thm)
   unless m.isEmpty do
-    pushMsg <| .trace { cls := `ematch } "E-matching" m
+    pushMsg <| .trace { cls := `ematch } "E-matching patterns" m
 
 private def ppOffset : M Unit := do
   let goal ← read

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

@@ -82,6 +82,13 @@ structure Trace where
   cases      : PHashSet Name := {}
   deriving Inhabited
 
+structure Counters where
+  /-- Number of times E-match theorem has been instantiated. -/
+  thm  : PHashMap Origin Nat := {}
+  /-- Number of times a `cases` has been performed on an inductive type/predicate -/
+  case : PHashMap Name Nat := {}
+  deriving Inhabited
+
 /-- State for the `GrindM` monad. -/
 structure State where
   /-- `ShareCommon` (aka `Hashconsing`) state. -/
@@ -110,6 +117,8 @@ structure State where
   issues     : List MessageData := []
   /-- `trace` for `grind?` -/
   trace      : Trace := {}
+  /-- Performance counters -/
+  counters   : Counters := {}
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 private def MethodsRef : Type := MethodsRefPointed.type
@@ -139,13 +148,25 @@ def getMainDeclName : GrindM Name :=
 def saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit := do
   if (← getConfig).trace then
     modify fun s => { s with trace.thms := s.trace.thms.insert { origin := thm.origin, kind := thm.kind } }
+  modify fun s => { s with
+    counters.thm := if let some n := s.counters.thm.find? thm.origin then
+      s.counters.thm.insert thm.origin (n+1)
+    else
+      s.counters.thm.insert thm.origin 1
+  }
 
 def saveCases (declName : Name) (eager : Bool) : GrindM Unit := do
   if (← getConfig).trace then
     if eager then
       modify fun s => { s with trace.eagerCases := s.trace.eagerCases.insert declName }
     else
       modify fun s => { s with trace.cases := s.trace.cases.insert declName }
+  modify fun s => { s with
+    counters.case := if let some n := s.counters.case.find? declName then
+      s.counters.case.insert declName (n+1)
+    else
+      s.counters.case.insert declName 1
+  }
 
 @[inline] def getMethodsRef : GrindM MethodsRef :=
   read
@@ -168,9 +189,9 @@ Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
 been hash-consed. We perform this step before we internalize expressions.
 -/
 def shareCommon (e : Expr) : GrindM Expr := do
-  modifyGet fun { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues, trace } =>
+  modifyGet fun { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues, trace, counters } =>
     let (e, scState) := ShareCommon.State.shareCommon scState e
-    (e, { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues, trace })
+    (e, { scState, nextThmIdx, congrThms, trueExpr, falseExpr, natZExpr, simpStats, lastTag, issues, trace, counters })
 
 /-- Returns `true` if `e` is the internalized `True` expression.  -/
 def isTrueExpr (e : Expr) : GrindM Bool :=

tests/lean/run/grind_ematch2.lean

@@ -40,6 +40,47 @@ example (as bs cs : Array α) (v₁ v₂ : α)
         : cs[j] = as[j] := by
   grind
 
+/--
+info: [grind] Counters
+  [thm] E-Matching instances
+    [thm] Array.get_set_ne ↦ 3
+    [thm] Array.size_set ↦ 3
+  [cases] Case splits
+    [cases] And ↦ 2
+---
+info: [diag] Diagnostics
+  [reduction] unfolded declarations (max: 11822, num: 2):
+    [reduction] LT.lt ↦ 11822
+    [reduction] getElem ↦ 64
+  [reduction] unfolded instances (max: 32, num: 1):
+    [reduction] Array.instGetElemNatLtSize ↦ 32
+  [reduction] unfolded reducible declarations (max: 7079, num: 7):
+    [reduction] Array.size ↦ 7079
+    [reduction] Array.toList ↦ 1885
+    [reduction] autoParam ↦ 1694
+    [reduction] outParam ↦ 124
+    [reduction] Ne ↦ 57
+    [reduction] GT.gt ↦ 40
+    [reduction] List.casesOn ↦ 24
+  [def_eq] heuristic for solving `f a =?= f b` (max: 5067, num: 2):
+    [def_eq] Nat.lt ↦ 5067
+    [def_eq] List.length ↦ 1691
+  [kernel] unfolded declarations (max: 106, num: 5):
+    [kernel] LT.lt ↦ 106
+    [kernel] outParam ↦ 46
+    [kernel] Array.size ↦ 36
+    [kernel] Array.toList ↦ 31
+    [kernel] autoParam ↦ 26
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+---
+info: [grind.ematch.instance] Array.size_set: (cs.set i₃ v₃ ⋯).size = cs.size
+[grind.ematch.instance] Array.size_set: (bs.set i₂ v₂ ⋯).size = bs.size
+[grind.ematch.instance] Array.size_set: (as.set i₁ v₁ ⋯).size = as.size
+[grind.ematch.instance] Array.get_set_ne: ∀ (hj : j < cs.size), i₃ ≠ j → (cs.set i₃ v₃ ⋯)[j] = cs[j]
+[grind.ematch.instance] Array.get_set_ne: ∀ (hj : j < bs.size), i₂ ≠ j → (bs.set i₂ v₂ ⋯)[j] = bs[j]
+[grind.ematch.instance] Array.get_set_ne: ∀ (hj : j < as.size), i₁ ≠ j → (as.set i₁ v₁ ⋯)[j] = as[j]
+-/
+#guard_msgs (info) in
 example (as bs cs ds : Array α) (v₁ v₂ v₃ : α)
         (i₁ i₂ i₃ j : Nat)
         (h₁ : i₁ < as.size)
@@ -52,6 +93,7 @@ example (as bs cs ds : Array α) (v₁ v₂ v₃ : α)
         (h₇ : j < ds.size)
         (h₈ : j < as.size)
         : ds[j] = as[j] := by
+  set_option diagnostics true in
   grind
 
 opaque f (a b : α) : α := a

tests/lean/run/grind_params.lean

@@ -44,11 +44,9 @@ x✝ : ¬R x
     [prop] P x
   [eqc] False propositions
     [prop] R x
-  [ematch] E-matching
-    [thm] pq:
-        ∀ {x : Nat}, P x → Q x
-        patterns: [Q #1]
-    [thm] qr: ∀ {x : Nat}, Q x → R x patterns: [Q #1]
+  [ematch] E-matching patterns
+    [thm] pq: [Q #1]
+    [thm] qr: [Q #1]
 -/
 #guard_msgs (error) in
 example : P x → R x := by

tests/lean/run/grind_pre.lean

@@ -34,6 +34,9 @@ h : c = true
     [eqc] {b = true, a = false}
     [eqc] {b, false}
     [eqc] {a, c, true}
+[grind] Counters
+  [cases] Case splits
+    [cases] And ↦ 2
 -/
 #guard_msgs (error) in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@@ -66,6 +69,10 @@ h : b = false
   [eqc] Equivalence classes
     [eqc] {b, false}
     [eqc] {a, c, true}
+[grind] Counters
+  [cases] Case splits
+    [cases] And ↦ 3
+    [cases] Or ↦ 3
 -/
 #guard_msgs (error) in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by