The above examples are toy examples to illustrate the basic features of LOOP-MODE. However, the most interesting applications of this module are metalanguage applications, in which Maude is used to define the syntax, parse, execute, and pretty print the execution results of a given object language or tool. In such applications, most of the hard work is done by the META-LEVEL module, but handling the input/output and maintaining the persistent state of the object language interpreter or tool is done by LOOP-MODE.
The metalanguage uses of Maude are a natural consequence of the good properties of rewriting logic as a logical and semantic framework. Indeed, one of the key goals of rewriting logic from its beginning has been to provide a semantic framework in which many models of computation--particularly concurrent and distributed ones--and languages can be naturally represented. Because of the intrinsic duality between logic and computation that rewriting logic supports, the very same reasons making rewriting logic a suitable semantic framework, make it also an attractive logical framework [32] to represent many different logics.
What is common to all these logical and semantic framework applications is that the models of computation, logics, or languages are represented in rewriting logic by mappings of the form
($) Phi: L --> RWLogic.The representations are typically very simple and natural. They map theories or modules in L to rewrite theories.
For language prototyping purposes, the obvious question to ask is: how can a rewriting logic language best support representation maps of the form ($), so that it becomes a metalanguage in which a very wide variety of programming, specification, and design languages, and of computational and logical systems can be both semantically defined, and implemented in it?
Our answer is: by being reflective. As already explained in Section 2.5, Maude's language design and implementation make systematic use of the fact that rewriting logic is reflective and provide efficient support of reflective computation by means of the META-LEVEL module.
Indeed, using META-LEVEL we can both make the above representation map Phi executable, and we can execute the resulting rewrite theory representing a theory or module in L, thus getting an implementation of L in Maude. Specifically, we can reify a representation map Phi of the form ($) by defining an abstract data type ModuleL representing modules in the logic or language L. Since in META-LEVEL we also have a data type Module whose terms represent rewrite theories, we can then internalize the representation map Phi as an equationally defined function
|¯Phi¯| : ModuleL --> Module.In fact, thanks to the general meta-result of Bergstra and Tucker [1], any computable representation map Phi can be specified in this way by a finite number of Church-Rosser and terminating equations.
Having this representation map defined in Maude, we can then execute in Maude the rewrite theory |¯Phi¯| (M) associated to a theory or module M in L. This has been done, for example, for linear logic in [33, 10], and for structured Maude modules in Full Maude. But it could also be done for a very wide range of other languages and logics using the same method.
By defining the data type ModuleL in an extension of META-LEVEL we can indeed define the syntax of L within Maude. However, to provide a satisfactory execution environment for L in Maude, we also have to support input/output and a persistent state for interacting with the interpreter for L that we want to define. That is, we want to be able to enter module definitions, execute commands, and get results of executions. This is precisely what LOOP-MODE makes possible. As a consequence, an environment for L in Maude will typically be realized by a module containing both META-LEVEL and LOOP-MODE as submodules.
To illustrate the way in which LOOP-MODE can be used in conjunction with META-LEVEL for metalanguage purposes, we discuss in some detail the way in which we make use of it in the implementation of Full Maude. The complete specification can be found in [19]. In Full Maude, the state of the system is given by a single object of class database. This object has attributes db, to keep the actual database in which all the modules being entered are stored, an attribute default, to keep the identifier of the current module by default, and attributes input and output to simplify the communication of the loop with the database. Using the notation for classes in object-oriented modules (see Section 3.2) we can declare the class database as follows23.
class database | db : Database, input : TermList,
output : QidList, default : ModId .
Since we assume that database is the only object class that has been defined--so that the only objects of sort Object will belong to the database class--to specify the admissible states in the persistent state of LOOP-MODE for Full Maude, it is enough to give the subsort declaration
subsort Object < State .
We now give the rules to initialize the loop, and to specify the communication between the loop--the input/output of the system--and the database. Depending on the kind of input that the database receives, its state will be changed or some output will be generated. Before giving the rules we need some declarations. We start declaring a constant o of sort Oid to identify the persistent database object, and a constant init to name the initial value of the loop.
op o : -> Oid . op init : -> System .
The rule specifying the initial value of the loop is given below. In it, initialDatabase is a constant naming the initial database24.
rl [init] :
init
=> [nil,
< o : database |
db : initialDatabase, input : nilTermList,
output : nil, default : nullModId >,
nil] .
To initialize the loop we have to write
Maude> loop init .
When some text has been introduced in the loop, the first argument of the operator [_,_,_] is different from nil, and we can use this fact to activate the following rule, that enters an input such as a module or a command from the user into the database. The constant grammar names the module containing the signature defining the top level syntax of Full Maude (see Appendix C). This grammar is used by the meta-parse function in META-LEVEL to parse the input. In case of being a syntactically valid input, the parsed input is placed in the input attribute of the database object; otherwise, an error message is placed in the output channel of the loop.
crl [in] :
[QIL,
< o : database | db : DB,
input : nilTermList,
output : nil,
default : MI >,
QIL']
=> if meta-parse(grammar, QIL) == error*
then [nil,
< o : database | db : DB,
input : nilTermList,
output : ('ERROR: 'incorrect 'input '.),
default : MI >,
QIL']
else [nil,
< o : database | db : DB,
input : meta-parse(grammar, QIL),
output : nil,
default : MI >,
QIL']
fi
if QIL =/= nil .
When the output attribute of the persistent object contains a nonempty list of quoted identifiers, the out rule moves it to the third argument of the loop. Then the Core Maude system displays it in the terminal.
crl [out] :
[QIL,
< o : database | db : DB, input : TL,
output : QIL', default : MI >,
QIL'']
=> [QIL,
< o : database | db : DB, input : TL,
output : nil, default : MI >,
(QIL' QIL'')]
if QIL' =/= nil .
For each particular language, the rewrite rules defining the system behavior for different language commands are specified according to the specific details of the language in question. We illustrate below the case of Full Maude. In Full Maude there is a function processUnit that takes as arguments the result of the call to meta-parse, an empty module of the kind of the module being introduced--named by the constant emptyStrFModule in the rule below--and the current database. It returns a modified copy of the database after processing the new module. Thus, for example, for the case of the constructor of functional modules in the module grammar
op fmod_is_endfm : Token DeclList -> PreModule .
the processing of a functional PreModule once it has been entered
into the system is done by the rule
rl [functional-module] :
< o : database | db : DB,
input : ('fmod_is_endfm[T, T']),
output : nil,
default : MI >
=> < o : database |
db : processUnit(T, T', emptyStrFModule, DB),
input : nilTermList,
output : ('Introduced 'module:
modIdToQid(parseModName(T))),
default : parseModName(T) > .
Note the message placed in the output channel, and the change in the current
module by default, which is now the new module just processed. Since the name
T of the module can be complex--a module expression--, some extra
parsing has to be performed by the auxiliary function parseModName.
User-defined commands are handled by rules as well. For example, the show module command, which prints the specified module, or the current one if no module name is specified, is handled by the following rules.
rl [show-module-1] :
< o : database | db : DB,
input : ({'show`module`.}'PreCommand),
output : nil, default : MI >
=> < o : database |
db : DB, input : nilTermList,
output : meta-pretty-print(
getFlatModule(MI, DB),
getTopModule(MI, DB)),
default : MI > .
rl [show-module-2] :
< o : database | db : DB, input : ('show`module_.[T]),
output : nil, default : MI >
=> < o : database |
db : DB, input : nilTermList,
output : meta-pretty-print(
getFlatModule(parseModExp(T), DB),
getTopModule(parseModExp(T), DB)),
default : MI > .
The functions getTopModule and getFlatModule return, respectively, the module as introduced by the user and its flattened version25 as stored in the database.