During the development of the Maude system we have put special emphasis on the creation of metaprogramming facilities to allow the generation of execution environments for a wide variety of languages and logics. The first most obvious area where Maude can be used as a metalanguage is in building language extensions for Maude itself. Our experience in this regard--first reported in [31], and further documented in [32,27,28,33]--is very encouraging.
We have been able to define in Core Maude a language, that we call Full Maude, with all the features of Maude plus notation for object-oriented programming, parameterized views, module expressions specifying tuples of any size, etc. Although the Maude distribution has included the specification/implementation of Full Maude since it was first distributed in 1999, Core Maude and Full Maude are now closer than ever before. Many of the features now available in Core Maude, like parameterized modules, views, and module expressions like summation, renaming and instantiation, were available in Full Maude long before they were available in Core Maude [31]. In fact, Full Maude has not only been a complement to Core Maude, but also a vehicle to experiment with new language features. Once these features have been mature enough to be implemented in the core language, we have made the effort to do so. Similarly, it is very likely that those features in Full Maude which are not yet available in Core Maude will become part of it sooner or later, and that new features will be added to Full Maude for purposes of language design and experimentation. This applies not only to Full Maude, but also to further language extensions based on Full Maude such as the strategy language proposed in [54], whose Core Maude implementation is currently underway.
Full Maude implements a complete user interface for the extended language. Using the META-LEVEL and LOOP-MODE modules, we have been able to define in Core Maude all the additional functionality required for parsing, evaluating, and pretty-printing modules in the extended language, and also for input/output interaction, as already discussed in Chapter 12. Thanks to the efficient implementation of the rewrite engine, the parser, and the META-LEVEL module, such a language extension executes with reasonable efficiency.
Full Maude contains Core Maude as a sublanguage, so that Core Maude modules can also be entered at the Full Maude level. However, currently there are a few syntactic restrictions that have to be satisfied by modules and commands in order to be acceptable inputs at the Full Maude level, including the fact that Full Maude inputs, for both modules and commands, must be enclosed in parentheses. These syntactic restrictions are explained in Section 14.5.
The structure of this chapter is as follows. Section 14.1 gives instructions on how to load and use Full Maude, how to enter modules, reduce terms, trace executions, etc. Section 14.2 explains how modules in Core Maude's database may be used in Full Maude. Section 14.3 introduces the additional module operations that are available in Full Maude. Section 14.4 explains how to move terms and modules up and down reflection levels. Finally, Section 14.5 enumerates the main differences between Full Maude and Core Maude.