equal
deleted
inserted
replaced
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 timing of a tactic can be done using the following |
27 wrapper function: |
27 wrapper function: |
28 *} |
28 *} |
29 |
29 |
30 ML{*fun timing_wrapper tac st = |
30 ML %linenosgray{*fun timing_wrapper tac st = |
31 let |
31 let |
32 val t_start = start_timing (); |
32 val t_start = start_timing (); |
33 val res = tac st; |
33 val res = tac st; |
34 val t_end = end_timing t_start; |
34 val t_end = end_timing t_start; |
35 in |
35 in |
36 (warning (#message t_end); res) |
36 (warning (#message t_end); res) |
37 end*} |
37 end*} |
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. 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 time between start and finish of the tactic |
44 will be calculated as the end time minus the start time. An example of the |
44 will be calculated as the end time minus the start time. An example of the |
45 wrapper is the proof |
45 wrapper is the proof |
46 |
46 |
51 apply(tactic {* |
51 apply(tactic {* |
52 timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *}) |
52 timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *}) |
53 done |
53 done |
54 |
54 |
55 text {* |
55 text {* |
56 where it returns something on the scale of 3 seconds. We choose to return |
56 where it returns something on the scale of 3 seconds. We chose to return |
57 this information as a string, but the timing information is also accessible |
57 this information as a string, but the timing information is also accessible |
58 in number format. |
58 in number format. |
59 |
59 |
60 \begin{readmore} |
60 \begin{readmore} |
61 Basic functions regarding timing are defined in @{ML_file |
61 Basic functions regarding timing are defined in @{ML_file |