A.1 Rewriting Commands

We use curly bracket pairs, { and } to enclose optional syntax.

reduce {in module :} term .

Causes the specified term to be reduced using the equations and membership axioms in the given module. reduce may be abbreviated to red. If the in clause is omitted the current module is assumed. Examples:

reduce 6 * 7 == 42 .
reduce in QID : conc('a, 'b) .

rewrite {[ number ]} {in module :} term .

Causes the specified term to be rewritten using the rules, equations and membership axioms in the given module. The default interpreter for rules applies rules using a top down (lazy) strategy and stops when the number of rule applications reaches the given bound. No rule will be applied if an equation can be applied. If the in clause is omitted the current module is assumed. If the upper bound clause is omitted, infinity is assumed. Examples:

rewrite 6 * 7 == 42 .
rewrite in FOO : f(6, g(a, b)) .
rewrite [50] f(6, g(a, b)) .
rewrite [1] in BAR : h(a) .

loop {in module :} term .

This command is used to initialize the read-eval-print loop in a module importing LOOP-MODE (see Section 2.8). The specified term is rewritten as far as possible using the rules, equations and membership axioms in the given module. If the result has a loop constructor symbol on the top then it becomes the current state of the loop; also, the list of quoted identifiers in the output position of the loop constructor is printed as a sequence of identifiers.

( identifier* )

This command is used to input a list of identifiers to the loop in a module importing LOOP-MODE. If the current module has not changed since the last rewriting command, the result of previous rewrites has a loop constructor symbol on the top, and the last rewriting command was not reduce then:

1. the sequence of identifiers in the parentheses are converted into a list of quoted identifiers and are placed under the input position of the loop constructor;
2. a nil list of quoted identifiers is placed under the output position of the loop constructor;
3. the new term is rewritten as far as possible using the rules, equations and membership axioms in the module to which the term belongs; and
4. if the new result has a loop constructor symbol on the top, this list of quoted identifiers in the output position of the loop constructor is printed as a sequence of identifiers.

continue {number} .

Attempts to continue rewriting the result of the last rewriting command using the rules, equations and membership axioms, stopping if the upper bound on the number of rule applications is reached. This command is only usable if the current module has not changed since the last rewriting command, and the last rewriting command was not reduce. If no upper bound clause is given, infinity is assumed.