The grammar

$\langle$MaudeTop$\rangle$ ::=
    $\left(\right.$ $\langle$SystemCommand$\rangle$ $\mid$ $\langle$Command$\rangle$ $\mid$ $\langle$DebuggerCommand$\rangle$ $\mid$
       $\langle$Module$\rangle$ $\mid$ $\langle$Theory$\rangle$ $\mid$ $\langle$View$\rangle$ $\left.\right)$$+$

$\langle$SystemCommand$\rangle$ ::= in $\langle$FileName$\rangle$ $\mid$ load $\langle$FileName$\rangle$ $\mid$
    quit $\mid$ eof $\mid$ popd $\mid$ pwd $\mid$
    cd $\langle$Directory$\rangle$ $\mid$ push $\langle$Directory$\rangle$ $\mid$
    ls $[$ $\langle$LsFlag$\rangle$ $]$ $[$ $\langle$Directory$\rangle$ $]$

$\langle$Command$\rangle$ ::= select $\langle$ModId$\rangle$ . $\mid$
    parse $[$ in $\langle$ModId$\rangle$ : $]$ $\langle$Term$\rangle$ . $\mid$
    $[$ debug $]$ reduce $[$ in $\langle$ModId$\rangle$ : $]$ $\langle$Term$\rangle$ . $\mid$
    $[$ debug $]$ rewrite $[$ [ $\langle$Nat$\rangle$ ] $]$ $[$ in $\langle$ModId$\rangle$ : $]$ $\langle$Term$\rangle$ . $\mid$
    $[$ debug $]$ frewrite $[$ [ $\langle$Nat$\rangle$ $[$ , $\langle$Nat$\rangle$ $]$ ] $]$ $[$ in $\langle$ModId$\rangle$ :
        $]$ $\langle$Term$\rangle$ . $\mid$
    $[$ debug $]$ erewrite $[$ [ $\langle$Nat$\rangle$ $[$ , $\langle$Nat$\rangle$ $]$ ] $]$ $[$ in $\langle$ModId$\rangle$ : $]$  
        $\langle$Term$\rangle$ . $\mid$
    $\left(\right.$ match $\mid$ xmatch $\left.\right)$ $[$ [ $\langle$Nat$\rangle$ ] $]$ $[$ in $\langle$ModId$\rangle$ : $]$
        $\langle$Term$\rangle$ <=? $\langle$Term$\rangle$ $[$ such that $\langle$Condition$\rangle$ $]$ . $\mid$
    search $[$ [ $\langle$Nat$\rangle$ ] $]$ $[$ in $\langle$ModId$\rangle$ : $]$
        $\langle$Term$\rangle$ $\langle$SearchType$\rangle$ $\langle$Term$\rangle$ $[$ such that $\langle$Condition$\rangle$ $]$ . $\mid$
    continue $\langle$Nat$\rangle$ . $\mid$
    loop $[$ in $\langle$ModId$\rangle$ : $]$ $\langle$Term$\rangle$ . $\mid$
    ( $\langle$TokenString$\rangle$ ) $\mid$
    trace $\left(\right.$ select $\mid$ deselect $\mid$ include $\mid$ exclude $\left.\right)$
        $\left(\right.$ $\langle$OpId$\rangle$ $\mid$ ( $\langle$OpForm$\rangle$ ) $\left.\right)$$+$ . $\mid$
    print $\left(\right.$ conceal $\mid$ reveal $\left.\right)$ $\left(\right.$ $\langle$OpId$\rangle$ $\mid$ ( $\langle$OpForm$\rangle$ ) $\left.\right)$$+$ . $\mid$
    break $\left(\right.$ select $\mid$ deselect $\left.\right)$ $\left(\right.$ $\langle$OpId$\rangle$ $\mid$ ( $\langle$OpForm$\rangle$ ) $\left.\right)$$+$ . $\mid$
    show $\langle$ShowItem$\rangle$ $[$ $\langle$ModId$\rangle$ $]$ . $\mid$
    show view $[$ $\langle$ViewId$\rangle$ $]$ . $\mid$
    show modules . $\mid$
    show views . $\mid$
    show search graph . $\mid$
    show path $[$ labels $]$ $\langle$Nat$\rangle$ .
    do clear memo . $\mid$
    set $\langle$SetOption$\rangle$ $\left(\right.$ on $\mid$ off $\left.\right)$ .

