feat: include counters for unfolded declarations at simp diagnostics

src/Lean/Elab/Tactic/Simp.lean

@@ -414,9 +414,9 @@ where
     return stats
 
 def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
-  -- TODO: collect current unfolding diag info
+  let origDiag := (← getThe Meta.State).diag
   let stats ← x
-  Simp.reportDiag stats
+  Simp.reportDiag stats origDiag
   return ()
 
 /-

src/Lean/Meta/Diagnostics.lean

@@ -18,6 +18,15 @@ def collectAboveThreshold [BEq α] [Hashable α] (counters : PHashMap α Nat) (t
       r := r.push (declName, counter)
   return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then lt d₁ d₂ else c₁ > c₂
 
+def subCounters [BEq α] [Hashable α] (newCounters oldCounters : PHashMap α Nat) : PHashMap α Nat := Id.run do
+  let mut result := {}
+  for (a, counterNew) in newCounters do
+    if let some counterOld := oldCounters.find? a then
+      result := result.insert a (counterNew - counterOld)
+    else
+      result := result.insert a counterNew
+  return result
+
 structure DiagSummary where
   data  : Array MessageData := #[]
   max   : Nat := 0
@@ -36,17 +45,17 @@ def mkDiagSummary (counters : PHashMap Name Nat) (threshold : Nat) (p : Name →
       data := data.push m!"{if data.isEmpty then "  " else "\n"}{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
     return { data, max := entries[0]!.2 }
 
-def mkDiagSummaryForUnfolded (instances := false) : MetaM DiagSummary := do
+def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do
   let threshold := diagnostics.threshold.get (← getOptions)
   let env ← getEnv
-  mkDiagSummary (← get).diag.unfoldCounter threshold fun declName =>
+  mkDiagSummary counters threshold fun declName =>
     getReducibilityStatusCore env declName matches .semireducible
     && isInstanceCore env declName == instances
 
-def mkDiagSummaryForUnfoldedReducible : MetaM DiagSummary := do
+def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary := do
   let threshold := diagnostics.threshold.get (← getOptions)
   let env ← getEnv
-  mkDiagSummary (← get).diag.unfoldCounter threshold fun declName =>
+  mkDiagSummary counters threshold fun declName =>
     getReducibilityStatusCore env declName matches .reducible
 
 def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
@@ -63,9 +72,10 @@ def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSumm
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
     let threshold := diagnostics.threshold.get (← getOptions)
-    let unfoldDefault ← mkDiagSummaryForUnfolded
-    let unfoldInstance ← mkDiagSummaryForUnfolded (instances := true)
-    let unfoldReducible ← mkDiagSummaryForUnfoldedReducible
+    let unfoldCounter := (← get).diag.unfoldCounter
+    let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
+    let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
+    let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
     let heu ← mkDiagSummary (← get).diag.heuristicCounter threshold
     let inst ← mkDiagSummaryForUsedInstances
     unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do

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

@@ -28,14 +28,21 @@ def mkSimpDiagSummary (counters : PHashMap Origin Nat) : MetaM DiagSummary := do
       data := data.push m!"{if data.isEmpty then "  " else "\n"}{key} ↦ {counter}"
     return { data, max := entries[0]!.2 }
 
-def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
+def reportDiag (diag : Simp.Diagnostics) (diagOrig : Meta.Diagnostics) : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
     let used ← mkSimpDiagSummary diag.usedThmCounter
     let tried ← mkSimpDiagSummary diag.triedThmCounter
-    unless used.isEmpty && tried.isEmpty do
+    let unfoldCounter := subCounters (← get).diag.unfoldCounter diagOrig.unfoldCounter
+    let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
+    let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
+    let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
+    unless used.isEmpty && tried.isEmpty && unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty do
       let m := MessageData.nil
       let m := appendSection m `simp "used theorems" used
       let m := appendSection m `simp "tried theorems" tried
+      let m := appendSection m `reduction "unfolded declarations" unfoldDefault
+      let m := appendSection m `reduction "unfolded instances" unfoldInstance
+      let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
       let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
       logInfo m
 

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

@@ -664,10 +664,11 @@ def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods :=
     return (r, { s with })
 where
   simpMain (e : Expr) : SimpM Result := withCatchingRuntimeEx do
+    let origDiag := (← getThe Meta.State).diag
     try
       withoutCatchingRuntimeEx <| simp e
     catch ex =>
-      reportDiag (← get).diag
+      reportDiag (← get).diag origDiag
       if ex.isRuntime then
         throwNestedTacticEx `simp ex
       else
@@ -679,10 +680,11 @@ def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Method
     pure (r, { s with })
 where
   dsimpMain (e : Expr) : SimpM Expr := withCatchingRuntimeEx do
+    let origDiag := (← getThe Meta.State).diag
     try
       withoutCatchingRuntimeEx <| dsimp e
     catch ex =>
-      reportDiag (← get).diag
+      reportDiag (← get).diag origDiag
       if ex.isRuntime then
         throwNestedTacticEx `simp ex
       else

tests/lean/run/simpDiag.lean

@@ -35,7 +35,7 @@ def ack : Nat → Nat → Nat
 info: [simp] used theorems (max: 1201, num: 3):
     ack.eq_3 ↦ 1201
   ⏎
-  Nat.reduceAdd ↦ 771
+  Nat.reduceAdd (builtin simproc) ↦ 771
   ⏎
   ack.eq_1 ↦ 768[simp] tried theorems (max: 3262, num: 3):
     BitVec.of_length_zero ↦ 3262
@@ -57,7 +57,7 @@ example : ack 4 4 = x := by
 info: [simp] used theorems (max: 19, num: 5):
     ack.eq_3 ↦ 19
   ⏎
-  Nat.reduceAdd ↦ 9
+  Nat.reduceAdd (builtin simproc) ↦ 9
   ⏎
   ack.eq_1 ↦ 7
   ⏎
@@ -84,3 +84,30 @@ example : ack 4 4 = x := by
   set_option diagnostics true in
   set_option diagnostics.threshold 0 in
   simp [ack.eq_2, ack.eq_1, ack.eq_3]
+
+@[reducible] def h (x : Nat) :=
+  match x with
+  | 0 => 10
+  | x + 1 => h x
+
+opaque q1 : Nat → Nat → Prop
+@[simp] axiom q1_ax (x : Nat) : q1 x 10
+
+/--
+info: [simp] used theorems (max: 1, num: 1):
+    q1_ax ↦ 1[simp] tried theorems (max: 7, num: 2):
+    BitVec.of_length_zero ↦ 7
+  ⏎
+  q1_ax ↦ 1[reduction] unfolded declarations (max: 287, num: 2):
+    Nat.rec ↦ 287
+  ⏎
+  OfNat.ofNat ↦ 28[reduction] unfolded instances (max: 14, num: 1):
+    instOfNatNat ↦ 14[reduction] unfolded reducible declarations (max: 287, num: 2):
+    h ↦ 287
+   Nat.casesOn ↦ 287use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+example : q1 x (h 40) := by
+  set_option diagnostics true in
+  set_option diagnostics.threshold 0 in
+  simp