Module importation

Recall that a functional module $M$ specifies a membership equational theory of the form $(\Sigma,E\cup A)$, with $\Sigma$ its signature, $A$ the equational attributes specified for its operators, and $E$ its set of equations and memberships. A submodule $M'$ of $M$ is either a module directly imported by $M$, or a submodule of one of the modules directly imported by $M$. Then $M'$ specifies a membership equational subtheory $(\Sigma',E' \cup A') \subseteq (\Sigma,E \cup A)$. Specifically, we have three inclusions: $\Sigma'\subseteq \Sigma$, $E'\subseteq E$, and $A'\subseteq A$. Furthermore, since in Maude subsort-overloaded operators must have the same equational attributes, Maude will enforce that the inclusion $A'\subseteq A$ satisfies this property.

In a similar way, a system module $Q$ specifies a rewrite theory $(\Sigma,E \cup A,\phi,R)$. A submodule $Q'$ of $Q$ will likewise specify a rewrite subtheory $(\Sigma',E' \cup A',\phi',R')\subseteq (\Sigma,E \cup A,\phi,R)$. This means that we have inclusions $\Sigma'\subseteq \Sigma$, $E'\subseteq E$, $A'\subseteq A$ (again, with the same equational attributes for subsort-overloaded operators), $\phi'\subseteq \phi$, and $R'\subseteq R$, where $\phi'\subseteq \phi$ is an inclusion of functions and means that the freezing function $\phi$ extends the function $\phi'$. Note that $Q'$ could be a functional module, which is then understood as the rewrite theory $(\Sigma',E' \cup A',\phi',\emptyset)$, where $\phi'$ specifies whatever freezing information has been given to the operators of $\Sigma'$ in $Q'$. A system module cannot be imported into a functional module.

In Maude, a module--any module expression giving rise to a module--can be imported as a submodule of another in three different modes: protecting, extending, or including. This is done with the syntax declarations

  protecting $\langle$ModuleExpression$\rangle$ .
  extending $\langle$ModuleExpression$\rangle$ .
  including $\langle$ModuleExpression$\rangle$ .

which can be abbreviated, respectively, to

  pr $\langle$ModuleExpression$\rangle$ .
  ex $\langle$ModuleExpression$\rangle$ .
  inc $\langle$ModuleExpression$\rangle$ .

In addition to being allowed as arguments of a protecting, extending, or including importation, module expressions can also appear as the source or target of a view (see Section 6.3.2), or as the parameter of a module, provided the top level is a theory (see Section 6.3.3).

Each of the importation modes places specific semantic constraints on the corresponding inclusion between the theory of the submodule and that of the supermodule. The user must be aware that, as explained later, the Maude system does not check that these constraints are satisfied, that is, the different modes of importation can be understood as promises by the user, which would need to be proved by him/herself. Although those importation modes have no effect operationally, they do crucially affect the interpretation given to a module by the theorem proving tools. If a user is doubtful about the appropriate importation mode the default should be to use the including mode, which places weaker requirements on the importation.

Importation statements take a module expression as argument, which may be a module name, the summation of module expressions, the renaming of a module expression, or the instantiation of a parameterized module expression. Modules are constructed for each subexpression of a module expression, and so each submodule signature must be legal. Modules and module expressions are cached both to save time and so that the same module corresponding to a module expression will not be imported twice via a diamond of imports. Mutually or self recursive imports occurring through module expressions are detected and disallowed. Cached modules generated by module expressions that no longer have any users (if the module(s) containing the module expression have been replaced) are deleted. When a module $M$ used in a module expression is modified, any modules generated for module expressions that depend on $M$ are deleted and any modules that depend on $M$ are reevaluated if you attempt to use them. Here the notion of ``depends on" is transitive through arbitrary nesting of importation and module expressions.

In addition to being imported by the explicit importation statements we have just introduced, modules can be imported in an implicit way (also in the three possible modes) by means of commands set protect/extend/include module on/off; see more details in Section 16.11 and the detailed example in Section 7.1.