**** TOPIC: Help
No Special Predicates.
 
Defined Predicates:
help : o
Lists all the special and defined predicates and declared constants that
are known to eLP.  They are organized into different topics.  For more
help on a given item X, use ``describe X''.
 
describe : A -> o
``describe X'' writes information about X.  X should be a special or
defined predicate, or a declared constant (or constructor).
 
document : string -> o
``document Outputfile'' writes all available on-line documentation [[ to the
file Outputfile for off-line reference ]].
 
 
Declared Constants:
doc : A1 -> string -> o
``doc C String'' succeeds if C is a constant that has been given documentation
string String.
 


**** TOPIC: Top-Level

Special Predicates:
top : o
Starts a new top level from which only ``pop'' can exit.
This is mainly useful in conjunction with higher-order predicates
and programs that augment the interpreter's context, such as
``switching'', ``=>'', ``==>'', ``pi'', etc.
 
pop : o
Pops to the previous top level, or signals an error if there are none.
 
 
Defined Predicates:
bye : o
Exits from eLP.
 
 
No Declared Constants.
 
 

**** TOPIC: Logical Primitives
Special Predicates:
true : o
Always succeeds.
 
',' : o -> o -> o
Conjunction.  ``G1, G2'' succeeds if G1 succeeds and then G2 succeeds.
 
';' : o -> o -> o
Disjunction. ``G1; G2'' succeeds if G1 succeeds, or if G1 fails, if G2 then
succeeds.
 
'=>' : o -> o -> o
Implication.  ``D => G'' succeeds if, under the assumption D, G succeeds.
Note that after G succeeds, D is not assumed for subsequent goals.  However,
if they fail, and the interpreter backtracks to obtain more solutions for
G, D will again be assumed.
 
