theory TimeLimit+
−
imports "../Base"+
−
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:} This can be achieved using the function +
−
  @{ML timeLimit in TimeLimit}.\smallskip+
−
+
−
  Assume you defined the Ackermann function:+
−
+
−
  *}+
−
+
−
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,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 [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, +
−
  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+
−