theory Timing+
−
imports "../Base"+
−
begin+
−
+
−
section {* Measuring the Time of an Operation\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+
−