| 
| 9 SML translator |
| 
| 9.2 Activating the SML translator |
|
| 9.1 Introduction |
9.1 Introduction
The SML translator was written by Ke Wei, as reported in [4].
We use the term RSLSML for the subset of RSL that is accepted
by the the translator. RSLSML excludes object arrays,
channels, axioms, abstract types, union types, implicit value and
function definitions. It only includes quantified expressions,
comprehended expressions, and implicit let expressions if
they conform to the rules given below in
sections 9.7.11, 9.7.6,
and 9.7.23.
The translator converts all RSL identifiers to unique SML identifiers,
which start with the original identifier. This ensures both
uniqueness and no clashes with SML reserved words. It is not intended
that the SML code be readable or changeable by hand, nor that users
need to know SML.
The translator produced code is intended for use with SML/NJ (SML of
New Jersey), which is based on SML'97 [5]. The run-time
system for SML/NJ is freely available for a variety of platforms from
http://cm.bell-labs.com/cm/cs/what/smlnj/. The translator
has been tested on Solaris, Linux and Windows 9X and NT.
The following lists mention known errors and problems.
- The arithmetic types Int (including Nat) and Real
are naively translated into Int and Real without regard for actual
limits and precision.
- The translation relies heavily on the syntactic form of the
input, which means that often a semantically equivalent piece of RSL
text cannot be translated or is translated differently. For
example, a record or variant type is accepted, but the equivalent
expansion into a sort, some value signatures, and some axioms is not
accepted.
Chris George, April 17, 2008
| 9.1 Introduction |
| |
| 9 SML translator |
| |
| 9.2 Activating the SML translator |
|