feat: improve set_option diagnostics true

src/Lean/Elab/Command.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Gabriel Ebner
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.SetOption

src/Lean/Meta.lean

@@ -49,3 +49,4 @@ import Lean.Meta.LazyDiscrTree
 import Lean.Meta.LitValues
 import Lean.Meta.CheckTactic
 import Lean.Meta.Canonicalizer
+import Lean.Meta.Diagnostics

src/Lean/Meta/Basic.lean

@@ -486,48 +486,6 @@ def recordInstance (declName : Name) : MetaM Unit := do
     let newC := if let some c := instanceCounter.find? declName then c + 1 else 1
     { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC }
 
-def collectAboveThreshold (counters : PHashMap Name Nat) (threshold : Nat) : Array (Name × Nat) := Id.run do
-  let mut r := #[]
-  for (declName, counter) in counters do
-    if counter > threshold then
-      r := r.push (declName, counter)
-  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then d₁.lt d₂ else c₁ > c₂
-
-def mkMessageBodyFor? (counters : PHashMap Name Nat) (threshold : Nat) : Option MessageData := Id.run do
-  let entries := collectAboveThreshold counters threshold
-  if entries.isEmpty then
-    return none
-  else
-    let mut m := MessageData.nil
-    for (declName, counter) in entries do
-      if m matches .nil then
-        m := m!"{declName} ↦ {counter}"
-      else
-        m := m ++ m!"\n{declName} ↦ {counter}"
-    return some m
-
-def appendOptMessageData (m : MessageData) (header : String) (m? : Option MessageData) : MessageData :=
-  if let some m' := m? then
-    if m matches .nil then
-      header ++ indentD m'
-    else
-      m ++ "\n" ++ header ++ indentD m'
-  else
-    m
-
-def reportDiag : MetaM Unit := do
-  if (← isDiagnosticsEnabled) then
-    let threshold := diagnostics.threshold.get (← getOptions)
-    let unfold? := mkMessageBodyFor? (← get).diag.unfoldCounter threshold
-    let heu?    := mkMessageBodyFor? (← get).diag.heuristicCounter threshold
-    let inst?   := mkMessageBodyFor? (← get).diag.instanceCounter threshold
-    if unfold?.isSome || heu?.isSome || inst?.isSome then
-      let m := appendOptMessageData MessageData.nil "unfolded declarations:" unfold?
-      let m := appendOptMessageData m "used instances:" inst?
-      let m := appendOptMessageData m "`isDefEq` heuristic:" heu?
-      let m := m ++ "\nuse `set_option diag.threshold <num>` to control threshold for reporting counters"
-      logInfo m
-
 def getLocalInstances : MetaM LocalInstances :=
   return (← read).localInstances
 

src/Lean/Meta/Diagnostics.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.PrettyPrinter
+import Lean.Meta.Basic
+import Lean.Meta.Instances
+
+namespace Lean.Meta
+
+private def collectAboveThreshold (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool) : Array (Name × Nat) := Id.run do
+  let mut r := #[]
+  for (declName, counter) in counters do
+    if counter > threshold then
+    if p declName then
+      r := r.push (declName, counter)
+  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then d₁.lt d₂ else c₁ > c₂
+
+private def mkMessageBodyFor? (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool := fun _ => true) : MetaM (Option MessageData) := do
+  let entries := collectAboveThreshold counters threshold p
+  if entries.isEmpty then
+    return none
+  else
+    let mut m := MessageData.nil
+    for (declName, counter) in entries do
+      unless m matches .nil do
+        m := m ++ "\n"
+      m := m ++ m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
+    return some m
+
+private def appendOptMessageData (m : MessageData) (header : String) (m? : Option MessageData) : MessageData :=
+  if let some m' := m? then
+    if m matches .nil then
+      header ++ indentD m'
+    else
+      m ++ "\n" ++ header ++ indentD m'
+  else
+    m
+
+def reportDiag : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    let threshold := diagnostics.threshold.get (← getOptions)
+    let mut m := MessageData.nil
+    let env ← getEnv
+    let unfoldDefault? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
+      getReducibilityStatusCore env declName matches .semireducible
+      && !isInstanceCore env declName
+    let unfoldInstance? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
+      getReducibilityStatusCore env declName matches .semireducible
+      && isInstanceCore env declName
+    let unfoldReducible? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
+      getReducibilityStatusCore env declName matches .reducible
+    let heu? ← mkMessageBodyFor? (← get).diag.heuristicCounter threshold
+    let inst? ← mkMessageBodyFor? (← get).diag.instanceCounter threshold
+    if unfoldDefault?.isSome || unfoldInstance?.isSome || unfoldReducible?.isSome || heu?.isSome || inst?.isSome then
+      m := appendOptMessageData m "unfolded declarations:" unfoldDefault?
+      m := appendOptMessageData m "unfolded instances:" unfoldInstance?
+      m := appendOptMessageData m "unfolded reducible declarations:" unfoldReducible?
+      m := appendOptMessageData m "used instances:" inst?
+      m := appendOptMessageData m "`isDefEq` heuristic:" heu?
+      m := m ++ "\nuse `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo m
+
+end Lean.Meta

src/Lean/Meta/Instances.lean

@@ -217,8 +217,11 @@ def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
 def getErasedInstances : CoreM (PHashSet Name) :=
   return Meta.instanceExtension.getState (← getEnv) |>.erased
 
+def isInstanceCore (env : Environment) (declName : Name) : Bool :=
+  Meta.instanceExtension.getState env |>.instanceNames.contains declName
+
 def isInstance (declName : Name) : CoreM Bool :=
-  return Meta.instanceExtension.getState (← getEnv) |>.instanceNames.contains declName
+  return isInstanceCore (← getEnv) declName
 
 def getInstancePriority? (declName : Name) : CoreM (Option Nat) := do
   let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none

src/Lean/ReducibilityAttrs.lean

@@ -14,7 +14,7 @@ Reducibility status for a definition.
 -/
 inductive ReducibilityStatus where
   | reducible | semireducible | irreducible
-  deriving Inhabited, Repr
+  deriving Inhabited, Repr, BEq
 
 builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
   registerPersistentEnvExtension {

tests/lean/run/diagRec.lean

@@ -9,12 +9,13 @@ info: 89
 ---
 info: unfolded declarations:
   Nat.rec ↦ 407
+  Or.rec ↦ 144
+  Acc.rec ↦ 108
+unfolded reducible declarations:
   Nat.casesOn ↦ 352
   Or.casesOn ↦ 144
-  Or.rec ↦ 144
   PProd.fst ↦ 126
-  Acc.rec ↦ 108
-use `set_option diag.threshold <num>` to control threshold for reporting counters
+use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics true in