tracing facilities for the code generator preprocessor

--- a/NEWS	Sat Jun 28 22:13:21 2014 +0200
+++ b/NEWS	Sat Jun 28 22:13:23 2014 +0200
@@ -169,6 +169,9 @@
 (only makes sense in practice, if outer syntax is delimited
 differently).
 
+* Code generator preprocessor: explicit control of simp tracing
+on a per-constant basis.  See attribute "code_preproc".
+
 * Command 'print_term_bindings' supersedes 'print_binds' for clarity,
 but the latter is retained some time as Proof General legacy.
 

--- a/src/Pure/Isar/code.ML	Sat Jun 28 22:13:21 2014 +0200
+++ b/src/Pure/Isar/code.ML	Sat Jun 28 22:13:23 2014 +0200
@@ -891,7 +891,7 @@
 end;
 
 
-(* code certificate access *)
+(* code certificate access with preprocessing *)
 
 fun retrieve_raw thy c =
   Symtab.lookup ((the_functions o the_exec) thy) c
@@ -918,7 +918,7 @@
   end;
 
 fun cert_of_eqns_preprocess ctxt functrans c =
-  perhaps (perhaps_loop (perhaps_apply functrans))
+  (perhaps o perhaps_loop o perhaps_apply) functrans
   #> (map o apfst) (preprocess eqn_conv ctxt)
   #> cert_of_eqns ctxt c;
 

--- a/src/Tools/Code/code_preproc.ML	Sat Jun 28 22:13:21 2014 +0200
+++ b/src/Tools/Code/code_preproc.ML	Sat Jun 28 22:13:23 2014 +0200
@@ -32,6 +32,11 @@
   val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'b), consts: string list }
     -> ({ algebra: code_algebra, eqngr: code_graph } -> Proof.context -> term -> 'a)
     -> Proof.context -> term -> 'b
+
+  val trace_none: Context.generic -> Context.generic
+  val trace_all: Context.generic -> Context.generic
+  val trace_only: string list -> Context.generic -> Context.generic
+  val trace_only_ext: string list -> Context.generic -> Context.generic
 end
 
 structure Code_Preproc : CODE_PREPROC =
@@ -268,6 +273,41 @@
   end;
 
 
+(** simplifier tracing **)
+
+structure Trace_Switch = Generic_Data
+(
+  type T = string list option;
+  val empty = SOME [];
+  val extend = I;
+  fun merge (NONE, d2) = NONE
+    | merge (d1, NONE) = NONE
+    | merge (SOME cs1, SOME cs2) = SOME (Library.merge (op =) (cs1, cs2));
+);
+
+val trace_none = Trace_Switch.put (SOME []);
+
+val trace_all = Trace_Switch.put NONE;
+
+fun gen_trace_only prep_const raw_cs context =
+  let
+    val cs = map (prep_const (Context.theory_of context)) raw_cs;
+  in Trace_Switch.put (SOME cs) context end;
+
+val trace_only = gen_trace_only (K I);
+val trace_only_ext = gen_trace_only Code.read_const;
+
+fun switch_trace c ctxt =
+  let
+    val d = Trace_Switch.get (Context.Proof ctxt);
+    val switch = case d of NONE => true | SOME cs => member (op =) cs c;
+    val _ = if switch
+      then tracing ("Preprocessing function equations for "
+        ^ Code.string_of_const (Proof_Context.theory_of ctxt) c)
+      else ();
+  in Config.put simp_trace switch ctxt end;
+
+
 (** the Waisenhaus algorithm **)
 
 (* auxiliary *)
@@ -321,7 +361,7 @@
         val thy = Proof_Context.theory_of ctxt;
         val functrans = (map (fn (_, (_, f)) => f ctxt)
           o #functrans o the_thmproc) thy;
-        val cert = Code.get_cert ctxt functrans c;
+        val cert = Code.get_cert (switch_trace c ctxt) functrans c;
         val (lhs, rhss) =
           Code.typargs_deps_of_cert thy cert;
       in ((lhs, rhss), cert) end;

--- a/src/Tools/Code_Generator.thy	Sat Jun 28 22:13:21 2014 +0200
+++ b/src/Tools/Code_Generator.thy	Sat Jun 28 22:13:23 2014 +0200
@@ -16,6 +16,15 @@
 
 ML_file "~~/src/Tools/cache_io.ML"
 ML_file "~~/src/Tools/Code/code_preproc.ML"
+
+attribute_setup code_preproc_trace = {*
+  (Scan.lift (Args.$$$ "off" >> K Code_Preproc.trace_none)
+  || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
+       >> Code_Preproc.trace_only_ext
+  || Scan.succeed Code_Preproc.trace_all)
+  >> (Thm.declaration_attribute o K)
+*} "tracing of the code generator preprocessor"
+
 ML_file "~~/src/Tools/Code/code_symbol.ML"
 ML_file "~~/src/Tools/Code/code_thingol.ML"
 ML_file "~~/src/Tools/Code/code_simp.ML"