The Maude system is built around the Core Maude interpreter, which accepts module hierarchies of (unparameterized) functional and system modules with user-definable mixfix syntax. It is implemented in C++ and consists of two parts: the rewrite engine and the mixfix front end.
The rewrite engine is highly modular and does not contain any Maude-specific code. Two key components are the "core" module and the "interface" module. The core module contains classes for objects which are not specific to an equational theory, such as equations, rules, sorts, and connected sort components. The "interface" module contains abstract base classes for objects that may have a different representation in different equational theories, such as symbols, term nodes, dag nodes, and matching automata. New equational theories can be "plugged in" by deriving from the classes in the "interface" module. To date, all combinations of associativity, commutativity, left and right identity, and idempotence have been implemented apart from those that contain both associativity and idempotence. New built-in symbols with special rewriting (equation or rule) semantics may be easily added.
The engine is designed to provide the look and feel of an interpreter with hooks for source level tracing/debugging and user interrupt handling. These goals prevent a number of optimizations that one would normally implement in a compiler, such as transforming the user's term rewriting system, or keeping pending evaluations on a stack and only building reduced terms. The actual implementation is a semi-compiler where the term rewriting system is compiled to a system of tables and automata, which is then interpreted. Typical performance with the current version is 800K-840K free-theory2 rewrites per second and 27K-111K associative-commutative (AC) rewrites per second on standard hardware (300 MHz Pentium II). The figure for AC rewriting is highly dependent on the complexity of the AC patterns (AC matching is NP-complete) and the size of the AC subjects. These results were obtained using fairly simple linear and nonlinear patterns and large (hundreds of nested AC operators) subjects.
The mixfix front end consists of a bison/flex based parser for Maude's surface syntax, a grammar generator (which generates the context-free grammar (CFG) for the mixfix parts of Maude over the user's signature), a context-free parser, a mixfix pretty printer, a fully reentrant debugger, the built-in functions for quoted identifiers, and the META-LEVEL module, together with a considerable amount of "glue" code holding everything together. Many of the C++ classes are derived from those in the rewrite engine. The Maude parser (MSCP) is implemented using SCP as the formal kernel [54]. The techniques used include beta-extended CFGs (that is, CFGs extended with "bubbles" (strings of identifiers) and precedence/gathering patterns). MSCP provides a basis for flexible syntax definition, and an efficient treatment of what might be called syntactic reflection, which is very useful for parsing inputs in extensions of Core Maude such as Full Maude, and in other languages with user-definable syntax that can likewise be implemented in Maude. The point is that we often need to parse the top level syntax, for example of a module, and then extract from it the grammar in which to parse the user-definable expressions in that module.
The functional module META-LEVEL efficiently implements key functionality of the universal theory U. In META-LEVEL Maude terms are reified as elements of a data type Term, and Maude modules are reified as terms in a data type Module. The processes of reducing a term to normal form in a functional module and of rewriting a term in a system module using Maude's default interpreter are respectively reified by functions meta-reduce and meta-rewrite. Similarly, the process of applying a rule of a system module to a subject term is reified by a function meta-apply. Furthermore, parsing and pretty printing of a term in a signature, as well as key sort operations, are also reified by corresponding metalevel functions.