src/Pure/ML-Systems/polyml-time-limit.ML
author wenzelm
Sat, 11 Jun 2005 23:17:28 +0200
changeset 16374 f4b7cf8975af
parent 14849 73a0a6e0426a
child 16993 2ec0b8159e8e
permissions -rw-r--r--
some cygwin support;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14849
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-time-limit.ML
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     2
    ID:         $Id$
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     3
    Author:     Tjark Weber
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     4
    Copyright   2004
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     5
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     6
Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     7
*)
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     8
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
     9
structure TimeLimit : sig
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    10
	exception TimeOut
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    11
	val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    12
end = struct
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    13
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    14
	exception TimeOut
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    15
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    16
	fun timeLimit t f x =
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    17
	let
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    18
		datatype ('a, 'b) union =
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    19
			INL of 'a | INR of 'b
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    20
		val result = Process.channel ()
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    21
		fun workerThread () =
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    22
			Process.send (result, SOME (INL (f x) handle exn => INR exn))
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    23
		val interrupt = Process.console workerThread
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    24
		val old_handle = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    25
			(fn _ => ((Process.send (result, NONE)) before (interrupt ()))))
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    26
	in
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    27
		Posix.Process.alarm t;
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    28
		case Process.receive result of
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    29
		  SOME (INL fx)  => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    30
		| SOME (INR exn) => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); raise exn)
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    31
		| NONE           => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    32
	end
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    33
73a0a6e0426a SML/NJs TimeLimit structure ported to Poly/ML
webertj
parents:
diff changeset
    34
end;