# HG changeset patch # User wenzelm # Date 1300652407 -3600 # Node ID dee23d63d4662ed64c0ef68dfe443c22c9ca0dbb # Parent 04f8c485121905015b3fbddfd22e3f8d5b921b33 pervasive cond_timeit; diff -r 04f8c4851219 -r dee23d63d466 src/HOL/Tools/Predicate_Compile/mode_inference.ML --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Sun Mar 20 20:20:41 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Sun Mar 20 21:20:07 2011 +0100 @@ -527,10 +527,10 @@ val rs = these (AList.lookup (op =) clauses p) fun check_mode m = let - val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => + val res = cond_timeit false "work part of check_mode for one mode" (fn _ => map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs) in - Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => + cond_timeit false "aux part of check_mode for one mode" (fn _ => case find_indices is_none res of [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res) | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is))) @@ -538,7 +538,7 @@ val _ = if show_mode_inference options then tracing ("checking " ^ string_of_int (length ms) ^ " modes ...") else () - val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms) + val res = cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms) val (ms', errors) = split res in ((p, (ms' : ((bool * mode) * bool) list)), errors) @@ -622,7 +622,7 @@ (check_modes_pred' mode_analysis_options options ctxt param_vs clauses (modes @ extra_modes)) modes val ((modes : (string * ((bool * mode) * bool) list) list), errors) = - Output.cond_timeit false "Fixpount computation of mode analysis" (fn () => + cond_timeit false "Fixpount computation of mode analysis" (fn () => if show_invalid_clauses options then fixp_with_state (fn (modes, errors) => let diff -r 04f8c4851219 -r dee23d63d466 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Mar 20 20:20:41 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Mar 20 21:20:07 2011 +0100 @@ -130,12 +130,12 @@ fun preprocess options t thy = let val _ = print_step options "Fetching definitions from theory..." - val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph" + val gr = cond_timeit (!Quickcheck.timing) "preprocess-obtain graph" (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr)) val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else () in - Output.cond_timeit (!Quickcheck.timing) "preprocess-process" + cond_timeit (!Quickcheck.timing) "preprocess-process" (fn () => (fold_rev (preprocess_strong_conn_constnames options gr) (Term_Graph.strong_conn gr) thy)) end diff -r 04f8c4851219 -r dee23d63d466 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Mar 20 20:20:41 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Mar 20 21:20:07 2011 +0100 @@ -1363,7 +1363,7 @@ val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt, modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt) val ((moded_clauses, needs_random), errors) = - Output.cond_timeit (!Quickcheck.timing) "Infering modes" + cond_timeit (!Quickcheck.timing) "Infering modes" (fn _ => infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses) val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy @@ -1373,19 +1373,19 @@ val _ = print_modes options modes val _ = print_step options "Defining executable functions..." val thy'' = - Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..." + cond_timeit (!Quickcheck.timing) "Defining executable functions..." (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy' |> Theory.checkpoint) val ctxt'' = ProofContext.init_global thy'' val _ = print_step options "Compiling equations..." val compiled_terms = - Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ => + cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ => compile_preds options (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses) val _ = print_compiled_terms options ctxt'' compiled_terms val _ = print_step options "Proving equations..." val result_thms = - Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ => + cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ => #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds (maps_modes result_thms) @@ -1393,7 +1393,7 @@ val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)))) val thy''' = - Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ => + cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ => fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [attrib thy ])] thy))