simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
authorwenzelm
Sun Mar 20 22:08:12 2011 +0100 (2011-03-20)
changeset 4201475417ef605ba
parent 42013 1694cc477045
child 42015 7b6e72a1b7dd
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Mar 20 21:44:38 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Mar 20 22:08:12 2011 +0100
     1.3 @@ -209,11 +209,8 @@
     1.4    | SOME NONE => error ("bad option: " ^ key)
     1.5    | NONE => default)
     1.6  
     1.7 -fun cpu_time f x =  (* FIXME !? *)
     1.8 -  let
     1.9 -    val start = Timing.start ()
    1.10 -    val result = Exn.capture (fn () => f x) ()
    1.11 -    val time = Time.toMilliseconds (#cpu (Timing.result start))
    1.12 -  in (Exn.release result, time) end
    1.13 +fun cpu_time f x =
    1.14 +  let val ({cpu, ...}, y) = Timing.timing f x
    1.15 +  in (y, Time.toMilliseconds cpu) end
    1.16  
    1.17  end
     2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 20 21:44:38 2011 +0100
     2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 20 22:08:12 2011 +0100
     2.3 @@ -332,12 +332,9 @@
     2.4  
     2.5  fun count x = (length oo filter o equal) x
     2.6  
     2.7 -fun cpu_time description f =  (* FIXME !? *)
     2.8 -  let
     2.9 -    val start = Timing.start ()
    2.10 -    val result = Exn.capture f ()
    2.11 -    val time = Time.toMilliseconds (#cpu (Timing.result start))
    2.12 -  in (Exn.release result, (description, time)) end
    2.13 +fun cpu_time description e =
    2.14 +  let val ({cpu, ...}, result) = Timing.timing e ()
    2.15 +  in (result, (description, Time.toMilliseconds cpu)) end
    2.16  (*
    2.17  fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
    2.18    let
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Mar 20 21:44:38 2011 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Mar 20 22:08:12 2011 +0100
     3.3 @@ -211,12 +211,9 @@
     3.4  
     3.5  val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
     3.6  
     3.7 -fun cpu_time description f =  (* FIXME !? *)
     3.8 -  let
     3.9 -    val start = Timing.start ()
    3.10 -    val result = Exn.capture f ()
    3.11 -    val time = Time.toMilliseconds (#cpu (Timing.result start))
    3.12 -  in (Exn.release result, (description, time)) end
    3.13 +fun cpu_time description e =
    3.14 +  let val ({cpu, ...}, result) = Timing.timing e ()
    3.15 +  in (result, (description, Time.toMilliseconds cpu)) end
    3.16  
    3.17  fun compile_term compilation options ctxt t =
    3.18    let
     4.1 --- a/src/Tools/quickcheck.ML	Sun Mar 20 21:44:38 2011 +0100
     4.2 +++ b/src/Tools/quickcheck.ML	Sun Mar 20 22:08:12 2011 +0100
     4.3 @@ -167,12 +167,9 @@
     4.4      val frees = Term.add_frees t [];
     4.5    in (frees, list_abs_free (frees, t)) end
     4.6  
     4.7 -fun cpu_time description f =  (* FIXME !? *)
     4.8 -  let
     4.9 -    val start = Timing.start ()
    4.10 -    val result = Exn.capture f ()
    4.11 -    val time = Time.toMilliseconds (#cpu (Timing.result start))
    4.12 -  in (Exn.release result, (description, time)) end
    4.13 +fun cpu_time description e =
    4.14 +  let val ({cpu, ...}, result) = Timing.timing e ()
    4.15 +  in (result, (description, Time.toMilliseconds cpu)) end
    4.16  
    4.17  fun limit ctxt (limit_time, is_interactive) f exc () =
    4.18    if limit_time then