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 PolyML 5.2.1 and later, this can be achieved 
  using the function @{ML timeLimit in TimeLimit}.\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 [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]
"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
  handle TimeLimit.TimeOut => ~1"
"~1"}

  where @{text TimeOut} is the exception raised when the time limit
  is reached.

  Note that @{ML  "timeLimit" in TimeLimit} 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 "timeLimit" in TimeLimit} relies.

\begin{readmore}
   The function @{ML "timeLimit" in TimeLimit} is defined in the structure
  @{ML_struct TimeLimit} which can be found in the file 
  @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}.
\end{readmore}

 
*}
end