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+
−