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