In this chapter we use curly bracket pairs, ‘{’ and ‘}’, to enclose optional syntax.
The following command line flags are supported.
Displays information on the usage of the Maude command and its line flags.
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.
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.
Specifies the natural number number in the range [0,232 − 1] as the seed for the pseudo-random number generator random in module RANDOM (see Section 7.3). The default seed is 0.
Causes the output of the print attribute to be set to stderr rather than stdout.
Causes Maude to use external object rewriting for loop mode.
Set the depth bound multiplier for associative unification. The default multiplier is 1.
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,
produces the same final answer as 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 18.4). 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 18.4). 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:
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.
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.
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 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.
Causes the specified term to be rewritten according to the given strategy in the given module. The command performs an exhaustive fair search for all the strategy solutions, unless the optional bound on the number of solutions is specified. If the in clause is omitted, the current module is assumed. srewrite may be abbreviated to srew.
For examples, see Section 10.1.
Like the previous command, but solutions are searched depth-first. dsrewite may be abbreviated to dsrew.
For more details, see Section 10.4.
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. If the keyword irredundant is used, a minimal set of unifiers is returned.
For examples, see Section 13.4.
Computes a complete set of order-sorted unifiers modulo the equations declared with the variant attribute (which must satisfy the finite variant property) plus the (supported) equational axioms in the given module for the provided unification problem. It may be necessary to satisfy an optional irreducibility condition on extra terms term”1, …, term”n. 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. If the keyword filtered is used, a minimal set of unifiers is returned.
For more details, see Section 14.9.
Computes a complete set of order-sorted matches modulo the equations declared with the variant attribute (which must satisfy the finite variant property) plus the (supported) equational axioms in the given module for the provided matching problem. It may be necessary to satisfy an optional irreducibility condition on extra terms term”1, …, term”n. If the cardinality of the set of matchers is greater than the specified bound, the matchers 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 more details, see Section 14.13.
Compute incrementally a set of most general variants of the given term in the (supported) equational theory of the given module, where the equations of interest must be declared with the variant attribute. The keyword irredundant is useful for theories that do have the finite variant property, since it will provide the set of most general variants of the given term. If the cardinality of the set of variants is greater than the specified bound, the variants beyond that bound are omitted. It may be necessary to satisfy an optional irreducibility condition on extra terms term”1, …, term”n. 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 and more details, see Section 14.4.
Performs a breadth-first narrowing search using variant-based unification starting at an initial state pattern1 (a term with variables) to a final state (a term with variables, possibly shared with the initial term) that unifies pattern2. If {fold} is added at the beginning, a folding narrowing search is used instead. Possible values for searchtype are (but their meaning differ from that of the search command of Section 5.4.3)
| =>1 | one step proof |
| =>+ | one or more steps proof |
| =>* | zero or more steps proof |
| =>! | only canonical final states, that cannot be further narrowed, |
| 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 vu-narrow [,m] ....
The search type =>1 is an abbreviation of the search type =>+ with the depth bound set to 1.
The optional variantopts is a comma-separated list of at least one of the options filter and delay for variant unification (see Section 15.6.1).
As usual, if the in clause is omitted, the current module is assumed.
For examples, see Section 15.6.
Performs a breadth-first folding narrowing search. It is a synonym of {fold} vu-narrow.
Cause the connected SMT solver to be queried with the specified term, containing only constants and operator from the smt.maude signatures. If the in clause is omitted, the current module is assumed.
For examples and more details, see Section 16.
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. Regarding strategy definitions, it determines whether the subject term is printed in each trace.
Determines whether membership axiom applications are printed.
Determines whether strategy definition 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:
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/strategy defintion 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.
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.
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 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 whether constants c of sort s are printed as (c).s even if desambiguation is not strictly needed. With on, all constants are qualified, even if not strictly necessary; with off, only constants that require desambiguation are qualified. Default is off.
Determines whether the number of rewrites is printed with the results of the reduce, rewrite, and continue commands in Section 23.2. Default is on.
Determines whether the cpu and real time used during rewriting is printed with the results of the reduce, rewrite, and continue commands in Section 23.2. Default is on.
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.
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 desugared 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 strategies in the given module (or in the current module if none is given).
Lists the strategy definitions 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).
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.
Selects/deselects operator symbols and labels from the current module for break points with the select option. Examples:
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.
Moreover, any command that involves the execution of rewriting or narrowing steps can be prefixed by the debug word to drop into the debugger before the first step takes place. These commands are reduce, rewrite, frewrite, erewrite, continue (in Section 23.2 ), search (in Section 23.4), srewrite, dsrewrite (in Section 23.5), variant unify, variant match, get variants, vu-narrow and fvu-narrow (in Section 23.6).
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.
Clear the memoization tables of the given module (or of the current module if none is given).
These commands control system level activities. Unlike all the above commands they are not followed by a period.
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:
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:
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:
Performs the same job as load but loads the named file only if it has changed (determined by the file system’s modify time) since it was last read (via in, load, sload or command line argument).1 Example:
Causes the interpreter to respond as if it had reached the end of file.