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

  Suppose you defined the Ackermann function inside Isabelle. 
*}

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 {* 
  You can measure how long the simplifier takes to verify a datapoint
  of this function. The timing of a tactic 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, in addition to a tactic, also takes a state @{text
  "st"} as argument and applies this state to the tactic. The reason is that
  tactics are lazy functions and you need to force them to run, otherwise the
  timing will be meaningless.  The time between start and finish of the tactic
  will be calculated as the end time minus the start time.  An example of the
  wrapper is 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 scale of 3 seconds. We choose 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/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