Module summation and renaming

The summation and renaming of object-oriented modules is similar to their non-object-oriented counterparts. Renaming maps, however, are in this case available for mapping classes, attributes, and messages. Therefore, in addition to the renamings available in Core Maude, Full Maude also supports renaming maps of the form:

  class $\langle$identifier$\rangle$ to $\langle$identifier$\rangle$
  attr $\langle$class-identifier$\rangle$ . $\langle$attr-identifier$\rangle$ to $\langle$class-identifier$\rangle$
  msg $\langle$identifier$\rangle$ to $\langle$identifier$\rangle$
  msg $\langle$identifier$\rangle$ : $\langle$type-list$\rangle$ -> $\langle$type$\rangle$ to $\langle$identifier$\rangle$

We illustrate the renaming of object-oriented modules with the following example:^15.3

  Maude> (show module OO-STACK2 * (class Stack{X} to Stack{X},
                                class Node{X} to Node{X},
                                attr Stack{X} . first to head,
                                msg _elt_ to element,
                                sort Int to Integer) .)

  omod OO-STACK2 * (sort Int to Integer,
                 msg _elt_ to element,
                 class Node`{X`} to Node`{X`},
                 class Stack`{X`} to Stack`{X`},
                 attr Stack`{X`} . first to head) {X :: CELL} is
    protecting QID .
    protecting INT * (sort Int to Integer) .
    including CONFIGURATION+ .
    including CONFIGURATION .
    protecting BOOL .
    subsort Qid < Oid .
    class Node`{X`} | next : Oid, node : Oid .
    class Stack`{X`} | head : Oid .
    op null : -> Oid .
    op o : Oid Integer -> Oid .
    msg _pop : Oid -> Msg .
    msg _push_ : Oid Oid -> Msg .
    msg _top_ : Oid Oid -> Msg .
    msg element : Oid X$Elt -> Msg .
    rl < O:Oid : Stack{X}| head : O':Oid >
       < O':Oid : Node{X}| next : O'':Oid >
       O:Oid pop
       => < O:Oid : Stack{X}| head : O'':Oid >
       [label pop] .
    rl < O:Oid : Stack{X}| head : O':Oid >
       < O':Oid : Node{X}| node : O'':Oid >
       < O'':Oid : X$Cell | contents : E:X$Elt >
       O:Oid top O''':Oid
       => < O:Oid : Stack{X}| none >
          < O':Oid : Node{X}| none >
          < O'':Oid : X$Cell | none >
          element(O'':Oid,E:X$Elt)
       [label top] .
    rl < O:Oid : Stack{X}| head : null >
       O:Oid push O':Oid
       => < O:Oid : Stack{X}| head : o(O:Oid,0)>
          < o(O:Oid,0): Node{X}| next : null,node : O':Oid >
       [label push2] .
    rl < O:Oid : Stack{X}| head : o(O:Oid,N:Integer)>
       O:Oid push O':Oid
       => < O:Oid : Stack{X}| head : o(O:Oid,N:Integer + 1)>
          < o(O:Oid,N:Integer + 1): Node{X}|
              next : o(O:Oid,N:Integer),node : O':Oid >
       [label push1] .
  endom