9.1 Introduction	9 SML translator	9.3 Declarations
9.2 Activating the SML translator

9.2 Activating the SML translator

rsltc -m <file>

where <file> takes the form X or X.rsl and contains the RSL scheme or object named X. It generates files X.sml and X_.sml. The latter is loaded by the former.

X.sml can be executed by starting the SML run-time system and then giving the command

use "<dir>/X.sml";

where <dir> is the directory where X.rsl is located. dir should be an absolute path starting with "/" and any intermediate separators must be Unix-style forward slash "/", not DOS-style "\". Note the semicolon ";" at the end of this command. If you forget it you will get a prompt = on the next line, and you can type it there.

9.2.1 Output

Executing the file X.sml generates some output which is not useful, but which we have not been able to get rid of. For example, the file

generates the following output

Standard ML of New Jersey, Version 110.0.7, September 28, 2000 [CM; autoload enabled]
- [opening /home/cwg/gentle/ug/ex/X.sml]
val it = () : unit
val it = () : unit
val it = () : unit
val it = true : bool
[starting dependency analysis]
[scanning /home/cwg/sml/rslml/rslml.cm]
[checking /home/cwg/sml/rslml/CM/x86-unix/rslml.cm.stable ... not usable]
[dependency analysis completed]
[Registering for AUTOLOAD...]
val it = () : unit
[Autoloading...]
[recovering /home/cwg/sml/rslml/CM/x86-unix/rslml.sml.bin... done]
[Autoloading done.]
[opening X_.sml]
structure RT_Int : <sig>
structure RT_Bool : <sig>
structure X : <sig>
open X
val it = () : unit
[t1] 3
val it = () : unit
[t2] true
val it = () : unit
val it = () : unit
val it = () : unit
val it = () : unit
-  

This shows the RSL library being loaded (see section 9.2.3). Don't worry that there is not a "stable" version: the .bin file is the compiled version. From the RSL library the structures RT_Int and RT_Bool are loaded, then the structure X generated from the RSL input.

Finally we get the results of the two test cases, followed in each case by the line

val it = () : unit

This is just SML reporting completion of the function that generated the test case: the current value (it) is the unit value "()" (which is just like its counterpart in RSL). The last three identical lines are the results of other functions used to load and run X.sml and X_.sml.

Finally there is a prompt "-" for the next command. It is possible to return to the file X.rsl, make any changes you wish, re-translate, and load X.sml again into SML with the use command.

9.2.2 Saving the output

In emacs, the output from the run of SML can be saved by returning to the buffer displaying RSL file and selecting the item Save results from SML run in the RSL menu. This saves the results in a file X.sml.results, if the file translated was X.rsl. The additional output produced by the SML system is removed, so that the example above for example would give

[t1] 3
[t2] true

Saving the results will also kill the SML buffer: it will restart next time you run SML.

9.2.3 RSL Library

X.sml contains the compilation directive

CM.autoload' "<DIR>/rslml.cm";

where DIR is the variable RSLML_PATH. This in turn causes the definitions in rslml.sml to be loaded. The first time this file is loaded in this way it is compiled; thereafter the compiled version is loaded.

rslml.sml contains definitions of SML structures for

• the basic types of RSL and standard functions on them: equality and conversions to strings for output

• parameterised structures for set, list, map and function types

• definitions of the infix and prefix operators on these types

• additional functions for translating quantified and comprehended expressions

We refer to these definitions below as the RSL library.

During translation, error messages may be generated with the standard file:line:column format showing from where in the RSL specification the message was generated. The cause of the error must be corrected and the translator run again.

During execution, run-time error messages may be produced. There are as follows, where x, y and z indicate values that are part of the generated message, c is a constant and v a variable:

Invalid integer literal x
Division by zero
Modulo zero
Integer exponentiation with negative exponent x
Cannot compute 0 ** 0
Invalid real literal x
Zero raised to non-positive power x
Negative number x raised to non-integer power y
hd applied to empty set
Cannot select from empty set
hd applied to empty list
tl applied to empty list
List applied to index outside index set
Cannot select from empty list hd applied to empty map
Map applied to value outside domain
Nondeterministic enumerated map
Maps do not compose
Cannot select from empty map
List x applied to non-index y
Text x applied to non-index y
Map x applied to non-domain value y
x union y has non-disjoint domains
Cannot compute function equality
Destructor x applied to wrong variant
Reconstructor x applied to wrong variant
Argument of x(y) not in subtype
Precondition of x(y) not satisfied
Result z of x(y) not in subtype
Case incomplete for value x
Value x of c not in subtype
Initial value x of v not in subtype
Value x of v not in subtype
chaos encountered
stop encountered
swap encountered

These messages are generated via exceptions that are caught within each test case, allowing following test cases to be executed.

The SML run-time system may also generate warning messages, for example if let or case expressions are not exhaustive.

9.2 Activating the SML translator
9.1 Introduction	9 SML translator	9.3 Declarations