mailbox.tex

这是我们参加06年全国开源软件的竞赛作品

\maybeclearpage
\section{The {\cf Mailbox}\marginref{Mailbox}{str-Mailbox}{strMailbox} structure}


The {\cf \small Mailbox}\marginref{Mailbox}{str-Mailbox}{strMailbox} structure provides buffered asynchronous channels, which we call mailboxes. 
\begin{synopsis}
\item {\kw{signature}} \textcf{MAILBOX}\label{sig-MAILBOX}
\item {\STRUCTURE} \textcf{Mailbox: MAILBOX}\label{str-Mailbox}
\end{synopsis}

\begin{interface}
\Nopagebreak
\item {\index{mbox@mbox!MAILBOX@\textcf{MAILBOX}}}{\kw{type}} \(\alpha\)~\textcf{mbox}
\Nopagebreak
\item {\index{mailbox@mailbox!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf mailbox: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}mbox}\)}

\Nopagebreak
\item {\index{sameMailbox@sameMailbox!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf sameMailbox: \((\alpha\mtoksep{}\mbox{\cf{}mbox}\mtoksep{}\verb,*,\mtoksep{}\alpha\mtoksep{}\mbox{\cf{}mbox})\rightarrow \mbox{\cf{}bool}\)}

\Nopagebreak
\item {\index{send@send!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf send: \((\alpha\mtoksep{}\mbox{\cf{}mbox}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}unit}\)}

\Nopagebreak
\item {\index{recv@recv!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf recv: \(\alpha\mtoksep{}\mbox{\cf{}mbox}\rightarrow \alpha\)}

\Nopagebreak
\item {\index{recvEvt@recvEvt!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf recvEvt: \(\alpha\mtoksep{}\mbox{\cf{}mbox}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}

\Nopagebreak
\item {\index{recvPoll@recvPoll!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf recvPoll: \(\alpha\mtoksep{}\mbox{\cf{}mbox}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}

\end{interface}

\begin{descr}
\item {\index{mbox@mbox!MAILBOX@\textcf{MAILBOX}}}{\kw{type}} \(\alpha\)~\textcf{mbox}\label{ty-MAILBOX.mbox}

\begin{speccomment}
\item 

	This is the type constructor for a mailbox. 	A mailbox is an unbounded, buffered communication channel.     \end{speccomment}
\item {\index{mailbox@mailbox!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf mailbox: \(\mbox{\cf{}unit}\rightarrow \alpha\mtoksep{}\mbox{\cf{}mbox}\)}\label{val-MAILBOX.mailbox}


\begin{speccomment}
\item {\cf \small mailbox ()         } 
creates a new mailbox.     \end{speccomment}
\item {\index{sameMailbox@sameMailbox!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf sameMailbox: \((\alpha\mtoksep{}\mbox{\cf{}mbox}\mtoksep{}\verb,*,\mtoksep{}\alpha\mtoksep{}\mbox{\cf{}mbox})\rightarrow \mbox{\cf{}bool}\)}\label{val-MAILBOX.sameMailbox}


\begin{speccomment}
\item {\cf \small same\-Mailbox (\mbox{\cf \small \textit{mb1}}, \mbox{\cf \small \textit{mb2}})         } 
returns {\cf \small true}, if \mbox{\cf \small \textit{mb1}} and \mbox{\cf \small \textit{mb2}} are the same mailbox.     \end{speccomment}
\item {\index{send@send!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf send: \((\alpha\mtoksep{}\mbox{\cf{}mbox}\mtoksep{}\verb,*,\mtoksep{}\alpha)\rightarrow \mbox{\cf{}unit}\)}\label{val-MAILBOX.send}


\begin{speccomment}
\item {\cf \small send (\mbox{\cf \small \textit{mb}}, \mbox{\cf \small \textit{msg}})         } 
sends the message \mbox{\cf \small \textit{msg}} to the mailbox \mbox{\cf \small \textit{mb}}. 	Note that unlike {\cf \small CML.\-send}\marginref{send}{val-CML.send}{valCMLsend}, this is a non-blocking 	operation.     \end{speccomment}
\item {\index{recv@recv!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf recv: \(\alpha\mtoksep{}\mbox{\cf{}mbox}\rightarrow \alpha\)}\label{val-MAILBOX.recv}


\begin{speccomment}
\item {\cf \small recv \mbox{\cf \small \textit{mb}}         } 
receive the next message from the mailbox \mbox{\cf \small \textit{mb}}. 	If, the mailbox is empty, then this blocks the calling 	thread until there is a message available.     \end{speccomment}
\item {\index{recvEvt@recvEvt!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf recvEvt: \(\alpha\mtoksep{}\mbox{\cf{}mbox}\rightarrow \alpha\mtoksep{}\mbox{\cf{}event}\)}\label{val-MAILBOX.recvEvt}


\begin{speccomment}
\item {\cf \small recv\-Evt \mbox{\cf \small \textit{mb}}         } 
returns the event value that represents the {\cf \small recv} operation 	on \mbox{\cf \small \textit{mb}}.     \end{speccomment}
\item {\index{recvPoll@recvPoll!MAILBOX@\textcf{MAILBOX}}}{\kw{val}} {\cf recvPoll: \(\alpha\mtoksep{}\mbox{\cf{}mbox}\rightarrow \alpha\mtoksep{}\mbox{\cf{}option}\)}\label{val-MAILBOX.recvPoll}


\begin{speccomment}
\item 

        This is the non-blocking version of {\cf \small recv}. 	If the corresponding blocking form would block (because the mailbox is 	empty), then this returns 	{\cf \small NONE}, otherwise it returns 	{\cf \small SOME} of the received 	message.\end{speccomment}
\end{descr}


Note that mailbox buffers are unbounded, which means that there is no flow control to prevent a producer from greatly outstriping a consumer, and thus exhausting memory. In situations where there is no natural limit to the rate of {\cf \small send}\marginref{send}{val-MAILBOX.send}{valMAILBOXsend} operations, it is recommended that the synchronous channels from the {\cf \small CML}\marginref{CML}{str-CML}{strCML} structure be used instead.
\begin{seealso}
{\cf CML} (\pageref{str-CML})
\end{seealso}