equal
deleted
inserted
replaced
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 Suppose you defined the Ackermann function inside Isabelle. |
14 Suppose you defined the Ackermann function on the Isabelle level. |
15 *} |
15 *} |
16 |
16 |
17 fun |
17 fun |
18 ackermann:: "(nat \<times> nat) \<Rightarrow> nat" |
18 ackermann:: "(nat \<times> nat) \<Rightarrow> nat" |
19 where |
19 where |
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 {* |
24 text {* |
25 You can measure how long the simplifier takes to verify a datapoint |
25 You can measure how long the simplifier takes to verify a datapoint |
26 of this function. The timing of a tactic can be done using the following |
26 of this function. The actual timing is done inside the |
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 |
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 |
42 tactics are lazy functions and you need to force them to run, otherwise the |
42 tactics are lazy functions and you need to force them to run, otherwise the |
43 timing will be meaningless. The time between start and finish of the tactic |
43 timing will be meaningless. The simplifier tactic, amongst others, can be |
44 will be calculated as the end time minus the start time. An example of the |
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 |
45 wrapper is the proof |
50 wrapper is the proof |
46 |
|
47 |
|
48 *} |
51 *} |
49 |
52 |
50 lemma "ackermann (3, 4) = 125" |
53 lemma "ackermann (3, 4) = 125" |
51 apply(tactic {* |
54 apply(tactic {* |
52 timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *}) |
55 timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *}) |