tracing facilities for the code generator preprocessor
authorhaftmann
Sat Jun 28 22:13:23 2014 +0200 (2014-06-28)
changeset 57430020cea57eaa4
parent 57429 4aef934d43ad
child 57431 02c408aed5ee
tracing facilities for the code generator preprocessor
NEWS
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code_Generator.thy
     1.1 --- a/NEWS	Sat Jun 28 22:13:21 2014 +0200
     1.2 +++ b/NEWS	Sat Jun 28 22:13:23 2014 +0200
     1.3 @@ -169,6 +169,9 @@
     1.4  (only makes sense in practice, if outer syntax is delimited
     1.5  differently).
     1.6  
     1.7 +* Code generator preprocessor: explicit control of simp tracing
     1.8 +on a per-constant basis.  See attribute "code_preproc".
     1.9 +
    1.10  * Command 'print_term_bindings' supersedes 'print_binds' for clarity,
    1.11  but the latter is retained some time as Proof General legacy.
    1.12  
     2.1 --- a/src/Pure/Isar/code.ML	Sat Jun 28 22:13:21 2014 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Sat Jun 28 22:13:23 2014 +0200
     2.3 @@ -891,7 +891,7 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -(* code certificate access *)
     2.8 +(* code certificate access with preprocessing *)
     2.9  
    2.10  fun retrieve_raw thy c =
    2.11    Symtab.lookup ((the_functions o the_exec) thy) c
    2.12 @@ -918,7 +918,7 @@
    2.13    end;
    2.14  
    2.15  fun cert_of_eqns_preprocess ctxt functrans c =
    2.16 -  perhaps (perhaps_loop (perhaps_apply functrans))
    2.17 +  (perhaps o perhaps_loop o perhaps_apply) functrans
    2.18    #> (map o apfst) (preprocess eqn_conv ctxt)
    2.19    #> cert_of_eqns ctxt c;
    2.20  
     3.1 --- a/src/Tools/Code/code_preproc.ML	Sat Jun 28 22:13:21 2014 +0200
     3.2 +++ b/src/Tools/Code/code_preproc.ML	Sat Jun 28 22:13:23 2014 +0200
     3.3 @@ -32,6 +32,11 @@
     3.4    val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'b), consts: string list }
     3.5      -> ({ algebra: code_algebra, eqngr: code_graph } -> Proof.context -> term -> 'a)
     3.6      -> Proof.context -> term -> 'b
     3.7 +
     3.8 +  val trace_none: Context.generic -> Context.generic
     3.9 +  val trace_all: Context.generic -> Context.generic
    3.10 +  val trace_only: string list -> Context.generic -> Context.generic
    3.11 +  val trace_only_ext: string list -> Context.generic -> Context.generic
    3.12  end
    3.13  
    3.14  structure Code_Preproc : CODE_PREPROC =
    3.15 @@ -268,6 +273,41 @@
    3.16    end;
    3.17  
    3.18  
    3.19 +(** simplifier tracing **)
    3.20 +
    3.21 +structure Trace_Switch = Generic_Data
    3.22 +(
    3.23 +  type T = string list option;
    3.24 +  val empty = SOME [];
    3.25 +  val extend = I;
    3.26 +  fun merge (NONE, d2) = NONE
    3.27 +    | merge (d1, NONE) = NONE
    3.28 +    | merge (SOME cs1, SOME cs2) = SOME (Library.merge (op =) (cs1, cs2));
    3.29 +);
    3.30 +
    3.31 +val trace_none = Trace_Switch.put (SOME []);
    3.32 +
    3.33 +val trace_all = Trace_Switch.put NONE;
    3.34 +
    3.35 +fun gen_trace_only prep_const raw_cs context =
    3.36 +  let
    3.37 +    val cs = map (prep_const (Context.theory_of context)) raw_cs;
    3.38 +  in Trace_Switch.put (SOME cs) context end;
    3.39 +
    3.40 +val trace_only = gen_trace_only (K I);
    3.41 +val trace_only_ext = gen_trace_only Code.read_const;
    3.42 +
    3.43 +fun switch_trace c ctxt =
    3.44 +  let
    3.45 +    val d = Trace_Switch.get (Context.Proof ctxt);
    3.46 +    val switch = case d of NONE => true | SOME cs => member (op =) cs c;
    3.47 +    val _ = if switch
    3.48 +      then tracing ("Preprocessing function equations for "
    3.49 +        ^ Code.string_of_const (Proof_Context.theory_of ctxt) c)
    3.50 +      else ();
    3.51 +  in Config.put simp_trace switch ctxt end;
    3.52 +
    3.53 +
    3.54  (** the Waisenhaus algorithm **)
    3.55  
    3.56  (* auxiliary *)
    3.57 @@ -321,7 +361,7 @@
    3.58          val thy = Proof_Context.theory_of ctxt;
    3.59          val functrans = (map (fn (_, (_, f)) => f ctxt)
    3.60            o #functrans o the_thmproc) thy;
    3.61 -        val cert = Code.get_cert ctxt functrans c;
    3.62 +        val cert = Code.get_cert (switch_trace c ctxt) functrans c;
    3.63          val (lhs, rhss) =
    3.64            Code.typargs_deps_of_cert thy cert;
    3.65        in ((lhs, rhss), cert) end;
     4.1 --- a/src/Tools/Code_Generator.thy	Sat Jun 28 22:13:21 2014 +0200
     4.2 +++ b/src/Tools/Code_Generator.thy	Sat Jun 28 22:13:23 2014 +0200
     4.3 @@ -16,6 +16,15 @@
     4.4  
     4.5  ML_file "~~/src/Tools/cache_io.ML"
     4.6  ML_file "~~/src/Tools/Code/code_preproc.ML"
     4.7 +
     4.8 +attribute_setup code_preproc_trace = {*
     4.9 +  (Scan.lift (Args.$$$ "off" >> K Code_Preproc.trace_none)
    4.10 +  || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
    4.11 +       >> Code_Preproc.trace_only_ext
    4.12 +  || Scan.succeed Code_Preproc.trace_all)
    4.13 +  >> (Thm.declaration_attribute o K)
    4.14 +*} "tracing of the code generator preprocessor"
    4.15 +
    4.16  ML_file "~~/src/Tools/Code/code_symbol.ML"
    4.17  ML_file "~~/src/Tools/Code/code_thingol.ML"
    4.18  ML_file "~~/src/Tools/Code/code_simp.ML"