1 theory Timing |
1 theory Timing |
2 imports "../Base" |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Measuring Time\label{rec:timing} (TBD) *} |
5 section {* Measuring Time\label{rec:timing} *} |
6 |
6 |
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_timing} and @{ML end_timing}.\smallskip |
13 |
13 |
|
14 Assume the following function defined in Isabelle. |
14 *} |
15 *} |
15 ML {* timeap *} |
|
16 |
16 |
17 fun |
17 fun |
18 ackermann:: "(nat * nat) \<Rightarrow> nat" |
18 ackermann:: "(nat * nat) \<Rightarrow> nat" |
19 where |
19 where |
20 "ackermann (0, n) = n + 1" |
20 "ackermann (0, n) = n + 1" |
21 | "ackermann (m, 0) = ackermann (m - 1, 1)" |
21 | "ackermann (m, 0) = ackermann (m - 1, 1)" |
22 | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))" |
22 | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))" |
23 |
23 |
24 text {* Does not work yet! *} |
24 text {* |
|
25 We can now measure how long the simplifier takes to verify a datapoint |
|
26 of this function. The timing can be done using the following wrapper function: |
|
27 *} |
|
28 |
|
29 ML{*fun timing_wrapper tac st = |
|
30 let |
|
31 val t_start = start_timing (); |
|
32 val res = tac st; |
|
33 val t_end = end_timing t_start; |
|
34 in |
|
35 (warning (#message t_end); res) |
|
36 end*} |
|
37 |
|
38 text {* |
|
39 Note that this function also takes a state @{text "st"} as an argument and |
|
40 applies this state to the tactic. This is because tactics are lazy functions |
|
41 and we need to force them to run, otherwise the timing will be meaningless. |
|
42 The used time will be calculated as the end time minus the start time. |
|
43 The wrapper can now be used in the proof |
|
44 *} |
25 |
45 |
26 lemma "ackermann (3, 4) = 125" |
46 lemma "ackermann (3, 4) = 125" |
27 apply(tactic {* timeap (asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"})) 1 *}) |
|
28 (* |
|
29 apply(tactic {* |
47 apply(tactic {* |
30 let |
48 timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *}) |
31 val start = start_timing (); |
|
32 val res = asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1; |
|
33 in |
|
34 (warning (#message (end_timing start)); res) |
|
35 end *})*) |
|
36 done |
49 done |
37 |
50 |
|
51 text {* |
|
52 where it returns something on the cale of 3 seconds. |
|
53 |
|
54 \begin{readmore} |
|
55 Basic functions regarding timing are defined in @{ML_file |
|
56 "Pure/ML-Systems/polyml_common.ML"} (for the PolyML compiler). Some more |
|
57 advanced functions are defined in @{ML_file "Pure/General/output.ML"}. |
|
58 \end{readmore} |
|
59 *} |
|
60 |
|
61 |
|
62 |
38 end |
63 end |