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 [18], and further documented here and in [19]--is very encouraging. We have been able to define in Core Maude a language extension with notation for object-oriented programming, parameterized modules, views (for module instantiation) and module expressions [18]. Furthermore, using the META-LEVEL and LOOP-MODE modules, we have also 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 Sections 2.5.6 and 2.8.
Thanks to the efficient implementation of the rewrite engine, the parser, and the module META-LEVEL, such a language extension executes with reasonable efficiency. In the future, however, we may support in Core Maude a significant part of the functionality currently supported by Full Maude. Full Maude contains Core Maude as a sublanguage, so that Core Maude modules can also be entered at the Full Maude level. However, at present 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. These syntactic restrictions are explained in Section 3.6; they will be removed in the future.
Since the execution environment for Full Maude has been implemented in Core Maude, to initialize the system so that we can start using it, the first thing we have to do is to load the FULL-MAUDE module in the system. Assuming that the file full-maude.maude, containing such specification, is located in the current directory, we just need to type the corresponding in command in the Maude prompt.
Maude> in full-maude.maudeThe Full Maude system is then loaded and we can use it as any other module. Before entering any module or executing any command in Full Maude we need to initialize the system. Full Maude uses the LOOP-MODE module in order to allow the entering of modules into the system and to maintain a persistent database in which to store all the modules, theories and views being introduced. To start the loop we need to type
Maude> loop init .where init is a constant of sort System giving the initial state of the Full Maude database.
We are now ready. Let us recall from Section 2.8 that to get something into the LOOP-MODE system, the text has to be enclosed in parentheses. This means that any module or command intended for Full Maude has to be written enclosed in parentheses. Notice that, since Core Maude is still active--indeed, it now provides what might be called the system programming level--it will handle any input not enclosed in parentheses. This allows the possibility of using both systems at the same time.