1 theory TimeLimit

     2 imports "../Base"

     3 begin

     4 

     5 section {* Restricting the Runtime of a Function\label{rec:timeout} *} 

     6 

     7 text {*

     8   {\bf Problem:}

     9   Your tool should run only a specified amount of time.\smallskip

    10 

    11   {\bf Solution:} This can be achieved using the function 

    12   @{ML timeLimit in TimeLimit}.\smallskip

    13 

    14   Assume you defined the Ackermann function on the ML-level.

    15 *}

    16 

    17 ML{*fun ackermann (0, n) = n + 1

    18   | ackermann (m, 0) = ackermann (m - 1, 1)

    19   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}

    20 

    21 text {*

    22 

    23   Now the call 

    24 

    25   @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"}

    26 

    27   takes a bit of time before it finishes. To avoid this, the call can be encapsulated 

    28   in a time limit of five seconds. For this you have to write

    29 

    30 @{ML_response_fake_both [display,gray]

    31 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 

    32   handle TimeLimit.TimeOut => ~1"

    33 "~1"}

    34 

    35   where @{text TimeOut} is the exception raised when the time limit

    36   is reached.

    37 

    38   Note that @{ML  "timeLimit" in TimeLimit} is only meaningful when you use PolyML 5.2.1

    39   or later, because this version of PolyML has the infrastructure for multithreaded 

    40   programming on which @{ML "timeLimit" in TimeLimit} relies.

    41 

    42 \begin{readmore}

    43    The function @{ML "timeLimit" in TimeLimit} is defined in the structure

    44   @{ML_struct TimeLimit} which can be found in the file 

    45   @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}.

    46 \end{readmore}

    47 

    48  

    49 *}

    50 end