Chapter 24
Core Maude Grammar

This chapter describes the syntax of Maude using the following extended BNF notation: the symbols ‘’ and ‘’ are used as metaparentheses; the symbol ‘∣’ is used to separate alternatives; square bracket pairs, ‘[’ and ‘]’, enclose optional syntax; ‘*’ indicates zero or more repetitions of preceding unit; ‘+’ indicates one or more repetitions of preceding unit; and the string “x” denotes x literally. As an application of this notation, A, A* indicates a non-empty list of A’s separated by commas. Finally, %%% indicates comments in the syntactic description, as opposed to comments in the Maude code.

24.1 The grammar

⟨MaudeTop⟩ ::=
     ⟨SystemCommand⟩ ∣ ⟨Command⟩ ∣ ⟨DebuggerCommand⟩ ∣
       ⟨Module⟩ ∣ ⟨Theory⟩ ∣ ⟨View⟩ +

⟨SystemCommand⟩ ::= in ⟨FileName⟩ ∣ load ⟨FileName⟩ ∣ sload ⟨FileName⟩ ∣
    quit ∣ eof ∣ popd ∣ pwd ∣
    cd ⟨Directory⟩ ∣ push ⟨Directory⟩ ∣
    ls [ ⟨LsFlag⟩ ] [ ⟨Directory⟩ ]

⟨Command⟩ ::= select ⟨ModId⟩ . ∣
    parse [ in ⟨ModId⟩ : ] ⟨Term⟩ . ∣
    [ debug ] reduce [ in ⟨ModId⟩ : ] ⟨Term⟩ . ∣
    [ debug ] rewrite [ [ ⟨Nat⟩ ] ] [ in ⟨ModId⟩ : ] ⟨Term⟩ . ∣
    [ debug ] frewrite [ ⟨DoubleBound⟩ ] [ in ⟨ModId⟩ :
        ] ⟨Term⟩ . ∣
    [ debug ] erewrite [ ⟨DoubleBound⟩ ] [ in ⟨ModId⟩ : ]
        ⟨Term⟩ . ∣
    [ debug ]  srewrite ∣ dsrewrite  [ [ ⟨Nat⟩ ] ] [ in ⟨ModId⟩ : ]
        ⟨Term⟩ using ⟨Strat⟩ . ∣
    check [ in ⟨ModId⟩ : ] ⟨Term⟩ . ∣
     match ∣ xmatch  [ [ ⟨Nat⟩ ] ] [ in ⟨ModId⟩ : ]
        ⟨Term⟩ <=? ⟨Term⟩ [ such that ⟨Condition⟩ ] . ∣
    unify [ [ ⟨Nat⟩ ] ] [ in ⟨ModId⟩ : ]
        ⟨UnificationEquation⟩   /\ ⟨UnificationEquation⟩ * . ∣
    [ debug ] variant unify [ [ ⟨Nat⟩ ] ] [ in ⟨ModId⟩ : ]
        ⟨UnificationEquation⟩   /\ ⟨UnificationEquation⟩ * . ∣
    [ debug ] get [ irredundant ] variants [ [ ⟨Nat⟩ ] ] [ in ⟨ModId⟩ : ] ⟨Term⟩ . ∣
     search ∣ vu-narrow  [ ⟨DoubleBound⟩ ] [ in ⟨ModId⟩ : ]
        ⟨Term⟩ ⟨SearchType⟩ ⟨Term⟩ [ such that ⟨Condition⟩ ] . ∣
    [ debug ] continue ⟨Nat⟩ . ∣
    loop [ in ⟨ModId⟩ : ] ⟨Term⟩ . ∣
    ( ⟨TokenString⟩ ) ∣
    trace  select ∣ deselect ∣ include ∣ exclude 
         ⟨OpId⟩ ∣ ( ⟨OpForm⟩ ) + . ∣
    print  conceal ∣ reveal   ⟨OpId⟩ ∣ ( ⟨OpForm⟩ ) + . ∣
    break  select ∣ deselect   ⟨OpId⟩ ∣ ( ⟨OpForm⟩ ) + . ∣
    show ⟨ShowItem⟩ [ ⟨ModId⟩ ] . ∣
    show view [ ⟨ViewId⟩ ] . ∣
    show modules . ∣
    show views . ∣
    show search graph . ∣
    show path [ labels ] ⟨Nat⟩ .
    do clear memo . ∣
    set ⟨SetOption⟩  on ∣ off  .

⟨DoubleBound⟩ ::= [ ⟨Nat⟩ [ , ⟨Nat⟩ ] ] ∣ [ , ⟨Nat⟩ ]

⟨SearchType⟩ ::= =>1 ∣ =>+ ∣ =>* ∣ =>!