$\langle$ShowItem$\rangle$ ::= module $\mid$ all $\mid$ sorts $\mid$ ops $\mid$ vars $\mid$ mbs $\mid$
    eqs $\mid$ rls $\mid$ summary $\mid$ kinds $\mid$ profile

$\langle$SetOption$\rangle$ ::= show $\langle$ShowOption$\rangle$ $\mid$
    print $\langle$PrintOption$\rangle$ $\mid$
    trace $[$ $\langle$TraceOption$\rangle$ $]$ $\mid$
    break $\mid$ verbose $\mid$ profile $\mid$
    clear $\left(\right.$ memo $\mid$ rules $\mid$ profile $\left.\right)$ $\mid$
    protect $\langle$ModId$\rangle$ $\mid$
    extend $\langle$ModId$\rangle$ $\mid$
    include $\langle$ModId$\rangle$

$\langle$ShowOption$\rangle$ ::= advise $\mid$ stats $\mid$ loop stats $\mid$ timing $\mid$
    loop timing $\mid$ breakdown $\mid$ command $\mid$ gc

$\langle$PrintOption$\rangle$ ::= mixfix $\mid$ flat $\mid$ with parentheses $\mid$
    with aliases $\mid$ conceal $\mid$ number $\mid$ rat $\mid$ color $\mid$
    format $\mid$ graph

$\langle$TraceOption$\rangle$ ::= condition $\mid$ whole $\mid$ substitution $\mid$ select $\mid$
    mbs $\mid$ eqs $\mid$ rls $\mid$ rewrite $\mid$ body

$\langle$DebuggerCommand$\rangle$ ::= resume . $\mid$ abort . $\mid$ step . $\mid$ where .

$\langle$Module$\rangle$ ::= fmod $\langle$ModId$\rangle$ $[$ $\langle$ParameterList$\rangle$ $]$ is $\langle$ModElt$\rangle$* endfm $\mid$
    mod $\langle$ModId$\rangle$ $[$ $\langle$ParameterList$\rangle$ $]$ is $\langle$ModElt'$\rangle$* endfm

$\langle$Theory$\rangle$ ::= fth $\langle$ModId$\rangle$ is $\langle$ModElt$\rangle$* endfth $\mid$
    th $\langle$ModId$\rangle$ is $\langle$ModElt'$\rangle$* endth

$\langle$View$\rangle$ ::= view $\langle$ViewId$\rangle$ from $\langle$ModExp$\rangle$ to $\langle$ModExp$\rangle$ is
             $\langle$ViewElt$\rangle$*
           endv

$\langle$ParameterList$\rangle$ ::= { $\langle$ParameterDecl$\rangle$ $\left(\right.$ , $\langle$ParameterDecl$\rangle$ $\left.\right)$* }

$\langle$ParameterDecl$\rangle$ ::= $\langle$ParameterId$\rangle$ :: $\langle$ModExp$\rangle$

$\langle$ModElt$\rangle$ ::= including $\langle$ModExp$\rangle$ . $\mid$
    extending $\langle$ModExp$\rangle$ . $\mid$
    protecting $\langle$ModExp$\rangle$ . $\mid$
    sorts $\langle$Sort$\rangle$$+$ . $\mid$
    subsorts $\langle$Sort$\rangle$$+$ $\left(\right.$ < $\langle$Sort$\rangle$$+$ $\left.\right)$$+$ . $\mid$
    op $\langle$OpForm$\rangle$ : $\langle$Type$\rangle$* $\langle$Arrow$\rangle$ $\langle$Type$\rangle$ $[$ $\langle$Attr$\rangle$ $]$ . $\mid$
    ops $\left(\right.$ $\langle$OpId$\rangle$ $\mid$ ( $\langle$OpForm$\rangle$ ) $\left.\right)$$+$ : $\langle$Type$\rangle$* $\langle$Arrow$\rangle$ $\langle$Type$\rangle$
           $[$ $\langle$Attr$\rangle$ $]$ . $\mid$
    vars $\langle$VarId$\rangle$$+$ : $\langle$Type$\rangle$ . $\mid$
    $\langle$Statement$\rangle$ $[$ $\langle$StatementAttr$\rangle$ $]$ .