pi : (A2 -> o) -> o
Universal quantification.  ``pi X \ G'' succeeds if G succeeds after
substituting a new parameter for X in G.  This new parameter may not
occur in the substitution term for any variable that is (implicitly or
explicitly) quantified `outside of' X.  Thus, ``pi X \ (X = Y)'' will
fail, since Y may not be instantiated with the parameter instantiating X.
However, ``pi X \ (X => X)'' will succeed, as will
``pi X \ (sigma Y \ (X = Y))''.
 
named_pi : string -> (A3 -> o) -> o
``named_pi Str X \ G'' behaves like ``pi X\ G'' (universal quantification)
and in addition, assigns the named given by the string Str to the new
parameter introduced for X. This name can be used for parsing and printing.
If a variable of name Str already exists in the current context, it will be
shadowed during the lifetime of the new parameter.
 
sigma : (A4 -> o) -> o
Existential quantification.  ``sigma X \ G'' succeeds if G succeeds after
a new free variable is substituted for X in G.
 
 
No Defined Predicates.
 
No Declared Constants.

**** TOPIC: Interpreter
Special Predicates:
fail : o
``fail'' always simply fails.
It could be defined by  ``fail :- pi C \ C''.
 
! : o
``!'' commits to the current clause and all the choices made since the
clause was selected.  Note that this will also commit to the particular choice
of unifier that was made when unifying the head of the clause with a goal.
This situation does not arise when unique most general unifiers exist.  A
common idiom to avoid this commitment is to move unification to occur after
the commitment has been made.
 
once : o -> o
``once G'' solves G and then commits to all choices made while solving
G.  It could (almost) be defined by
 once G :- pi a \ ((a :- G, !) => a).
except that a cut in G will commit to the current clause selection.
Thus, with the defined ``once'', ``?- once (!, fail) ; true.'' would
succeed, while the special ``once'' fails.
  The primary reason for making ``once'' a special predicate is that it will
eagerly remove the choice points from the stack, thus providing the only
effective way of controlling stack growth in eLP.  Another use is to achieve
closing of streams, when it is guaranteed that they will no longer be read
from or written to.  For example:
  read_first_item File Item :-
    once (reading File Instream \ (seeing Instream (reread X \ (Item = X;
      error (writesans "First item, ", write X,
             writesans ", contains undeclared constants."))))).
 
'=' : A5 -> A5 -> o
``M = N'' simply unifies M and N.  '=' could be defined by ``M = M.''
 
error : o -> o
``error G'' signals an error by writing "eLP Error: " and then solves G.
G is intended to write out an error message.  For example,
  ``error (writesans "Cannot take square root of ", write N,
           writesans ", a negative number.")''
 
error_catch : o -> o -> o
``error_catch G EG'' solves G.  If an error occurs (either signalled by
eLP or with the ``error'' special predicate) while solving G, EG will be
invoked after the error message has been printed.
 
 
default : (o -> o) -> o
``default'' destructively establishes a default for an environment
parameter on the current top-level.  It is applicable only to
  [[ ('==>' Module) ]], (searching Directory), (switching Sw Onoff),
  [[ (prompting String), (grammar Directory), or (depth_bounding Int) ]]
and such constants as
 [[ using_none ]], searching_none, [[ or standard_grammar ]]. 
It is intended primarily for the user's init file.
 
 
Defined Predicates:
solve : o -> o
``solve G'' simply solves goal G.
Writing ``solve G'' instead of ``G'' in the body of a clause has the effect
that any commit in G, will not commit to the current clause.  Thus
  ``(!, fail); true''         will fail, and
  ``solve (!, fail); true''   will succeed.
 
not : o -> o
``not G'' succeeds if G fails.
 
 
No Declared Constants.

**** TOPIC: Input
Special Predicates:
reread : (A6 -> o) -> o
``reread X \ G'' reads a term M from the current input stream and then
solves the goal ``(X \ G) M''.  The type of M is unified with the type of X,
and an error is signalled if this type-unification fails.  When G fails, the
next item from the current input stream is read and passed as argument to
(X \ G).  reread fails when the end of the input stream is reached.
See also ``read''.
 
 
Defined Predicates:
read : (A7 -> o) -> o
``read (X \ G)'' reads a term M from the current input stream and then
solves the goal ``(X \ G) M''.  The type of M is unified with the type of X,
and an error is signalled if this type-unification fails.  When G fails,
the read also fails.  If the end of the input stream is reached, read
signals an error.  See also ``reread''.

 
 
No Declared Constants.


**** TOPIC: Output
Special Predicates:
write : A8 -> o
``write X'' writes X to the current output stream.  Various switches control
how the output appears, but it should always be possible to ``read'' something
that was written.
 
writetype : A9 -> o
``writetype X'' writes the type of X to the current output stream.
 
writesans : string -> o
``writesans String'' writes the string String to the current output stream
without surrounding double-quotes.  It can therefore not be read again.
 
writeered : A10 -> o
``writeered X'' writes an eta-reduced version of X to the current output
stream.
 
tab : int -> o
``tab N'' tabs to position N in the current output stream.  If this position
cannot be calculated, or if the cursor is beyond this position, it has no
effect.
 
 
Defined Predicates:
nl : o
Writes a newline to the current output stream.
 
 
No Declared Constants.

**** TOPIC: Modules
Special Predicates:
searches : o
Writes a message giving information about which directories are currently
searched for files containing modules.
 
load : string -> o
``load Module'' tries to find a file "Module.mod" in the directories
assumed with ``searching'' (which always contains the current directory).
Gives an error message if no such file can be found.  If the given module
already exists, its clauses are completely erased before the new clauses are
installed.
 
'==>' : string -> o -> o
``Module ==> G'' makes all the clauses in Module visible while trying to
solve G.  It also affects parsing (on read), since constants in M are now
recognized.  M is loaded, if it is not already known, which may lead to a
whole avalanche of loads, in case M imports modules that have not been loaded
either.  Modules can be loaded and made visible by default using a line such
as ``default ('==>' "lists").'' in the initialization file.
 
uses : o
Writes a message with information about which modules are currently visible.
 
 
Defined Predicates:
searching : string -> o -> o
``searching Directory G'' adds Directory to the list of directories to
search for files containing modules.  The most recently added directory
is looked in first.
 
search : string -> o
``search Directory'' starts a new top level on which Directory is searched
for files containing modules.
 
use : string -> o
``use Module'' starts a new top level in which M's clauses and type
declarations are visible.  See ``'==>'''.
 
 
Declared Constants:
searching_none : o -> o
``default searching_none'' will destructively remove all directories but the
current one (that is, "./") from the search path.  A goal constructed from
``searching_none'' will result in an error.
 
using_none : o -> o
``default using_none'' destructively makes all modules except elp (the
system module) invisible.  A goal constructed from ``using_none'' will
result in an error.

**** TOPIC: Switching
Special Predicates:
switching : sw -> onoff -> o -> o
``switching Sw Onoff G'' sets switch Sw to Onoff while solving G.
 
switches : o
Displays information about the current value of switches.
 
 
Defined Predicates:
switch : sw -> onoff -> o
``switch Sw Onoff'' enters a new top-level in which switch Sw is Onoff.
 
trace : trace_opt -> o
``trace Opt'' starts a new top-level, in which tracing of option Opt is on.
 
 
Declared Constants:
on : onoff
The on-value for switches.
 
off : onoff
The off-value for switches.


**** TOPIC: Switches
No Special Predicates.
 
No Defined Predicates.
 
Declared Constants:
projfirst : sw
If on, projections will be tried first during the depth-first search for
a unifier.
 
tracing : trace_opt -> sw
``(tracing Opt)'' is a switch that controls whether Opt will be traced.
 
warning : warn_opt -> sw
``(warning Wopt)'' is a switch that controls whether the warning Wopt will
be given.
 
**** TOPIC: Trace Options
No Special Predicates.
 
No Defined Predicates.
 
Declared Constants:
match : trace_opt
If ``(tracing match)'' is on, messages are printed when MATCH is 
entered and when it selects a substitution term.  MATCH is the only
place where unification can branch.  Tabbing of MATCH is separate
from tabbing in the tracing of goals or clauses.
 
unify : trace_opt
If ``(tracing unify)'' is on, messages are printed when UNIFY is 
entered.



**** TOPIC: Warnings
No Special Predicates.
 
No Defined Predicates.
 
Declared Constants:
typevar : warn_opt
If ``(warning typevar)'' is off, the unifier will not issue warning messages
when the result type of an argument to MATCH is a type variable.  In such
a situation, the unifier is incomplete --- hence the warning.  This often
signifies that the types in a program or query were underspecified.
 
**** TOPIC: Arithmetic
Special Predicates:
'is' : int -> int -> o
``X is Y'' succeeds when X is (unifies with) the term encoding the value
of the expression represented by Y (which must not have free variables).
The interpreter currently only allows the evaluation of integer expressions
with outermost operations ~, +, -, *, div, mod, ascii and size.  Such
expressions can further involve the operations chr, str, hd_char, ^, and
substring.
 
'=:=' : int -> int -> o
``X =:= Y'' succeeds when both X and Y are integers, and X is equal to Y.
 
'=\=' : int -> int -> o
``X =\= Y'' succeeds when both X and Y are integers, and X is not equal
to Y.
 
'<' : int -> int -> o
``X < Y'' succeeds when both X and Y are integers, and X is less than Y.
 
'>' : int -> int -> o
``X > Y'' succeeds when both X and Y are integers, and X is greater than Y.
 
'=<' : int -> int -> o
``X =< Y'' succeeds when both X and Y are integers, and X is less than or
equal to Y.
 
'>=' : int -> int -> o
``X >= Y'' succeeds when both X and Y are integers, and X is greater than
or equal to Y.
 
 
No Defined Predicates.
 
Declared Constants:
'+' : int -> int -> int
``N + M'' is not treated specially by the unifier, that is, 1 + 1 will not
unify with 2, but it can be evaluated using the ``is'' special predicate.
Note that the + operator must be surrounded by whitespace.
 
'-' : int -> int -> int
``N - M'' is not treated specially by the unifier, that is, 1 - 1 will not
unify with 0, but it can be evaluated using the ``is'' special predicate.
Note that the - operator must be surrounded by whitespace.
 
'*' : int -> int -> int
``N * M'' is not treated specially by the unifier, that is, 1 * 1 will not
unify with 1, but it can be evaluated using the ``is'' special predicate.
Note that the * operator must be surrounded by whitespace.
 
'div' : int -> int -> int
``N div M'' is not treated specially by the unifier, that is, 3 div 2 will
not unify with 1, but it can be evaluated using the ``is'' special predicate
(interpreted as integer division, rounding down).
 
'mod' : int -> int -> int
``N mod M'' is not treated specially by the unifier, that is, 3 mod 2 will
not unify with 1, but it can be evaluated using the ``is'' special predicate.
Note that the mod operator must be surrounded by whitespace.
 
~ : int -> int
``~ N'' is integer negation.  ``~ N'' is not treated specially by the
the unifier, that is ~(~2) does not unify with 2, but it can be evaluated
using the special predicate ``is''.



**** TOPIC: Lists
No Special Predicates.
 
No Defined Predicates.
 
Declared Constants:
nil : list A11
``nil'' stands (by convention) for the empty list.  It is not interpreted
specially, but used by the lists library module.
 
'::' : A12 -> list A12 -> list A12
``X :: L'' stands (by convention) for a list with head X and tail L.  '::'
is not treated specially by the interpreter, but used by the lists library
module.  It associates to the right.  For example, ``1::2::3::4::nil'' is
the list of the integers from 1 through 4.
 
**** TOPIC: Characters and Strings
Special Predicates:
'isc' : char -> char -> o
``X isc Y'' succeeds when X is (unifies with) the term encoding the value
of the expression represented by Y (which must not have free variables).
The interpreter currently only allows the evaluation of character expressions
with outermost operations chr and char_of.  Such expressions can further
involve the operations str, ^, substring, ascii, size, ~. +, -, *, div,
and mod.
 
'iss' : string -> string -> o
``X iss Y'' succeeds when X is (unifies with) the term encoding the value
of the expression represented by Y (which must not have free variables).
The interpreter currently only allows the evaluation of string expressions
with outermost operations str, ^, and substring.  Such expressions can further
involve the operations chr, char_of, ascii, size, ~, +, -, *, div, and mod.
 
 
No Defined Predicates.
 
Declared Constants:
chr : int -> char
``chr'' is the constructor for acsii characters.  Its type is
``int -> char''.   When it is evaluated on the right hand side of
an ``isc'', an ``iss'', or an ``is'', it will cause a failure if the
integer argument is negative or greater than 255.

``ascii \"a\"'' does not unify with 97 (the acsii code for a).  When it
is evaluated on the right hand side of an ``isc'', an ``iss'', or an ``is'',
it will return an integer between 0 and 255.
 
str : char -> string
``str'' converts an ascii character into the corresponding string of length
one.  It has type ``char -> string''.
 
char_of : string -> int -> char
``char_of S N'' is for acquiring the character N places in from the left
of the string S.  ``char_of S N'' is not treated specially by the unifier,
thaat is, ``char_of \"HiThere\" 2'' does not unify with ``chr 87''
(the character representation of T).  When it is evaluated on the right hand
side of an ``isc'', an ``iss'', or an ``is'', it will return a character in
the form ``chr X'', provided that the string has size at least N + 1, and
otherwise and exception is raised.
 
'^' : string -> string -> string
``^'' concatenates two strings.  ``X ^ Y'' is not treated specially by
the unifier, that is \"Hi\" ^ \"There\" will not unify with \"HiThere\",
but it can be evaluated to \"HiThere\" using the special predicate ``iss''.
 
substring : string -> int -> int -> string
``substring S F L'' is for computing the substring of the string S,
starting F characters in from the left for a length of L characters.
``substring S F L'' is not treated specially by the unifier, that is
``substring 3 2 \"HiThere\"'' will not unify with \"Th\", but it
can be evaluated to \"Th\" using the special predicate ``iss''.
 
size : string -> int
``size S'' is for computing the number of characters in a string S.
``size S'' is not treated specially by the unifier, that is
``size \"HiThere\"'' will not unify with 7, but it can be evaluated 
to 7 using the special predicate ``is''.