⟨UnificationEquation⟩ ::= ⟨Term⟩ =? ⟨Term⟩

⟨ShowItem⟩ ::= module ∣ all ∣ sorts ∣ ops ∣ vars ∣ mbs ∣
    eqs ∣ rls ∣ strats ∣ sds ∣ summary ∣ kinds ∣ profile

⟨SetOption⟩ ::= show ⟨ShowOption⟩ ∣
    print ⟨PrintOption⟩ ∣
    trace [ ⟨TraceOption⟩ ] ∣
    break ∣ verbose ∣ profile ∣
    clear  memo ∣ rules ∣ profile  ∣
    protect ⟨ModId⟩ ∣
    extend ⟨ModId⟩ ∣
    include ⟨ModId⟩

⟨ShowOption⟩ ::= advise ∣ stats ∣ loop stats ∣ timing ∣
    loop timing ∣ breakdown ∣ command ∣ gc

⟨PrintOption⟩ ::= mixfix ∣ flat ∣ with parentheses ∣
    with aliases ∣ conceal ∣ number ∣ rat ∣ color ∣
    format ∣ graph ∣ attribute ∣ attribute newline ∣
    constants with sorts

⟨TraceOption⟩ ::= condition ∣ whole ∣ substitution ∣ select ∣
    mbs ∣ eqs ∣ rls ∣ sds ∣ rewrite ∣ body

⟨DebuggerCommand⟩ ::= resume . ∣ abort . ∣ step . ∣ where .

⟨Module⟩ ::= fmod ⟨ModId⟩ [ ⟨ParameterList⟩ ] is ⟨ModElt⟩* endfm ∣
    mod ⟨ModId⟩ [ ⟨ParameterList⟩ ] is ⟨ModElt’⟩* endm ∣
    smod ⟨ModId⟩ [ ⟨ParameterList⟩ ] is ⟨SmodElt⟩* endsm

⟨Theory⟩ ::= fth ⟨ModId⟩ is ⟨ModElt⟩* endfth ∣
    th ⟨ModId⟩ is ⟨ModElt’⟩* endth ∣
    sth ⟨ModId⟩ is ⟨SmodElt⟩* endsth

⟨View⟩ ::= view ⟨ViewId⟩ [ ⟨ParameterList⟩ ] from ⟨ModExp⟩ to ⟨ModExp⟩ is
             ⟨ViewElt⟩*
           endv

⟨ParameterList⟩ ::= { ⟨ParameterDecl⟩  , ⟨ParameterDecl⟩ * }

⟨ParameterDecl⟩ ::= ⟨ParameterId⟩ :: ⟨ModExp⟩

⟨ModElt⟩ ::= including ⟨ModExp⟩ . ∣
    extending ⟨ModExp⟩ . ∣
    protecting ⟨ModExp⟩ . ∣
    sorts ⟨Sort⟩+ . ∣
    subsorts ⟨Sort⟩+  < ⟨Sort⟩+ + . ∣
    op ⟨OpForm⟩ : ⟨Type⟩* ⟨Arrow⟩ ⟨Type⟩ [ ⟨Attr⟩ ] . ∣
    ops  ⟨OpId⟩ ∣ ( ⟨OpForm⟩ ) + : ⟨Type⟩* ⟨Arrow⟩ ⟨Type⟩
           [ ⟨Attr⟩ ] . ∣
    vars ⟨VarId⟩+ : ⟨Type⟩ . ∣
    ⟨Statement⟩ [ ⟨StatementAttr⟩ ] .

⟨ViewElt⟩ ::= var ⟨varId⟩+ : ⟨Type⟩ . ∣
    sort ⟨Sort⟩ to ⟨Sort⟩ . ∣
    label ⟨LabelId⟩ to ⟨LabelId⟩ . ∣
    op ⟨OpForm⟩ to ⟨OpForm⟩ .  ∣
    op ⟨OpForm⟩ : ⟨Type⟩* ⟨Arrow⟩ ⟨Type⟩ to ⟨OpForm⟩ . ∣
    op ⟨Term⟩ to term ⟨Term⟩ . ∣
    strat ⟨StratId⟩ to ⟨StratId⟩ . ∣
    strat ⟨StratId⟩ [ : ⟨Type⟩* ] @ ⟨Type⟩ to ⟨StratId⟩ . ∣
    strat ⟨StratCall⟩ to expr ⟨Strat⟩ .

⟨ModExp⟩ ::= ⟨ModId⟩ ∣
    ( ⟨ModExp⟩ ) ∣
    ⟨ModExp⟩ + ⟨ModExp⟩ ∣
    ⟨ModExp⟩ * ⟨Renaming⟩
    ⟨ModExp⟩ { ⟨ViewId⟩  , ⟨ViewId⟩ * }

