added timers to N2M
authorblanchet
Tue Mar 22 07:57:01 2016 +0100 (2016-03-22)
changeset 626851e5cf471e703
parent 62684 cb20e8828196
child 62686 6e8924f957f6
added timers to N2M
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Mar 22 07:18:36 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Mar 22 07:57:01 2016 +0100
     1.3 @@ -249,6 +249,9 @@
     1.4            fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_results) fp_bs
     1.5              unsorted_As' killed_As' fp_eqs no_defs_lthy;
     1.6  
     1.7 +        val time = time lthy;
     1.8 +        val timer = time (Timer.startRealTimer ());
     1.9 +
    1.10          val fp_abs_inverses = map #abs_inverse fp_absT_infos;
    1.11          val fp_type_definitions = map #type_definition fp_absT_infos;
    1.12  
    1.13 @@ -273,6 +276,8 @@
    1.14              fp_bs xtor_co_recs lthy
    1.15            |>> split_list;
    1.16  
    1.17 +        val timer = time (timer ("High-level " ^ co_prefix fp ^ "recursors"));
    1.18 +
    1.19          val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss),
    1.20               fp_sugar_thms) =
    1.21            if fp = Least_FP then
    1.22 @@ -294,6 +299,8 @@
    1.23                 corec_disc_thmss, corec_sel_thmsss))
    1.24              ||> (fn info => (NONE, SOME info));
    1.25  
    1.26 +        val timer = time (timer ("High-level " ^ co_prefix fp ^ "induction principles"));
    1.27 +
    1.28          val names_lthy = lthy |> fold Variable.declare_typ (As @ Cs @ Xs);
    1.29          val phi = Proof_Context.export_morphism names_lthy lthy;
    1.30  
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 22 07:18:36 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 22 07:57:01 2016 +0100
     2.3 @@ -276,7 +276,7 @@
     2.4  
     2.5  fun time ctxt timer msg = (if Config.get ctxt bnf_timing
     2.6    then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
     2.7 -    "ms")
     2.8 +    " ms")
     2.9    else (); Timer.startRealTimer ());
    2.10  
    2.11  val preN = "pre_"