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

sort = sorts
subsort = subsorts
var = vars

Command only synonyms:

advise = advisory = advisories
alias = aliases
attr = attribute
cmd = command
cond = condition
cont = continue
dsrew = dsrewrite
eqs = eq
erew = erewrite
flat = flattened
frew = frewrite
kinds = components
label = labels
mbs = mb
nar = narrow
paren = parens = parentheses
q = quit
rat = rational
red = reduce
rew = rewrite
rls  = rl = rule = rules
s.t. = such that
srew = srewrite
subst = substitution
sds = sd

Module only synonyms:

assoc = associative
ceq = cq
comm = commutative
config = configuration
ctor = constructor
ex = extending
id: = identity:
idem = idempotent
inc = including
iter = iterated
msg = message
obj = object
owise = otherwise
poly = polymorphic
prec = precedence
pr = protecting
strat = strategy       %%% reduction strategy attribute
strats = strat         %%% rewriting strategy declaration

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