1 \documentclass[draft
]{article
}
9 \newcommand{\mbb}[1]{\mathbb{#1}}
10 \newcommand{\mbf}[1]{\mathbf{#1}}
11 \renewcommand{\mit}[1]{\mathit{#1}}
12 \newcommand{\mrm}[1]{\mathrm{#1}}
13 \newcommand{\mtt}[1]{\mathtt{#1}}
14 \newcommand{\mcal}[1]{\mathcal{#1}}
15 \newcommand{\msf}[1]{\mathsf{#1}}
18 \newcommand{\ttt}[1]{\texttt{#1}}
21 \newenvironment{stackAux
}[2]{%
22 \setlength{\arraycolsep}{0pt
}
23 \begin{array
}[#1]{#2}}{
25 \newenvironment{stackCC
}{
26 \begin{stackAux
}{c
}{c
}}{\end{stackAux
}}
27 \newenvironment{stackCL
}{
28 \begin{stackAux
}{c
}{l
}}{\end{stackAux
}}
29 \newenvironment{stackTL
}{
30 \begin{stackAux
}{t
}{l
}}{\end{stackAux
}}
31 \newenvironment{stackTR
}{
32 \begin{stackAux
}{t
}{r
}}{\end{stackAux
}}
33 \newenvironment{stackBC
}{
34 \begin{stackAux
}{b
}{c
}}{\end{stackAux
}}
35 \newenvironment{stackBL
}{
36 \begin{stackAux
}{b
}{l
}}{\end{stackAux
}}
38 \newcommand{\stagger}[2]{%
40 \multicolumn{2}{l
}{#1}&\\%
41 &
\multicolumn{2}{r
}{#2}%
44 \newcommand{\axiom}[1]{{\displaystyle\strut{#1}}}
45 \newcommand{\infrule}[2]{{\frac{\displaystyle\strut{#1}}{\displaystyle\strut{#2}}}}
46 \newcommand{\judge}[2]{\infrule{#1}{#2}}
50 \title{Formal Specification of the ML Basis system
}
51 \author{Copyright
\copyright\
2004\\
52 Henry Cejtin, Matthew Fluet, Suresh Jagannathan, and Stephen Weeks
}
56 This
document formally specifies the ML Basis system (MLB) in
{\mlton}
57 used to program in the large. The system has been designed to be a
58 natural extension of Standard ML, and the specification is given in
59 the style of The Definition of Standard ML~
\cite{MTHM97
} (henceforeth,
60 the Definition). This section adopts (often silently) abbreviations,
61 conventions, definitions, and notation from the Definition.
63 \section{Syntax of MLB
}
64 For MLB there are further reserved words, identifier classes and
65 derived forms. There are no further special constants; comments and
66 lexical analysis are as for the Core and Modules. The derived forms
67 appear in Appendix~
\ref{sec:mlb:DerivedForms
}.
69 \subsection{Reserved Words
}
70 The following are the additional reserved words used in MLB.
72 \mtt{bas
} \quad\quad \mtt{basis
}
74 Note that many of the reserved words from the Core and Modules are not
75 used by the grammar of MLB. However, as the grammar includes
76 identifiers from the grammars of the Core and Modules, it is useful to
77 consider the reserved words from the Core and Modules to be reserved
80 \subsection{Identifiers
}
81 The additional identifier class for MLB are $
\mrm{BasId
}$ (basis
82 identifiers). Basis identifiers must be alphanumeric, not starting
83 with a prime. The class of each identifier occurence is determined by
84 the grammatical rules which follow. Henceforth, therefore, we
85 consider all identifier classes to be disjoint.
87 \subsection{Infixed operators
}
88 The grammar of MLB does not directly admit fixity directives.
89 However, the static and dynamic semantics for MLB will import source
90 files that must be parsed in the scope of fixity directives and that
91 may introduce additional fixity directives into scope.
92 Figure~
\ref{fig:mlb:S:FixityEnv
} formalizes the Definition's notion of
93 \emph{infix status
} as a
\emph{fixity environment
}.
97 & &
\mrm{InfixStatus
} = \
{\mtt{nonfix
}\
} \cup \bigcup_{d
\in \
{0,
\ldots,
9\
}} \
{\mtt{infix
}~d,
\mtt{infixr
}~d\
} \\
98 \mit{FE
} &
\in &
\mrm{FixEnv
} =
\mrm{VId
} \xrightarrow{\mrm{fin
}} \mrm{InfixStatus
} \end{array
}
100 \caption{Fixity Environment
}\label{fig:mlb:S:FixityEnv
}
103 \subsection{Grammar for MLB
}
104 The phrase classes for MLB are shown in
105 Figure~
\ref{fig:mlb:S:PhraseClasses
}.
109 \mrm{BasExp
} &
\mbox{basis expressions
} \\
110 \mrm{BasDec
} &
\mbox{basis-level declaration
} \\
111 \mrm{BasBind
} &
\mbox{basis bindings
} \\
112 \mrm{BStrBind
} &
\mbox{(basis) structure bindings
} \\
113 \mrm{BSigBind
} &
\mbox{(basis) signature bindings
} \\
114 \mrm{BFunBind
} &
\mbox{(basis) functor bindings
}
117 \caption{MLB Phrase Classes
}\label{fig:mlb:S:PhraseClasses
}
119 We use the variable $
\mit{basexp
}$ to range over $
\mrm{BasExp
}$, etc.
120 The conventions adopted in presenting the grammatical rules for MLB
121 are the same as for the Core and Modules. The grammatical rules are
122 shown in Figure~
\ref{fig:mlb:S:GrammaticalRules
}.
127 \mtt{bas
}~
\mit{basdec
} ~
\mtt{end
}
130 &
\mbox{basis identifier
} \\&&
131 \mtt{let
}~
\mit{basdec
} ~
\mtt{in
}~
\mit{basexp
} ~
\mtt{end
}
132 &
\mbox{local declaration
} \\
135 \mtt{basis
}~
\mit{basbind
}
137 \mtt{local
}~
\mit{basdec
}_1 ~
\mtt{in
}~
\mit{basdec
}_2 ~
\mtt{end
}
139 \mtt{open
}~
\mit{basid
}_1
\cdots \mit{basid
}_n
140 &
\mbox{open ($n
\geq 1$)
} \\&&
141 \mtt{structure
}~
\mit{bstrbind
}
142 &
\mbox{(basis) structure binding
} \\&&
143 \mtt{signature
}~
\mit{bsigbind
}
144 &
\mbox{(basis) signature binding
} \\&&
145 \mtt{functor
}~
\mit{bfunbind
}
146 &
\mbox{(basis) functor binding
} \\&&
149 \mit{basdec
}_1~
\langle\mtt{;
}\rangle~
\mit{basdec
}_2
150 &
\mbox{sequential
} \\&&
152 \mbox{import ML basis
} \\&&
154 &
\mbox{import source
} \\
156 \mit{basbind
} & ::= &
157 \mit{basid
} ~
\mtt{=
}~
\mit{basexp
} ~
\langle\mtt{and
}~
\mit{basbind
}\rangle \\
158 \mit{bstrbind
} & ::= &
159 \mit{strid
}_1 ~
\mtt{=
}~
\mit{strid
}_2 ~
\langle\mtt{and
}~
\mit{bstrbind
}\rangle \\
160 \mit{bsigbind
} & ::= &
161 \mit{sigid
}_1 ~
\mtt{=
}~
\mit{sigid
}_2 ~
\langle\mtt{and
}~
\mit{bsigbind
}\rangle \\
162 \mit{bfunbind
} & ::= &
163 \mit{funid
}_1 ~
\mtt{=
}~
\mit{funid
}_2 ~
\langle\mtt{and
}~
\mit{bfunbind
}\rangle
166 \caption{Grammar: Basis Expressions, Declarations, and Bindings
}\label{fig:mlb:S:GrammaticalRules
}
169 \subsection{Syntactic Restrictions
}
171 \item No binding $
\mit{basbind
}$ may bind the same identifier twice.
172 \item No binding $
\mit{bstrbind
}$, $
\mit{bsigbind
}$ or $
\mit{bfunbind
}$ may bind the same identifier twice.
173 \item MLB may not be cyclic; i.e., successively replacing
174 $
\msf{path.mlb
}$ with its parsed $
\mrm{BasDec
}$ must terminate.
178 The static and dynamic semantics for MLB will interpret
179 $
\msf{path.sml
}$ as a parsed $
\mrm{TopDec
}$ and
180 $
\msf{path.mlb
}$ as a parsed $
\mrm{BasDec
}$. Parsing a $
\mrm{TopDec
}$
181 takes a fixity environment as input and returns a fixity environment
182 as output; the output fixity environment corresponds to fixity
183 directives introduced by and whose scope is not limited by the parsed
186 Paths and parsers are given in Figure~
\ref{fig:mlb:S:PathsParser
}. A
187 (fixed) $
\mrm{Parser
}$ $
\mcal{P
}$ provides the interpretation of
188 $
\msf{path.sml
}$ and $
\msf{path.mlb
}$ imports.
193 \msf{path.sml
} &
\in &
\mrm{SourcePath
} \\
194 \msf{path.mlb
} &
\in &
\mrm{MLBasisPath
}
197 \mcal{P
} &
\in &
\mrm{Parser
} =
198 ((
\mrm{FixEnv
} \times \mrm{SourcePath
})
199 \xrightarrow{\mrm{fin
}} (
\mrm{FixEnv
} \times \mrm{TopDec
}))
201 (
\mrm{MLBasisPath
} \xrightarrow{\mrm{fin
}} \mrm{BasDec
})
205 \caption{Parser
}\label{fig:mlb:S:PathsParser
}
208 For a file extension $
\msf{.ext
}$, $
\msf{path.ext
}$ denotes either an
209 absolute path or a relative path (relative to the $
\mrm{BasDec
}$ being
210 parsed) to a file in the underlying file system. Paths that denote the same
211 file in the underlying file system are considered equal, though they may
212 have distinct textual representations. An implementation
213 may allow additional extensions (e.g., $
\mtt{.ML
}$, $
\mtt{.fun
}$,
214 $
\mtt{.sig
}$) in elements of $
\mrm{SourcePath
}$. An implementation
215 may additionally allow path variables to appear in
216 paths. $
\mrm{Parser
}$ could be refined by a
\emph{current working
217 directory
}, to formally specify the interpretation of relative paths,
218 and an
\emph{path map
}, to formally specify the
219 interpretation of path variables, but the above suffices
220 for the development in the following sections.
222 \section{Static Semantics for MLB
}
224 \subsection{Semantic Objects
}
225 The simple objects for the MLB static semantics are exactly as for
226 Modules. The compound objects are those for Modules, augmented by
227 those in Figure~
\ref{fig:mlb:SS:CompoundObjects
}.
231 \mit{BE
} &
\in &
\mrm{BasEnv
} =
\mrm{BasId
} \xrightarrow{\mrm{fin
}} \mrm{MBasis
} \\
232 \mit{M
} ~
\mrm{or
}~
\mit{FE
},
\mit{BE
},
\mit{B
} &
\in &
233 \mrm{MBasis
} =
\mrm{FixEnv
} \times \mrm{BasEnv
} \times \mrm{Basis
} \\
234 \Psi &
\in &
\mrm{BasCache
} =
\mrm{MLBasisPath
} \xrightarrow{\mrm{fin
}} \mrm{MBasis
}
237 \caption{Compound Semantic Objects
}\label{fig:mlb:SS:CompoundObjects
}
239 The operations of projection, injection and modification are as for
242 \subsection{Inference Rules
}
243 As for the Core and for Modules, the rules for MLB static semantics
244 allow sentences of the form
246 A
\vdash \mit{phrase
} \longrightarrow A'
248 to be inferred. Some hypotheses in rules are not of this form; they
249 are called
\emph{side-conditions
}. The convention for options is as
250 in the Core and Modules semantics.
254 \textbf{Basis Expressions
} \hfill
255 \fbox{$
\mit{M
},
\Psi \vdash \mit{basexp
} \longrightarrow \mit{M
}',
\Psi'$
}
260 \mit{M
},
\Psi \vdash \mit{basdec
} \longrightarrow \mit{M
}',
\Psi'
262 \mit{M
},
\Psi \vdash \mtt{bas
}~
\mit{basdec
} ~
\mtt{end
} \longrightarrow \mit{M
}',
\Psi'
268 \mit{M
}(
\mit{basid
}) =
\mit{M
}'
270 \mit{M
},
\Psi \vdash \mit{basid
} \longrightarrow \mit{M
}',
\Psi
275 \label{eqn:mlb:SS:localDeclaration
}
277 \mit{M
},
\Psi \vdash \mit{basdec
} \longrightarrow \mit{M
}_1,
\Psi_1 \quad
278 \mit{M
} \oplus \mit{M
}_1,
\Psi_1 \vdash \mit{basexp
} \longrightarrow \mit{M
}_2,
\Psi_2
280 \mit{M
},
\Psi \vdash \mtt{let
}~
\mit{basdec
} ~
\mtt{in
}~
\mit{basexp
} ~
\mtt{end
} \longrightarrow \mit{M
}_2,
\Psi_2
288 \item[(
\ref{eqn:mlb:SS:localDeclaration
})
] The use of $
\oplus$, here
289 and elsewhere, ensures that the type names generated by the first
290 sub-phrase are distinct from the names generated by the second sub-phrase.
296 \textbf{Basis-level Declarations
} \hfill
297 \fbox{$
\mit{M
},
\Psi \vdash \mit{basdec
} \longrightarrow \mit{M
}',
\Psi'$
}
302 \mit{M
},
\Psi \vdash \mit{basbind
} \longrightarrow \mit{BE
}',
\Psi'
304 \mit{M
},
\Psi \vdash \msf{basis
}~
\mit{basbind
} \longrightarrow \mit{BE
}' ~
\mrm{in
}~
\mrm{MBasis
},
\Psi'
310 \mit{M
},
\Psi \vdash \mit{basdec
}_1
\longrightarrow \mit{M
}_1,
\Psi_1 \quad
311 \mit{M
} \oplus \mit{M
}_1,
\Psi_1 \vdash \mit{basdec
}_2
\longrightarrow \mit{M
}_2,
\Psi_2 \quad
313 \mit{M
},
\Psi \vdash \mtt{local
}~
\mit{basdec
}_1 ~
\mtt{in
}~
\mit{basdec
}_2 ~
\mtt{end
} \longrightarrow \mit{M
}_2,
\Psi_2
319 \mit{M
}(
\mit{basid
}_1) =
\mit{M
}_1
\quad \cdots \quad
320 \mit{M
}(
\mit{basid
}_n) =
\mit{M
}_n
322 \mit{M
},
\Psi \vdash \mtt{open
}~
\mit{basid
}_1
\cdots \mit{basid
}_n
\longrightarrow \mit{M
}_1
\oplus \cdots \oplus \mit{M
}_n,
\Psi
328 \mit{B
}~
\mrm{of
}~
\mit{M
} \vdash \mit{bstrbind
} \longrightarrow SE
330 \mit{M
},
\Psi \vdash \mtt{structure
}~
\mit{bstrbind
}
331 \longrightarrow \mit{SE
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi
337 \mit{B
}~
\mrm{of
}~
\mit{M
} \vdash \mit{bsigbind
} \longrightarrow G
339 \mit{M
},
\Psi \vdash \mtt{signature
}~
\mit{bsigbind
}
340 \longrightarrow \mit{G
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi
346 \mit{B
}~
\mrm{of
}~
\mit{M
} \vdash \mit{bfunbind
} \longrightarrow F
348 \mit{M
},
\Psi \vdash \mtt{functor
}~
\mit{bfunbind
}
349 \longrightarrow \mit{F
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi
356 \mit{M
},
\Psi \vdash \quad \longrightarrow \
{\
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi
362 \mit{M
},
\Psi \vdash \mit{basdec
}_1
\longrightarrow \mit{M
}_1,
\Psi_1 \quad
363 \mit{M
} \oplus \mit{M
}_1,
\Psi_1 \vdash \mit{basdec
}_2
\longrightarrow \mit{M
}_2,
\Psi_2
365 \mit{M
},
\Psi \vdash \mit{basdec
}_1 ~
\langle\mtt{;
}\rangle~
\mit{basdec
}_2
\longrightarrow \mit{M
}_1
\oplus \mit{M
}_2,
\Psi_2
370 \label{eqn:mlb:SS:path.sml
}
372 \mcal{P
}(
\mit{FE
}~
\mrm{of
}~
\mit{M
},
\msf{path.sml
}) = (
\mit{FE
}',
\mit{topdec
})
\quad
373 \mit{B
}~
\mrm{of
}~
\mit{M
} \vdash \mit{topdec
} \Rightarrow \mit{B
}'
375 \mit{M
},
\Psi \vdash \msf{path.sml
} \longrightarrow (
\mit{FE
}',\
{\
},
\mit{B
}'),
\Psi
381 \Psi(
\msf{path.mlb
}) =
\mit{M
}'
383 \mit{M
},
\Psi \vdash \msf{path.mlb
} \longrightarrow \mit{M
}',
\Psi
389 \msf{path.mlb
} \notin \mrm{Dom
}~
\Psi \quad
390 \mcal{P
}(
\msf{path.mlb
}) =
\mit{basdec
} \quad
391 \
{\
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi \vdash \mit{basdec
} \longrightarrow \mit{M
}',
\Psi'
393 \mit{M
},
\Psi \vdash \msf{path.mlb
} \longrightarrow \mit{M
}',
\Psi' + \
{\msf{path.mlb
} \mapsto \mit{M
}'\
}
401 \item[(
\ref{eqn:mlb:SS:path.sml
})
]
402 Note the use of the Definition's
403 $
\mit{B
} \vdash \mit{topdec
} \Rightarrow \mit{B
}'$.
409 \textbf{Basis Bindings
} \hfill
410 \fbox{$
\mit{M
},
\Psi \vdash \mit{basbind
} \longrightarrow \mit{BE
}',
\Psi'$
}
415 \mit{M
},
\Psi \vdash \mit{basexp
} \longrightarrow \mit{M
}',
\Psi'
\quad
416 \langle\mit{M
} +
\mrm{tynames
}~
\mit{M
}',
\Psi'
\vdash \mit{basbind
} \longrightarrow \mit{BE
}'',
\Psi''
\rangle
418 \mit{M
},
\Psi \vdash \mit{basid
} ~
\mtt{=
}~
\mit{basexp
} ~
\langle\mtt{and
}~
\mit{basbind
}\rangle \longrightarrow
419 \
{\mit{basid
} \mapsto \mit{M
}'\
} \langle+
\mit{BE
}''
\rangle,
\Psi'
\langle'
\rangle
425 \textbf{(Basis) Structure Bindings
} \hfill
426 \fbox{$
\mit{B
} \vdash \mit{bstrbind
} \longrightarrow \mit{SE
}$
}
430 \label{eqn:mlb:SS:bstrbind
}
432 \mit{B
}(
\mit{strid
}_2) = E
\quad
433 \langle\mit{B
} +
\mrm{tynames
}~
\mit{E
} \vdash \mit{bstrbind
} \longrightarrow \mit{SE
}\rangle
435 \mit{B
} \vdash \mit{strid
}_1 ~
\mtt{=
}~
\mit{strid
}_2 ~
\langle\mtt{and
}~
\mit{bstrbind
}\rangle \longrightarrow
436 \
{\mit{strid
}_1
\mapsto \mit{E
}\
} \langle+
\mit{SE
}\rangle
444 \item[(
\ref{eqn:mlb:SS:bstrbind
})
] Note that $
\mit{bstrbind
} \subset
445 \mit{strbind
}$. Hence, this rule can be derived from the
446 Definition's $
\mit{B
} \vdash \mit{strbind
} \Rightarrow \mit{SE
}$.
452 \textbf{(Basis) Signature Bindings
} \hfill
453 \fbox{$
\mit{B
} \vdash \mit{bsigbind
} \longrightarrow \mit{G
}$
}
457 \label{eqn:mlb:SS:bsigbind
}
460 \mit{B
}(
\mit{sigid
}_2) =
\Sigma \quad \Sigma = (
\mit{T
})
\mit{E
} \quad
461 \mit{T
} \cap (
\mit{T
}~
\mrm{of
}~
\mit{B
}) =
\emptyset \\
462 \mit{T
} =
\mrm{tynames
}~
\mit{E
} \setminus (
\mit{T
}~
\mrm{of
}~
\mit{B
})
\quad
463 \langle\mit{B
} \vdash \mit{bsigbind
} \longrightarrow \mit{G
}\rangle
466 \mit{B
} \vdash \mit{sigid
}_1 ~
\mtt{=
}~
\mit{sigid
}_2 ~
\langle\mtt{and
}~
\mit{bsigbind
}\rangle \longrightarrow
467 \
{\mit{sigid
}_1
\mapsto \Sigma\
} \langle+
\mit{G
}\rangle
475 \item[(
\ref{eqn:mlb:SS:bsigbind
})
] Note that $
\mit{bsigbind
} \subset
476 \mit{sigbind
}$. Hence, this rule can be derived from the
477 Definition's $
\mit{B
} \vdash \mit{sigbind
} \Rightarrow \mit{G
}$. As such, the
478 following comment from the Definition applies:
480 The bound names of $
\mit{B
}(
\mit{sigid
}_2)$ can always be renamed to
481 satisfy $
\mit{T
} \cap (
\mit{T
}~
\mrm{of
}~
\mit{B
}) =
\emptyset$, if necessary.
488 \textbf{(Basis) Functor Bindings
} \hfill
489 \fbox{$
\mit{B
} \vdash \mit{bfunbind
} \longrightarrow \mit{F
}$
}
495 \mit{B
}(
\mit{funid
}_2) =
\Phi \quad \Phi = (
\mit{T
})(
\mit{E
},(
\mit{T
}')
\mit{E
}')
\quad
496 \mit{T
} \cap (
\mit{T
}~
\mrm{of
}~
\mit{B
}) =
\emptyset \\
497 \mit{T
}' =
\mrm{tynames
}~
\mit{E
}'
\setminus ((
\mit{T
}~
\mrm{of
}~
\mit{B
})
\cup \mit{T
})
\quad
498 \langle\mit{B
} \vdash \mit{bfunbind
} \longrightarrow \mit{F
}\rangle
501 \mit{B
} \vdash \mit{funid
}_1 ~
\mtt{=
}~
\mit{funid
}_2 ~
\langle\mtt{and
}~
\mit{bfunbind
}\rangle \longrightarrow
502 \
{\mit{funid
}_1
\mapsto \Phi\
} \langle+
\mit{F
}\rangle
506 \section{Dynamic Semantics for MLB
}
508 \subsection{Reduced Syntax
}
509 The syntax of MLB is unchanged for the purposes of the dynamic
510 semantics for MLB. However, the $
\mrm{Parser
}$ $
\mcal{P
}$ returns a
511 $
\mit{topdec
}$ in the reduced syntax of Modules.
513 \subsection{Compound Objects
}
514 The compound objects for the MLB dynamic semantics, extra to those
515 for the Modules dynamic semantics, are shown in Figure~
\ref{fig:mlb:DS:CompoundObjects
}.
519 \mit{BE
} &
\in &
\mrm{BasEnv
} =
\mrm{BasId
} \xrightarrow{\mrm{fin
}} \mrm{MBasis
} \\
520 \mit{M
} ~
\mrm{or
}~
\mit{FE
},
\mit{BE
},
\mit{B
} &
\in &
\mrm{MBasis
} =
521 \mrm{FixEnv
} \times \mrm{BasEnv
} \times \mrm{Basis
} \\
522 \Psi &
\in &
\mrm{BasCache
} =
\mrm{MLBasisPath
} \xrightarrow{\mrm{fin
}} \mrm{MBasis
}
525 \caption{Compound Semantic Objects
}\label{fig:mlb:DS:CompoundObjects
}
528 \subsection{Inference Rules
}
529 The semantic rules allow sentences of the form
531 s, A
\vdash \mit{phrase
} \longrightarrow A', s'
533 to be inferred, where $s$, $s'$ are the states before and after the
534 evaluation represented by the sentence. Some hypotheses in rules are
535 not of this form; they are called
\emph{side-conditions
}. The
536 convention for options is as in the Core and Modules semantics.
538 The state and exception conventions are adopted as in the Core and
539 Modules dynamic semantics. However, it can be shown that the only
540 MLB phrases whose evaluation may cause a side-effect or generate an
541 exception packet are of the form $
\mit{basexp
}$, $
\mit{basdec
}$ or
546 \textbf{Basis Expressions
} \hfill
547 \fbox{$
\mit{M
},
\Psi \vdash \mit{basexp
} \longrightarrow \mit{M
}',
\Psi' / p$
}
552 \mit{M
},
\Psi \vdash \mit{basdec
} \longrightarrow \mit{M
}',
\Psi'
554 \mit{M
},
\Psi \vdash \mtt{bas
}~
\mit{basdec
} ~
\mtt{end
} \longrightarrow \mit{M
}',
\Psi'
560 \mit{M
}(
\mit{basid
}) =
\mit{M
}'
562 \mit{M
},
\Psi \vdash \mit{basid
} \longrightarrow \mit{M
}',
\Psi
568 \mit{M
},
\Psi \vdash \mit{basdec
} \longrightarrow \mit{M
}_1,
\Psi_1 \quad
569 \mit{M
} \oplus \mit{M
}_1,
\Psi_1 \vdash \mit{basexp
} \longrightarrow \mit{M
}_2,
\Psi_2
571 \mit{M
},
\Psi \vdash \mtt{let
}~
\mit{basdec
} ~
\mtt{in
}~
\mit{basexp
} ~
\mtt{end
} \longrightarrow \mit{M
}_2,
\Psi_2
577 \textbf{Basis-level Declarations
} \hfill
578 \fbox{$
\mit{M
},
\Psi \vdash \mit{basdec
} \longrightarrow \mit{M
}',
\Psi' / p$
}
583 \mit{M
},
\Psi \vdash \mit{basbind
} \longrightarrow \mit{BE
}',
\Psi'
585 \mit{M
},
\Psi \vdash \msf{basis
}~
\mit{basbind
} \longrightarrow \mit{BE
}' ~
\mrm{in
}~
\mrm{MBasis
},
\Psi'
591 \mit{M
},
\Psi \vdash \mit{basdec
}_1
\longrightarrow \mit{M
}_1,
\Psi_1 \quad
592 \mit{M
} +
\mit{M
}_1,
\Psi_1 \vdash \mit{basdec
}_2
\longrightarrow \mit{M
}_2,
\Psi_2 \quad
594 \mit{M
},
\Psi \vdash \mtt{local
}~
\mit{basdec
}_1 ~
\mtt{in
}~
\mit{basdec
}_2 ~
\mtt{end
} \longrightarrow \mit{M
}_2,
\Psi_2
600 \mit{M
}(
\mit{basid
}_1) =
\mit{M
}_1
\quad \cdots \quad
601 \mit{M
}(
\mit{basid
}_n) =
\mit{M
}_n
603 \mit{M
},
\Psi \vdash \mtt{open
}~
\mit{basid
}_1
\cdots \mit{basid
}_n
\longrightarrow \mit{M
}_1 +
\cdots +
\mit{M
}_n,
\Psi
609 \mit{B
}~
\mrm{of
}~
\mit{M
} \vdash \mit{bstrbind
} \longrightarrow SE
611 \mit{M
},
\Psi \vdash \mtt{structure
}~
\mit{bstrbind
}
612 \longrightarrow \mit{SE
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi
618 \mrm{Inter
}~(
\mit{B
}~
\mrm{of
}~
\mit{M
})
\vdash \mit{bsigbind
} \longrightarrow G
620 \mit{M
},
\Psi \vdash \mtt{signature
}~
\mit{bsigbind
}
621 \longrightarrow \mit{G
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi
627 \mit{B
}~
\mrm{of
}~
\mit{M
} \vdash \mit{bfunbind
} \longrightarrow F
629 \mit{M
},
\Psi \vdash \mtt{functor
}~
\mit{bfunbind
}
630 \longrightarrow \mit{F
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi
637 \mit{M
},
\Psi \vdash \quad \longrightarrow \
{\
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi
643 \mit{M
},
\Psi \vdash \mit{basdec
}_1
\longrightarrow \mit{M
}_1,
\Psi_1 \quad
644 \mit{M
} +
\mit{M
}_1,
\Psi_1 \vdash \mit{basdec
}_2
\longrightarrow \mit{M
}_2,
\Psi_2
646 \mit{M
},
\Psi \vdash \mit{basdec
}_1 ~
\langle\mtt{;
}\rangle~
\mit{basdec
}_2
\longrightarrow \mit{M
}_1
\oplus \mit{M
}_2,
\Psi_2
651 \label{eqn:mlb:DS:path.sml
}
653 \mcal{P
}(
\mit{FE
}~
\mrm{of
}~
\mit{M
},
\msf{path.sml
}) = (
\mit{FE
}',
\mit{topdec
})
\quad
654 \mit{B
}~
\mrm{of
}~
\mit{M
} \vdash \mit{topdec
} \Rightarrow \mit{B
}'
656 \mit{M
},
\Psi \vdash \msf{path.sml
} \longrightarrow (
\mit{FE
}',\
{\
},
\mit{B
}'),
\Psi
662 \Psi(
\msf{path.mlb
}) =
\mit{M
}'
664 \mit{M
},
\Psi \vdash \msf{path.mlb
} \longrightarrow \mit{M
}',
\Psi
670 \msf{path.mlb
} \notin \mrm{Dom
}~
\Psi \quad
671 \mcal{P
}(
\msf{path.mlb
}) =
\mit{basdec
} \quad
672 \
{\
} ~
\mrm{in
}~
\mrm{MBasis
},
\Psi \vdash \mit{basdec
} \longrightarrow \mit{M
}',
\Psi'
674 \mit{M
},
\Psi \vdash \msf{path.mlb
} \longrightarrow \mit{M
}',
\Psi' + \
{\msf{path.mlb
} \mapsto \mit{M
}'\
}
682 \item[(
\ref{eqn:mlb:DS:path.sml
})
]
683 Note the use of the Definition's
684 $
\mit{B
} \vdash \mit{topdec
} \Rightarrow \mit{B
}'$.
690 \textbf{Basis Bindings
} \hfill
691 \fbox{$
\mit{M
},
\Psi \vdash \mit{basbind
} \longrightarrow \mit{BE
}',
\Psi' / p$
}
696 \mit{M
},
\Psi \vdash \mit{basexp
} \longrightarrow \mit{M
}',
\Psi'
\quad
697 \langle\mit{M
},
\Psi'
\vdash \mit{basbind
} \longrightarrow \mit{BE
}'',
\Psi''
\rangle
699 \mit{M
},
\Psi \vdash \mit{basid
} ~
\mtt{=
}~
\mit{basexp
} ~
\langle\mtt{and
}~
\mit{basbind
}\rangle \longrightarrow
700 \
{\mit{basid
} \mapsto \mit{M
}'\
} \langle+
\mit{BE
}''
\rangle,
\Psi'
\langle'
\rangle
706 \textbf{(Basis) Structure Bindings
} \hfill
707 \fbox{$
\mit{B
} \vdash \mit{bstrbind
} \longrightarrow \mit{SE
}$
}
711 \label{eqn:mlb:DS:bstrbind
}
713 \mit{B
}(
\mit{strid
}_2) = E
\quad
714 \langle\mit{B
} \vdash \mit{bstrbind
} \longrightarrow \mit{SE
}\rangle
716 \mit{B
} \vdash \mit{strid
}_1 ~
\mtt{=
}~
\mit{strid
}_2 ~
\langle\mtt{and
}~
\mit{bstrbind
}\rangle \longrightarrow
717 \
{\mit{strid
}_1
\mapsto \mit{E
}\
} \langle+
\mit{SE
}\rangle
725 \item[(
\ref{eqn:mlb:DS:bstrbind
})
] Note that $
\mit{bstrbind
} \subset
726 \mit{strbind
}$. Hence, this rule can be derived from the
727 Definition's $
\mit{B
} \vdash \mit{strbind
} \Rightarrow \mit{SE
} / p$, noting that
728 the derivation may neither cause a side-effect nor generate an
735 \textbf{(Basis) Signature Bindings
} \hfill
736 \fbox{$
\mit{IB
} \vdash \mit{bsigbind
} \longrightarrow \mit{G
}$
}
740 \label{eqn:mlb:DS:bsigbind
}
742 \mit{IB
}(
\mit{sigid
}_2) = I
\quad
743 \langle\mit{IB
} \vdash \mit{bsigbind
} \longrightarrow \mit{G
}\rangle
745 \mit{IB
} \vdash \mit{sigid
}_1 ~
\mtt{=
}~
\mit{sigid
}_2 ~
\langle\mtt{and
}~
\mit{bsigbind
}\rangle \longrightarrow
746 \
{\mit{sigid
}_1
\mapsto I\
} \langle+
\mit{G
}\rangle
754 \item[(
\ref{eqn:mlb:DS:bsigbind
})
] Note that $
\mit{bsigbind
} \subset
755 \mit{sigbind
}$. Hence, this rule can be derived from the
756 Definition's $
\mit{IB
} \vdash \mit{sigbind
} \Rightarrow \mit{G
}$, noting that
757 the derivation may neither cause a side-effect nor generate an
764 \textbf{(Basis) Functor Bindings
} \hfill
765 \fbox{$
\mit{B
} \vdash \mit{bfunbind
} \longrightarrow \mit{F
}$
}
770 \mit{B
}(
\mit{funid
}_2) = (
\mit{strid
}:
\mit{I
},
\mit{strexp
},
\mit{B
})
\quad
771 \langle\mit{B
} \vdash \mit{bfunbind
} \longrightarrow \mit{F
}\rangle
773 \mit{B
} \vdash \mit{funid
}_1 ~
\mtt{=
}~
\mit{funid
}_2 ~
\langle\mtt{and
}~
\mit{bfunbind
}\rangle \longrightarrow
774 \
{\mit{funid
}_1
\mapsto (
\mit{strid
}:
\mit{I
},
\mit{strexp
},
\mit{B
})\
} \langle+
\mit{F
}\rangle
779 \section{Derived Forms
}
780 \label{sec:mlb:DerivedForms
}
781 Figure~
\ref{fig:mlb:DF:bindings
} shows derived forms for structure,
782 signature, and functor bindings in MLB. These derived forms are
783 a useful shorthand for specifying import and export filters.
787 \begin{tabular
}{|l|l|
}
788 \multicolumn{1}{c
}{Derived Form
} &
789 \multicolumn{1}{c
}{Equivalent Form
} \\
790 \multicolumn{2}{c
}{} \\
791 \multicolumn{2}{l
}{\textbf{(Basis) Structure Bindings
} $
\mit{bstrbind
}$
} \\
793 $
\mit{strid
} ~
\langle\mtt{and
}~
\mit{bstrbind
}\rangle$ &
794 $
\mit{strid
} ~
\mtt{=
}~
\mit{strid
} ~
\langle\mtt{and
}~
\mit{bstrbind
}\rangle$ \\
796 \multicolumn{2}{c
}{} \\
797 \multicolumn{2}{l
}{\textbf{(Basis) Signature Bindings
} $
\mit{bsigbind
}$
} \\
799 $
\mit{sigid
} ~
\langle\mtt{and
}~
\mit{bsigbind
}\rangle$ &
800 $
\mit{sigid
} ~
\mtt{=
}~
\mit{sigid
} ~
\langle\mtt{and
}~
\mit{bsigbind
}\rangle$ \\
802 \multicolumn{2}{c
}{} \\
803 \multicolumn{2}{l
}{\textbf{(Basis) Functor Bindings
} $
\mit{bfunbind
}$
} \\
805 $
\mit{funid
} ~
\langle\mtt{and
}~
\mit{bfunbind
}\rangle$ &
806 $
\mit{funid
} ~
\mtt{=
}~
\mit{funid
} ~
\langle\mtt{and
}~
\mit{bfunbind
}\rangle$ \\
810 \caption{Derived forms of (Basis) Structure, Signature, and Functor Bindings
}\label{fig:mlb:DF:bindings
}
813 \bibliographystyle{alpha
}