| author | Christian Urban <urbanc@in.tum.de> |
| Mon, 02 Mar 2009 10:06:06 +0000 | |
| changeset 155 | b6fca043a796 |
| parent 154 | e81ebb37aa83 |
| child 157 | 76cdc8f562fc |
| permissions | -rw-r--r-- |
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Timing |
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../Base" |
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
| 155 | 5 |
section {* Measuring the Time of an Operation\label{rec:timing} (TBD) *}
|
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
text {*
|
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
{\bf Problem:}
|
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
You want to measure the running time of a tactic or function.\smallskip |
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
{\bf Solution:} Time can be measured using the function
|
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
@{ML start_timing} and @{ML end_timing}.\smallskip
|
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
*} |
| 155 | 15 |
ML {* timeap *}
|
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
| 155 | 17 |
fun |
18 |
ackermann:: "(nat * nat) \<Rightarrow> nat" |
|
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))" |
|
23 |
||
24 |
text {* Does not work yet! *}
|
|
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
|
| 155 | 26 |
lemma "ackermann (3, 4) = 125" |
27 |
apply(tactic {* timeap (asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"})) 1 *})
|
|
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 |
|
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
|
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
end |