Additional module operations in Full Maude

As for Core Maude, in Full Maude we can use the keywords protecting, extending, and including (or pr, ex, and inc in abbreviated form) to define structured specifications, as well as summation, renaming, and instantiation operations on parameterized modules (see Chapter 6). All the predefined modules introduced in Chapter 7, plus the module META-LEVEL and its submodules, described in Chapter 11, are also available in Full Maude.^14.2

In addition to the module operations available in Core Maude, Full Maude supports the following extensions:

• Tuple and power expressions which, given any nonzero natural number, generate parameterized modules specifying tuples and powers of the corresponding size.
      TUPLE[$\langle$NonzeroNaturalNumber$\rangle$]{$\langle$ViewExpression$\rangle$}
      POWER[$\langle$NonzeroNaturalNumber$\rangle$]{$\langle$ViewExpression$\rangle$}
  

  See Section 14.3.1.

• Parameterized views, and the instantiation of parameterized modules with instantiations of views. See Section 14.3.2.

• Object-oriented modules, extending all the module operations available in Core Maude to this new type of modules. Thus, in Full Maude we may rename object-oriented modules, with renamings of classes, attributes, and messages, or use object-oriented modules in the summation of modules. Full Maude also supports object-oriented theories, views from object-oriented theories to object-oriented modules, and object-oriented parameterized modules, as well as the instantiation of such object-oriented parameterized modules. We devote Chapter 15 to the study of object-oriented modules.

As in Core Maude, a module or theory importing some combination of modules or theories, given by module expressions, can be seen as a structured module with more or less complex relationships among its component submodules. For execution purposes, however, we typically want to convert this structured module into an equivalent unstructured module, that is, into a ``flattened'' module without submodules; this flattened module will then be compiled into the Maude rewrite engine. By systematically using the metaprogramming capabilities of Maude, we can both evaluate module expressions into structured module hierarchies and flatten such hierarchies into unstructured modules for execution. All such module operations are defined by equations that operate on the metalevel term representations of modules. This is essentially the idea behind the implementation of Full Maude in Maude.

In Full Maude, the use of module expressions is somewhat more general than in Core Maude. A Full Maude module expression can be used in any place where a module name is expected. Thus, as in Core Maude, in Full Maude, module expressions can be used as:

• arguments of a protecting, extending, or including importation,
• the source or target of a view, or
• the parameter of a module, provided the top level is a theory.

Furthermore, in Full Maude, they can also be used, e.g., to express the module in which a red or rew command will be executed,

  Maude> (red in BOOL * (op true to T, op false to F) : T or F .)
  result Bool :
    T

or as argument of any other command requiring a module name,

  Maude> (show ops LIST{Nat} .)
    op $reverse : List{Nat}List{Nat}-> List{Nat}.
    op $size : List{Nat}Nat -> Nat .
    op append : List{Nat}List{Nat}-> List{Nat}.
    op append : List{Nat}NeList{Nat}-> NeList{Nat}.
    op append : NeList{Nat}List{Nat}-> NeList{Nat}.
    ...

Of course, this works with any module, and not only with predefined modules. For example, let us do the same with the instantiation of the SET-MAX module presented in Section 6.3.4 (which we assume is in file set-max.maude) with the view IntAsToset described in Section 6.3.2. Although we can use Core Maude modules in Full Maude, we do not have access to user-defined Core Maude views from Full Maude. Any such view must be entered into Full Maude before it is used in a module instantiation. Note that although Core Maude modules are implicitly entered into Full Maude's database, they are recompiled, and therefore, any view required for recompiling the corresponding module must also be entered. The evaluation of the module expression SET-MAX{IntAsToset} requires views TOSET and IntAsToset.

  Maude> load set-max.maude
  Maude> select FULL-MAUDE .
  Maude> loop init .

         Full Maude 2.3 `(November 20th`, 2006`)

  Maude> (view TOSET from TRIV to TOSET is
            sort Elt to Elt .
          endv)
  Introduced view TOSET

  Maude> (view IntAsToset from TOSET to INT is
            sort Elt to Int .
          endv)
  Introduced view IntAsToset

  Maude> (red in SET-MAX{IntAsToset} : max((5, 4, 8, 4, 6, 5)) .)
  result NzNat :
    8

Similarly, after entering the Full Maude version of the RingToRat view, we can reduce the same expression we reduced in Section 6.3.4 as follows:

  Maude> (red in RAT-POLY{Qid} :
            (((2 / 3) (('X ^ 2) ('Y ^ 3)))
             ++ ((7 / 5) (('Y ^ 2) ('Z ^ 5))))
            (((1 / 7) ('U ^ 2)) ++ (1 / 2)) .)
  result Poly{RingToRat,Qid} :
    (1/3('X ^ 2)'Y ^ 3)
    ++ (1/5('U ^ 2)('Y ^ 2)'Z ^ 5)
    ++ (2/21('U ^ 2)('X ^ 2)'Y ^ 3)
    ++ (7/10('Y ^ 2)'Z ^ 5)

As we will see below, a module expression can also be used as the parameter of a view, provided the top level is a theory.