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 

  @{ML_matchresult_fake_both [display,gray] \<open>ackermann (4, 12)\<close> \<open>\<dots>\<close>}

  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_matchresult_fake_both [display,gray]
\<open>Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) 
  handle TIMEOUT => ~1\<close>
\<open>~1\<close>}

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

  Note that @{ML \<open>apply\<close> 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 \<open>apply\<close> in Timeout} relies.

\begin{readmore}
   The function @{ML \<open>apply\<close> in Timeout} is defined in the structure
  @{ML_structure Timeout} which can be found in the file 
  @{ML_file "Pure/Concurrent/timeout.ML"}.
\end{readmore}

 
\<close>
end