$\langle$ViewElt$\rangle$ ::= var $\langle$varId$\rangle$$+$ : $\langle$Type$\rangle$ . $\mid$
    sort $\langle$Sort$\rangle$ to $\langle$Sort$\rangle$ . $\mid$
    label $\langle$LabelId$\rangle$ to $\langle$LabelId$\rangle$ . $\mid$
    op $\langle$OpForm$\rangle$ to $\langle$OpForm$\rangle$ .  $\mid$
    op $\langle$OpForm$\rangle$ : $\langle$Type$\rangle$* $\langle$Arrow$\rangle$ $\langle$Type$\rangle$ to $\langle$OpForm$\rangle$ . $\mid$
    op $\langle$Term$\rangle$ to $\langle$Term$\rangle$ .

$\langle$ModExp$\rangle$ ::= $\langle$ModId$\rangle$ $\mid$
    ( $\langle$ModExp$\rangle$ ) $\mid$
    $\langle$ModExp$\rangle$ + $\langle$ModExp$\rangle$ $\mid$
    $\langle$ModExp$\rangle$ * $\langle$Renaming$\rangle$
    $\langle$ModExp$\rangle$ { $\langle$ViewId$\rangle$ $\left(\right.$ , $\langle$ViewId$\rangle$ $\left.\right)$* }

$\langle$Renaming$\rangle$ ::= ( $\langle$RenamingItem$\rangle$ $\left(\right.$ , $\langle$RenamingItem$\rangle$ $\left.\right)$* )

$\langle$RenamingItem$\rangle$ ::= sort $\langle$Sort$\rangle$ to $\langle$Sort$\rangle$ $\mid$
    label $\langle$LabelId$\rangle$ to $\langle$LabelId$\rangle$ $\mid$
    op $\langle$OpForm$\rangle$ $\langle$ToPartRenamingItem$\rangle$ $\mid$
    op $\langle$OpForm$\rangle$ : $\langle$Type$\rangle$* $\langle$Arrow$\rangle$ $\langle$Type$\rangle$ $\langle$ToPartRenamingItem$\rangle$

$\langle$ToPartRenamingItem$\rangle$ ::= to $\langle$OpForm$\rangle$ $[$ $\langle$Attr$\rangle$ $]$

$\langle$Arrow$\rangle$ ::= -> $\mid$ ~>

$\langle$Type$\rangle$ ::= $\langle$Sort$\rangle$ $\mid$ $\langle$Kind$\rangle$

$\langle$Kind$\rangle$ ::= [ $\langle$Sort$\rangle$ $\left(\right.$, $\langle$Sort$\rangle$ $\left.\right)$* ]

$\langle$Sort$\rangle$ ::= $\langle$SortId$\rangle$ $\mid$ $\langle$Sort$\rangle$ { $\langle$Sort$\rangle$ $\left(\right.$ , $\langle$Sort$\rangle$ $\left.\right)$* }

$\langle$ModElt'$\rangle$ ::= $\langle$ModElt$\rangle$ $\mid$
    $\langle$Statement'$\rangle$ $[$ $\langle$StatementAttr$\rangle$ $]$ .

$\langle$Statement$\rangle$  ::=  mb $[$ $\langle$Label$\rangle$ $]$ $\langle$Term$\rangle$ : $\langle$Sort$\rangle$ $\mid$
    cmb $[$ $\langle$Label$\rangle$ $]$ $\langle$Term$\rangle$ : $\langle$Sort$\rangle$ if $\langle$Condition$\rangle$ $\mid$
    eq $[$ $\langle$Label$\rangle$ $]$ $\langle$Term$\rangle$ = $\langle$Term$\rangle$ $\mid$
    ceq $[$ $\langle$Label$\rangle$ $]$ $\langle$Term$\rangle$ = $\langle$Term$\rangle$ if $\langle$Condition$\rangle$

$\langle$Statement'$\rangle$ ::= rl $[$ $\langle$Label$\rangle$ $]$ $\langle$Term$\rangle$ => $\langle$Term$\rangle$ $\mid$
    crl $[$ $\langle$Label$\rangle$ $]$ $\langle$Term$\rangle$ => $\langle$Term$\rangle$ if $\langle$Condition'$\rangle$

