RUNNING THE TYPECHECKERS
------------------------

This file describes the features common to all of the systems (using
fomega in examples for the sake of concreteness).  For more
information about the individual typecheckers, see the README files in
the appropriate subdirectories.


THE READ-EVAL-PRINT LOOP
------------------------

To run the fomega typechecker interactively, type "fomega".  A welcome
banner will be printed, followed by a ">" prompt.  At this point, you
can type expressions terminated by semicolons:

    > x = plus 5 6;
    x = 11 : Int
    > f = fun(i:Int) plus i x;
    f = <val> : Int -> Int
    > f 5;
    it = 16 : Int

Each expression in turn is parsed, typechecked, compiled, and
executed, and the result printed.  The top-level environment is then
extended with a binding of the given name (or "it" if no name was
given explicitly) to the resulting value.

[Because of poor communication between the fomega front-end and the
SML-NJ back-end, some spurious diagnostic messages may be printed in
addition to what is shown here.  Also, the fmeet implementation does
not currently include a code generator: only the types of expressions
are printed.]

Types can be declared in the same way, using "==" instead of "=":

    > P == Some(X) {v:X, f:X->Int};
    > p1 = pack {v=3, f=fun(i:Int) plus i 1} 
    -        as P
    -        hiding Int
    -        end;
    p1 = <val> : P


BATCH-MODE EXECUTION
--------------------

If the system is started with a filename argument

    fomega test.f

then input is read from this file instead of from the terminal. 


SYNTAX
------

Term definitions have the form

    x = e;

or simply

    e;

Type definitions have the form

    A == T;

The systems differ in the syntax of expressions and types.  See the
individual README files and examples for more detailed information.

The comment character is %.  Everything from the % to the end of the
line is ignored.

To exit the system, send an EOF character (^D).


PERVASIVE ENVIRONMENT
---------------------

Each typechecker comes with a pervasive environment that is loaded
before the executable typechecker is dumped.  The file "perv" controls
the contents of this environment.


COMMANDS
--------

In addition to expressions and type definitions, the top-level
read-eval-print loop responds to commands of the following forms:

    use "file";         Read the contents of "file" as if they had
                        been typed directly to the system.  If "file"
                        is not given with an extension, an appropriate
                        suffix is added (".f" for fomega or ".fm" for
                        fmeet).  If "file" has no explicit path and it
                        cannot be found in the current directory, the
                        subdirectory "examples" is also searched.
    
    use file;           Same as the above, if "file" contains no
                        special characters.

    !<command> [<arg>]; Execute the internal command <command> with
                        the optional argument <arg>.  (See below.)


COMMAND-LINE SWITCHES
---------------------

The following command-line switches are recognized by all of the
typecheckers: 

    -o file           Redirect the typechecker's output (but not NJ-SML's
                      spurious low-level diagnostic messages) to a file
                      named "file"

    -set flag         Set one of the internal flags (see below)

    -reset flag       Reset an internal flag

    -latex            Same as "-set latex -set TERSE"

    -sml              Immediately escapes to the SML read-eval-print
                      loop instead of running the typechecker.  (This
                      is mainly useful when rebuilding the typechecker.)


INTERNAL FLAGS AND COMMANDS
---------------------------

The typecheckers include a number of internal flags, mostly used to
control the display of internal diagnostics and debugging information.
Some useful ones are:

    latex               Controls latex interaction mode (see below)
    
    TERSE               Controls printing of banners and inessential
                        diagnostics 

    echo                Controls the echoing of input lines when the
                        latex flag is false


The useful internal commands include:

    besilent            Temporarily suppress all output.  (This is
                        useful when typesetting latex documents, for
                        establishing bindings or setting flags that
                        should not appear in the final output.)

    beloud              Overrides a previous "besilent"
    

LATEX INTERACTION MODE
----------------------

To support the typesetting of documents with lambda-calculus examples,
all the typecheckers support a "latex mode," established using the
"-latex" command-line switch or the "set latex" command.  

In latex mode, lines of input that do not begin with either ">" or
"%%%" are passed straight through from the input to the output.  The
delimiters "<<" and ">>" can be used to indicate expressions that are
to be set in the same typeface as the lambda-calculus portions of the
input. 

Lines beginning with ">" are echoed, and then passed to the parser,
typechecker, and evaluator as if they had been typed without the >.
The echoed input and the system's responses are enclosed in a verbatim
environment.

Lines beginning with "%%%" are passed to the parser without echoing
them.