theory TimeLimit

imports "../Appendix"

begin

section \<open>Restricting the Runtime of a Function\label{rec:timeout}\<close> 

text \<open>

  {\bf Problem:}

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

  {\bf Solution:} In Isabelle 2016-1 and later, this can be achieved 

  using the function @{ML apply in Timeout}.\smallskip

  Assume you defined the Ackermann function on the ML-level.

\<close>

ML %grayML\<open>fun ackermann (0, n) = n + 1

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

  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))\<close>

text \<open>

  Now the call 

  takes a bit of time before it finishes. To avoid this, the call can be encapsulated 

  in a time limit of five seconds. For this you have to write

"Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) 

  handle TIMEOUT => ~1"

"~1"}

  where \<open>TimeOut\<close> is the exception raised when the time limit

  is reached.

  Note that @{ML  "apply" in Timeout} is only meaningful when you use PolyML 5.2.1

  or later, because this version of PolyML has the infrastructure for multithreaded 

  programming on which @{ML "apply" in Timeout} relies.

\begin{readmore}

   The function @{ML "apply" in Timeout} is defined in the structure

  @{ML_file "Pure/concurrent/timeout.ML"}.

\end{readmore}

\<close>

end