This appendix describes the syntax of Maude using the following extended BNF
notation: the symbols `{' and `}' are used as meta-parentheses; the
symbol `|' is used to separate alternatives; square bracket pairs,
`[' and `]' enclose optional syntax; `*' indicate zero or
more repetitions of preceding unit; `+' indicate one or more repetitions
of preceding unit; and "x" denotes x literally. As an
application of this notation, A{, A}... indicates a
nonempty list of A's separated by commas. Finally, %%%
indicates
comments in the syntactic description, as opposed to comments in the Maude
code.
<MaudeTop> ::= { <SystemCommand> | <Command> | <DebuggerCommand> | <Module> }+ <SystemCommand> ::= in <FileName> | quit | eof | popd | pwd | cd <Directory> | push <Directory> | ls [ <LsFlag> ] [ <Directory> ] | <Command> ::= select <ModId> . | parse [ in <ModId> : ] <Term> . | reduce [ in <ModId> : ] <Term> . | rewrite [ [ <Nat> ] ] [ in <ModId> : ] <Term> . | { match | xmatch } [ [ <Nat> ] ] [ in <ModId> : ] <Term> <=? <Term> . | continue <Nat> . | loop [ in <ModId> : ] <Term> . | ( <TokenString> ) | trace { select | deselect } { <OpId> | ( <OpForm> ) }+ . | show <ShowItem> [ <ModId> ] . | set <SetOption> { on | off } . <ShowItem> ::= module | all | sorts | ops | vars | mbs | eqs | rls | summary | components <SetOption> ::= show <ShowOption> | print <PrintOption> | trace [ <TraceOption> ] | include <ModId> <ShowOption> ::= stats | timing | command | gc <PrintOption> ::= mixfix | flat | with parentheses | graph <TraceOption> ::= condition | whole | substitution | select | mbs | eqs | rls <DebuggerCommand> ::= debug reduce [ in <ModId> : ] <Term> . | debug rewrite [ [ <Nat> ] ] [ in <ModId> : ] <Term> . | debug continue <Nat> . | resume . | abort . | step . | where . <Module> ::= fmod <ModId> is <ModElt>* endfm | mod <ModId> is <ModElt'>* endfm | <ModElt> ::= including <ModId> . | sorts <SortId>+ . | subsort <SortId>+ { < <SortId>+ }+ . | op <OpForm> : <SortId>* -> <SortId> [ <Attr> ] . | ops { <OpId> | ( <OpForm> ) }+ : <SortId>* -> <SortId> [ <Attr> ] . | var <VarId>+ : <SortId> . | mb <Term> : <SortId> . | cmb <Term> : <SortId> if <Condition> . | eq <Term> = <Term> . | ceq <Term> = <Term> if <Condition> . <ModElt'> ::= <ModElt> | rl [ [ <LabelId> ] : ] <Term> => <Term> . | crl [ [ <LabelId> ] : ] <Term> => <Term> if <Condition> . <Condition> ::= <Term> = <Term> | <Term> <Attr> ::= [ { assoc | comm | [ left | right ] id: <Term> | idem | memo | strat ( <Nat>+ ) | prec Nat | gather ( { e | E | & }+ ) | special ( <Hook>+ ) }+ ] <Hook> ::= id-hook <Token> [ ( <TokenString> ) ] | { op-hook | term-hook } ( <TokenString> ) <FileName> %%% OS dependent <Directory> %%% OS dependent <LsFlag> %%% OS dependent <ModId> %%% simple identifier, by convention all caps <SortId> %%% simple identifier, by convention capitalized <VarId> %%% simple identifier, by convention capitalized <OpId> %%% identifier possibly with underscores <OpForm> ::= <OpId> | ( <OpForm> ) | <OpForm>+ <Nat> %%% a natural number <Term> ::= <Token> | ( <Term> ) | <Term>+ <Token> %%% Any symbol other than ( or ) <TokenString> ::= <Token> | ( <TokenString> ) | <TokenString>* <LabelId> %%% simple identifier