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