structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;
--- a/src/HOL/Matrix/Compute_Oracle/report.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/report.ML Sun Mar 20 21:28:11 2011 +0100
@@ -11,9 +11,9 @@
fun timeit f =
let
- val t1 = start_timing ()
+ val t1 = Timing.start ()
val x = f ()
- val t2 = #message (end_timing t1)
+ val t2 = Timing.message (Timing.result t1)
val _ = writeln ((report_space ()) ^ "--> "^t2)
in
x
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Mar 20 21:28:11 2011 +0100
@@ -209,11 +209,11 @@
| SOME NONE => error ("bad option: " ^ key)
| NONE => default)
-fun cpu_time f x =
+fun cpu_time f x = (* FIXME !? *)
let
- val start = start_timing ()
+ val start = Timing.start ()
val result = Exn.capture (fn () => f x) ()
- val time = Time.toMilliseconds (#cpu (end_timing start))
+ val time = Time.toMilliseconds (#cpu (Timing.result start))
in (Exn.release result, time) end
end
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 20 21:28:11 2011 +0100
@@ -332,11 +332,11 @@
fun count x = (length oo filter o equal) x
-fun cpu_time description f =
+fun cpu_time description f = (* FIXME !? *)
let
- val start = start_timing ()
+ val start = Timing.start ()
val result = Exn.capture f ()
- val time = Time.toMilliseconds (#cpu (end_timing start))
+ val time = Time.toMilliseconds (#cpu (Timing.result start))
in (Exn.release result, (description, time)) end
(*
fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sun Mar 20 21:28:11 2011 +0100
@@ -211,11 +211,11 @@
val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
-fun cpu_time description f =
+fun cpu_time description f = (* FIXME !? *)
let
- val start = start_timing ()
+ val start = Timing.start ()
val result = Exn.capture f ()
- val time = Time.toMilliseconds (#cpu (end_timing start))
+ val time = Time.toMilliseconds (#cpu (Timing.result start))
in (Exn.release result, (description, time)) end
fun compile_term compilation options ctxt t =
--- a/src/HOL/ex/SAT_Examples.thy Sun Mar 20 21:20:07 2011 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Sun Mar 20 21:28:11 2011 +0100
@@ -536,13 +536,12 @@
fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
| and_to_list fm acc = rev (fm :: acc)
val clauses = and_to_list prop_fm []
- val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula)
- clauses
- val cterms = map (Thm.cterm_of @{theory}) terms
- val timer = start_timing ()
- val thm = sat.rawsat_thm @{context} cterms
+ val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
+ val cterms = map (Thm.cterm_of @{theory}) terms
+ val start = Timing.start ()
+ val thm = sat.rawsat_thm @{context} cterms
in
- (end_timing timer, !sat.counter)
+ (Timing.result start, ! sat.counter)
end;
*}
--- a/src/Provers/blast.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Provers/blast.ML Sun Mar 20 21:28:11 2011 +0100
@@ -914,7 +914,7 @@
fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
if b then
- writeln (#message (end_timing start) ^ " for search. Closed: "
+ writeln (Timing.message (Timing.result start) ^ " for search. Closed: "
^ string_of_int (!nclosed) ^
" tried: " ^ string_of_int (!ntried) ^
" tactics: " ^ string_of_int (length tacs))
@@ -1256,7 +1256,7 @@
val hyps = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
fun cont (tacs,_,choices) =
- let val start = start_timing ()
+ let val start = Timing.start ()
in
case Seq.pull(EVERY' (rev tacs) i st) of
NONE => (writeln ("PROOF FAILED for depth " ^
@@ -1265,7 +1265,7 @@
else ();
backtrack choices)
| cell => (if (!trace orelse !stats)
- then writeln (#message (end_timing start) ^ " for reconstruction")
+ then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
else ();
Seq.make(fn()=> cell))
end
@@ -1273,13 +1273,13 @@
handle PROVE => Seq.empty
(*Public version with fixed depth*)
-fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
+fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
fun blast_tac cs i st =
((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
- (timing_depth_tac (start_timing ()) cs) 0) i
+ (timing_depth_tac (Timing.start ()) cs) 0) i
THEN flexflex_tac) st
handle TRANS s =>
((if !trace then warning ("blast: " ^ s) else ());
@@ -1299,7 +1299,7 @@
let
val state as State {fullTrace = ft, ...} = initialize thy;
val res = timeap prove
- (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I);
+ (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I);
val _ = fullTrace := !ft;
in res end;
--- a/src/Pure/General/markup.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/General/markup.ML Sun Mar 20 21:28:11 2011 +0100
@@ -100,7 +100,7 @@
val elapsedN: string
val cpuN: string
val gcN: string
- val timingN: string val timing: timing -> T
+ val timingN: string val timing: Timing.timing -> T
val subgoalsN: string
val proof_stateN: string val proof_state: int -> T
val stateN: string val state: T
@@ -312,7 +312,7 @@
val cpuN = "cpu";
val gcN = "gc";
-fun timing ({elapsed, cpu, gc, ...}: timing) =
+fun timing {elapsed, cpu, gc} =
(timingN,
[(elapsedN, Time.toString elapsed),
(cpuN, Time.toString cpu),
--- a/src/Pure/General/output.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/General/output.ML Sun Mar 20 21:28:11 2011 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/General/output.ML
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
-Output channels and timing messages.
+Isabelle output channels.
*)
signature BASIC_OUTPUT =
@@ -10,11 +10,6 @@
val tracing: string -> unit
val warning: string -> unit
val legacy_feature: string -> unit
- val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
- val timeit: (unit -> 'a) -> 'a
- val timeap: ('a -> 'b) -> 'a -> 'b
- val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
- val timing: bool Unsynchronized.ref
end;
signature OUTPUT =
@@ -111,31 +106,6 @@
fun legacy_feature s = warning ("Legacy feature! " ^ s);
-
-
-(** timing **)
-
-(*conditional timing with message*)
-fun cond_timeit flag msg e =
- if flag then
- let
- val start = start_timing ();
- val result = Exn.capture e ();
- val end_msg = #message (end_timing start);
- val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
- in Exn.release result end
- else e ();
-
-(*unconditional timing*)
-fun timeit e = cond_timeit true "" e;
-
-(*timed application function*)
-fun timeap f x = timeit (fn () => f x);
-fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
-
-(*global timing mode*)
-val timing = Unsynchronized.ref false;
-
end;
structure Basic_Output: BASIC_OUTPUT = Output;
--- a/src/Pure/General/timing.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/General/timing.ML Sun Mar 20 21:28:11 2011 +0100
@@ -4,19 +4,45 @@
Basic support for time measurement.
*)
-val seconds = Time.fromReal;
+signature BASIC_TIMING =
+sig
+ val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
+ val timeit: (unit -> 'a) -> 'a
+ val timeap: ('a -> 'b) -> 'a -> 'b
+ val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
+end
-fun start_timing () =
+signature TIMING =
+sig
+ include BASIC_TIMING
+ type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
+ type start
+ val start: unit -> start
+ val result: start -> timing
+ val message: timing -> string
+end
+
+structure Timing: TIMING =
+struct
+
+(* timer control *)
+
+type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
+
+abstype start = Start of
+ Timer.real_timer * Time.time * Timer.cpu_timer *
+ {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
+with
+
+fun start () =
let
val real_timer = Timer.startRealTimer ();
val real_time = Timer.checkRealTimer real_timer;
val cpu_timer = Timer.startCPUTimer ();
val cpu_times = Timer.checkCPUTimes cpu_timer;
- in (real_timer, real_time, cpu_timer, cpu_times) end;
+ in Start (real_timer, real_time, cpu_timer, cpu_times) end;
-type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time};
-
-fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing =
+fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) =
let
val real_time2 = Timer.checkRealTimer real_timer;
val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
@@ -27,10 +53,34 @@
val elapsed = real_time2 - real_time;
val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
val cpu = usr2 - usr + sys2 - sys + gc;
+ in {elapsed = elapsed, cpu = cpu, gc = gc} end;
- val message =
- (toString elapsed ^ "s elapsed time, " ^
- toString cpu ^ "s cpu time, " ^
- toString gc ^ "s GC time") handle Time.Time => "";
- in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
+end;
+
+
+(* timing messages *)
+
+fun message {elapsed, cpu, gc} =
+ Time.toString elapsed ^ "s elapsed time, " ^
+ Time.toString cpu ^ "s cpu time, " ^
+ Time.toString gc ^ "s GC time" handle Time.Time => "";
+fun cond_timeit enabled msg e =
+ if enabled then
+ let
+ val timing_start = start ();
+ val res = Exn.capture e ();
+ val end_msg = message (result timing_start);
+ val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
+ in Exn.release res end
+ else e ();
+
+fun timeit e = cond_timeit true "" e;
+fun timeap f x = timeit (fn () => f x);
+fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
+
+end;
+
+structure Basic_Timing: BASIC_TIMING = Timing;
+open Basic_Timing;
+
--- a/src/Pure/IsaMakefile Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/IsaMakefile Sun Mar 20 21:28:11 2011 +0100
@@ -21,7 +21,6 @@
BOOTSTRAP_FILES = \
General/exn.ML \
- General/timing.ML \
ML-Systems/compiler_polyml-5.2.ML \
ML-Systems/compiler_polyml-5.3.ML \
ML-Systems/ml_name_space.ML \
@@ -101,6 +100,7 @@
General/symbol.ML \
General/symbol_pos.ML \
General/table.ML \
+ General/timing.ML \
General/url.ML \
General/xml.ML \
General/xml_data.ML \
--- a/src/Pure/Isar/outer_syntax.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Sun Mar 20 21:28:11 2011 +0100
@@ -271,7 +271,7 @@
fun load_thy name init pos text =
let
val (lexs, commands) = get_syntax ();
- val time = ! Output.timing;
+ val time = ! Toplevel.timing;
val _ = Present.init_theory name;
--- a/src/Pure/Isar/toplevel.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML Sun Mar 20 21:28:11 2011 +0100
@@ -218,7 +218,7 @@
val quiet = Unsynchronized.ref false;
val debug = Runtime.debug;
val interact = Unsynchronized.ref false;
-val timing = Output.timing;
+val timing = Unsynchronized.ref false;
val profiling = Unsynchronized.ref 0;
val skip_proofs = Unsynchronized.ref false;
--- a/src/Pure/ML-Systems/polyml_common.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Sun Mar 20 21:28:11 2011 +0100
@@ -14,10 +14,12 @@
else use "ML-Systems/single_assignment_polyml.ML";
use "ML-Systems/multithreading.ML";
-use "General/timing.ML";
use "ML-Systems/ml_pretty.ML";
use "ML-Systems/use_context.ML";
+val seconds = Time.fromReal;
+
+
(** ML system and platform related **)
--- a/src/Pure/ML-Systems/smlnj.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Sun Mar 20 21:28:11 2011 +0100
@@ -13,7 +13,6 @@
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
-use "General/timing.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
structure PolyML = struct end;
@@ -21,8 +20,9 @@
use "ML-Systems/use_context.ML";
+val seconds = Time.fromReal;
+
(*low-level pointer equality*)
-
CM.autoload "$smlnj/init/init.cmi";
val pointer_eq = InlineT.ptreql;
--- a/src/Pure/PIDE/document.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/PIDE/document.ML Sun Mar 20 21:28:11 2011 +0100
@@ -241,9 +241,9 @@
val is_proof = Keyword.is_proof (Toplevel.name_of tr);
val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
- val start = start_timing ();
+ val start = Timing.start ();
val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
- val _ = timing tr (end_timing start);
+ val _ = timing tr (Timing.result start);
val _ = List.app (Toplevel.error_msg tr) errs;
val res =
(case result of
--- a/src/Pure/ProofGeneral/preferences.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML Sun Mar 20 21:28:11 2011 +0100
@@ -156,7 +156,7 @@
bool_pref Pattern.trace_unify_fail
"trace-unification"
"Output error diagnostics during unification",
- bool_pref Output.timing
+ bool_pref Toplevel.timing
"global-timing"
"Whether to enable timing in Isabelle.",
bool_pref Toplevel.debug
--- a/src/Pure/ROOT.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/ROOT.ML Sun Mar 20 21:28:11 2011 +0100
@@ -21,6 +21,7 @@
use "General/alist.ML";
use "General/table.ML";
use "General/output.ML";
+use "General/timing.ML";
use "General/properties.ML";
use "General/markup.ML";
use "General/scan.ML";
--- a/src/Pure/System/session.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/System/session.ML Sun Mar 20 21:28:11 2011 +0100
@@ -101,13 +101,12 @@
(dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
if timing then
let
- val start = start_timing ();
+ val start = Timing.start ();
val _ = use root;
- val stop = end_timing start;
val _ =
Output.raw_stderr ("Timing " ^ item ^ " (" ^
string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
- #message stop ^ ")\n");
+ Timing.message (Timing.result start) ^ ")\n");
in () end
else use root;
finish ()))
--- a/src/Pure/Tools/find_consts.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/Tools/find_consts.ML Sun Mar 20 21:28:11 2011 +0100
@@ -69,7 +69,7 @@
fun find_consts ctxt raw_criteria =
let
- val start = start_timing ();
+ val start = Timing.start ();
val thy = ProofContext.theory_of ctxt;
val low_ranking = 10000;
@@ -114,7 +114,7 @@
|> sort (rev_order o int_ord o pairself snd)
|> map (apsnd fst o fst);
- val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
+ val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
in
Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
Pretty.str "" ::
--- a/src/Pure/Tools/find_theorems.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Pure/Tools/find_theorems.ML Sun Mar 20 21:28:11 2011 +0100
@@ -464,7 +464,7 @@
fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
- val start = start_timing ();
+ val start = Timing.start ();
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
@@ -480,7 +480,7 @@
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
- val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
+ val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
in
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
Pretty.str "" ::
--- a/src/Tools/quickcheck.ML Sun Mar 20 21:20:07 2011 +0100
+++ b/src/Tools/quickcheck.ML Sun Mar 20 21:28:11 2011 +0100
@@ -167,11 +167,11 @@
val frees = Term.add_frees t [];
in (frees, list_abs_free (frees, t)) end
-fun cpu_time description f =
+fun cpu_time description f = (* FIXME !? *)
let
- val start = start_timing ()
+ val start = Timing.start ()
val result = Exn.capture f ()
- val time = Time.toMilliseconds (#cpu (end_timing start))
+ val time = Time.toMilliseconds (#cpu (Timing.result start))
in (Exn.release result, (description, time)) end
fun limit ctxt (limit_time, is_interactive) f exc () =