1 theory TimeLimit |
1 theory TimeLimit |
2 imports Base |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Restricting the Runtime of a Function *} |
5 section {* Restricting the Runtime of a Function *} |
6 |
6 |
7 |
|
8 text {* |
7 text {* |
9 {\bf Problem:} |
8 {\bf Problem:} |
10 Your tool should run only a specified amount of seconds.\smallskip |
9 Your tool should run only a specified amount of time.\smallskip |
11 |
10 |
12 {\bf Solution:} This can be achieved using time limits.\smallskip |
11 {\bf Solution:} This can be achieved using the function |
|
12 @{ML timeLimit in TimeLimit}.\smallskip |
13 |
13 |
14 Assume the following function should run only five seconds: |
14 Assume the following well-known function: |
15 |
15 |
16 *} |
16 *} |
17 |
17 |
18 ML {* |
18 ML {* |
19 fun ackermann (0, n) = n + 1 |
19 fun ackermann (0, n) = n + 1 |
20 | ackermann (m, 0) = ackermann (m - 1, 1) |
20 | ackermann (m, 0) = ackermann (m - 1, 1) |
21 | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) |
21 | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) |
22 *} |
22 *} |
23 |
23 |
24 ML {* ackermann (3, 12) *} |
24 text {* |
25 |
25 |
26 (* takes more than 10 seconds *) |
26 Now the call |
27 |
27 |
28 text {* |
28 @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"} |
29 The call can be encapsulated in a time limit of five seconds as follows: |
|
30 *} |
|
31 |
29 |
32 ML {* |
30 takes a bit long. To avoid this, the call can be encapsulated |
33 TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (3, 12) |
31 in a time limit of five seconds. For this you have to write: |
34 handle TimeOut => ~1 |
32 |
|
33 @{ML_response [display] |
|
34 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
|
35 handle TimeOut => ~1" |
|
36 "~1"} |
|
37 |
|
38 where @{ML_text TimeOut} is the exception raised when the time limit |
|
39 is reached. |
|
40 |
|
41 Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML, |
|
42 because PolyML has a rich infrastructure for multithreading programming on |
|
43 which @{ML "timeLimit" in TimeLimit} relies. |
|
44 |
|
45 \begin{readmore} |
|
46 The function @{ML "timeLimit" in TimeLimit} is defined in the structure |
|
47 @{ML_struct TimeLimit} which can be found in the file |
|
48 @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}. |
|
49 \end{readmore} |
|
50 |
|
51 |
35 *} |
52 *} |
36 |
53 |
37 text {* |
|
38 The function "TimeLimit.timeLimit" has type "???" and is defined in |
|
39 TODO: refer to code *} |
|
40 |
|
41 end |
54 end |