1 theory Timing |
1 theory Timing |
2 imports "../Base" |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Measuring the Time of an Operation\label{rec:timing} *} |
5 section {* Measuring the Time of an Operation\label{rec:timing} (TBD) *} |
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 *} |
14 *} |
|
15 ML {* timeap *} |
15 |
16 |
16 ML{*fun ackermann (0, n) = n + 1 |
17 fun |
17 | ackermann (m, 0) = ackermann (m - 1, 1) |
18 ackermann:: "(nat * nat) \<Rightarrow> nat" |
18 | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *} |
19 where |
|
20 "ackermann (0, n) = n + 1" |
|
21 | "ackermann (m, 0) = ackermann (m - 1, 1)" |
|
22 | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))" |
19 |
23 |
20 ML {* |
24 text {* Does not work yet! *} |
21 let |
|
22 val start = start_timing () |
|
23 val res = ackermann (3,12) |
|
24 val time = (end_timing start) |
|
25 in |
|
26 (res,time) |
|
27 end |
|
28 *} |
|
29 |
25 |
30 text {* |
26 lemma "ackermann (3, 4) = 125" |
31 check what @{text "#all"} does? |
27 apply(tactic {* timeap (asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"})) 1 *}) |
32 *} |
28 (* |
|
29 apply(tactic {* |
|
30 let |
|
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 |
33 |
37 |
34 end |
38 end |