Parameterized modules

System modules and functional modules can be parameterized. A parameterized system module has syntax

mod M{$X_1$ :: $T_1$ , ... , $X_n$ :: $T_n$} is ... endm

with $n\geq 1$. Parameterized functional modules have completely analogous syntax.

The {$X_1$ :: $T_1$ , ..., $X_n$ :: $T_n$} part is called the interface, where each pair $X_i \texttt{ :: } T_i$ is a parameter, and each $X_i$ is an identifier--the parameter name or parameter label--and each $T_i$ is an expression that yields a theory--the parameter theory. Each parameter name in an interface must be unique, although there is no uniqueness restriction on the parameter theories of a module--we can have, e.g., two TRIV parameters. The parameter theories of a functional module must be functional theories.

In a parameterized module $M$, all the sorts and statement labels coming from theories in its interface must be qualified by their names. Thus, given a parameter $X_i \texttt{ :: } T_i$, each sort $S$ in $T_i$ must be qualified as $X_i\texttt{\$}S$, and each label $l$ of a statement occurring in $T_i$ must be qualified as $X_i\texttt{\$}l$. In fact, the parameterized module $M$ is flattened as follows. For each parameter $X_i \texttt{ :: } T_i$, a renamed copy of the theory $T_i$, called $X_i \texttt{ :: } T_i$ is included. The renaming maps each sort $S$ to $X_i\texttt{\$}S$, and each label $l$ of a statement occurring in $T_i$ to $X_i\texttt{\$}l$. The renaming percolates down through nested inclusions of theories, but has no effect on importations of modules. Thus, if $T_i$ includes a theory $T'$, when the renamed theory $X_i \texttt{ :: } T_i$ is created and included into $M$, and the renamed theory $X_i \texttt{ :: } T'$ will also be created and included into $X_i \texttt{ :: } T_i$.^6.5However, the renaming will have no effect on modules imported by either the $T_i$ or $T'$; for example, if BOOL is imported by one of these theories, it is not renamed, but imported in the same way into $M$.

For example, a parameterized module PRELIM-SET with TRIV as interface can be defined as follows:

  fmod PRELIM-SET{X :: TRIV} is
    protecting BOOL .
    sorts Set NeSet .
    subsorts X$Elt < NeSet < Set .
    op empty : -> Set .
    op _,_ : Set Set -> Set [assoc comm id: empty] .
    op _,_ : NeSet NeSet -> NeSet [ditto] .
    op _in_ : X$Elt Set -> Bool .
    op _-_ : Set Set -> Set .   *** set difference
    
    var  E : X$Elt .
    vars S S' : Set .
    eq E, E = E .
    eq E in E, S = true .
    eq E in S = false [owise] .
    eq (E, S) - (E, S') = S - (E, S') .
    eq S - S' = S [owise] .
  endfm

In Maude--unlike OBJ3 and other similar languages--sorts are not systematically qualified by their module name. This convention of not qualifying sorts may be particularly weak when dealing with parameterized modules. However, given that Maude supports ad-hoc overloading and that constants can be qualified in order to be disambiguated (see Section 3.9.3), the problem of ambiguity in a signature is reduced to collisions of sorts. For example, in a module one may very easily need sets of integers and sets of quoted identifiers, in which case, given the specification of the PRELIM-SET module above, we would get two Set sorts from different importations which would be confused into one sort. Our solution consists in qualifying parameterized sorts, not with the module expression they belong to, but with the name of the view or views used in the instantiation of the parameterized module. Since we assume that all views are named, these names are the ones used in the qualification. Specifically, in the body of a parameterized module $M${ $X_1 \texttt{ :: } T_1 \texttt{ , } \dots \texttt{ , } X_n \texttt{ :: } T_n$}, any sort $S$ can be written in the form $S${ $X_1\texttt{ , }\ldots\texttt{ , }X_n$}. When the module is instantiated with views $V_1 \ldots V_n$, then this sort is instantiated to $S${ $V_1\texttt{ , }\ldots\texttt{ , }V_n$}.

Note that, although we strongly recommend it, the parameterization of sorts is optional, and therefore, for example, the above PRELIM-SET specification is a perfectly valid parameterized module.

Sorts declared in the parameterized module $M${ $X_1 \texttt{ :: } T_1 \texttt{ , } \dots \texttt{ , } X_n \texttt{ :: } T_n$} may in general be parameterized as $S${ $Y_1\texttt{ , }\ldots\texttt{ , }Y_m$}, with $m\geq 1$, and where each $Y_j$ is an $X_i$. It is recommended that all sorts declared in a parameterized module be parameterized with $m=n$ and $Y_j=X_j$ for $1\leq j \leq n$, but this is not enforced--parameterized sorts may duplicate, omit, or reorder parameters and unparameterized sorts are also allowed.

Thus, the previous PRELIM-SET module to define sets could instead have been specified in a better way as follows:

  fmod BASIC-SET{X :: TRIV} is
    protecting BOOL .
    sorts Set{X} NeSet{X} .
    subsorts X$Elt < NeSet{X} < Set{X} .
    op empty : -> Set{X} .
    op _,_ : Set{X} Set{X} -> Set{X} [assoc comm id: empty] .
    op _,_ : NeSet{X} NeSet{X} -> NeSet{X} [ditto] .
    op _in_ : X$Elt Set{X} -> Bool .
    op _-_ : Set{X} Set{X} -> Set{X} .   *** set difference
    
    var  E : X$Elt .
    vars S S' : Set{X} .
    eq E, E = E .
    eq E in E, S = true .
    eq E in S = false [owise] .
    eq (E, S) - (E, S') = S - (E, S') .
    eq S - S' = S [owise] .
  endfm

