synmod.tex

\section{Syntax of Modules}
\label{syn-mod-sec}
For Modules there are further reserved words, identifier classes and derived
forms. There are no further special constants; 
comments and lexical analysis are as for the Core.
The derived forms for modules appear in 
Appendix~\ref{derived-forms-app}.

%For Modules there are further keywords and identifier classes, but no
%further special constants and at present no further derived forms.  
%Comments and lexical analysis are as for the Core.

\subsection{Reserved Words}
The\index{14.1} following are the additional reserved words used in Modules.
% (cvr
% \begin{verbatim}
%              eqtype  functor    include   sharing
%              sig     signature  struct  structure
% \end{verbatim}

\begin{verbatim}
             eqtype  include  sharing  sig  struct  :>
\end{verbatim}
% cvr)
\subsection{Identifiers}
\label{syn-mod-identifiers-sec}
The additional syntax classes for Modules are \SigId\ (signature identifiers), \FunId\ (functor identifiers), and \ModId\ (unresolved identifiers that may be resolved to either structure or functor identifiers)
; they may be either alphanumeric -- not
starting with a prime -- or symbolic.  Functor and module identifiers
may be long, in the sense of Section \ref{cyn-core-identifiers-sec}.
(Long) module identifiers range of the union of (long) structure identifiers and (long) functor identifiers: the interpretation of a (long) module identifier cannot be determined grammatically, but
is resolved during elaboration.
Otherwise, the class of each identifier occurrence
is determined by the grammatical rules which follow.
Henceforth, therefore, we consider all identifier classes (excluding \ModId\ and \LongModId) to be disjoint.

\subsection{Infixed operators}
In addition to the scope rules for fixity directives given for the Core syntax,
there is a further scope limitation:
% (cvr
% if $\dir$ occurs in a  structure-level declaration $\strdec$ in any of the 
% phrases
% \[ \LET\ \dec\ \IN\ \cdots\ \END \]
% \[ \LOCAL\ \strdec\ \IN\ \cdots\ \END \] % (cvr)
% \[ \STRUCT\ \strdec\ \END \]
% then the scope of $\dir$ does not extend beyond the phrase.
if $\dir$ occurs in a declaration $\dec$ in any of the 
phrases
\[ \LET\ \dec\ \IN\ \cdots\ \END \]
\[ \STRUCT\ \dec\ \END \]
\[ \SIG\ \spec\ \END \]
then the scope of $\dir$ does not extend beyond the phrase.
% cvr)

% (cvr
% One effect of this limitation is that fixity is local to a generative
% structure expression -- in particular, to such an expression occurring
% as a functor body.  A more liberal scheme (which is under consideration)
% would allow fixity directives to appear also as specifications, so that
% fixity may be dictated by a signature expression; furthermore, it would allow an ~$\OPEN$~
% or ~$\INCLUDE$~ construction to restore the fixity which prevailed
% in the structures being opened, or in the signatures being included.
% This scheme is not adopted at present.
One effect of this limitation is that fixity is local to a basic
structure expression -- in particular, to such an expression occurring
as a functor body. 
Similarly, fixity is local to a basic signature expression.

Fixity directives (but not ~$\OP$~) are omitted from the Modules semantic rules, since they affect only parsing.

% cvr)

