theory TimeLimit

imports "../Appendix"

begin

section {* Restricting the Runtime of a Function\label{rec:timeout} *} 

text {*

  {\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.

*}

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

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

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

text {*

  Now the call 

  @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"}

  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

@{ML_response_fake_both [display,gray]

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

  handle TIMEOUT => ~1"

"~1"}

  where @{text TimeOut} 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_struct Timeout} which can be found in the file 

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

\end{readmore}

*}

end