Rewriting commands

reduce $\lbrace$in module :$\rbrace$ 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. For examples, see Section 4.9.

rewrite $\lbrace$[ bound ]$\rbrace$ $\lbrace$in module :$\rbrace$ 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 them using a rule-fair 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. rewrite may be abbreviated to rew. For examples, see Section 5.4.1.

frewrite $\lbrace$[ bound $\lbrace$,number$\rbrace$ ]$\rbrace$ $\lbrace$in module :$\rbrace$ term .

Like the previous command, causes the specified term to be rewritten using the rules, equations, and membership axioms in the given module. But now the default interpreter for rules applies them using a rule- and position-fair strategy and stops when the number of rule applications reaches the given bound. This strategy causes multiple passes over the term, with at most number rule rewrites taking place at each position. If the in clause is omitted, the current module is assumed. If the upper bound clause is omitted, infinity is assumed. If the number of rewrites per position is omitted, 1 is assumed. frewrite may be abbreviated to frew. For examples, see Section 5.4.2.

Unlike rewrite, which uses a leftmost outermost strategy for applying rules and reduces the whole term with equations after each successful rule rewrite, frewrite attempts to be position fair by making a number of depth-first traversals of the term. On each traversal, each position that existed at the start of the traversal is entitled to at most $\mathit{number}$ rule rewrites when its turn comes around. After a rule rewrite succeeds, only the subterm that was rewritten is reduced with equations in order to avoid destroying positions that have not yet had their turn for the current traversal. Traversals are made until $\mathit{bound}$ rule rewrites have been made, or until no more rewrites are possible. When operators have the assoc or iter attributes, term depth and positions are relative to the flattened or compact form of the term, respectively. Thus, fair rewriting treats a whole stack of an iter operator as a single position for the purposes of position fairness.

The are a couple of caveats with frewrite:

• If position-fair rewriting stops in mid traversal, then the sort of the (incompletely reduced) result has not yet been calculated and is printed as (sort not calculated).
• Position-fair rewriting is not substitution fair; this is particularly apparent if you have a multiset of messages and objects, as in Section 8.2.

erewrite $\lbrace$[ bound $\lbrace$,number$\rbrace$ ]$\rbrace$ $\lbrace$in module :$\rbrace$ term .

Works like the frewrite command and in addition it allows messages to be exchanged with external objects that do not reside in the configuration. It is abbreviated to erew.

continue $\lbrace$number$\rbrace$ .

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. In the case where the last rewriting command was frewrite, the number given to the continue command increases the bound on the number of traversals, leaving the number of rewrites per position unchanged. In particular, considerable extra information about the current traversal is saved by the frewrite command so that, for example,

  frewrite [n, k] t .
  continue m .

produces the same final answer as

  frewrite [s, k] t .

when s = n + m. For an erewrite command, the same state information is preserved as for frewrite, but in this case nothing can be guaranteed, due to the interaction with the external environment.

loop $\lbrace$in module :$\rbrace$ term .

This command is used to initialize the read-eval-print loop in a module importing LOOP-MODE (see Section 12.1). 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 at 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 (see Section 12.1). If the current module has not changed since the last rewriting command, the result of previous rewrites has a loop constructor symbol at the top, and the last rewriting command was not reduce then:

1. the sequence of identifiers in the parentheses is converted into a list of quoted identifiers and is 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 at the top, the list of quoted identifiers in the output position of the loop constructor is printed as a sequence of identifiers.

set clear rules on . / set clear rules off .

Normally, each rewrite or frewrite command and each loop mode invocation resets the rule state for each symbol. For most symbols the rule state consists of the next rule to be executed in a round-robin scheme but for counter symbols the rule state consists of the next number to rewrite to. Setting clear rules to off means the rule state will not be reset between commands.