theory Timing
imports "../Base"
begin

section {* Measuring Time\label{rec:timing} (TBD) *} 

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

*}
ML {* timeap *}

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 {* Does not work yet! *}

lemma "ackermann (3, 4) = 125"
apply(tactic {* timeap  (asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"})) 1 *})
(*
apply(tactic {* 
  let 
    val start = start_timing ();
    val res = asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1;
  in
    (warning (#message  (end_timing start)); res)
  end *})*)
done

end