1 theory Timing

     2 imports "../Base"

     3 begin

     4 

     5 section {* Measuring Time\label{rec:timing} *} 

     6 

     7 text {*

     8  {\bf Problem:}

     9   You want to measure the running time of a tactic or function.\smallskip

    10 

    11   {\bf Solution:} Time can be measured using the function 

    12   @{ML start_timing} and @{ML end_timing}.\smallskip

    13 

    14   Suppose you defined the Ackermann function inside Isabelle. 

    15 *}

    16 

    17 fun 

    18  ackermann:: "(nat \<times> 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 {* 

    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 

    27   wrapper function:

    28 *}

    29 

    30 ML %linenosgray{*fun timing_wrapper tac st =

    31 let 

    32   val t_start = start_timing ();

    33   val res = tac st;

    34   val t_end = end_timing t_start;

    35 in

    36   (warning (#message t_end); res)

    37 end*}

    38 

    39 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

    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

    44   will be calculated as the end time minus the start time.  An example of the

    45   wrapper is the proof

    46 

    47 

    48 *}

    49 

    50 lemma "ackermann (3, 4) = 125"

    51 apply(tactic {* 

    52   timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})

    53 done

    54 

    55 text {*

    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

    58   in number format.

    59 

    60   \begin{readmore}

    61   Basic functions regarding timing are defined in @{ML_file 

    62   "Pure/ML-Systems/polyml_common.ML"} (for the PolyML compiler). Some more

    63   advanced functions are defined in @{ML_file "Pure/General/output.ML"}.

    64   \end{readmore}

    65 *}

    66 

    67 

    68 

    69 end