equal
deleted
inserted
replaced
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 can be done using the following wrapper function: |
26 of this function. The timing of a tactic can be done using the following |
|
27 wrapper function: |
27 *} |
28 *} |
28 |
29 |
29 ML{*fun timing_wrapper tac st = |
30 ML{*fun timing_wrapper tac st = |
30 let |
31 let |
31 val t_start = start_timing (); |
32 val t_start = start_timing (); |
34 in |
35 in |
35 (warning (#message t_end); res) |
36 (warning (#message t_end); res) |
36 end*} |
37 end*} |
37 |
38 |
38 text {* |
39 text {* |
39 Note that this function, in addition to a tactic for which it measures the |
40 Note that this function, in addition to a tactic, also takes a state @{text |
40 time, also takes a state @{text "st"} as argument and applies this state to |
41 "st"} as argument and applies this state to the tactic. The reason is that |
41 the tactic. The reason is that tactics are lazy functions and you need to force |
42 tactics are lazy functions and you need to force them to run, otherwise the |
42 them to run, otherwise the timing will be meaningless. The time between start |
43 timing will be meaningless. The time between start and finish of the tactic |
43 and finish of the tactic will be calculated as the end time minus the start time. |
44 will be calculated as the end time minus the start time. An example of the |
44 An example for the wrapper is the proof |
45 wrapper is the proof |
|
46 |
45 |
47 |
46 *} |
48 *} |
47 |
49 |
48 lemma "ackermann (3, 4) = 125" |
50 lemma "ackermann (3, 4) = 125" |
49 apply(tactic {* |
51 apply(tactic {* |