theory Timing
imports "../Base"
begin

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

text {*
 {\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_timing} and @{ML end_timing}.\smallskip

  Assume the following function defined in Isabelle. 
*}

fun 
 ackermann:: "(nat * 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 {* 
  We can now measure how long the simplifier takes to verify a datapoint
  of this function. The timing can be done using the following wrapper function:
*}

ML{*fun timing_wrapper tac st =
let 
  val t_start = start_timing ();
  val res = tac st;
  val t_end = end_timing t_start;
in
  (warning (#message t_end); res)
end*}

text {*
  Note that this function also takes a state @{text "st"} as an argument and
  applies this state to the tactic. This is because tactics are lazy functions
  and we need to force them to run, otherwise the timing will be meaningless.
  The used time will be calculated as the end time minus the start time.
  The wrapper can now be used in the proof
*}

lemma "ackermann (3, 4) = 125"
apply(tactic {* 
  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})
done

text {*
  where it returns something on the cale of 3 seconds.

  \begin{readmore}
  Basic functions regarding timing are defined in @{ML_file 
  "Pure/ML-Systems/polyml_common.ML"} (for the PolyML compiler). Some more
  advanced functions are defined in @{ML_file "Pure/General/output.ML"}.
  \end{readmore}
*}



end