1995-11-14 09:11:31 -08:00
|
|
|
(***********************************************************************)
|
|
|
|
(* *)
|
1996-04-30 07:53:58 -07:00
|
|
|
(* Objective Caml *)
|
1995-11-14 09:11:31 -08:00
|
|
|
(* *)
|
|
|
|
(* David Nowak and Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
|
|
|
|
(* *)
|
1996-04-30 07:53:58 -07:00
|
|
|
(* Copyright 1996 Institut National de Recherche en Informatique et *)
|
1999-11-17 10:59:06 -08:00
|
|
|
(* en Automatique. All rights reserved. This file is distributed *)
|
2001-12-07 05:41:02 -08:00
|
|
|
(* under the terms of the GNU Library General Public License, with *)
|
|
|
|
(* the special exception on linking described in file ../../LICENSE. *)
|
1995-11-14 09:11:31 -08:00
|
|
|
(* *)
|
|
|
|
(***********************************************************************)
|
|
|
|
|
|
|
|
(* $Id$ *)
|
|
|
|
|
2001-10-29 12:07:20 -08:00
|
|
|
(** First-class synchronous communication.
|
1995-11-15 08:40:01 -08:00
|
|
|
|
2001-10-29 12:07:20 -08:00
|
|
|
This module implements synchronous inter-thread communications over
|
1995-11-15 08:40:01 -08:00
|
|
|
channels. As in John Reppy's Concurrent ML system, the communication
|
|
|
|
events are first-class values: they can be built and combined
|
2001-10-29 12:07:20 -08:00
|
|
|
independently before being offered for communication.
|
|
|
|
*)
|
1995-11-14 09:11:31 -08:00
|
|
|
|
1995-11-15 08:40:01 -08:00
|
|
|
type 'a channel
|
2001-12-04 08:16:05 -08:00
|
|
|
(** The type of communication channels carrying values of type ['a]. *)
|
2001-10-29 12:07:20 -08:00
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val new_channel : unit -> 'a channel
|
2001-10-29 12:07:20 -08:00
|
|
|
(** Return a new channel. *)
|
1995-11-14 09:11:31 -08:00
|
|
|
|
|
|
|
type 'a event
|
2001-12-04 08:16:05 -08:00
|
|
|
(** The type of communication events returning a result of type ['a]. *)
|
2001-10-29 12:07:20 -08:00
|
|
|
|
|
|
|
(** [send ch v] returns the event consisting in sending the value [v]
|
|
|
|
over the channel [ch]. The result value of this event is [()]. *)
|
2001-12-04 08:16:05 -08:00
|
|
|
val send : 'a channel -> 'a -> unit event
|
2001-10-29 12:07:20 -08:00
|
|
|
|
|
|
|
(** [receive ch] returns the event consisting in receiving a value
|
|
|
|
from the channel [ch]. The result value of this event is the
|
|
|
|
value received. *)
|
2001-12-04 08:16:05 -08:00
|
|
|
val receive : 'a channel -> 'a event
|
2001-10-29 12:07:20 -08:00
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val always : 'a -> 'a event
|
2001-10-29 12:07:20 -08:00
|
|
|
(** [always v] returns an event that is always ready for
|
|
|
|
synchronization. The result value of this event is [v]. *)
|
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val choose : 'a event list -> 'a event
|
2001-10-29 12:07:20 -08:00
|
|
|
(** [choose evl] returns the event that is the alternative of
|
|
|
|
all the events in the list [evl]. *)
|
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val wrap : 'a event -> ('a -> 'b) -> 'b event
|
2001-10-29 12:07:20 -08:00
|
|
|
(** [wrap ev fn] returns the event that performs the same communications
|
|
|
|
as [ev], then applies the post-processing function [fn]
|
|
|
|
on the return value. *)
|
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val wrap_abort : 'a event -> (unit -> unit) -> 'a event
|
2001-10-29 12:07:20 -08:00
|
|
|
(** [wrap_abort ev fn] returns the event that performs
|
|
|
|
the same communications as [ev], but if it is not selected
|
|
|
|
the function [fn] is called after the synchronization. *)
|
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val guard : (unit -> 'a event) -> 'a event
|
2001-10-29 12:07:20 -08:00
|
|
|
(** [guard fn] returns the event that, when synchronized, computes
|
|
|
|
[fn()] and behaves as the resulting event. This allows to
|
|
|
|
compute events with side-effects at the time of the synchronization
|
|
|
|
operation. *)
|
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val sync : 'a event -> 'a
|
2001-10-29 12:07:20 -08:00
|
|
|
(** ``Synchronize'' on an event: offer all the communication
|
|
|
|
possibilities specified in the event to the outside world,
|
|
|
|
and block until one of the communications succeed. The result
|
|
|
|
value of that communication is returned. *)
|
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val select : 'a event list -> 'a
|
2001-10-29 12:07:20 -08:00
|
|
|
(** ``Synchronize'' on an alternative of events.
|
|
|
|
[select evl] is shorthand for [sync(choose evl)]. *)
|
|
|
|
|
2001-12-04 08:16:05 -08:00
|
|
|
val poll : 'a event -> 'a option
|
2001-10-29 12:07:20 -08:00
|
|
|
(** Non-blocking version of {!Event.sync}: offer all the communication
|
|
|
|
possibilities specified in the event to the outside world,
|
|
|
|
and if one can take place immediately, perform it and return
|
|
|
|
[Some r] where [r] is the result value of that communication.
|
|
|
|
Otherwise, return [None] without blocking. *)
|
|
|
|
|