feat: improve simp theorem tracing

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

@@ -166,6 +166,7 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
     | none   => pure ()
   match (← unfold? e) with
   | some e' =>
+    trace[Meta.Tactic.simp.rewrite] "unfold {mkConst e.getAppFn.constName!}, {e} ==> {e'}"
     recordSimpTheorem e.getAppFn.constName!
     reduce e'
   | none => return e

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

@@ -62,7 +62,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
       else
         let proof ← instantiateMVars (mkAppN val xs)
         if (← hasAssignableMVar proof) then
-          trace[Meta.Tactic.simp.rewrite] "{thm}, has unassigned metavariables after unification"
+          trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, has unassigned metavariables after unification"
           return none
         pure <| some proof
       let rhs := (← instantiateMVars type).appArg!
@@ -70,9 +70,9 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
         return none
       if thm.perm then
         if !(← Expr.acLt rhs e) then
-          trace[Meta.Tactic.simp.rewrite] "{thm}, perm rejected {e} ==> {rhs}"
+          trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, perm rejected {e} ==> {rhs}"
           return none
-      trace[Meta.Tactic.simp.rewrite] "{thm}, {e} ==> {rhs}"
+      trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, {e} ==> {rhs}"
       recordSimpTheorem thm.name
       return some { expr := rhs, proof? }
     else
@@ -80,7 +80,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
         -- We do not report unification failures when `lhs` is a metavariable
         -- Example: `x = ()`
         -- TODO: reconsider if we want thms such as `(x : Unit) → x = ()`
-        trace[Meta.Tactic.simp.unify] "{thm}, failed to unify{indentExpr lhs}\nwith{indentExpr e}"
+        trace[Meta.Tactic.simp.unify] "{← ppSimpTheorem thm}, failed to unify{indentExpr lhs}\nwith{indentExpr e}"
       return none
   /- Check whether we need something more sophisticated here.
      This simple approach was good enough for Mathlib 3 -/

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

@@ -84,8 +84,12 @@ instance : ToFormat SimpTheorem where
     let prio := f!":{s.priority}"
     name ++ prio ++ perm
 
-instance : ToMessageData SimpTheorem where
-  toMessageData s := format s
+@[specialize] def SimpTheorem.toMessageDataM [Monad m]
+    (resolve : Name → m MessageData) (s : SimpTheorem) : m MessageData := do
+  let perm := if s.perm then ":perm" else ""
+  let name ← resolve s.name
+  let prio := m!":{s.priority}"
+  return name ++ prio ++ perm
 
 instance : BEq SimpTheorem where
   beq e₁ e₂ := e₁.proof == e₂.proof

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

@@ -102,6 +102,16 @@ def getSimpCongrTheorems : M SimpCongrTheorems :=
 def recordSimpTheorem (n : Name) : SimpM Unit :=
   modify fun s => { s with usedTheorems := s.usedTheorems.insert n }
 
+def ppSimpTheorem (s : SimpTheorem) : SimpM MessageData :=
+  s.toMessageDataM fun n => do
+    if (← getEnv).contains n then
+      return ← mkConstWithLevelParams n
+    if (← getLCtx).contains ⟨n⟩ then
+      return mkFVar ⟨n⟩
+    if let some stx := (← read).namedStx.find? n then
+      return stx
+    return n
+
 end Simp
 
 export Simp (SimpM)

tests/lean/1079.lean.expected.out

@@ -1,12 +1,12 @@
 1079.lean:3:2-6:12: error: alternative 'isFalse' has not been provided
-[Meta.Tactic.simp.rewrite] _uniq.82:1000, m ==> n
-[Meta.Tactic.simp.rewrite] eq_self:1000, n = n ==> True
-[Meta.Tactic.simp.unify] ite_self:1000, failed to unify
+[Meta.Tactic.simp.rewrite] h:1000, m ==> n
+[Meta.Tactic.simp.rewrite] @eq_self:1000, n = n ==> True
+[Meta.Tactic.simp.unify] @ite_self:1000, failed to unify
       if ?c then ?a else ?a
     with
       if True then Ordering.eq else Ordering.gt
-[Meta.Tactic.simp.rewrite] ite_true:1000, if True then Ordering.eq else Ordering.gt ==> Ordering.eq
-[Meta.Tactic.simp.unify] eq_self:1000, failed to unify
+[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then Ordering.eq else Ordering.gt ==> Ordering.eq
+[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
       ?a = ?a
     with
       Ordering.eq = Ordering.lt