[MLton] cvs commit: MAIL: extracted MLB formalism to separate document
Matthew Fluet
fluet@mlton.org
Tue, 12 Oct 2004 19:16:23 -0700
fluet 04/10/12 19:16:23
Modified: doc/user-guide Makefile main.tex mlb.tex
Added: doc/mlb-formal .cvsignore Makefile bib.bib macros.tex
mlb-formal.tex
Removed: doc/user-guide mlb-formal.tex
Log:
MAIL: extracted MLB formalism to separate document
Revision Changes Path
1.1 mlton/doc/mlb-formal/.cvsignore
Index: .cvsignore
===================================================================
*~
*.aux
*.bbl
*.blg
*.log
*.toc
TAGS
core
mlb-formal
mlb-formal.dvi
mlb-formal.pdf
mlb-formal.ps
mlb-formal.ps.gz
1.1 mlton/doc/mlb-formal/Makefile
Index: Makefile
===================================================================
TEX_FILES = \
bib.bib \
mlb-formal.tex
all: mlb-formal.ps mlb-formal.pdf
mlb-formal.dvi: $(TEX_FILES)
latex mlb-formal; bibtex mlb-formal; latex mlb-formal; latex mlb-formal
mlb-formal.pdf: $(TEX_FILES)
latex mlb-formal
bibtex mlb-formal
latex mlb-formal
pdflatex mlb-formal
mlb-formal.ps: mlb-formal.dvi
dvips -o mlb-formal.ps mlb-formal
.PHONY: clean
clean:
../../bin/clean
.PHONY: tags
tags:
etags *.tex
1.1 mlton/doc/mlb-formal/bib.bib
Index: bib.bib
===================================================================
@string{and = " and "}
@string{harper = "Robert Harper"}
@string{macqueen = "David~B. MacQueen"}
@string{milner = "Robin Milner"}
@string{tofte = "Mads Tofte"}
@book(MTHM97,
author = milner # and # tofte # and # harper # and # macqueen,
title = "The Definition of Standard ML (Revised)",
publisher = "MIT Press",
year = 1997)
1.1 mlton/doc/mlb-formal/macros.tex
Index: macros.tex
===================================================================
\newcommand{\mlton}{MLton}
1.1 mlton/doc/mlb-formal/mlb-formal.tex
Index: mlb-formal.tex
===================================================================
\documentclass[draft]{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amssymb}
\include{macros}
% math fonts
\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\renewcommand{\mit}[1]{\mathit{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mtt}[1]{\mathtt{#1}}
\newcommand{\mcal}[1]{\mathcal{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
% text fonts
\newcommand{\ttt}[1]{\texttt{#1}}
% formatting
\newenvironment{stackAux}[2]{%
\setlength{\arraycolsep}{0pt}
\begin{array}[#1]{#2}}{
\end{array}}
\newenvironment{stackCC}{
\begin{stackAux}{c}{c}}{\end{stackAux}}
\newenvironment{stackCL}{
\begin{stackAux}{c}{l}}{\end{stackAux}}
\newenvironment{stackTL}{
\begin{stackAux}{t}{l}}{\end{stackAux}}
\newenvironment{stackTR}{
\begin{stackAux}{t}{r}}{\end{stackAux}}
\newenvironment{stackBC}{
\begin{stackAux}{b}{c}}{\end{stackAux}}
\newenvironment{stackBL}{
\begin{stackAux}{b}{l}}{\end{stackAux}}
\newcommand{\stagger}[2]{%
\begin{array}{ccc}%
\multicolumn{2}{l}{#1}&\\%
&\multicolumn{2}{r}{#2}%
\end{array}}
\newcommand{\axiom}[1]{{\displaystyle\strut{#1}}}
\newcommand{\infrule}[2]{{\frac{\displaystyle\strut{#1}}{\displaystyle\strut{#2}}}}
\newcommand{\judge}[2]{\infrule{#1}{#2}}
\begin{document}
\title{Formal Specification of MLBs}
\author{Copyright \copyright\ 2004\\
Henry Cejtin, Matthew Fluet, Suresh Jagannathan, and Stephen Weeks}
\date{\today}
\maketitle
%
This document formally specifies the ML Basis system (MLBs) in {\mlton}
used to program in the large. The system has been designed to be a
natural extension of Standard ML, and the specification is given in
the style of The Definition of Standard ML~\cite{MTHM97} (henceforeth,
the Definition). This section adopts (often silently) abbreviations,
conventions, definitions, and notation from the Definition.
%
\section{Syntax of MLBs}
For MLBs 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 and Modules. The derived forms
appear in Appendix~\ref{sec:mlb:DerivedForms}.
%
\subsection{Reserved Words}
The following are the additional reserved words used in MLBs.
\begin{displaymath}
\mtt{bas} \quad\quad \mtt{basis}
\end{displaymath}
Note that many of the reserved words from the Core and Modules are not
used by the grammar of MLBs. However, as the grammar includes
identifiers from the grammars of the Core and Modules, it is useful to
consider the reserved words from the Core and Modules to be reserved
in MLBs as well.
%
\subsection{Identifiers}
The additional identifier class for MLBs are $\mrm{BasId}$ (basis
identifiers). Basis identifiers must be alphanumeric, not starting
with a prime. The class of each identifier occurence is determined by
the grammatical rules which follow. Henceforth, therefore, we
consider all identifier classes to be disjoint.
%
\subsection{Infixed operators}
The grammar of MLBs does not directly admit fixity directives.
However, the static and dynamic semantics for MLBs will import source
files that must be parsed in the scope of fixity directives and that
may introduce additional fixity directives into scope.
Figure~\ref{fig:mlb:S:FixityEnv} formalizes the Definition's notion of
\emph{infix status} as a \emph{fixity environment}.
\begin{figure}[h]
\begin{displaymath}
\begin{array}{rcl}
& & \mrm{InfixStatus} = \{\mtt{nonfix}\} \cup \bigcup_{d \in \{0,\ldots,9\}} \{\mtt{infix}~d, \mtt{infixr}~d\} \\
\mit{FE} & \in & \mrm{FixEnv} = \mrm{VId} \xrightarrow{\mrm{fin}} \mrm{InfixStatus} \end{array}
\end{displaymath}
\caption{Fixity Environment}\label{fig:mlb:S:FixityEnv}
\end{figure}
%
\subsection{Grammar for MLBs}
The phrase classes for MLBs are shown in
Figure~\ref{fig:mlb:S:PhraseClasses}.
\begin{figure}[h]
\begin{displaymath}
\begin{array}{ll}
\mrm{BasExp} & \mbox{basis expressions} \\
\mrm{BasDec} & \mbox{basis-level declaration} \\
\mrm{BasBind} & \mbox{basis bindings} \\
\mrm{BStrBind} & \mbox{(basis) structure bindings} \\
\mrm{BSigBind} & \mbox{(basis) signature bindings} \\
\mrm{BFunBind} & \mbox{(basis) functor bindings}
\end{array}
\end{displaymath}
\caption{MLBs Phrase Classes}\label{fig:mlb:S:PhraseClasses}
\end{figure}
We use the variable $\mit{basexp}$ to range over $\mrm{BasExp}$, etc.
The conventions adopted in presenting the grammatical rulse for MLBs
are the same as for the Core and Modules. The grammatical rules are
showin in Figure~\ref{fig:mlb:S:GrammaticalRules}.
\begin{figure}[h]
\begin{displaymath}
\begin{array}{rcll}
\mit{basexp} & ::= &
\mtt{bas}~ \mit{basdec} ~\mtt{end}
& \mbox{basic} \\&&
\mit{basid}
& \mbox{basis identifier} \\&&
\mtt{let}~ \mit{basdec} ~\mtt{in}~ \mit{basexp} ~\mtt{end}
& \mbox{local declaration} \\
\mit{basdec} & ::= &
\mtt{basis}~ \mit{basbind}
& \mbox{basis} \\&&
\mtt{local}~ \mit{basdec}_1 ~\mtt{in}~ \mit{basdec}_2 ~\mtt{end}
& \mbox{local} \\&&
\mtt{open}~ \mit{basid}_1 \cdots \mit{basid}_n
& \mbox{open ($n \geq 1$)} \\&&
\mtt{structure}~ \mit{bstrbind}
& \mbox{(basis) structure binding} \\&&
\mtt{signature}~ \mit{bsigbind}
& \mbox{(basis) signature binding} \\&&
\mtt{functor}~ \mit{bfunbind}
& \mbox{(basis) functor binding} \\&&
\quad
& \mbox{empty} \\&&
\mit{basdec}_1~\langle\mtt{;}\rangle~\mit{basdec}_2
& \mbox{sequential} \\&&
\msf{path.mlb} &
\mbox{import ML basis} \\&&
\msf{path.sml}
& \mbox{import source} \\
\mit{basbind} & ::= &
\mit{basid} ~\mtt{=}~ \mit{basexp} ~\langle\mtt{and}~ \mit{basbind}\rangle \\
\mit{bstrbind} & ::= &
\mit{strid}_1 ~\mtt{=}~ \mit{strid}_2 ~\langle\mtt{and}~ \mit{bstrbind}\rangle \\
\mit{bsigbind} & ::= &
\mit{sigid}_1 ~\mtt{=}~ \mit{sigid}_2 ~\langle\mtt{and}~ \mit{bsigbind}\rangle \\
\mit{bfunbind} & ::= &
\mit{funid}_1 ~\mtt{=}~ \mit{funid}_2 ~\langle\mtt{and}~ \mit{bfunbind}\rangle
\end{array}
\end{displaymath}
\caption{Grammar: Basis Expressions, Declarations, and Bindings}\label{fig:mlb:S:GrammaticalRules}
\end{figure}
%
\subsection{Syntactic Restrictions}
\begin{itemize}
\item No binding $\mit{basbind}$ may bind the same identifier twice.
\item No binding $\mit{bstrbind}$, $\mit{bsigbind}$ or $\mit{bfunbind}$ may bind the same identifier twice.
\item MLBs may not be cyclic; i.e., successively replacing
$\msf{path.mlb}$ with it's parsed $\mrm{BasDec}$ must terminate.
\end{itemize}
%
\subsection{Parsing}
The static and dynamic semantics for MLBs will interpret
$\msf{path.sml}$ as a parsed $\mrm{TopDec}$ and
$\msf{path.mlb}$ as a parsed $\mrm{BasDec}$. Parsing a $\mrm{TopDec}$
takes a fixity environment as input and returns a fixity environment
as output; the output fixity environment corresponds to fixity
directives introduced by and whose scope is not limited by the parsed
$\mrm{TopDec}$.
Paths and parsers are given in Figure~\ref{fig:mlb:S:PathsParser}. A
(fixed) $\mrm{Parser}$ $\mcal{P}$ provides the interpretation of
$\msf{path.sml}$ and $\msf{path.mlb}$ imports.
\begin{figure}[h]
\begin{displaymath}
\begin{array}{c}
\begin{array}{rcl}
\msf{path.sml} & \in & \mrm{SourcePath} \\
\msf{path.mlb} & \in & \mrm{MLBasisPath}
\end{array} \\
\begin{array}{rcl}
\mcal{P} & \in & \mrm{Parser} =
((\mrm{FixEnv} \times \mrm{SourcePath})
\xrightarrow{\mrm{fin}} (\mrm{FixEnv} \times \mrm{TopDec}))
\times
(\mrm{MLBasisPath} \xrightarrow{\mrm{fin}} \mrm{BasDec})
\end{array}
\end{array}
\end{displaymath}
\caption{Parser}\label{fig:mlb:S:PathsParser}
\end{figure}
%
For a file extension $\msf{.ext}$, $\msf{path.ext}$ denotes either an
absolute path or a relative path (relative to the $\mrm{BasDec}$ being
parsed) to a file in the underlying file system. Paths that denote the same
file in the underlying file system are considered equal, though they may
have distinct textual representations. An implementation
may allow additional extensions (e.g., $\mtt{.ML}$, $\mtt{.fun}$,
$\mtt{.sig}$) in elements of $\mrm{SourcePath}$. An implementation
may additionally allow path variables to appear in
paths. $\mrm{Parser}$ could be refined by a \emph{current working
directory}, to formally specify the interpretation of relative paths,
and an \emph{path map}, to formally specify the
interpretation of path variables, but the above suffices
for the development in the following sections.
%
\section{Static Semantics for MLBs}
%
\subsection{Semantic Objects}
The simple objects for the MLBs static semantics are exactly as for
Modules. The compound objects are those for Modules, augmented by
those in Figure~\ref{fig:mlb:SS:CompoundObjects}.
\begin{figure}[h]
\begin{displaymath}
\begin{array}{rcl}
\mit{BE} & \in & \mrm{BasEnv} = \mrm{BasId} \xrightarrow{\mrm{fin}} \mrm{MBasis} \\
\mit{M} ~\mrm{or}~ \mit{FE},\mit{BE},\mit{B} & \in &
\mrm{MBasis} = \mrm{FixEnv} \times \mrm{BasEnv} \times \mrm{Basis} \\
\Psi & \in & \mrm{BasCache} = \mrm{MLBasisPath} \xrightarrow{\mrm{fin}} \mrm{MBasis}
\end{array}
\end{displaymath}
\caption{Compound Semantic Objects}\label{fig:mlb:SS:CompoundObjects}
\end{figure}
The operations of projection, injection and modification are as for
Modules.
%
\subsection{Inference Rules}
As for the Core and for Modules, the rules for MLBs static semantics
allow sentences of the form
\begin{displaymath}
A \vdash \mit{phrase} \longrightarrow A'
\end{displaymath}
to be inferred. Some hypotheses in rules are not of this form; they
are called \emph{side-conditions}. The convention for options is as
in the Core and Modules semantics.
\vspace{2\parsep}
{\large\noindent
\textbf{Basis Expressions} \hfill
\fbox{$\mit{M}, \Psi \vdash \mit{basexp} \longrightarrow \mit{M}', \Psi'$}
}\nopagebreak
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi'
}{
\mit{M}, \Psi \vdash \mtt{bas}~ \mit{basdec} ~\mtt{end} \longrightarrow \mit{M}', \Psi'
}
\end{equation}
\begin{equation}
\judge{
\mit{M}(\mit{basid}) = \mit{M}'
}{
\mit{M}, \Psi \vdash \mit{basid} \longrightarrow \mit{M}', \Psi
}
\end{equation}
\begin{equation}
\label{eqn:mlb:SS:localDeclaration}
\judge{
\mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}_1, \Psi_1 \quad
\mit{M} \oplus \mit{M}_1, \Psi_1 \vdash \mit{basexp} \longrightarrow \mit{M}_2, \Psi_2
}{
\mit{M}, \Psi \vdash \mtt{let}~ \mit{basdec} ~\mtt{in}~ \mit{basexp} ~\mtt{end} \longrightarrow \mit{M}_2, \Psi_2
}
\end{equation}
\begin{samepage}
\noindent
\textit{Comments}:
\begin{itemize}
\item[(\ref{eqn:mlb:SS:localDeclaration})] The use of $\oplus$, here
and elsewhere, ensures that the type names generated by the first
sub-phrase are distinct from the names generated by the second sub-phrase.
\end{itemize}
\end{samepage}
\vspace{2\parsep}
{\large\noindent
\textbf{Basis-level Declarations} \hfill
\fbox{$\mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi'$}
}\nopagebreak
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basbind} \longrightarrow \mit{BE}', \Psi'
}{
\mit{M}, \Psi \vdash \msf{basis}~ \mit{basbind} \longrightarrow \mit{BE}' ~\mrm{in}~ \mrm{MBasis}, \Psi'
}
\end{equation}
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basdec}_1 \longrightarrow \mit{M}_1, \Psi_1 \quad
\mit{M} \oplus \mit{M}_1, \Psi_1 \vdash \mit{basdec}_2 \longrightarrow \mit{M}_2, \Psi_2 \quad
}{
\mit{M}, \Psi \vdash \mtt{local}~ \mit{basdec}_1 ~\mtt{in}~ \mit{basdec}_2 ~\mtt{end} \longrightarrow \mit{M}_2, \Psi_2
}
\end{equation}
\begin{equation}
\judge{
\mit{M}(\mit{basid}_1) = \mit{M}_1 \quad \cdots \quad
\mit{M}(\mit{basid}_n) = \mit{M}_n
}{
\mit{M}, \Psi \vdash \mtt{open}~ \mit{basid}_1 \cdots \mit{basid}_n \longrightarrow \mit{M}_1 \oplus \cdots \oplus \mit{M}_n, \Psi
}
\end{equation}
\begin{equation}
\judge{
\mit{B}~\mrm{of}~\mit{M} \vdash \mit{bstrbind} \longrightarrow SE
}{
\mit{M}, \Psi \vdash \mtt{structure}~ \mit{bstrbind}
\longrightarrow \mit{SE} ~\mrm{in}~ \mrm{MBasis}, \Psi
}
\end{equation}
\begin{equation}
\judge{
\mit{B}~\mrm{of}~\mit{M} \vdash \mit{bsigbind} \longrightarrow G
}{
\mit{M}, \Psi \vdash \mtt{signature}~ \mit{bsigbind}
\longrightarrow \mit{G } ~\mrm{in}~ \mrm{MBasis}, \Psi
}
\end{equation}
\begin{equation}
\judge{
\mit{B}~\mrm{of}~\mit{M} \vdash \mit{bfunbind} \longrightarrow F
}{
\mit{M}, \Psi \vdash \mtt{functor}~ \mit{bfunbind}
\longrightarrow \mit{F} ~\mrm{in}~ \mrm{MBasis}, \Psi
}
\end{equation}
\begin{equation}
\judge{
}{
\mit{M}, \Psi \vdash \quad \longrightarrow \{\} ~\mrm{in}~ \mrm{MBasis}, \Psi
}
\end{equation}
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basdec}_1 \longrightarrow \mit{M}_1, \Psi_1 \quad
\mit{M} \oplus \mit{M}_1, \Psi_1 \vdash \mit{basdec}_2 \longrightarrow \mit{M}_2, \Psi_2
}{
\mit{M}, \Psi \vdash \mit{basdec}_1 ~\langle\mtt{;}\rangle~ \mit{basdec}_2 \longrightarrow \mit{M}_1 \oplus \mit{M}_2, \Psi_2
}
\end{equation}
\begin{equation}
\label{eqn:mlb:SS:path.sml}
\judge{
\mcal{P}(\mit{FE}~\mrm{of}~\mit{M}, \msf{path.sml}) = (\mit{FE}', \mit{topdec}) \quad
\mit{B}~\mrm{of}~\mit{M} \vdash \mit{topdec} \Rightarrow \mit{B}'
}{
\mit{M}, \Psi \vdash \msf{path.sml} \longrightarrow (\mit{FE}',\{\},\mit{B}'), \Psi
}
\end{equation}
\begin{equation}
\judge{
\Psi(\msf{path.mlb}) = \mit{M}'
}{
\mit{M}, \Psi \vdash \msf{path.mlb} \longrightarrow \mit{M}', \Psi
}
\end{equation}
\begin{equation}
\judge{
\msf{path.mlb} \notin \mrm{Dom}~\Psi \quad
\mcal{P}(\msf{path.mlb}) = \mit{basdec} \quad
\{\} ~\mrm{in}~ \mrm{MBasis}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi'
}{
\mit{M}, \Psi \vdash \msf{path.mlb} \longrightarrow \mit{M}', \Psi' + \{\msf{path.mlb} \mapsto \mit{M}'\}
}
\end{equation}
\begin{samepage}
\noindent
\textit{Comments}:
\begin{itemize}
\item[(\ref{eqn:mlb:SS:path.sml})]
Note the use of the Definition's
$\mit{B} \vdash \mit{topdec} \Rightarrow \mit{B}'$.
\end{itemize}
\end{samepage}
\vspace{2\parsep}
{\large\noindent
\textbf{Basis Bindings} \hfill
\fbox{$\mit{M}, \Psi \vdash \mit{basbind} \longrightarrow \mit{BE}', \Psi'$}
}\nopagebreak
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basexp} \longrightarrow \mit{M}', \Psi' \quad
\langle\mit{M} + \mrm{tynames}~\mit{M}', \Psi' \vdash \mit{basbind} \longrightarrow \mit{BE}'', \Psi''\rangle
}{
\mit{M}, \Psi \vdash \mit{basid} ~\mtt{=}~ \mit{basexp} ~\langle\mtt{and}~\mit{basbind}\rangle \longrightarrow
\{\mit{basid} \mapsto \mit{M}'\} \langle+ \mit{BE}''\rangle, \Psi'\langle'\rangle
}
\end{equation}
\vspace{2\parsep}
{\large\noindent
\textbf{(Basis) Structure Bindings} \hfill
\fbox{$\mit{B} \vdash \mit{bstrbind} \longrightarrow \mit{SE}$}
}\nopagebreak
\begin{equation}
\label{eqn:mlb:SS:bstrbind}
\judge{
\mit{B}(\mit{strid}_2) = E \quad
\langle\mit{B} + \mrm{tynames}~\mit{E} \vdash \mit{bstrbind} \longrightarrow \mit{SE}\rangle
}{
\mit{B} \vdash \mit{strid}_1 ~\mtt{=}~ \mit{strid}_2 ~\langle\mtt{and}~\mit{bstrbind}\rangle \longrightarrow
\{\mit{strid}_1 \mapsto \mit{E}\} \langle+ \mit{SE}\rangle
}
\end{equation}
\begin{samepage}
\noindent
\textit{Comments}:
\begin{itemize}
\item[(\ref{eqn:mlb:SS:bstrbind})] Note that $\mit{bstrbind} \subset
\mit{strbind}$. Hence, this rule can be derived from the
Definition's $\mit{B} \vdash \mit{strbind} \Rightarrow \mit{SE}$.
\end{itemize}
\end{samepage}
\vspace{2\parsep}
{\large\noindent
\textbf{(Basis) Signature Bindings} \hfill
\fbox{$\mit{B} \vdash \mit{bsigbind} \longrightarrow \mit{G}$}
}\nopagebreak
\begin{equation}
\label{eqn:mlb:SS:bsigbind}
\judge{
\begin{stackCC}
\mit{B}(\mit{sigid}_2) = \Sigma \quad \Sigma = (\mit{T})\mit{E} \quad
\mit{T} \cap (\mit{T}~\mrm{of}~\mit{B}) = \emptyset \\
\mit{T} = \mrm{tynames}~\mit{E} \setminus (\mit{T}~\mrm{of}~\mit{B}) \quad
\langle\mit{B} \vdash \mit{bsigbind} \longrightarrow \mit{G}\rangle
\end{stackCC}
}{
\mit{B} \vdash \mit{sigid}_1 ~\mtt{=}~ \mit{sigid}_2 ~\langle\mtt{and}~\mit{bsigbind}\rangle \longrightarrow
\{\mit{sigid}_1 \mapsto \Sigma\} \langle+ \mit{G}\rangle
}
\end{equation}
\begin{samepage}
\noindent
\textit{Comments}:
\begin{itemize}
\item[(\ref{eqn:mlb:SS:bsigbind})] Note that $\mit{bsigbind} \subset
\mit{sigbind}$. Hence, this rule can be derived from the
Definition's $\mit{B} \vdash \mit{sigbind} \Rightarrow \mit{G}$. As such, the
following comment from the Definition applies:
\begin{quote}
The bound names of $\mit{B}(\mit{sigid}_2)$ can always be renamed to
satisfy $\mit{T} \cap (\mit{T}~\mrm{of}~\mit{B}) = \emptyset$, if necessary.
\end{quote}
\end{itemize}
\end{samepage}
\vspace{2\parsep}
{\large\noindent
\textbf{(Basis) Functor Bindings} \hfill
\fbox{$\mit{B} \vdash \mit{bfunbind} \longrightarrow \mit{F}$}
}\nopagebreak
\begin{equation}
\judge{
\begin{stackCC}
\mit{B}(\mit{funid}_2) = \Phi \quad \Phi = (\mit{T})(\mit{E},(\mit{T}')\mit{E}') \quad
\mit{T} \cap (\mit{T}~\mrm{of}~\mit{B}) = \emptyset \\
\mit{T}' = \mrm{tynames}~\mit{E}' \setminus ((\mit{T}~\mrm{of}~\mit{B}) \cup \mit{T}) \quad
\langle\mit{B} \vdash \mit{bfunbind} \longrightarrow \mit{F}\rangle
\end{stackCC}
}{
\mit{B} \vdash \mit{funid}_1 ~\mtt{=}~ \mit{funid}_2 ~\langle\mtt{and}~\mit{bfunbind}\rangle \longrightarrow
\{\mit{funid}_1 \mapsto \Phi\} \langle+ \mit{F}\rangle
}
\end{equation}
%
\section{Dynamic Semantics for MLBs}
%
\subsection{Reduced Syntax}
The syntax of MLBs is unchanged for the purposes of the dynamic
semantics for MLBs. However, the $\mrm{Parser}$ $\mcal{P}$ returns a
$\mit{topdec}$ in the reduced syntax of Modules.
%
\subsection{Compound Objects}
The compound objects for the MLBs dynamic semantics, extra to those
for the Modules dynamic semantics, are shown in Figure~\ref{fig:mlb:DS:CompoundObjects}.
\begin{figure}[h]
\begin{displaymath}
\begin{array}{rcl}
\mit{BE} & \in & \mrm{BasEnv} = \mrm{BasId} \xrightarrow{\mrm{fin}} \mrm{MBasis} \\
\mit{M} ~\mrm{or}~ \mit{FE},\mit{BE},\mit{B} & \in & \mrm{MBasis} =
\mrm{FixEnv} \times \mrm{BasEnv} \times \mrm{Basis} \\
\Psi & \in & \mrm{BasCache} = \mrm{MLBasisPath} \xrightarrow{\mrm{fin}} \mrm{MBasis}
\end{array}
\end{displaymath}
\caption{Compound Semantic Objects}\label{fig:mlb:DS:CompoundObjects}
\end{figure}
%
\subsection{Inference Rules}
The semantic rules allow sentences of the form
\begin{displaymath}
s, A \vdash \mit{phrase} \longrightarrow A', s'
\end{displaymath}
to be inferred, where $s$, $s'$ are the states before and after the
evaluation represented by the sentence. Some hypotheses in rules are
not of this form; they are called \emph{side-conditions}. The
convention for options is as in the Core and Modules semantics.
The state and exception conventions are adopted as in the Core and
Modules dynamic semantics. However, it can be shown that the only
MLBs phrases whose evaluation may cause a side-effect or generate an
exception packet are of the form $\mit{basexp}$, $\mit{basdec}$ or
$\mit{basbind}$.
\vspace{2\parsep}
{\large\noindent
\textbf{Basis Expressions} \hfill
\fbox{$\mit{M}, \Psi \vdash \mit{basexp} \longrightarrow \mit{M}', \Psi' / p$}
}\nopagebreak
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi'
}{
\mit{M}, \Psi \vdash \mtt{bas}~ \mit{basdec} ~\mtt{end} \longrightarrow \mit{M}', \Psi'
}
\end{equation}
\begin{equation}
\judge{
\mit{M}(\mit{basid}) = \mit{M}'
}{
\mit{M}, \Psi \vdash \mit{basid} \longrightarrow \mit{M}', \Psi
}
\end{equation}
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}_1, \Psi_1 \quad
\mit{M} \oplus \mit{M}_1, \Psi_1 \vdash \mit{basexp} \longrightarrow \mit{M}_2, \Psi_2
}{
\mit{M}, \Psi \vdash \mtt{let}~ \mit{basdec} ~\mtt{in}~ \mit{basexp} ~\mtt{end} \longrightarrow \mit{M}_2, \Psi_2
}
\end{equation}
\vspace{2\parsep}
{\large\noindent
\textbf{Basis-level Declarations} \hfill
\fbox{$\mit{M}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi' / p$}
}\nopagebreak
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basbind} \longrightarrow \mit{BE}', \Psi'
}{
\mit{M}, \Psi \vdash \msf{basis}~ \mit{basbind} \longrightarrow \mit{BE}' ~\mrm{in}~ \mrm{MBasis}, \Psi'
}
\end{equation}
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basdec}_1 \longrightarrow \mit{M}_1, \Psi_1 \quad
\mit{M} + \mit{M}_1, \Psi_1 \vdash \mit{basdec}_2 \longrightarrow \mit{M}_2, \Psi_2 \quad
}{
\mit{M}, \Psi \vdash \mtt{local}~ \mit{basdec}_1 ~\mtt{in}~ \mit{basdec}_2 ~\mtt{end} \longrightarrow \mit{M}_2, \Psi_2
}
\end{equation}
\begin{equation}
\judge{
\mit{M}(\mit{basid}_1) = \mit{M}_1 \quad \cdots \quad
\mit{M}(\mit{basid}_n) = \mit{M}_n
}{
\mit{M}, \Psi \vdash \mtt{open}~ \mit{basid}_1 \cdots \mit{basid}_n \longrightarrow \mit{M}_1 + \cdots + \mit{M}_n, \Psi
}
\end{equation}
\begin{equation}
\judge{
\mit{B}~\mrm{of}~\mit{M} \vdash \mit{bstrbind} \longrightarrow SE
}{
\mit{M}, \Psi \vdash \mtt{structure}~ \mit{bstrbind}
\longrightarrow \mit{SE} ~\mrm{in}~ \mrm{MBasis}, \Psi
}
\end{equation}
\begin{equation}
\judge{
\mrm{Inter}~(\mit{B}~\mrm{of}~\mit{M}) \vdash \mit{bsigbind} \longrightarrow G
}{
\mit{M}, \Psi \vdash \mtt{signature}~ \mit{bsigbind}
\longrightarrow \mit{G } ~\mrm{in}~ \mrm{MBasis}, \Psi
}
\end{equation}
\begin{equation}
\judge{
\mit{B}~\mrm{of}~\mit{M} \vdash \mit{bfunbind} \longrightarrow F
}{
\mit{M}, \Psi \vdash \mtt{functor}~ \mit{bfunbind}
\longrightarrow \mit{F} ~\mrm{in}~ \mrm{MBasis}, \Psi
}
\end{equation}
\begin{equation}
\judge{
}{
\mit{M}, \Psi \vdash \quad \longrightarrow \{\} ~\mrm{in}~ \mrm{MBasis}, \Psi
}
\end{equation}
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basdec}_1 \longrightarrow \mit{M}_1, \Psi_1 \quad
\mit{M} + \mit{M}_1, \Psi_1 \vdash \mit{basdec}_2 \longrightarrow \mit{M}_2, \Psi_2
}{
\mit{M}, \Psi \vdash \mit{basdec}_1 ~\langle\mtt{;}\rangle~ \mit{basdec}_2 \longrightarrow \mit{M}_1 \oplus \mit{M}_2, \Psi_2
}
\end{equation}
\begin{equation}
\label{eqn:mlb:DS:path.sml}
\judge{
\mcal{P}(\mit{FE}~\mrm{of}~\mit{M}, \msf{path.sml}) = (\mit{FE}', \mit{topdec}) \quad
\mit{B}~\mrm{of}~\mit{M} \vdash \mit{topdec} \Rightarrow \mit{B}'
}{
\mit{M}, \Psi \vdash \msf{path.sml} \longrightarrow (\mit{FE}',\{\},\mit{B}'), \Psi
}
\end{equation}
\begin{equation}
\judge{
\Psi(\msf{path.mlb}) = \mit{M}'
}{
\mit{M}, \Psi \vdash \msf{path.mlb} \longrightarrow \mit{M}', \Psi
}
\end{equation}
\begin{equation}
\judge{
\msf{path.mlb} \notin \mrm{Dom}~\Psi \quad
\mcal{P}(\msf{path.mlb}) = \mit{basdec} \quad
\{\} ~\mrm{in}~ \mrm{MBasis}, \Psi \vdash \mit{basdec} \longrightarrow \mit{M}', \Psi'
}{
\mit{M}, \Psi \vdash \msf{path.mlb} \longrightarrow \mit{M}', \Psi' + \{\msf{path.mlb} \mapsto \mit{M}'\}
}
\end{equation}
\begin{samepage}
\noindent
\textit{Comments}:
\begin{itemize}
\item[(\ref{eqn:mlb:DS:path.sml})]
Note the use of the Definition's
$\mit{B} \vdash \mit{topdec} \Rightarrow \mit{B}'$.
\end{itemize}
\end{samepage}
\vspace{2\parsep}
{\large\noindent
\textbf{Basis Bindings} \hfill
\fbox{$\mit{M}, \Psi \vdash \mit{basbind} \longrightarrow \mit{BE}', \Psi' / p$}
}\nopagebreak
\begin{equation}
\judge{
\mit{M}, \Psi \vdash \mit{basexp} \longrightarrow \mit{M}', \Psi' \quad
\langle\mit{M}, \Psi' \vdash \mit{basbind} \longrightarrow \mit{BE}'', \Psi''\rangle
}{
\mit{M}, \Psi \vdash \mit{basid} ~\mtt{=}~ \mit{basexp} ~\langle\mtt{and}~\mit{basbind}\rangle \longrightarrow
\{\mit{basid} \mapsto \mit{M}'\} \langle+ \mit{BE}''\rangle, \Psi'\langle'\rangle
}
\end{equation}
\vspace{2\parsep}
{\large\noindent
\textbf{(Basis) Structure Bindings} \hfill
\fbox{$\mit{B} \vdash \mit{bstrbind} \longrightarrow \mit{SE}$}
}\nopagebreak
\begin{equation}
\label{eqn:mlb:DS:bstrbind}
\judge{
\mit{B}(\mit{strid}_2) = E \quad
\langle\mit{B} \vdash \mit{bstrbind} \longrightarrow \mit{SE}\rangle
}{
\mit{B} \vdash \mit{strid}_1 ~\mtt{=}~ \mit{strid}_2 ~\langle\mtt{and}~\mit{bstrbind}\rangle \longrightarrow
\{\mit{strid}_1 \mapsto \mit{E}\} \langle+ \mit{SE}\rangle
}
\end{equation}
\begin{samepage}
\noindent
\textit{Comments}:
\begin{itemize}
\item[(\ref{eqn:mlb:DS:bstrbind})] Note that $\mit{bstrbind} \subset
\mit{strbind}$. Hence, this rule can be derived from the
Definition's $\mit{B} \vdash \mit{strbind} \Rightarrow \mit{SE} / p$, noting that
the derivation may neither cause a side-effect nor generate an
exception packet.
\end{itemize}
\end{samepage}
\vspace{2\parsep}
{\large\noindent
\textbf{(Basis) Signature Bindings} \hfill
\fbox{$\mit{IB} \vdash \mit{bsigbind} \longrightarrow \mit{G}$}
}\nopagebreak
\begin{equation}
\label{eqn:mlb:DS:bsigbind}
\judge{
\mit{IB}(\mit{sigid}_2) = I \quad
\langle\mit{IB} \vdash \mit{bsigbind} \longrightarrow \mit{G}\rangle
}{
\mit{IB} \vdash \mit{sigid}_1 ~\mtt{=}~ \mit{sigid}_2 ~\langle\mtt{and}~\mit{bsigbind}\rangle \longrightarrow
\{\mit{sigid}_1 \mapsto I\} \langle+ \mit{G}\rangle
}
\end{equation}
\begin{samepage}
\noindent
\textit{Comments}:
\begin{itemize}
\item[(\ref{eqn:mlb:DS:bsigbind})] Note that $\mit{bsigbind} \subset
\mit{sigbind}$. Hence, this rule can be derived from the
Definition's $\mit{IB} \vdash \mit{sigbind} \Rightarrow \mit{G}$, noting that
the derivation may neither cause a side-effect nor generate an
exception packet.
\end{itemize}
\end{samepage}
\vspace{2\parsep}
{\large\noindent
\textbf{(Basis) Functor Bindings} \hfill
\fbox{$\mit{B} \vdash \mit{bfunbind} \longrightarrow \mit{F}$}
}\nopagebreak
\begin{equation}
\judge{
\mit{B}(\mit{funid}_2) = (\mit{strid}:\mit{I},\mit{strexp},\mit{B}) \quad
\langle\mit{B} \vdash \mit{bfunbind} \longrightarrow \mit{F}\rangle
}{
\mit{B} \vdash \mit{funid}_1 ~\mtt{=}~ \mit{funid}_2 ~\langle\mtt{and}~\mit{bfunbind}\rangle \longrightarrow
\{\mit{funid}_1 \mapsto (\mit{strid}:\mit{I},\mit{strexp},\mit{B})\} \langle+ \mit{F}\rangle
}
\end{equation}
\appendix
\section{Derived Forms}
\label{sec:mlb:DerivedForms}
Figure~\ref{fig:mlb:DF:bindings} shows derived forms for structure,
signature, and functor bindings in MLBs. These derived forms are
a useful shorthand for specifying import and export filters.
\begin{figure}[h]
\begin{center}
\begin{tabular}{|l|l|}
\multicolumn{1}{c}{Derived Form} &
\multicolumn{1}{c}{Equivalent Form} \\
\multicolumn{2}{c}{} \\
\multicolumn{2}{l}{\textbf{(Basis) Structure Bindings} $\mit{bstrbind}$} \\
\hline
$\mit{strid} ~\langle\mtt{and}~ \mit{bstrbind}\rangle$ &
$\mit{strid} ~\mtt{=}~ \mit{strid} ~\langle\mtt{and}~ \mit{bstrbind}\rangle$ \\
\hline
\multicolumn{2}{c}{} \\
\multicolumn{2}{l}{\textbf{(Basis) Signature Bindings} $\mit{bsigbind}$} \\
\hline
$\mit{sigid} ~\langle\mtt{and}~ \mit{bsigbind}\rangle$ &
$\mit{sigid} ~\mtt{=}~ \mit{sigid} ~\langle\mtt{and}~ \mit{bsigbind}\rangle$ \\
\hline
\multicolumn{2}{c}{} \\
\multicolumn{2}{l}{\textbf{(Basis) Functor Bindings} $\mit{bfunbind}$} \\
\hline
$\mit{funid} ~\langle\mtt{and}~ \mit{bfunbind}\rangle$ &
$\mit{funid} ~\mtt{=}~ \mit{funid} ~\langle\mtt{and}~ \mit{bfunbind}\rangle$ \\
\hline
\end{tabular}
\end{center}
\caption{Derived forms of (Basis) Structure, Signature, and Functor Bindings}\label{fig:mlb:DF:bindings}
\end{figure}
\bibliographystyle{alpha}
\bibliography{bib}
\end{document}
1.25 +0 -1 mlton/doc/user-guide/Makefile
Index: Makefile
===================================================================
RCS file: /cvsroot/mlton/mlton/doc/user-guide/Makefile,v
retrieving revision 1.24
retrieving revision 1.25
diff -u -r1.24 -r1.25
--- Makefile 27 Sep 2004 22:52:09 -0000 1.24
+++ Makefile 13 Oct 2004 02:16:22 -0000 1.25
@@ -21,7 +21,6 @@
man-page.tex \
mingw.tex \
mlb.tex \
- mlb-formal.tex \
netbsd.tex \
nj-deviations.tex \
openbsd.tex \
1.17 +0 -3 mlton/doc/user-guide/main.tex
Index: main.tex
===================================================================
RCS file: /cvsroot/mlton/mlton/doc/user-guide/main.tex,v
retrieving revision 1.16
retrieving revision 1.17
diff -u -r1.16 -r1.17
--- main.tex 22 Aug 2004 20:37:04 -0000 1.16
+++ main.tex 13 Oct 2004 02:16:22 -0000 1.17
@@ -46,8 +46,5 @@
\bibliographystyle{alpha}
\bibliography{bib}
\appendix
-\begin{latexonly}
-\input{mlb-formal}
-\end{latexonly}
\input{nj-deviations}
\end{document}
1.11 +4 -7 mlton/doc/user-guide/mlb.tex
Index: mlb.tex
===================================================================
RCS file: /cvsroot/mlton/mlton/doc/user-guide/mlb.tex,v
retrieving revision 1.10
retrieving revision 1.11
diff -u -r1.10 -r1.11
--- mlb.tex 1 Oct 2004 14:43:21 -0000 1.10
+++ mlb.tex 13 Oct 2004 02:16:22 -0000 1.11
@@ -11,13 +11,10 @@
programmer's intuitive notion (and the Definition of SML's formal
notion) of the top-level environment (a \emph{basis}). The system has
been designed to be a natural extension of Standard ML;
-\begin{latexonly}
-\appref{mlb-formal}
-\end{latexonly}
-\begin{htmlonly}
-a separate document
-\end{htmlonly}
-gives a formal specification of MLBs in the style of the Definition.
+the
+\htmladdnormallink{Formal Specification of MLBs}
+ {http://www.mlton.org/doc/MLBs/mlb-formal.ps}
+is given in the style of the Definition.
We briefly highlight some of the key features provided by MLBs:
\begin{itemize}