1(* ========================================================================== *)
2(* FILE          : tttTimeout.sml                                             *)
3(* DESCRIPTION   : Timing out PolyML functions.                               *)
4(* AUTHOR        : (c) Thibault Gauthier, University of Innsbruck             *)
5(* DATE          : 2017                                                       *)
6(* ========================================================================== *)
7
8structure tttTimeout :> tttTimeout =
9struct
10
11exception TacTimeOut;
12
13datatype 'a result = Res of 'a | Exn of exn;
14
15fun capture f x = Res (f x) handle e => Exn e
16
17fun release (Res y) = y
18  | release (Exn x) = raise x
19
20open Thread;
21
22fun timeLimit time f x =
23  let
24    val result_ref = ref NONE
25    val worker =
26      let
27        fun worker_call () = result_ref := SOME (capture f x)
28      in
29        Thread.fork (fn () => worker_call (),[])
30      end
31    val watchdog =
32      let
33        fun watchdog_call () =
34        (
35        OS.Process.sleep time;
36        if Thread.isActive worker
37          then (Thread.interrupt worker;
38                if Thread.isActive worker
39                then Thread.kill worker
40                else ()
41              )
42          else ()
43        )
44      in
45        Thread.fork (fn () => watchdog_call (),[])
46      end
47    fun self_wait () =
48      (
49      if Thread.isActive worker
50        then self_wait ()
51        else
52          case !result_ref of
53            NONE => Exn TacTimeOut
54          | SOME s => s
55      )
56    val result = self_wait ()
57  in
58    release result
59  end
60
61fun timeOut t f x = timeLimit (Time.fromReal t) f x
62
63end
64