next up previous contents
Next: Module renaming Up: Module summation and renaming Previous: Module summation and renaming   Contents


The summation module expression

The summation module operation creates a new module that includes all the information in its summands. The syntax for a summation of module expressions is

  ModuleExpression + ModuleExpression
with + associative and commutative.

Summation expressions are flattened before being evaluated, so that A + (B + C) and (C + A) + B both create a single new module A + B + C, The evaluation of a summation module expression results in the creation of a new module, with such a module expression as its name, which imports the module expressions being combined. The new module will be generated having one type or another, depending on the types of the arguments of the summation module expression. A summation is a functional module if all the summands are functional modules and a system module otherwise.

Although the use of the summation module expression is more interesting in combination with other module expressions, let us consider as an example the following module, in which the union of the predefined FLOAT and STRING modules (see Chapter 7) are imported together in protecting mode to illustrate its use.

  fmod FLOAT-STRING is
    protecting FLOAT + STRING .
    ...
  endfm

Notice that a declaration

  protecting A + B .

is not equivalent to a sequence of declarations

  protecting A .
  protecting B .

because in general the modules A and B may share sorts and operators. The same happens with extending declarations, for the same reason. However, a declaration of the form

  including A + B .

is indeed equivalent to a sequence of declarations

  including A .
  including B .


next up previous contents
Next: Module renaming Up: Module summation and renaming Previous: Module summation and renaming   Contents
The Maude Team