When this module is instantiated with the predefined view Int, the sort Set{X} becomes Set{Int}, and when it is instantiated with the predefined view Qid (see Section 7.11.1) it becomes Set{Qid}. In the following sections we will see additional examples of how this qualification convention for the sorts of a parameterized module avoids many unintended collisions of sort names, thus making renaming practically unnecessary.^6.6

As another simple example of parameterized module, we consider a module MAYBE{X :: TRIV} in which we declare a sort Maybe{X} as a supersort of the sort Elt of the parameter theory and a constant maybe of this sort Maybe{X}. This technique is useful to declare a partial function as a total function, as we will see in the PFUN module of Section 14.3.2.

  fmod MAYBE{X :: TRIV} is
    sort Maybe{X} .
    subsort X$Elt < Maybe{X} .
    op maybe : -> Maybe{X} [ctor] .
  endfm

The PRELIM-SET, BASIC-SET, and MAYBE modules above have only one parameter. In general, however, parameterized modules can have several parameters. It can furthermore happen that several parameters are declared with the same parameter theory, that is, we can have, for example, an interface of the form {X :: TRIV, Y :: TRIV} involving two copies of the theory TRIV. Therefore, parameters cannot be treated as normal submodules, since we do not want them to be shared when their labels are different. We regard the relationship between the body of a parameterized module and the interface of its parameters not as an inclusion, but as a module constructor which is evaluated generating renamed copies of the parameters, which are then included. For the above interface, two copies of the theory TRIV are generated, with names $\texttt{X}\;\texttt{::}\;\texttt{TRIV}$ and $\texttt{Y}\;\texttt{::}\;\texttt{TRIV}$. As already mentioned, in such copies of parameter theories, sorts are renamed as follows: if $Z$ is the label of a parameter theory $T$, then each sort $S$ in $T$ is renamed to $Z\texttt{\$}S$ and each statement label $l$ is renamed to $Z\texttt{\$}l$. All occurrences of these sorts and labels in the body of the parameterized module must mention their corresponding renaming.

Let us consider as an example the following module PAIR, in which we would like to point out the use of the qualifications for the sorts coming from each of the parameters.

  fmod PAIR{X :: TRIV, Y :: TRIV} is
    sort Pair{X, Y} .
    op <_;_> : X$Elt Y$Elt -> Pair{X, Y} .
    op 1st : Pair{X, Y} -> X$Elt .
    op 2nd : Pair{X, Y} -> Y$Elt .
    
    var A : X$Elt .
    var B : Y$Elt .
    eq 1st(< A ; B >) = A .
    eq 2nd(< A ; B >) = B .
  endfm

As already mentioned, if a parameter theory is structured, this renaming process for parameter theories is carried out not only at the top level, but for the whole ``theory part,'' that is, renaming subtheories but not renaming submodules. Consider, for example, the following parameterized module defining a lexicographical ordering on pairs of elements of two totally strictly ordered sets.

  fmod LEX-PAIR{X :: STOSET, Y :: STOSET} is
    sort Pair{X, Y} .
    op <_;_> : X$Elt Y$Elt -> Pair{X, Y} .
    op _<_ : Pair{X, Y} Pair{X, Y} -> Bool .
    op 1st : Pair{X, Y} -> X$Elt .
    op 2nd : Pair{X, Y} -> Y$Elt .
    
    vars A A' : X$Elt .
    vars B B' : Y$Elt .
    eq 1st(< A ; B >) = A .
    eq 2nd(< A ; B >) = B .
    eq < A ; B > < < A' ; B' > = (A < A') or (A == A' and B < B') .
  endfm

Representing by boxes the modules (with initiality constraints), by ovals the theories (with loose semantics), by triple arrows the protecting and parameter importations, and by single arrows the including importations, we can depict the structure of the LEX-PAIR functional module defining a lexicographic order on pairs as in Figure 6.2, where we have two copies not only of STOSET but also of the SPOSET and TAOSET subtheories (see also Figure 6.1 in page ), but only one copy of the BOOL submodule.

Figure 6.2: Structure of LEX-PAIR

The parameter theory of a module can be any module expression whose result is a theory. The following module defines bags of elements with an occurrences operation that returns the number of occurrences of a particular element in a given bag.

  fmod BAG{X :: TRIV * (sort Elt to Element)} is
    protecting NAT .
    sorts Bag{X} NeBag{X} .
    subsorts X$Element < NeBag{X} < Bag{X} .
    op mt : -> Bag{X} .
    op __ : Bag{X} Bag{X} -> Bag{X} [assoc comm id: mt] .
    op __ : Bag{X} NeBag{X} -> NeBag{X} [ditto] .
    op occurrences : X$Element Bag{X} -> Nat .
    
    vars E E' : X$Element .
    var  S : Bag{X} .
    eq occurrences(E, E S) = 1 + occurrences(E, S) .
    eq occurrences(E, S) = 0 [owise] .
  endfm

Module instantiation will be explained in the next section, and then we shall see some execution examples.