\subsection{Grammar for Modules}
\label{mod-gram-sec}
The\index{14.2} phrase classes for Modules are shown in Figure~\ref{mod-phr}.
% (cvr
% We use the variable $\strexp$ to range over StrExp, etc
We use the variable $\atmodexp$ to range over AtModExp, etc.
% cvr)
The conventions adopted in presenting the grammatical 
%\pagebreak
\begin{figure}[tp]
\vspace{4pt}
\makeatletter{}
\tabskip\@centering
\halign to\textwidth
{#\hfil\tabskip1em&#\hfil\tabskip\@centering\cr
% StrExp & structure expressions \cr % (cvr)
AtModExp & atomic module expressions \cr % (cvr)
ModExp & module expressions \cr % (cvr)
\cr
% StrDec & structure-level declarations \cr % (cvr)
StrBind & structure bindings \cr % (cvr)
FunBind & functor bindings\cr
SigBind & signature bindings \cr
\cr
SigExp & signature expressions \cr
% SigDec & signature declarations \cr % (cvr)
\cr
Spec & specifications \cr
ValDesc & value descriptions\cr
TypDesc & type descriptions\cr
DatDesc & datatype descriptions\cr
ConDesc & constructor descriptions\cr
ExDesc & exception descriptions\cr
StrDesc & structure descriptions\cr % (cvr)
FunDesc & functor descriptions\cr % (cvr)
% SharEq & sharing equations\cr % (cvr)
% \cr
% FunDec & functor declarations\cr  % (cvr)
% (cvr 
% FunSigExp & functor signature expressions\cr 
% FunSpec & functor specifications\cr
% FunDesc & functor descriptions\cr
% TopDec  & top-level declarations\cr
% cvr)
}
\makeatother
\caption{Modules Phrase Classes\index{15.1}}
\label{mod-phr}
\end{figure}
rules for Modules
are the same as for the Core.
% (cvr
% The grammatical rules are shown in Figures~\ref{str-syn},
% \ref{spec-syn} and \ref{prog-syn}.
The grammatical rules are shown in Figures~\ref{str-syn} and
\ref{spec-syn}.
% cvr)
% (cvr
% It should be noted that functor specifications (FunSpec) cannot
% occur in programs;
% neither can the associated functor descriptions (FunDesc)
% and functor signature expressions (FunSigExp).  The purpose of a $\funspec$
% is to specify the static attributes (i.e. functor signature) of one
% or more functors. This will be useful, in fact essential, for
% separate compilation of functors. If, for example, a functor $g$
% refers to another functor $f$ then --- in order to compile $g$ in
% the absence of the declaration of $f$ --- at least the specification
% of $f$ (i.e. its functor signature) must be available. At present there is no
% special grammatical form for  a separately compilable ``chunk'' of text
% -- which we may like to call call a {\sl module} -- containing a $\fundec$
% together with a $\funspec$ specifying its global references. However, below in
% the semantics for Modules it is defined when a
% declared functor matches a functor signature specified for it. This determines
% exactly those functor environments (containing declared functors
% such as $f$) into which the separately compiled ``chunk''
% containing the declaration of $g$ may be loaded.
% cvr)

%\newpage
\begin{figure}[tp]
\vspace{4pt}
\makeatletter{}
\tabskip\@centering
\halign to\textwidth
{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr
% cvr
% \strexp & ::=	& \encstrexp	& generative\cr
% 	&	& \longstrid	& structure identifier\cr
% 	&	& \funappstr	& functor application\cr
%         &       & \letstrexp    & local declaration\cr
\atmodexp & ::=	& \decatmodexp	& basic\cr
	&	& \opp\longmodid & module identifier\cr
%	&	& \anonatmodexp	& module projection\cr
	&	& \letatmodexp	& local declaration\cr
        &       & \paratmodexp  & \cr
\noalign{\vspace{6pt}}
\modexp & ::=	& \atmodexp	& atomic \cr
        &       & \appmodexp    &  functor application \cr
	&	& \conmodexp	& transparent constraint\cr
        &       & \absmodexp	& opaque constraint\cr
        &       & \genfunctormodexp & generative functor \cr
        &       & \appfunctormodexp & applicative functor \cr
	&	& \recmodexp	& recursive structure\cr
%
% \strdec	& ::=	& \dec                          & declaration \cr
%         &       & \singstrdec    		& structure \cr
%         &       & \localstrdec                  & local \cr
%         &       & \emptystrdec                  & empty \cr
% 	&	& \seqstrdec			& sequential\cr
\noalign{\vspace{6pt}}
\strbind & ::=   & \strbinder & structure binding \cr	
         &       & \asstrbinder & package binding \cr
%\modbind & ::=   & \modbinder \cr
% (cvr
\noalign{\vspace{6pt}} 
\funbind & ::= & \funbinder           & functor binding \cr
         &     & \asfunbinder         & package binding \cr
% cvr)
\noalign{\vspace{6pt}}
\sigbind & ::=   & \sigbinder \cr
% (cvr
\noalign{\vspace{6pt}}
\sigexp	& ::=	& \specsigexp    	& basic\cr
	&	& \sigid		& signature identifier\cr
%	&	& \wheresigexp		& type realisation\cr
	&	& \mbox{$\sigexp\ \WHERE\ \TYPE\ $} & type realisation\cr
	&	&  \qquad\qquad \mbox{$ \tyidseq\ \longtycon\ \tteq\ \ty $} & \cr
	&	& \opfunsigexp		& opaque functor signature\cr
	&	& \trfunsigexp		& transparent functor signature\cr
	&	& \recsigexp		& recursive structure signature\cr
% sigexp	& ::=	& \encsigexp    	& generative\cr
%	&	& \sigid		& signature identifier\cr
% \noalign{\vspace{6pt}}
% \sigdec & ::=   & \singsigdec           & single\cr
%         &       & \emptysigdec          & empty\cr
%         &       & \seqsigdec            & sequential\cr
% cvr)
%\noalign{\vspace{6pt}}
}
\makeatother
\vspace{3pt}
\caption{Grammar: Structure and Signature Expressions\index{16.1}}
\label{str-syn}
\end{figure}

