Chapter 18
Complete List of Maude Commands

In this chapter we use curly bracket pairs, ‘{’ and ‘}’, to enclose optional syntax.

18.1 Command line flags

The following command line flags are supported.

Displays information on the usage of the Maude command and its line flags.

Displays the Maude version number.

Turns off mixfix printing; useful if Maude is being run by some other program that does not want to deal with the intricacies of mixfix parsing.

By default ANSI escape codes for color and other effects are disabled if the standard output is not a terminal or the TERM environment variable is set to dumb. These flags allow the default behavior to be overridden.

By default Tecla-based command line editing is disabled if the standard output is not a terminal or the TERM environment variable is set to dumb or emacs. These flags allow the default behavior to be overridden.

Causes Maude not to read in the standard prelude.

Disables control-C handling.

Pretends to be interactive, and enables control-C handling even though standard output is not a terminal.

Generates an XML log for selected commands in the given file.

Causes Maude not to show the welcome banner at start-up.

Specifies the natural number number in the range [0,2³² - 1] as the seed for the pseudo-random number generator random in module RANDOM (see Section 7.3). The default seed is 0.

Switches off advisories at start up.

Disables the automatic line wrapping of output.

18.2 Rewriting commands

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.

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.

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 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 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.

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.

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.

This command is used to initialize the read-eval-print loop in a module importing LOOP-MODE (see Section 13.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.

This command is used to input a list of identifiers to the loop in a module importing LOOP-MODE (see Section 13.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.

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.

18.3 Matching commands

Matching commands are used to directly invoke the rewriting engine’s term pattern matcher. They can be useful for figuring out exactly what subjects can be matched by a complex pattern.

Performs straightforward matching in the given module. This kind of matching is used by the engine for applying membership axioms. The result is a list of at most number matching substitutions such that the subject term matches the pattern and the substitution satisfies the optional condition (whose syntactic form is the same as the one of conditions for conditional equations and memberships; see Section 4.3). If the upper bound clause is omitted, infinity is assumed. For examples, see Section 4.9.

Works similarly to the previous command, except that it performs matching with extension for those theories that need it (those including the assoc or iter attributes). If the subject term (after theory normalization) has a symbol f from an extension theory on top, only a piece of the top theory layer with f on top need be matched. This kind of matching is used by the engine for applying equations and rules in order to accurately simulate equivalence class rewriting. The result is a list of all matches satisfying the given condition. If only part of the subject was matched, that part is given. For examples, see Sections 4.8 and 4.9.

18.4 Searching commands

Performs a breadth-first search for rewrite proofs starting at subject to a final state that matches pattern and satisfies an optional condition (whose syntactic form is the same as the one of conditions for conditional equations and memberships; see Section 4.3). Possible values for searchtype are

=>1	one step proof
=>+	one or more steps proof
=>*	zero or more steps proof
=>!	only canonical final states, that cannot be further rewritten,
	are allowed as solutions

The optional bound argument provides an upper bound in the number of solutions to be found; if it is omitted, infinity is assumed.

The optional depth argument indicates the maximum depth of the search. If it is omitted, infinity is assumed. It is also possible to give a depth bound without giving a bound on the number of solutions returned by requesting a search of the form search [,m] ....

The search type =>1 is an abbreviation of the search type =>+ with the depth bound set to 1.

As usual, if the in clause is omitted, the current module is assumed.

For examples, see Section 5.4.3.

Displays the search graph generated by the last search.

Displays the path to a given state, identified by the number, in a search graph.

Works like the command above, but only shows labels of applied rules instead of the full path.

18.5 Unification command

Computes a complete set of order-sorted unifiers modulo the (supported) equational axioms in the given module for the provided unification problem. If the cardinality of the set of unifiers is greater than the specified bound, the unifiers beyond that bound are omitted. The module can be any module or theory declared in the current Maude session; as usual, if the in clause is omitted, the current module is used.

For examples, see Section 12.4.

18.6 Tracing commands

Tracing produces detailed information about each rewrite performed and each conditional rewrite attempted. Since this typically results in an unmanageably huge volume of output, there are commands to control what is actually displayed.

These commands turn tracing on and off. If tracing is turned on, all trace information will be generated internally, even if none of it is displayed, thus considerably slowing the speed of interpretation.

Determines whether the evaluations of conditions are traced.

Determines whether the whole term is printed before and after a rewrite.

Determines whether the substitution is printed.

Determines whether membership axiom applications are printed.

Determines whether equation applications are printed.

Determines whether rule applications are printed.

Determines whether only trace information for selected operator symbols is printed (rather than all symbols).

Selects/deselects operator symbols and labels from the current module for tracing with the select option. Examples:

  trace select foo bar baz .  
  trace deselect baz .

Controls which modules are traced. Examples:

  trace exclude META-LEVEL .  
  trace include MY-MOD1 MY-MOD2 .

Determines whether the redex and its replacement are printed.

Determines whether the “start of rewrite” line (i.e., the one beginning with *’s) and the body of the equation/rule/membership being used are printed; if turned off, just the label and the substitution are printed. By setting both body and rewrite to off (see previous command), these options reduce a trace to a list of labels much like that produced by the show path labels number command.

Determines whether trace information for built-in operator symbols is printed.

18.7 Print attribute commands

In print attribute mode, when a statement is executed, the items in its print attribute are printed, with variables taking their value in the current substitution.

These commands turn print attribute mode on and off. It is off by default.

These commands determine whether a newline is printed following the items of a print attribute. By default a newline is printed (even if there are no items).

Note that print attribute mode is like trace mode, break mode, and profile mode in that in this mode all execution takes the slow path. This is true even if no print attributes are encountered.

18.8 Print option commands

Controls whether operators with mixfix syntax are printed in either mixfix or prefix form. User-defined syntax is supported for pretty-printing, even though it is not currently supported for parsing. It is sometimes advantageous to have uniform prefix notation for output; for example, if the output is going to be postprocessed by some other tool. Default is on.

If on, terms that are internally represented by graphs (currently, result terms together with terms being reduced and terms in substitutions during tracing) are printed as graph representations rather than as terms, together with the number of operator symbols in the full term. This can be useful in some pathological cases where the size of the term is exponential on the size of the graph. Default is off.

Controls whether arguments under operators with the associative attribute are printed in flattened form or not. Default is on.

If on, mixfix terms are printed with additional parentheses to make grouping explicit. Default is off.

Controls if variables aliases are used. Default is on.

Controls if special output convention for natural numbers is used. Default is on.

Controls if special output convention for rational numbers is used. Default is on.

Controls if reduction status coloring is used. Default is off.

Controls if format attributes are obeyed. Default is on.

Controls if argument hiding is used. Default is off.

Controls which operators have their arguments hidden.

18.9 Show option commands

Determines whether the number of rewrites is printed with the results of the reduce, rewrite, and continue commands in Section 18.2. Default is on.

As above but for loop mode.

Determines whether the cpu and real time used during rewriting is printed with the results of the reduce, rewrite, and continue commands in Section 18.2. Default is on.

As above but for loop mode.

Determines whether the full form of certain commands is printed before they are executed. Default is on.

Determines whether a breakdown of rewrites is dispayed. Default is off.

Determines which message is printed when a garbage collect is performed. Default is off.

Determines whether advisories are displayed. Default is on.

18.10 Show commands

Lists the names of all the modules that are currently in the module database maintained by the system.

Prints out a representation of the given module (or of the current module if none is given).

Prints out a flattened representation of the given module (or of the current module if none is given).

Prints out a representation of the sort and subsort information for the given module (or for the current module if none is given).

Lists the operators in the given module (or in the current module if none is given).

Lists the variables in the given module (or in the current module if none is given).

Lists the membership axioms in the given module (or in the current module if none is given).

Lists the equations in the given module (or in the current module if none is given).

Lists the rules in the given module (or in the current module if none is given).

Lists the connected components (kinds) of the poset of sorts for the given module (or for the current module if none is given).

Shows a summary of statistics for the context free grammar and term rewriting system generated for the given module (or for the current module if none is given).

Lists the names of all the views that are currently in the view database maintained by the system.

Prints out the given view (or of the last view entered into the system if none is given).

18.11 Profiler commands

Turns profiling on and off. Default is off.

Controls whether profile is clear before each command. Default is on.

Shows current profile for the given module (or in the current module if none is given). It shows both percentages and absolute rewrite counts.

18.12 Debugger commands

Controls whether break points are obeyed.

Selects/deselects operator symbols and labels from the current module for break points with the select option. Examples:

  break select foo bar baz .  
  break deselect baz .

Works just like the reduce command in Section 18.2, except that it drops into the debugger before executing the first rewrite.

Works just like the rewrite command in Section 18.2, except that it drops into the debugger before executing the first rewrite.

Works just like the frewrite command in Section 18.2, except that it drops into the debugger before executing the first rewrite.

Works just like the erewrite command in Section 18.2, except that it drops into the debugger before executing the first rewrite.

Only usable from the debugger. Exits the debugger and resumes the current rewriting activity.

Only usable from the debugger. Exits the debugger and abandons the current rewriting activity.

Only usable from the debugger. Performs a single step of the current rewriting activity with tracing switched on.

Only usable from the debugger. Prints the stack of pending rewrite tasks together with explanations of how they arose.

18.13 Miscellaneous commands

Causes the specified term to be parsed using the signature of the given module. If the in clause is omitted, the current module is assumed.

Selects a named module to be the current module. All commands that require a module refer to the current module, unless a module is explicitly given. The current module is usually the last module entered or used; for example, after the command show module AMODULE, the AMODULE module becomes the current module.

Adds or removes the named module from the set of modules that are automatically imported in protecting mode in every module.

Adds or removes the named module from the set of modules that are automatically imported in extending mode in every module.

Adds or removes the named module from the set of modules that are automatically imported in including mode in every module.

Controls display of extra information, depending on command. Default is off.

Controls whether the memoization tables are cleared before each command.

18.14 System level commands

These commands control system level activities. Unlike all the above commands they are not followed by a period.

Prints the path of the working directory.

Runs the UNIX ls command to list the files in the specified directories or working directory if none specified. The allowable flags depend on your local implementation of ls. Example:

  ls -lF /usr/bin/usr/local

Changes the working directory to directory-name.

Saves the current working directory on a stack and then changes the working directory to directory-name.

Changes the working directory to that which is on the top of the directory stack and pops the directory stack.

Causes a specified file to be included at this point. For files specified by a bare file name, it checks (with .maude, .fm, .obj extensions) if the filename is in one of these locations: (a) the current directory; (b) the directories in the MAUDE_LIB environment variable, and (c) the directory containing the executable. Otherwise, the full file name must be given, together with a full path name if the file is not in the current working directory. The in command may be nested, i.e., the included file may contain in commands. Example:

  in ../Examples/foo.maude

Notice that compilation of operator declarations and statements is done lazily, so that the module is not necessarily fully compiled when included. This implies that some warnings and advisories will only show up when a reduction actually takes place in the module. This also holds for a module that is entered by writing it in the prompt instead of a file.

Performs the same job as in but does not produce detailed output as modules are entered. Example:

  load ../Examples/foo.maude

Causes the interpreter to respond as if it had reached the end of file.

Causes the interpreter to exit.