# HG changeset patch
# User haftmann
# Date 1377198943 -7200
# Node ID 8e8941fea27836e02bfbe383c15a58d7400aa4ee
# Parent  3a93bc5d33707809d928c3e39da8a5ba4946f570
separate tracing option for code_simp

diff -r 3a93bc5d3370 -r 8e8941fea278 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Aug 22 21:15:43 2013 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu Aug 22 21:15:43 2013 +0200
@@ -13,6 +13,7 @@
   val static_conv: theory -> simpset option -> string list -> conv
   val static_tac: theory -> simpset option -> string list -> Proof.context -> int -> tactic
   val setup: theory -> theory
+  val trace: bool Config.T
 end;
 
 structure Code_Simp : CODE_SIMP =
@@ -33,6 +34,18 @@
 fun simpset_default thy = the_default (Simpset.get thy);
 
 
+(* diagonstic *)
+
+val trace = Attrib.setup_config_bool @{binding "code_simp_trace"} (K false);
+
+fun set_trace ctxt =
+  let
+    val global = Config.get ctxt trace;
+  in
+    ctxt |> Config.map Simplifier.simp_trace (fn b => b orelse global)
+  end;
+
+
 (* build simpset and conversion from program *)
 
 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
@@ -49,7 +62,8 @@
 fun simpset_program thy some_ss program =
   simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss);
 
-fun lift_ss_conv f ss ct = f (Simplifier.put_simpset ss (Proof_Context.init_global (theory_of_cterm ct))) ct;
+fun lift_ss_conv f ss ct =
+  f (Proof_Context.init_global (theory_of_cterm ct) |> Simplifier.put_simpset ss |> set_trace) ct;
 
 fun rewrite_modulo thy some_ss program =
   lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program);