\subsection{Syntactic Restrictions}
\begin{itemize}
% (cvr
% \item No\index{16.2} binding $\strbind$, $\sigbind$, or $\funbind$ may bind the
%       same identifier twice.
% \item No description $\valdesc$, $\typdesc$, $\datdesc$, 
%       $\exndesc$, $\strdesc$ or $\fundesc$ may describe the same identifier
%       twice; this applies also to value constructors within a $\datdesc$.
\item No\index{16.2} binding $\strbind$, $\funbind$, or $\sigbind$ may bind the
      same identifier twice.
\item No description $\valdesc$, $\typdesc$, $\datdesc$, 
       $\exndesc$ or $\strdesc$ or $\fundesc$ may describe the same identifier
       twice; this applies also to value constructors within a $\datdesc$.
\item No ${\it tyvarseq}$ may contain the same ${\it tyvar}$ twice.
\item No $\datdesc$, $\valdesc$ 
or $\exndesc$ may describe 
$\TRUE$, $\FALSE$, $\NIL$, $\CONS$ or $\REF$.
No $\datdesc$ or $\exndesc$ may describe {\tt it}.
% cvr)
\end{itemize}
%\clearpage %containing figure 'Grammar: Specifications'
\begin{figure}[tp]
\vspace{4pt}
\makeatletter{}
\tabskip\@centering
\halign to\textwidth
{#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr
\spec	& ::=	& \valspec		& value\cr
	&	& \typespec		& type\cr
	&	& \eqtypespec		& eqtype\cr
	&	& \datatypespec		& datatype\cr
% (cvr
        &       & \datatyperepspec & replication \cr
% cvr)        
	&       & \exceptionspec        & exception\cr
        &	& \structurespec	& structure\cr
        &       & \functorspec          & functor\cr
        &       & \signaturespec        & signature\cr
%	&	& \sharingspec	        & sharing\cr
%       &       & \localspec    	& local\cr
%       &       & \openspec             & open ($n\geq 1$) \cr
        &       & \includespec             & include \cr
        &       & \emptyspec            & empty \cr
 	&	& \seqspec		& sequential\cr
%	&	& \sharespec	        & sharing \cr
	&	& {\mbox{$\spec\ \SHARING\ \TYPE\ $}}      & sharing \cr
        &       & \qquad{\mbox{$\longtycon_1\ \tteq\ \cdots\ 
                                \tteq\ \longtycon_n $}}    & \qquad ($n\geq2$)\cr
        &       & \longinfix    & infix (L) directive\cr
        &       & \longinfixr   & infix (R) directive\cr
        &       & \longnonfix   & nonfix directive\cr
\noalign{\vspace{6pt}}
\valdesc & ::=   & \valdescription \cr
\noalign{\vspace{6pt}}
\typdesc & ::=   & \typdescription \cr
\noalign{\vspace{6pt}}
\datdesc & ::=   & \datdescription \cr
\noalign{\vspace{6pt}}
\condesc & ::=   & \condescription \cr
\noalign{\vspace{6pt}}
\exndesc & ::=   & \exndescription \cr
\noalign{\vspace{6pt}}
% \strdesc & ::=   & \strdescription \cr
\strdesc & ::=   & \strdescription \cr
\fundesc & ::=   & \fundescription \cr
% (cvr
% \noalign{\vspace{6pt}}
% \shareq & ::=   & \strshareq            & structure sharing\cr
%         &       &                       & \qquad ($n\geq 2$) \cr
%         &       & \typshareq            & type sharing \cr
%         &       &                       & \qquad ($n\geq 2$) \cr
%         &       & \multshareq           & multiple\cr
% cvr)
\noalign{\vspace{6pt}}
}
\makeatother
\vspace{3pt}
\caption{Grammar: Specifications\index{17}}
\label{spec-syn}
\end{figure}
%\clearpage %starting with Figure 'Grammar: Functors and Top-level declarations'

