1 theory Timing

     2 imports "../Base"

     3 begin

     4 

     5 section {* Measuring the Time of an Operation\label{rec:timing} *} 

     6 

     7 text {*

     8  {\bf Problem:}

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

    10 

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

    12   @{ML start_timing} and @{ML end_timing}.\smallskip

    13 

    14 *}

    15 

    16 ML{*fun ackermann (0, n) = n + 1

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

    18   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}

    19 

    20 ML {*

    21 let

    22   val start = start_timing ()

    23   val res = ackermann (3,12)

    24   val time = (end_timing start)

    25 in

    26  (res,time)

    27 end

    28 *}

    29 

    30 text {*

    31   check what @{text "#all"} does?

    32 *}

    33 

    34 end