Term Syntax and Display

We describe the syntax of the input language. Tokens are either identifiers (made of alphanumeric characters and the characters ``_" and ``?") or operators (made up of special characters, excluding parentheses, quotes, braces, and brackets).

Identifiers have two special subsets: numerals (all characters numeric) and variables (starting with ``?"). Other identifiers are called ``constants". Operators starting with a caret are operator variables and an initial colon represents an operation on operators which may be iterated.

Constants and operators other than variables must be declared to be used. Predeclared constants include ``RAISE" (a built-in theorem), ``true" and ``false". Built-in operators include ``=", ``," (pairing), ``@" (function application), ``=>", ``=>>", ``<=", and ``<<=" (theorem embedding infixes), ``+!", ``*!", ``-!", ``/!", ``%!", ``=!", and ``<!" (operators of the built-in unsigned integer arithmetic).

Single identifiers of whatever class are terms. Any term enclosed in parentheses is a term. A term preceded by an operator (here used as a unary prefix) is a term. An operator flanked by terms is a term (here the operator is used as an infix). A term enclosed in brackets is a term (a constant function whose value is the enclosed term).

In the current version, each operator used as a prefix has associated with it a default left argument (selected by the user). In other words, all unary prefix terms are abbreviations for binary infix terms. If an operator for which a default left argument has not been declared is used as a prefix, a bogus value is used which signals an error condition to the prover. It should be noted that the ``left" movement command can for this reason be used with prefix terms. The declareunary command above should be used for prefixes which are not also to be used as infixes; the declareprefix command below can be used to set desired behavior where overloading is intended.

The default operator precedence assigns to all infixes and prefixes the same precedence and associates to the right as far as possible. The user can assign integer precedences to prefixes/infixes (and this information can be stored in theories); higher precedences bind more tightly; even precedence associates to the right and odd to the left.

Two lists are used by the parser and are actually components of the theory type: PREFIXINFO contains operators with default left arguments and PRECEDENCEINFO contains precedence information. Saved theories are actually stored in default precedence in the current version, and the precedence list is loaded at the end of the process. Parsing is done in a first pass independent of declaration checking; the parser will parse and display terms which the prover will tell you contain undeclared constants or operators.

There is some pretty-printing built into the prover's display function; some indenting is done in a way which is intended to suggest the structure of terms. There are commands to set the right margin of the display and to set the ``depth" of the display.

Commands which relate to term display include:

declareprefix <string> <string>:

Declares the default left argument of a prefix (the first argument) to be a constant indicated by the second argument.

setprecedence <string> <integer>:

Sets precedence of an operator (the first argument) to an integer value (the second argument). Even precedence operators associate to the right and odd precedence operators to the left.

declaretypeinfo <string> <string>:

Assigns an implicit strongly Cantorian type to a variable (the first parameter, without leading ?). The effect is to cause the type infix : to function as a unary operator on that variable with invisible left argument determined by the second parameter. This information is currently not stored in theory files.

detypeinfo <string>:

Removes implicit type from a variable.

showprecs:

Shows a table of precedences (including explicit indication of left or right association).

clearprecs:

Restores all precedences to the default.

setline <integer>:

Set the right margin for term displays.

setdepth <integer>:

Limit the depth to which terms are displayed. Negative values cause all terms to be displayed; this is the default.

nodepth:

Removes any limit on depth of display (sets the relevant variable to a negative value).