% (cvr
% \begin{figure}[t]
% \vspace{4pt}
% \makeatletter{}
% \tabskip\@centering
% \halign to\textwidth
% {#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr
% \fundec & ::=  & \singfundec           & single\cr
%         &      & \emptyfundec          & empty\cr
%         &      & \seqfundec            & sequence\cr
% \noalign{\vspace{6pt}}
% \funbind & ::= & \funstrbinder           & functor binding \cr
%          &     & \qquad\qquad\qquad\qquad\optfunbinda \cr}
% \vspace*{6pt}
% \halign to\textwidth
% {#\hfil\tabskip1em&\hfil$#$\hfil&#\hfil&#\hfil\tabskip\@centering\cr

% \funsigexp & ::= & \longfunsigexpa       & functor signature expression\cr
% \noalign{\vspace{6pt}}
%  \funspec & ::= & \singfunspec          & functor specification\cr
%         &     & \emptyfunspec		& empty\cr
%         &     & \seqfunspec		& sequence\cr
%  \noalign{\vspace{6pt}}
%  \fundesc & ::= & \longfundesc\cr
%  \noalign{\vspace{6pt}}

% \topdec  & ::= & \strdec               & structure-level declaration\cr
%          &     & \sigdec               & signature declaration\cr
%          &     & \fundec               & functor declaration\cr
% % \noalign{\vspace{6pt}}
% %\program & ::= & \longprog             & \cr
% %from version 1:
% %\program & ::= & \strdec               & structure-level declaration\cr
% %         &     & \sigdec               & signature declaration\cr
% %         &     & \fundec               & functor declaration\cr
% %         &     & \seqprog              & sequence\cr
% \noalign{\vspace{6pt}\parbox{12cm}{{\sl Note:}\/ No $\topdec$ may
% contain, as an initial segment, a shorter top-level declaration followed by a semicolon.}
% }
% }
% \makeatother
% \vspace{3pt}
% \caption{Grammar: Functors and Top-level Declarations\index{18.1}}
% \label{prog-syn}
% \end{figure}
% cvr)

% (cvr
% \subsection{Closure Restrictions}
% \label{closure-restr-sec}
% The\index{18.2} semantics presented in later sections requires no restriction on
% reference to non-local identifiers. For example, it allows a signature 
% expression to refer to external signature identifiers and
% (via ~$\SHARING$~ or ~$\OPEN$~) to external structure identifiers; it also
% allows a functor to refer to external identifiers of any kind.

% However, implementers who want to provide a simple facility for
% separate compilation may want to impose the following restrictions
% (ignoring references to identifiers bound in the initial basis
% $\B_0$, which may occur anywhere):

% %However, in the present version of the language,
% %apart from references to identifiers bound in the initial basis $B_0$
% %(which may occur anywhere), it is required that signatures only refer
% %non-locally to signature identifiers and that functors only
% %refer non-locally to functor and signature identifiers.
% %These restrictions ease separate
% %compilation; however, they may be relaxed in a future version of the language.
% %
% %More precisely, the restrictions are as follows (ignoring reference to
% %identifiers bound in $B_0$):
% \begin{enumerate}
% \item In any signature binding ~$\sigid\ \mbox{{\tt =}}\ \sigexp$~,
% the only non-local
% references in $\sigexp$ are to signature identifiers.
% \item In any functor description ~$\funid\ \longfunsigexpa$~,
% the only non-local
% references in $\sigexp$ and $\sigexp'$ are to signature identifiers,
% except that $\sigexp'$ may refer to $\strid$ and its components.
% \item In any functor binding ~$\funstrbinder$~, the only non-local
% references in $\sigexp$, $\sigexp'$ and $\strexp$ are to functor and signature
% identifiers,
% except that both $\sigexp'$ and $\strexp$ may refer to $\strid$ and
% its components.
% \end{enumerate}
% In the last two cases the final qualification allows, for example, sharing
% constraints to be specified between functor argument and result.
% (For a completely precise definition of these closure restrictions,
% see the comments to rules \ref{single-sigdec-rule} 
% (page~\pageref{single-sigdec-rule}), twice
% \ref{singfunspec-rule} (page~\pageref{singfunspec-rule})
% and \ref{singfundec-rule} (page~\pageref{singfundec-rule})
% in the static semantics of modules, Section~\ref{statmod-sec}.)
%
% The\index{19.1} 
% significance of these restrictions is that they may ease separate
% compilation; this may be seen as follows. If one takes a {\sl module}
% to be a sequence of signature declarations, functor specifications
% and functor declarations satisfying the above restrictions then the
% elaboration of a module can be made to depend on the initial
% static basis alone (in particular, it will not rely on
% structures outside the module). Moreover, the elaboration 
% of a module cannot create new free structure or type names, so 
% name consistency (as defined in Section~\ref{consistency-sec}, 
% page \pageref{consistency-sec}) is automatically preserved
% across separately compiled modules. On the other hand,
% imposing these restrictions may force the programmer to write
% many more sharing equations than is needed if functors
% and signature expressions can refer to free structures.
% cvr)