The tuple and power module expressions

The evaluation of an $n$-tuple module expression consists in the generation of a parameterized functional module with the number of TRIV parameters specified by the argument $n$. A sort for tuples of such size, and the corresponding constructor (_,...,_) and selector operators p1_, ..., pn_, are also defined. For example, the module expression TUPLE[2] automatically generates as result the following module (notice the backquotes in the declaration of the tuple constructor).

 (fmod TUPLE[2]{C1 :: TRIV, C2 :: TRIV} is
    sorts Tuple{C1, C2} .
    op `(_`,_`) : C1$Elt C2$Elt -> Tuple{C1, C2} [ctor].
    op p1_ : Tuple{C1, C2} -> C1$Elt .
    op p2_ : Tuple{C1, C2} -> C2$Elt .
    var E1 : C1$Elt .
    var E2 : C2$Elt .
    eq p1(E1, E2) = E1 .
    eq p2(E1, E2) = E2 .
  endfm)

In the Clear [9] and OBJ [44] family of languages, module operations take theories, modules, and views, and return new theories and modules (see Chapter 6); on the other hand, the TUPLE[_] operation takes a nonzero natural number $n$ and returns a parameterized TUPLE[$n$] module; this is impossible to achieve with the Clear/OBJ repertoire of module operations. Even though an $n$-tuple module expression is in principle of a completely different nature from the usual Clear/OBJ module operations, the way Full Maude handles it is the same as the way it handles any other module expression. Its evaluation produces a new unit, a parameterized functional module in this case, with the module expression as its name.

Suppose that we want to specify a library in which we have the information on the books in a record structure with the title, author, year of publication, publisher, and number of copies available. We may use a specification beginning as follows:

 (fmod LIBRARY is
    pr TUPLE[5]{String, String, Nat, String, Nat}
         * (op p1_ to title,
            op p2_ to author,
            op p3_ to year,
            op p4_ to publisher,
            op p5_ to copies) .
    ---- ...
  endfm)

The particular case of a tuple in which all component sorts are equal is provided by the $n$-power module expression. For example, the module expression POWER[5] automatically generates as result the following module:

 (fmod POWER[5]{X :: TRIV} is
    protecting TUPLE[5]{X, X, X, X, X}
      * (sort Tuple{X, X, X, X, X} to Power{X}) .
  endfm)

We can use the power module expression in any place where a module name is expected, like in a reduction

  Maude> (red in POWER[10]{Nat} : p5 (0, 1, 2, 3, 4, 5, 6, 7, 8, 9) .)
  result NzNat :
    4

or in an importation to build other modules:

 (fmod PERSON-RECORD is
    pr POWER[3]{String}
         * (sort Tuple{String, String, String} to PersonRecord,
            op p1_ to firstname, 
            op p2_ to lastname,
            op p3_ to address) .
    op fullName : PersonRecord -> String .
    vars F L A : String .
    eq fullName((F, L, A)) = F + " " + L .
  endfm)

  Maude> (red fullName(("John", "Smith", "Maude Ave")) .)
  result String :
    "John Smith"