$\langle$Label$\rangle$ ::= [ $\langle$LabelId$\rangle$ ] :

$\langle$Condition$\rangle$ ::= $\langle$ConditionFragment$\rangle$ $\left(\right.$ /\ $\langle$ConditionFragment$\rangle$ $\left.\right)$*

$\langle$Condition'$\rangle$ ::= $\langle$ConditionFragment'$\rangle$
                 $\left(\right.$ /\ $\langle$ConditionFragment'$\rangle$ $\left.\right)$*

$\langle$ConditionFragment$\rangle$ ::= $\langle$Term$\rangle$ = $\langle$Term$\rangle$ $\mid$ $\langle$Term$\rangle$ := $\langle$Term$\rangle$
                        $\mid$ $\langle$Term$\rangle$ : $\langle$Sort$\rangle$

$\langle$ConditionFragment'$\rangle$ ::= $\langle$ConditionFragment$\rangle$ $\mid$ $\langle$Term$\rangle$ => $\langle$Term$\rangle$

$\langle$Attr$\rangle$ ::=
    [ $\left(\right.$ assoc $\mid$ comm $\mid$
        $[$ left $\mid$ right $]$ id: $\langle$Term$\rangle$ $\mid$
        idem $\mid$ iter $\mid$ memo $\mid$ ditto $\mid$
        config $\mid$ obj $\mid$ msg $\mid$
        metadata $\langle$StringId$\rangle$
        strat ( $\langle$Nat$\rangle$$+$ ) $\mid$
        poly ( $\langle$Nat$\rangle$$+$ ) $\mid$
        frozen $[$ ( $\langle$Nat$\rangle$$+$ ) $]$ $\mid$
        prec $\langle$Nat$\rangle$ $\mid$
        gather ( $\left(\right.$ e $\mid$ E $\mid$ & $\left.\right)$$+$ ) $\mid$
        format ( $\langle$Token$\rangle$$+$ ) $\mid$
        special ( $\langle$Hook$\rangle$$+$ ) $\left.\right)$$+$ ]

$\langle$StatementAttr$\rangle$ ::=
    [ $\left(\right.$ nonexec $\mid$ otherwise $\mid$
        metadata $\langle$StringId$\rangle$
        label $\langle$LabelId$\rangle$ $\left.\right)$$+$ ]

$\langle$Hook$\rangle$ ::= id-hook $\langle$Token$\rangle$ $[$ ( $\langle$TokenString$\rangle$ ) $]$ $\mid$
    $\left(\right.$ op-hook $\mid$ term-hook $\left.\right)$ ( $\langle$TokenString$\rangle$ )

$\langle$FileName$\rangle$    %%% OS dependent
$\langle$Directory$\rangle$   %%% OS dependent
$\langle$LsFlag$\rangle$      %%% OS dependent

$\langle$StringId$\rangle$    %%% characters enclosed in double quotes "..."
$\langle$ModId$\rangle$       %%% simple identifier, by convention all capitals
$\langle$ViewId$\rangle$      %%% simple identifier, by convention capitalized
$\langle$ParameterId$\rangle$ %%% simple identifier, by convention single cap.
$\langle$SortId$\rangle$      %%% simple identifier, by convention capitalized
$\langle$VarId$\rangle$       %%% simple identifier, by convention capitalized
$\langle$OpId$\rangle$        %%% identifier possibly with underscores
$\langle$OpForm$\rangle$ ::= $\langle$OpId$\rangle$ $\mid$ ( $\langle$OpForm$\rangle$ ) $\mid$ $\langle$OpForm$\rangle$$+$
$\langle$Nat$\rangle$         %%% a natural number
$\langle$Term$\rangle$ ::= $\langle$Token$\rangle$ $\mid$ ( $\langle$Term$\rangle$ ) $\mid$ $\langle$Term$\rangle$$+$
$\langle$Token$\rangle$       %%% Any symbol other than ( or )
$\langle$TokenString$\rangle$ ::= $\langle$Token$\rangle$ $\mid$ ( $\langle$TokenString$\rangle$ ) $\mid$ $\langle$TokenString$\rangle$*
$\langle$LabelId$\rangle$     %%% simple identifier

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