module Monitor:sig
..end
type
key
type ('a, 'b, 'c)
t = {
|
enter : |
|
leave : |
|
is_pending : |
|
get_pendings : |
|
wait : |
|
finished : |
Given a monitor m
, defined as create comb y0
:
m
is informed of the start of a computation by sending
a message m.enter xi
where xi
is the input of the
computation, an identifier for the computation being returned.m
is informed of the end of a computation by sending
a message m.leave (id, yi)
where id
is the computation
identifier as previously returned by enter
, and yi
is
the result of the computation.m.is_pending id
returns whether the computation whose
identifier is passed is pending (a computation is pending
if it has been "entered" but not yet "leaved").m.get_pendings ()
returns the list of pending computations.m
is informed that no more computation will be entered
by sending a message m.finished ()
.m.wait ()
will return the combined result
comb y1 (comb y2 (... (comb yn y0)))
, once all the announced
events have occurred. Observe that at most one such call is allowed.val create : ('b -> 'c -> 'c) -> 'c -> ('a, 'b, 'c) t
create comb y0
returns a monitor for computations of type
'a -> 'b
, comb
being used to combine results with initial
result y0
.