# HG changeset patch
# User nipkow
# Date 1709031587 -3600
# Node ID 9c00a46d69d09634e802e7726de4214198e979aa
# Parent  6dbe7910dcfc72cd8b63b90b391335f33bd88024
new simplifier trace_op for tracing simproc calls

diff -r 6dbe7910dcfc -r 9c00a46d69d0 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Tue Feb 27 10:49:48 2024 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML	Tue Feb 27 11:59:47 2024 +0100
@@ -396,7 +396,8 @@
 val _ = Theory.setup
   (Simplifier.set_trace_ops
     {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term,
-     trace_apply = simp_apply})
+     trace_apply = simp_apply,
+     trace_simproc = fn _ => fn ctxt => fn cont => cont ctxt})
 
 val _ =
   Protocol_Command.define "Simplifier_Trace.reply"
diff -r 6dbe7910dcfc -r 9c00a46d69d0 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Feb 27 10:49:48 2024 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Feb 27 11:59:47 2024 +0100
@@ -867,14 +867,17 @@
 type trace_ops =
  {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
   trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
-    Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
+    Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option,
+  trace_simproc: {name: string, goal: cterm} ->
+    Proof.context -> (Proof.context -> thm option) -> thm option};
 
 structure Trace_Ops = Theory_Data
 (
   type T = trace_ops;
   val empty: T =
    {trace_invoke = fn _ => fn ctxt => ctxt,
-    trace_apply = fn _ => fn ctxt => fn cont => cont ctxt};
+    trace_apply = fn _ => fn ctxt => fn cont => cont ctxt,
+    trace_simproc = fn _ => fn ctxt => fn cont => cont ctxt};
   fun merge (trace_ops, _) = trace_ops;
 );
 
@@ -883,6 +886,7 @@
 val trace_ops = Trace_Ops.get o Proof_Context.theory_of;
 fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt;
 fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt;
+fun trace_simproc args ctxt = #trace_simproc (trace_ops ctxt) args ctxt;
 
 
 
@@ -1057,8 +1061,11 @@
           if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then
             (cond_tracing' ctxt simp_debug (fn () =>
               print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
-             (let val ctxt' = Config.put simp_trace (Config.get ctxt simp_debug) ctxt
-              in case Morphism.form_context' ctxt' proc eta_t' of
+             (let
+                val ctxt' = Config.put simp_trace (Config.get ctxt simp_debug) ctxt
+                val res = trace_simproc {name = name, goal = eta_t'} ctxt'
+                  (fn ctxt'' => Morphism.form_context' ctxt'' proc eta_t')
+              in case res of
                 NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
               | SOME raw_thm =>
                   (cond_tracing ctxt (fn () =>