theory TimeLimitimports "../Base"beginsection {* 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:} In PolyML 5.2.1 and later, this can be achieved using the function @{ML timeLimit in TimeLimit}.\smallskip Assume you defined the Ackermann function on the ML-level.*}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_fake_both [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 5.2.1 or later, because this version of PolyML has the infrastructure for multithreaded 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