theory TimeLimit

imports Base

begin

section {* Restricting the Runtime of a Function *} 

text {*

  {\bf Problem:}

  Your tool should run only a specified amount of seconds.\smallskip

  {\bf Solution:} This can be achieved using time limits.\smallskip

  Assume the following function should run only five seconds:

  *}

ML {*

fun ackermann (0, n) = n + 1

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

  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))

*}

ML {* ackermann (3, 12) *}

(* takes more than 10 seconds *)

text {*

  The call can be encapsulated in a time limit of five seconds as follows:

  *}

ML {* 

TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (3, 12) 

  handle TimeOut => ~1

*}

text {*

  The function "TimeLimit.timeLimit" has type "???" and is defined in

  TODO: refer to code *}

end