⟨Renaming⟩ ::= ( ⟨RenamingItem⟩  , ⟨RenamingItem⟩ * )

⟨RenamingItem⟩ ::= sort ⟨Sort⟩ to ⟨Sort⟩ ∣
    label ⟨LabelId⟩ to ⟨LabelId⟩ ∣
    op ⟨OpForm⟩ ⟨ToPartRenamingItem⟩ ∣
    op ⟨OpForm⟩ : ⟨Type⟩* ⟨Arrow⟩ ⟨Type⟩ ⟨ToPartRenamingItem⟩
    strat ⟨StratId⟩ to ⟨StratId⟩ ∣
    strat ⟨StratId⟩ [ : ⟨Type⟩* ] @ ⟨Type⟩ to ⟨StratId⟩ ∣

⟨ToPartRenamingItem⟩ ::= to ⟨OpForm⟩ [ ⟨Attr⟩ ]

⟨Arrow⟩ ::= -> ∣ ~>

⟨Type⟩ ::= ⟨Sort⟩ ∣ ⟨Kind⟩

⟨Kind⟩ ::= [ ⟨Sort⟩ , ⟨Sort⟩ * ]

⟨Sort⟩ ::= ⟨SortId⟩ ∣ ⟨Sort⟩ { ⟨Sort⟩  , ⟨Sort⟩ * }

⟨ModElt’⟩ ::= ⟨ModElt⟩ ∣
    ⟨Statement’⟩ [ ⟨StatementAttr⟩ ] .

⟨SmodElt⟩ ::= including ⟨ModExp⟩ . ∣
    extending ⟨ModExp⟩ . ∣
    protecting ⟨ModExp⟩ . ∣
    vars ⟨VarId⟩+ : ⟨Type⟩ . ∣
    strats ⟨StratId⟩+ [ : ⟨Type⟩* ] @ ⟨Type⟩ [ ⟨StratAttr⟩ ] .
    ⟨StratStatement⟩ [ ⟨StatementAttr⟩ ] .

⟨Statement⟩  ::=  mb [ ⟨Label⟩ ] ⟨Term⟩ : ⟨Sort⟩ ∣
    cmb [ ⟨Label⟩ ] ⟨Term⟩ : ⟨Sort⟩ if ⟨Condition⟩ ∣
    eq [ ⟨Label⟩ ] ⟨Term⟩ = ⟨Term⟩ ∣
    ceq [ ⟨Label⟩ ] ⟨Term⟩ = ⟨Term⟩ if ⟨Condition⟩

⟨Statement’⟩ ::= rl [ ⟨Label⟩ ] ⟨Term⟩ => ⟨Term⟩ ∣
    crl [ ⟨Label⟩ ] ⟨Term⟩ => ⟨Term⟩ if ⟨Condition’⟩

⟨StratStatement⟩ ::= sd ⟨StratCall⟩ := ⟨Strat⟩ ∣
    csd ⟨StratCall⟩ := ⟨Strat⟩ if ⟨Condition⟩

⟨Label⟩ ::= [ ⟨LabelId⟩ ] :

⟨Condition⟩ ::= ⟨ConditionFragment⟩  /\ ⟨ConditionFragment⟩ *

⟨Condition’⟩ ::= ⟨ConditionFragment’⟩
                  /\ ⟨ConditionFragment’⟩ *

⟨ConditionFragment⟩ ::= ⟨Term⟩ = ⟨Term⟩ ∣ ⟨Term⟩ := ⟨Term⟩
                        ∣ ⟨Term⟩ : ⟨Sort⟩

⟨ConditionFragment’⟩ ::= ⟨ConditionFragment⟩ ∣ ⟨Term⟩ => ⟨Term⟩

⟨Attr⟩ ::=
    [  assoc ∣ comm ∣
        [ left ∣ right ] id: ⟨Term⟩ ∣
        idem ∣ iter ∣ memo ∣ ditto ∣
        config ∣ obj ∣ msg ∣ ctor ∣
        metadata ⟨StringId⟩
        strat ( ⟨Nat⟩+ ) ∣
        poly ( ⟨Nat⟩+ ) ∣
        frozen [ ( ⟨Nat⟩+ ) ] ∣
        prec ⟨Nat⟩ ∣
        gather (  e ∣ E ∣ & + ) ∣
        format ( ⟨Token⟩+ ) ∣
        special ( ⟨Hook⟩+ ) + ]

⟨StratAttr⟩ ::= [ metadata ⟨StringId⟩ ]

⟨StatementAttr⟩ ::=
    [  nonexec ∣
        metadata ⟨StringId⟩ ∣
        label ⟨LabelId⟩  ∣
        print ⟨PrintItem⟩* + ]

