2.5.2 The Module META-LEVEL

In Maude, key functionality of a metalevel theory M with several descent functions has been efficiently implemented in a functional module META-LEVEL, by using as the interpreter function I Maude's own interpreter. Furthermore, several other useful functions of the universal theory U are also built-in for efficiency reasons.

We summarize below the key functionality provided by META-LEVEL. We recall that Maude's functional modules are equational theories that are assumed to be Church-Rosser and terminating modulo some axioms for which matching algorithms are available in the implementation, and that system modules are rewrite theories whose equational part satisfies the same requirements as a functional module, and where the equations and the rules are assumed to be weakly coherent [61, 60] modulo the axioms (see Section 4.3). In META-LEVEL:

• Maude terms are reified as elements of a data type Term of terms;
• Maude modules are reified as terms in a data type Module of modules;
• the processes of reducing a term to normal form in a functional module and of finding whether such a normal form has a given sort are reified by a descent function meta-reduce;
• the process of applying a rule of a system module to a subject term is reified by a descent function meta-apply;
• the process of rewriting a term in a system module using Maude's default interpreter is reified by a descent function meta-rewrite; and
• parsing and pretty printing of a term in a module, as well as key sort operations such as comparing sorts in the subsort ordering of a signature, are also reified by corresponding metalevel functions.

META-LEVEL imports the module QID-LIST (lists of quoted identifiers) from the standard library of predefined modules, which contains in turn the modules QID, MACHINE-INT, and BOOL. We first introduce the syntax used in META-LEVEL for representing terms; then we explain how modules are represented; and finally we discuss the different built-in functions, namely, the descent functions, and the parsing and sort functions.