Module renaming

The syntax of a renaming module expression is

  $\langle$ModuleExpression$\rangle$ * ( $\langle$Renaming$\rangle$ )

where $\langle$Renaming$\rangle$ is a comma-separated sequence of renaming items of the forms:

  sort $\langle$identifier$\rangle$ to $\langle$identifier$\rangle$
  op $\langle$identifier$\rangle$ to $\langle$identifier$\rangle$
  op $\langle$identifier$\rangle$ to $\langle$identifier$\rangle$ [ $\langle$attribute-set$\rangle$ ]
  op $\langle$identifier$\rangle$ : $\langle$type-list$\rangle$ -> $\langle$type$\rangle$ to $\langle$identifier$\rangle$
  op $\langle$identifier$\rangle$ : $\langle$type-list$\rangle$ -> $\langle$type$\rangle$ to $\langle$identifier$\rangle$
       [ $\langle$attribute-set$\rangle$ ]
  label $\langle$identifier$\rangle$ to $\langle$identifier$\rangle$

Renaming (_*(_)) binds tighter than summation (_+_), and it groups to the left. Note that, in addition to the typical renamings of sorts and operators, renaming of labels is also supported (which may be useful for metalevel applications). Note also how the renaming of operators allows changing the attributes of the operator being renamed. The only attributes currently allowed in operator maps are prec, gather, and format. The idea is that when you rename an operator, the old syntactic properties may no longer be legal and are reset to defaults, unless you explicitly set them with these attributes; for example, when a change in the syntax of the operator could cause a parsing different from the intended one. Let us see an example in which modifying the grammatical attributes of an operator is useful. Consider the following module defining lists of natural numbers with a max operator returning the greatest of the elements in a list of natural numbers.

  fmod NAT-LIST-MAX is
    pr NAT .
    sort NeNatList .
    subsort Nat < NeNatList .
    op __ : NeNatList NeNatList -> NeNatList [ctor assoc] .
    op max : NeNatList -> Nat .
    var N : Nat .
    var NL : NeNatList .
    eq max(N) = N .
    eq max(N NL) = if N > max(NL) then N else max(NL) fi .
  endfm

We may obtain the maximum of a list of natural numbers as follows.

  Maude> red max(4 2 5 3) .
  result NzNat: 5

Suppose now that we want to change the syntax of the function max in the NAT-LIST-MAX module above to maximum_.

  fmod NAIVE-NAT-LIST-MIXFIX-MAX is
    pr NAT-LIST-MAX * (op max : NeNatList -> Nat to maximum_) .
  endfm

We can do the following reduction:

  Maude> red maximum 2 3 4 1 .
  result NeNatList: 2 3 4 1

This result may seem strange, but it makes perfect sense. What has happened is that it has been parsed as (maximum 2) 3 4 1, the only possible parse given the default precedence values and gathering patterns assigned. Since by default maximum_ has precedence 15 and gathering E, it cannot take the list 2 3 4 1 as argument because __ has precedence 41. However, since __ has gathering e E, maximum 2 is a valid argument for it (see Section 3.9 for a detailed discussion on the use of precedence values and gathering patterns and their default values). We can of course obtain the intended result by placing parentheses around the set of numbers,

  Maude> red maximum (2 3 4 1) .
  result NzNat: 4

but it is more convenient to change the precedence values of the operators. We can, for example, raise the precedence of maximum_.

  fmod NAT-LIST-MIXFIX-MAX is
    pr NAT-LIST-MAX 
         * (op max : NeNatList -> Nat to maximum_ [prec 41]) .
  endfm

having then the following reduction.

  Maude> red maximum 2 3 4 1 .
  result NzNat: 4

Notice that if maximum_ has precedence 41, then (maximum 2) 3 4 1 is no longer a valid parse.

A renaming can be considered as a function that, given a module $M$ and a list of mappings $S$, returns a copy of the module, with such a module expression as its name, in which the names of sorts, operators, etc. are changed as indicated by the mappings. However, renaming a module that has imports is a subtle issue. Given a structured specification, the renaming not only causes the creation of a copy of the top module in the structure, but renames also the part of the submodule structure that is affected by the renaming. For any other submodule $M'$ in the structure which is affected by the mappings, a renamed copy of it is generated with name $M'\texttt{ * (}S'\texttt{)}$, where $S'$ is the subset of mappings in $S$ that affect $M'$.

A module expression $A\texttt{ * (}R\texttt{)}$ evaluates to $A$ if $A$ has no content that is affected by the renaming $R$. Otherwise $A\texttt{ * (}R\texttt{)}$ evaluates to a new module $A\texttt{ * (}R'\texttt{)}$ where $R'$ is obtained by deleting those renaming items that do not affect $A$, and canonizing the types in operator renamings with respect to $A$ (see below). If $A$ imports modules $B$ and $C$, $A\texttt{ * (}R'\texttt{)}$ will import modules obtained by evaluating $B\texttt{ * (}R'\texttt{)}$ and $C\texttt{ * (}R'\texttt{)}$.

There are some subtle cases. Consider for example the following three modules:

  fmod RENAMING-EX-A is
    sort Foo .
    op a : -> Foo .
    op f : Foo -> Foo .
  endfm

  fmod RENAMING-EX-B is
    including RENAMING-EX-A .
    sort Bar .
    subsort Foo < Bar .
    op f : Bar -> Bar .
  endfm

  fmod RENAMING-EX-C is
    inc RENAMING-EX-B * (op f : Bar -> Bar to g) .
  endfm

Here, the operator f in the module RENAMING-EX-A looks as though it is not affected by the renaming in the module RENAMING-EX-C, but because of the subsort declaration Foo < Bar in RENAMING-EX-B, it should be renamed for consistency. This is internally handled by the Maude system by canonizing the type Bar occurring in the renaming

  op f : Bar -> Bar to g

to the kind expression [Foo,Bar], which includes all of the sorts in the kind [Bar] occurring in RENAMING-EX-B. Thus, the module expression

  RENAMING-EX-B * (op f : Bar -> Bar to g)

evaluates to a new module

  RENAMING-EX-B * (op f : [Foo,Bar] -> [Foo,Bar] to g)

which includes the module expression

  RENAMING-EX-A * (op f : [Foo,Bar] -> [Foo,Bar] to g)

which evaluates to a new module

  RENAMING-EX-A * (op f : [Foo] -> [Foo] to g)

in which f has been renamed.

In general, * does not distribute over +. Consider this other example:

  fmod RENAMING-EX-D is
    sorts Foo Bar .
  endfm

  fmod RENAMING-EX-E is
    inc RENAMING-EX-D .
    op f : Foo -> Foo .
  endfm

  fmod RENAMING-EX-F is
    inc RENAMING-EX-D .
    subsort Foo < Bar .
    op f : Bar -> Bar .
  endfm

It is not the case that the module expressions

  (RENAMING-EX-E + RENAMING-EX-F) * (op f : Bar -> Bar to g)

and

  (RENAMING-EX-E * (op f : Bar -> Bar to g)) 
    + (RENAMING-EX-F * (op f : Bar -> Bar to g))

evaluate to the same module, because in the latter the operator f occurring in RENAMING-EX-E will not be renamed, since f : Bar -> Bar does not occur in RENAMING-EX-E.

Operators with the poly attribute are only affected by operator renamings that do not specify types. Renaming a module does not change its module type, that is, renamed functional modules (resp. system modules) remain functional (resp. system).