pervasive cond_timeit;
authorwenzelm
Sun Mar 20 21:20:07 2011 +0100 (2011-03-20)
changeset 42011dee23d63d466
parent 42010 04f8c4851219
child 42012 2c3fe3cbebae
pervasive cond_timeit;
src/HOL/Tools/Predicate_Compile/mode_inference.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Sun Mar 20 20:20:41 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Sun Mar 20 21:20:07 2011 +0100
     1.3 @@ -527,10 +527,10 @@
     1.4      val rs = these (AList.lookup (op =) clauses p)
     1.5      fun check_mode m =
     1.6        let
     1.7 -        val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => 
     1.8 +        val res = cond_timeit false "work part of check_mode for one mode" (fn _ => 
     1.9            map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)
    1.10        in
    1.11 -        Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => 
    1.12 +        cond_timeit false "aux part of check_mode for one mode" (fn _ => 
    1.13          case find_indices is_none res of
    1.14            [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
    1.15          | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
    1.16 @@ -538,7 +538,7 @@
    1.17      val _ = if show_mode_inference options then
    1.18          tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
    1.19        else ()
    1.20 -    val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
    1.21 +    val res = cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
    1.22      val (ms', errors) = split res
    1.23    in
    1.24      ((p, (ms' : ((bool * mode) * bool) list)), errors)
    1.25 @@ -622,7 +622,7 @@
    1.26        (check_modes_pred' mode_analysis_options options ctxt param_vs clauses
    1.27          (modes @ extra_modes)) modes
    1.28      val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
    1.29 -      Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
    1.30 +      cond_timeit false "Fixpount computation of mode analysis" (fn () =>
    1.31        if show_invalid_clauses options then
    1.32          fixp_with_state (fn (modes, errors) =>
    1.33            let
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Mar 20 20:20:41 2011 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Mar 20 21:20:07 2011 +0100
     2.3 @@ -130,12 +130,12 @@
     2.4  fun preprocess options t thy =
     2.5    let
     2.6      val _ = print_step options "Fetching definitions from theory..."
     2.7 -    val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
     2.8 +    val gr = cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
     2.9            (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
    2.10            |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
    2.11      val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
    2.12    in
    2.13 -    Output.cond_timeit (!Quickcheck.timing) "preprocess-process"
    2.14 +    cond_timeit (!Quickcheck.timing) "preprocess-process"
    2.15        (fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
    2.16          (Term_Graph.strong_conn gr) thy))
    2.17    end
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Mar 20 20:20:41 2011 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Mar 20 21:20:07 2011 +0100
     3.3 @@ -1363,7 +1363,7 @@
     3.4      val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
     3.5        modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
     3.6      val ((moded_clauses, needs_random), errors) =
     3.7 -      Output.cond_timeit (!Quickcheck.timing) "Infering modes"
     3.8 +      cond_timeit (!Quickcheck.timing) "Infering modes"
     3.9        (fn _ => infer_modes mode_analysis_options
    3.10          options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
    3.11      val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
    3.12 @@ -1373,19 +1373,19 @@
    3.13      val _ = print_modes options modes
    3.14      val _ = print_step options "Defining executable functions..."
    3.15      val thy'' =
    3.16 -      Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
    3.17 +      cond_timeit (!Quickcheck.timing) "Defining executable functions..."
    3.18        (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
    3.19        |> Theory.checkpoint)
    3.20      val ctxt'' = ProofContext.init_global thy''
    3.21      val _ = print_step options "Compiling equations..."
    3.22      val compiled_terms =
    3.23 -      Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
    3.24 +      cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
    3.25          compile_preds options
    3.26            (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
    3.27      val _ = print_compiled_terms options ctxt'' compiled_terms
    3.28      val _ = print_step options "Proving equations..."
    3.29      val result_thms =
    3.30 -      Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
    3.31 +      cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
    3.32        #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
    3.33      val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
    3.34        (maps_modes result_thms)
    3.35 @@ -1393,7 +1393,7 @@
    3.36      val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
    3.37        (fn thm => Context.mapping (Code.add_eqn thm) I))))
    3.38      val thy''' =
    3.39 -      Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
    3.40 +      cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
    3.41        fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
    3.42        [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
    3.43          [attrib thy ])] thy))