theory TimeLimit

imports "../Base"

begin

section {* Restricting the Runtime of a Function *} 

text {*

  {\bf Problem:}

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

  {\bf Solution:} This can be achieved using the function 

  @{ML timeLimit in TimeLimit}.\smallskip

  *}

ML {* 

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] "ackermann (4, 12)" "\<dots>"}

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

@{ML_response [display]

"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 

  handle TimeOut => ~1"

"~1"}

  where @{ML_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, 

  because PolyML has a rich infrastructure for multithreading 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