B The Grammar of Core Maude

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