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