⟨StatementAttrEq⟩ ::=
    [  ⟨StatementAttr⟩ ∣ otherwise ∣ variant + ]

⟨StatementAttrRl⟩ ::=
    [  ⟨StatementAttr⟩ ∣ narrowing + ]

⟨PrintItem⟩ ::= ⟨StringId⟩ ∣ ⟨VarId⟩ ∣ ⟨VarAndSortId⟩

⟨Hook⟩ ::= id-hook ⟨Token⟩ [ ( ⟨TokenString⟩ ) ] ∣
     op-hook ∣ term-hook  ⟨Token⟩ ( ⟨TokenString⟩ )

⟨Strat⟩ ::= idle ∣ fail ∣
    ⟨RuleApp⟩ ∣ top( ⟨RuleApp⟩ ) ∣
    ⟨Strat⟩ ? ⟨Strat⟩ : ⟨Strat⟩ ∣
    ⟨TestVariant⟩ ⟨Term⟩ [ such that ⟨Condition⟩ ]
    ⟨Strat⟩ ; ⟨Strat⟩ ∣
    ⟨Strat⟩ | ⟨Strat⟩ ∣
    ⟨Strat⟩ * ∣
    ⟨MrewVariant⟩ ⟨Term⟩ [ such that ⟨Condition⟩ ] by ⟨VarStratList⟩
    ⟨StratCall⟩
    ⟨Strat⟩ +
    ⟨Strat⟩ or-else ⟨Strat⟩
    not( ⟨Strat⟩ )
    ⟨Strat⟩ !
    try( ⟨Strat⟩ )
    test( ⟨Strat⟩ )

⟨RuleApp⟩ ::= ⟨LabelId⟩ [ [ ⟨Substitution⟩ ] ] [ { ⟨Strat⟩ (, ⟨Strat⟩)* } ]

⟨Substitution⟩ ::= ⟨VarId⟩ <- ⟨Term⟩ ∣
    ⟨Substitution⟩ , ⟨Substitution⟩

⟨StratCall⟩ ::= ⟨StratId⟩ [ () ] ∣
    ⟨StratId⟩ ( ⟨Term⟩ (, ⟨Term⟩)* )

⟨VarStratList⟩ ::= ⟨VarId⟩ using ⟨Strat⟩ ∣
    ⟨VarStratList⟩ , ⟨VarStratList⟩

⟨TestVariant⟩ ::= match ∣ xmatch ∣ amatch

⟨MrewVariant⟩ ::= matchrew ∣ xmatchrew ∣ amatchrew

⟨FileName⟩    %%% OS dependent
⟨Directory⟩   %%% OS dependent
⟨LsFlag⟩      %%% OS dependent

⟨StringId⟩    %%% characters enclosed in double quotes "..."
⟨ModId⟩       %%% simple identifier, by convention all capitals
⟨ViewId⟩      %%% simple identifier, by convention capitalized
⟨ParameterId⟩ %%% simple identifier, by convention single capital
⟨SortId⟩      %%% simple identifier, by convention capitalized
⟨VarId⟩       %%% simple identifier, by convention capitalized
⟨VarAndSortId⟩ %%% an identifier consisting of a variable name
                   followed by a colon followed by a sort name
⟨OpId⟩        %%% identifier possibly with underscores
⟨OpForm⟩ ::= ⟨OpId⟩ ∣ ( ⟨OpForm⟩ ) ∣ ⟨OpForm⟩+
⟨Nat⟩         %%% a natural number
⟨Term⟩ ::= ⟨Token⟩ ∣ ( ⟨Term⟩ ) ∣ ⟨Term⟩+
⟨Token⟩       %%% sequence of printable ASCII characters delimited by
                  whitespace. The symbols (, ), [, ], {, } and comma form
                  separate tokens themselves, unless backquoted
⟨TokenString⟩ ::= ⟨Token⟩ ∣ ( ⟨TokenString⟩ ) ∣ ⟨TokenString⟩*
⟨LabelId⟩     %%% simple identifier
⟨StratId⟩     %%% simple identifier

In parsing module expressions, instantiation has higher precedence than renaming, which in turn has higher precedence than summation.

24.2 Synonyms

Command only synonyms:

Module only synonyms:

24.3 Lexical Issues

Tokens are sequences of printable ASCII characters delimited by white space, except that ‘(’, ‘)’, ‘[’, ‘]’, ‘{’, ‘}’, and ‘,’ are always considered as single character tokens, unless backquoted.

Single line comments are started by one of *** or ---, and ended by the end of line. Multiline comments are started by ***( and ended by ). Parentheses (whether backquoted or not) must balance within multiline comments.

String identifiers use C backslash conventions [86, Section A2.5.2].