A quick start using Terzo.
		      ==========================

This is a short tutorial describing how to start the Terzo
lambda-prolog interpreter, enter a module, and how to execute a query.


		       Invoking the interpreter
		       ======== === ===========

Proper installation instructions for Terzo are in the Install file
that comes with the distribution.  A result of this installation (on
Unix systems) will be a small shell script for running SML and loading
the necessary binary file.

Assuming that this script is named Terzo and the directory which
contains it is in your path, then you start Terzo by simply typing

% Terzo

(If this doesn't work, ask your system administrator for the proper
Unix command.)

Once the iterpreter has started, you should be greeted with the
"Terzo> " prompt.  You are now at the "loader" level of the
interpreter.


			     Terzo Loader
			     ===== ======

The loader has only a few tasks.  It is responsible for reading files
containing lambda Prolog, setting switches, and invoking two other
levels of the interpreter (the module enry level and the logic
interpreter).  The loader makes use of a simple script language.  It's
commands are:

	load  quit  end  print  show  begin  help  set  query

To use these commands, you must preceed each with the # symbol.
Arguments may also be needed.  All lines to the loader are terminated
with a period.  White space is ignored, and strings, switch identifiers,
and module identifiers are the only recognized datatypes. Strings and
module identifiers are the same as defined for the lambda prolog
language, and switch identifiers are the same as lcid's in the lambda
prolog language (see the file lexical.txt for details).

These commands are described in more detail in the file 
loadercommands.txt.  The following example dialog with the load
contains three commands and the loader's response.

+------------------------------------------------------------------+
| Terzo> #show path.                                               |
| path                            /share/pub/miller/terzo/lib/ .   |
| Terzo> #load "list_util.mod".                                    |
| [reading file /share/pub/miller/terzo/lib/list_util.mod]         |
| module ListUtil                                                  |
| [closed file /share/pub/miller/terzo/lib/list_util.mod]          |
| Terzo> #print ListUtil.                                          |
| type :: A -> list A -> list A.                                   |
| infixr :: 5.                                                     |
| type append list A -> list A -> list A -> o.                     |
| type join list A -> list A -> list A -> o.                       |
| kind list type -> type.                                          |
| type memb A -> list A -> o.                                      |
| type memb_and_rest A -> list A -> list A -> o.                   |
| type member A -> list A -> o.                                    |
| type nil list A.                                                 |
| type nth_and_rest int -> A -> list A -> list A -> o.             |
| type nth_item int -> A -> list A -> o.                           |
| Terzo>                                                           |
+------------------------------------------------------------------+


			  Module Entry Level
			  ====== ===== =====

The module entry level or loop is started with a "#begin." statement.
Unless an error occurs, all following statements are read as lines in
a lambda Prolog module.  This loop ends when a matching "#end."
statement is read or end of file is reached.  For instance:

+------------------------------------------------------------------+
| Terzo> #begin.                                                   |
| |module list_append.                                             |
| list_append|	type append  list A -> list A -> list A -> o.      |
| list_append|	                                                   |
| list_append|	append nil K K.                                    |
| list_append|	append (X::XS) YS (X::ZS) :- append XS YS ZS.      |
| list_append|	#end.                                              |
| module list_append                                               |
| Terzo>                                                           |
+------------------------------------------------------------------+

The interpreter now has the module list_append available to it. 

Generally, modules are entered into files and brought into the Terzo
system via the #load command.


		       Logic Interpreter Level
		       ===== =========== =====

The #query loader command is used to call the logic interpreter.  To
initial the lambda Prolog interpreter, we must first determine which
module and which goal formulas to give it.

To execute a single query against a module from the loader, use the
#query command with two arguments: the first argument is a
comma-separated list of module names (all of which must already have
been loaded successfully) and the goal.  For example,

+------------------------------------------------------------------+
| Terzo> #query list_append append (1::2::nil) (1000::nil) X.      |
|                                                                  |
| X = 1 :: 2 :: 1000 :: nil                                        |
|                                                                  |
| Terzo>                                                           |
+------------------------------------------------------------------+

After printing the solution for X, it was necessary to press a
carriage return: if you had wanted the interpreter to look for another
solutions, you would have needed to enter a semicolon here.

To enter an interactive loop with the interpreter, use #query with
only the first argument.  For example,

+------------------------------------------------------------------+
| Terzo> #query list_append.                                       |
| ?- append X Y Z.                                                 |
| X = nil                                                          |
| Y = Z                                                            |
| Z = Z ;                                                          |
|                                                                  |
| X = X1 :: nil                                                    |
| Y = Y                                                            |
| Z = X1 :: Y ;                                                    |
|                                                                  |
| X = X1 :: X2 :: nil                                              |
| Y = Y                                                            |
| Z = X1 :: X2 :: Y                                                |
|                                                                  |
| ?- quit.                                                         |
| Terzo> #quit.                                                    |
| %                                                                |
+------------------------------------------------------------------+

The "quit." command exits the interactive query interpreter, while the
"#quit." command exits the loader.

			     Loader Script Language
			     ====== ====== ========

Using the #load command, the loader can read not only lambda Prolog
files but scripts for the loader.  The # mark is used to determine if
a line is meant for the loader or is part of the lambda Prolog module.

For example, the following is a text file that contains many of the
example loader commands.

+------------------------------------------------------------------+
| #show path.
| #load "list_util.mod".
| #print ListUtil.
| #begin.
| module list_append.
| type append  list A -> list A -> list A -> o.
| append nil K K.
| append (X::XS) YS (X::ZS) :- append XS YS ZS.
| #end.
| #query list_append append (1::2::nil) (1000::nil) X.
+------------------------------------------------------------------+

If these lines are storied in a file, say simple.script, they can be
loaded as follows.

+---------------------------------------------------------------------+
| Terzo> #load "/share/pub/miller/elios/lProlog/terzo/simple.script". |
| [reading file /share/pub/miller/elios/lProlog/terzo/simple.script]  |
| path                            /share/pub/miller/terzo/lib/ .      |
| [reading file /share/pub/miller/terzo/lib/list_util.mod]            |
| module ListUtil                                                     |
| [closed file /share/pub/miller/terzo/lib/list_util.mod]             |
| type :: A -> list A -> list A.                                      |
| infixr :: 5.                                                        |
| type append list A -> list A -> list A -> o.                        |
| type join list A -> list A -> list A -> o.                          |
| kind list type -> type.                                             |
| type memb A -> list A -> o.                                         |
| type memb_and_rest A -> list A -> list A -> o.                      |
| type member A -> list A -> o.                                       |
| type nil list A.                                                    |
| type nth_and_rest int -> A -> list A -> list A -> o.                |
| type nth_item int -> A -> list A -> o.                              |
| module list_append                                                  |
|                                                                     |
| X = 1 :: 2 :: 1000 :: nil                                           |
|                                                                     |
| [closed file /share/pub/miller/elios/lProlog/terzo/simple.script]   |
| Terzo>                                                              |
+---------------------------------------------------------------------+