From 81ced3bd0fe7ffab8e6201ee26438d05fecd4dd5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 29 Dec 2023 16:11:08 -0800
Subject: [PATCH] feat: trace `simproc`s

---
 src/Lean/Meta/Tactic/Simp/Simproc.lean    |  8 +++++---
 tests/lean/simprocTrace.lean              | 14 ++++++++++++++
 tests/lean/simprocTrace.lean.expected.out |  1 +
 3 files changed, 20 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/simprocTrace.lean
 create mode 100644 tests/lean/simprocTrace.lean.expected.out

diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean
index ade0d493fe..431b2427c3 100644
--- a/src/Lean/Meta/Tactic/Simp/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean
@@ -138,9 +138,10 @@ def SimprocEntry.try? (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM
   | none => return none
   | some step => return some (← step.addExtraArgs extraArgs)
 
-def simproc? (tag : String) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM (Option Step) := do
+def simproc? (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM (Option Step) := do
   let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
   if candidates.isEmpty then
+    let tag := if post then "post" else "pre"
     trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"
     return none
   else
@@ -148,6 +149,7 @@ def simproc? (tag : String) (s : SimprocTree) (erased : PHashSet Name) (e : Expr
       unless erased.contains simprocEntry.declName do
         if let some step ← simprocEntry.try? numExtraArgs e then
           trace[Debug.Meta.Tactic.simp] "simproc result {e} => {step.result.expr}"
+          recordSimpTheorem (.decl simprocEntry.declName post)
           return some step
     return none
 
@@ -159,11 +161,11 @@ register_builtin_option simprocs : Bool := {
 def preSimproc? (e : Expr) : SimpM (Option Step) := do
   unless simprocs.get (← getOptions) do return none
   let s := (← getMethods).simprocs
-  simproc? "pre" s.pre s.erased e
+  simproc? (post := false) s.pre s.erased e
 
 def postSimproc? (e : Expr) : SimpM (Option Step) := do
   unless simprocs.get (← getOptions) do return none
   let s := (← getMethods).simprocs
-  simproc? "post" s.post s.erased e
+  simproc? (post := true) s.post s.erased e
 
 end Lean.Meta.Simp
diff --git a/tests/lean/simprocTrace.lean b/tests/lean/simprocTrace.lean
new file mode 100644
index 0000000000..9ce59a2159
--- /dev/null
+++ b/tests/lean/simprocTrace.lean
@@ -0,0 +1,14 @@
+import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Offset
+
+def foo (x : Nat) : Nat :=
+  x + 10
+
+simproc reduce_foo (foo _) := fun e => open Lean Meta in do
+  let some n ← evalNat e.appArg! |>.run | return none
+  return some (.done { expr := mkNatLit (n+10) })
+
+set_option tactic.simp.trace true
+example : x + foo 2 = 12 + x := by
+  simp
+  rw [Nat.add_comm]
diff --git a/tests/lean/simprocTrace.lean.expected.out b/tests/lean/simprocTrace.lean.expected.out
new file mode 100644
index 0000000000..3be1a6624f
--- /dev/null
+++ b/tests/lean/simprocTrace.lean.expected.out
@@ -0,0 +1 @@
+Try this: simp only [reduce_foo]