1(* ========================================================================== *)
2(* FILE          : smlTimeout.sml                                             *)
3(* DESCRIPTION   : Timing out PolyML functions.                               *)
4(* AUTHOR        : (c) Thibault Gauthier, University of Innsbruck             *)
5(* DATE          : 2017                                                       *)
6(* ========================================================================== *)
7
8structure smlTimeout :> smlTimeout =
9struct
10
11open HolKernel Abbrev boolLib aiLib Thread
12
13exception FunctionTimeout
14
15datatype 'a result = Res of 'a | Exn of exn
16
17fun capture f x = Res (f x) handle e => Exn e
18
19fun release (Res y) = y
20  | release (Exn x) = raise x
21
22val attrib = [Thread.InterruptState Thread.InterruptAsynch,
23  Thread.EnableBroadcastInterrupt true]
24
25fun timeLimit t f x =
26  let
27    val resultref = ref NONE
28    val worker = Thread.fork (fn () => resultref := SOME (capture f x), attrib)
29    val watcher = Thread.fork (fn () =>
30      (OS.Process.sleep t; interruptkill worker), [])
31    fun self_wait () =
32      (
33      if Thread.isActive worker then self_wait () else
34    case !resultref of
35      NONE => Exn FunctionTimeout
36    | SOME (Exn Interrupt) => Exn FunctionTimeout
37    | SOME s => s
38      )
39    val result = self_wait ()
40  in
41    release result
42  end
43
44fun timeout t f x = timeLimit (Time.fromReal t) f x
45
46val (TC_OFF : tactic -> tactic) = trace ("show_typecheck_errors", 0)
47
48fun timeout_tactic t tac g =
49  SOME (fst (timeout t (TC_OFF tac) g))
50  handle Interrupt => raise Interrupt | _ => NONE
51
52end (* struct *)
53
54(* test
55  load "smlTimeout"; open smlTimeout;
56  fun loop () = loop ();
57  timeout 5.0 loop ();
58*)
59
60