154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Timing
|
346
|
2 |
imports "../Appendix"
|
154
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 |
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
section {* Measuring Time\label{rec:timing} *}
|
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
|
460
|
12 |
@{ML start in Timing} and @{ML result in Timing}.\smallskip
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
191
|
14 |
Suppose you defined the Ackermann function on the Isabelle level.
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
*}
|
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
155
|
17 |
fun
|
168
|
18 |
ackermann:: "(nat \<times> nat) \<Rightarrow> nat"
|
155
|
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 |
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
text {*
|
168
|
25 |
You can measure how long the simplifier takes to verify a datapoint
|
191
|
26 |
of this function. The actual timing is done inside the
|
175
|
27 |
wrapper function:
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
*}
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
|
185
|
30 |
ML %linenosgray{*fun timing_wrapper tac st =
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
let
|
460
|
32 |
val t_start = Timing.start ();
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
val res = tac st;
|
460
|
34 |
val t_end = Timing.result t_start;
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
in
|
460
|
36 |
(writeln (Timing.message t_end); res)
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
end*}
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
text {*
|
175
|
40 |
Note that this function, in addition to a tactic, also takes a state @{text
|
185
|
41 |
"st"} as argument and applies this state to the tactic (Line 4). The reason is that
|
175
|
42 |
tactics are lazy functions and you need to force them to run, otherwise the
|
191
|
43 |
timing will be meaningless. The simplifier tactic, amongst others, can be
|
|
44 |
forced to run by just applying the state to it. But ``fully'' lazy tactics,
|
|
45 |
such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force
|
|
46 |
them to run.
|
|
47 |
|
|
48 |
The time between start and finish of the simplifier will be calculated
|
|
49 |
as the end time minus the start time. An example of the
|
175
|
50 |
wrapper is the proof
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
51 |
*}
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
|
155
|
53 |
lemma "ackermann (3, 4) = 125"
|
|
54 |
apply(tactic {*
|
456
|
55 |
timing_wrapper (simp_tac (@{simpset} addsimps @{thms "eval_nat_numeral"}) 1) *})
|
155
|
56 |
done
|
154
e81ebb37aa83
updated to repository version; added a section about timing
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
text {*
|
185
|
59 |
where it returns something on the scale of 3 seconds. We chose to return
|
168
|
60 |
this information as a string, but the timing information is also accessible
|
|
61 |
in number format.
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
\begin{readmore}
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
Basic functions regarding timing are defined in @{ML_file
|
460
|
65 |
"Pure/General/timing.ML"} (for the PolyML compiler). Some more
|
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
advanced functions are defined in @{ML_file "Pure/General/output.ML"}.
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
\end{readmore}
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
*}
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
|
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
|
456
|
72 |
end
|