equal
deleted
inserted
replaced
7 text {* |
7 text {* |
8 {\bf Problem:} |
8 {\bf Problem:} |
9 You want to measure the running time of a tactic or function.\smallskip |
9 You want to measure the running time of a tactic or function.\smallskip |
10 |
10 |
11 {\bf Solution:} Time can be measured using the function |
11 {\bf Solution:} Time can be measured using the function |
12 @{ML start_timing} and @{ML end_timing}.\smallskip |
12 @{ML start in Timing} and @{ML result in Timing}.\smallskip |
13 |
13 |
14 Suppose you defined the Ackermann function on the Isabelle level. |
14 Suppose you defined the Ackermann function on the Isabelle level. |
15 *} |
15 *} |
16 |
16 |
17 fun |
17 fun |
27 wrapper function: |
27 wrapper function: |
28 *} |
28 *} |
29 |
29 |
30 ML %linenosgray{*fun timing_wrapper tac st = |
30 ML %linenosgray{*fun timing_wrapper tac st = |
31 let |
31 let |
32 val t_start = start_timing (); |
32 val t_start = Timing.start (); |
33 val res = tac st; |
33 val res = tac st; |
34 val t_end = end_timing t_start; |
34 val t_end = Timing.result t_start; |
35 in |
35 in |
36 (writeln (#message t_end); res) |
36 (writeln (Timing.message t_end); res) |
37 end*} |
37 end*} |
38 |
38 |
39 text {* |
39 text {* |
40 Note that this function, in addition to a tactic, also takes a state @{text |
40 Note that this function, in addition to a tactic, also takes a state @{text |
41 "st"} as argument and applies this state to the tactic (Line 4). The reason is that |
41 "st"} as argument and applies this state to the tactic (Line 4). The reason is that |
60 this information as a string, but the timing information is also accessible |
60 this information as a string, but the timing information is also accessible |
61 in number format. |
61 in number format. |
62 |
62 |
63 \begin{readmore} |
63 \begin{readmore} |
64 Basic functions regarding timing are defined in @{ML_file |
64 Basic functions regarding timing are defined in @{ML_file |
65 "Pure/ML-Systems/polyml_common.ML"} (for the PolyML compiler). Some more |
65 "Pure/General/timing.ML"} (for the PolyML compiler). Some more |
66 advanced functions are defined in @{ML_file "Pure/General/output.ML"}. |
66 advanced functions are defined in @{ML_file "Pure/General/output.ML"}. |
67 \end{readmore} |
67 \end{readmore} |
68 *} |
68 *} |
69 |
69 |
70 |
70 |