theory Timing

imports "../Appendix"

begin

section \<open>Measuring Time\label{rec:timing}\<close> 

text \<open>

 {\bf Problem:}

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

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

  @{ML start in Timing} and @{ML result in Timing}.\smallskip

  Suppose you defined the Ackermann function on the Isabelle level. 

\<close>

fun 

 ackermann:: "(nat \<times> nat) \<Rightarrow> nat"

where

    "ackermann (0, n) = n + 1"

  | "ackermann (m, 0) = ackermann (m - 1, 1)"

  | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))"

text \<open>

  You can measure how long the simplifier takes to verify a datapoint

  of this function. The actual timing is done inside the

  wrapper function:

\<close>

ML %linenosgray\<open>fun timing_wrapper tac st =

let 

  val t_start = Timing.start ();

  val res = tac st;

  val t_end = Timing.result t_start;

in

  (writeln (Timing.message t_end); res)

end\<close>

text \<open>

  Note that this function, in addition to a tactic, also takes a state \<open>st\<close> as argument and applies this state to the tactic (Line 4). The reason is that

  tactics are lazy functions and you need to force them to run, otherwise the

  timing will be meaningless. The simplifier tactic, amongst others,  can be 

  forced to run by just applying the state to it. But ``fully'' lazy tactics,

  such as @{ML \<open>resolve_tac\<close>}, need even more ``standing-on-ones-head'' to force

  them to run. 

  The time between start and finish of the simplifier will be calculated 

  as the end time minus the start time.  An example of the

  wrapper is the proof

\<close>

lemma "ackermann (3, 4) = 125"

apply(tactic \<open>

  timing_wrapper (simp_tac (@{context} addsimps @{thms "eval_nat_numeral"}) 1)\<close>)

done

text \<open>

  where it returns something on the scale of 3 seconds. We chose to return

  this information as a string, but the timing information is also accessible

  in number format.

  \begin{readmore}

  Basic functions regarding timing are defined in @{ML_file 

  "Pure/General/timing.ML"} (for the PolyML compiler). Some more

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

  \end{readmore}

\<close>

end