Chapter 19

The META-LEVEL module is purely functional. This is because all its descent functions are deterministic, even though they may manipulate intrinsically nondeterministic entities such as rewrite theories. For example, the metaSearch descent function with a bound of, say, 3, is entirely deterministic, since given the meta-representations of the desired system module and t of the initial term plus the bound 3, the result yielded by search for , t and 3 at the object level, and therefore by metaSearch at the metalevel, is uniquely determined.

Although META-LEVEL is very powerful, its purely functional nature means that it has no notion of state. Therefore, reflective applications where user interaction in a state-changing manner is essential require using META-LEVEL in the context of additional features supporting such an interaction. Maude’s meta-interpreters feature makes possible very flexible kinds of reflective interactions in which Maude interpreters are encapsulated as external objects and can reflectively interact with both other Maude interpreters and with various other external objects, including the user.

19.1 Maude meta-interpreters

Conceptually a meta-interpreter is an external object that is an independent Maude interpreter, complete with module and view databases, which sends and receives messages. The module META-INTERPRETER in the meta-interpreter.maude file contains command and reply messages that cover almost the entirety of the Maude interpreter. For example, it can be instructed to insert or show modules and views, or carry out computations in a named module. As response, the meta-interpreter replies with messages acknowledging operations carried out or containing results. Meta-interpreters can be created and destroyed as needed, and because a meta-interpreter is a complete Maude interpreter, it can host meta-interpreters itself and so on in a tower of reflection. Furthermore, the original META-LEVEL functional module can itself be used from inside a meta-interpreter after it is inserted.

Internally, the guts of the Maude interpreter implementation are encapsulated in a C++ class called Interpreter and the top-level interpreter that one interacts with on the command line is an instance of this class together with a small amount of glue code that enables it to communicate over the standard I/O streams. Meta-interpreters are also instances of this class, with a small amount of glue code that enables them to exchange messages with an enclosing object-oriented rewriting execution context. Currently, both the object-level interpreter and any existing meta-interpreters all run the same single threaded process, and control flow is managed through the object-oriented rewriting mechanism.

The metarepresentation of terms, modules, and views is shared with the META-LEVEL functional module in Chapter 17. The API to meta-interpreters defined in the META-INTERPRETER module includes several sorts and constructors, a built-in object identifier interpreterManager, and a large collection of command and response messages (see file meta-interpreter.maude for the complete details).

protecting META-LEVEL .

sort RewriteCount .
subsort Nat < RewriteCount .
sorts InterpreterOption InterpreterOptionSet .
subsort InterpreterOption < InterpreterOptionSet .

op none : -> InterpreterOptionSet [ctor] .
op interpreter : Nat -> Oid [ctor] .

op createInterpreter : Oid Oid InterpreterOptionSet -> Msg [ctor msg ...] .
op createdInterpreter : Oid Oid Oid -> Msg [ctor msg ...] .

op insertModule : Oid Oid Module -> Msg [ctor msg ...] .
op insertedModule : Oid Oid -> Msg [ctor msg ...] .
op insertView : Oid Oid View -> Msg [ctor msg ...] .
op insertedView : Oid Oid -> Msg [ctor msg ...] .
op erewriteTerm : Oid Oid Bound Nat Qid Term -> Msg [ctor msg ...] .
op erewroteTerm : Oid Oid RewriteCount Term Type -> Msg [ctor msg ...] .
op quit : Oid Oid -> Msg [ctor msg ...] .
op bye : Oid Oid -> Msg [ctor msg ...] .
op interpreterManager : -> Oid [special (...)].

All messages in this module follow the standard Maude message format, with the first two arguments being the object identifiers of the target and of the sender. The interpreterManager object identifier refers to a special external object that is responsible for creating new meta-interpreters in the current execution context. Such meta-interpreters have object identifiers of the form interpreter(n) for any natural number n.

19.2 A Russian dolls example

Let us illustrate the flexibility and generality of meta-interpreters with a short example. The example, which we call RUSSIAN-DOLLS after the Russian nesting dolls, performs a computation in a meta-interpreter that itself exists in a tower of meta-interpreters nested to a user-definable depth and requires only two equations and two rules.


op me : -> Oid .
op User : -> Cid .
op depth:_ : Nat -> Attribute .
op computation:_ : Term -> Attribute .

vars X Y Z : Oid .
var AS : AttributeSet .
var N : Nat .
var T : Term .

op newMetaState : Nat Term -> Term .
eq newMetaState(0, T) = T .
eq newMetaState(s N, T)
= upTerm(
< me : User | depth: N, computation: T >
createInterpreter(interpreterManager, me, none)) .

rl < X : User | AS >
createdInterpreter(X, Y, Z)
=> < X : User | AS >
insertModule(Z, X, upModule(’RUSSIAN-DOLLS, true)) .
rl < X : User | depth: N, computation: T, AS >
insertedModule(X, Y)
=> < X : User | AS >
erewriteTerm(Y, X, unbounded, 1, RUSSIAN-DOLLS, newMetaState(N, T)) .

The visible state of the computation resides in a Maude object of identifier me and class User. The object holds two values in respective attributes: the depth of the meta-interpreter, which is recorded as a Nat, with 0 as the top level, and the computation to perform, which is recorded as a Term.

The operator newMetaState takes a depth and a metaterm to evaluate. If the depth is zero, then it simply returns the metaterm as the new metastate; otherwise, a new configuration is created, consisting of a portal (needed for rewriting with external objects to locate where messages exchanged with external objects leave and enter the configuration), the user-visible object holding the decremented depth and computation, and a message addressed to the interpreterManager external object, requesting the creation of a new meta-interpreter, and this configuration is lifted to the metalevel using the built-in upTerm operator imported from the functional metalevel.

The first rule of the RUSSIAN-DOLLS module handles the createdInterpreter message from interpreterManager, which carries the object identifier of the newly created meta-interpreter. It uses upModule to lift its own module, RUSSIAN-DOLLS, to the metalevel and sends a request to insert this meta-module into the new meta-interpreter. The second rule handles the insertedModule message from the new meta-interpreter. It calls the newMetaState operator to create a new metastate and then sends a request to the new meta-interpreter to perform an unbounded number of rewrites, with external object support and one rewrite per location per traversal in the metalevel copy of the RUSSIAN-DOLLS module that was just inserted.

We start the computation with an erewrite command on a configuration that consists of a portal, a user object, and a createInterpreter message:

Maude> erewrite
< me : User | depth: 0, computation: (’_+_[’s_^2[’0.Zero], s_^2[’0.Zero]]) >
createInterpreter(interpreterManager, me, none) .
result Configuration:
< me : User | none >
erewroteTerm(me, interpreter(0), 1, s_^4[’0.Zero], NzNat)

With depth 0, this results in the evaluation of the meta-representation of 2 + 2 directly in a meta-interpreter, with no nesting. Passing a depth of 1 results in the evaluation instead being done in a nested meta-interpreter.

Maude> erewrite
< me : User | depth: 1,
computation: (’_+_[’s_^2[’0.Zero],’s_^2[’0.Zero]]) >
createInterpreter(interpreterManager, me, none) .
result Configuration:
< me : User | none >
erewroteTerm(me, interpreter(0), 5,
_‘[_‘][’’s_^4.Sort,’’0.Zero.Constant],’’NzNat.Sort]], Configuration)

Notice here that the top-level reply message erewroteTerm(...) contains a result that is a metaconfiguration, which contains the reply ’erewroteTerm[...] metamessage from the inner meta-interpreter.

Additional examples of the use of standard streams and meta-interpreters can be found in the next section, where they are used to develop a simple execution environment.

19.3 An execution environment for Mini-Maude using IO and meta-interpreters

We illustrate in this section the use of standard streams and meta-interpreters to develop programming environments for our languages. Specifically, we present an environment for the MiniMaude language introduced in Section 18.3. The same techniques may be used to develop your language of choice. Once you have defined a grammar (MINI-MAUDE-SYNTAX in the case of MiniMaude) and a transformation from parse terms to Maude (as provided by the processModule operation in the MINI-MAUDE module) you can build an execution environment using the techniques shown in this section.

The MiniMaude language has been designed to be as simple as possible, but there were several features we wanted it to include:

As pointed out in the previous section, the main difference between the metalevel and a meta-interpreter is that the metalevel is functional but the meta-interpreter is not, and we can interact with it through messages. Being non-functional, meta-interpreters provide functionality, for instance, to store modules and views in its database, and then operate on them. We will use that functionality in this section to illustrate its use and some of its possibilities. Indeed, meta-interpreters provide the same functionality as the metalevel, plus some additional features to insert elements in its database and retrieve them. In other words, we can say that it provides the desired functionality at both the object level and at the metalevel.

In our case, we will store a minimum of information in an object that will request inputs from the user using the standard input stream and will attempt to parse it in the MiniMaude grammar. To be able to parse inputs using the meta-interpreter, we will start by introducing the MINI-MAUDE-SYNTAX module in it. Once it is there, we can try to parse the inputs. When the standard stream receives a getLine message, it responds with the string typed by the user until a return key is pressed. To be able to parse multi-line inputs, we will need to request new lines until the input is completed. Of course, at any time we may get a parse error or an ambiguity, in which cases we need to report the given error.

Once the input is completed, we may have a module or a reduce command. If it is a module, we need to extract the signature first and then to solve the bubbles in its equations. The process must be carried out in two steps, since the signature may refer to submodules in the database of the meta-interpreter, but the equations with the bubbles processed are to be inserted in the top module. If the input corresponds to a reduce command, the term must be parsed, and then reduced by the meta-interpreter.

Although the process is quite systematic, different cases must be taken into account. To simplify the processing, we use an attribute state that keeps track of the different alternatives. Figure 19.1 shows a state diagram of the execution environment. This object also keeps the identifier of the meta-interpreter, the name of the last entered module, and the partial input introduced.


Figure 19.1:MiniMaude’s statechart.

view Oid from TRIV to CONFIGURATION is
sort Elt to Oid .

view Module from TRIV to META-MODULE is
sort Elt to Module .

protecting MINI-MAUDE .
including STD-STREAM .
including LEXICAL .
including MAYBE{Oid} * (op maybe to null) .
including MAYBE{Qid} * (op maybe to null) .
including MAYBE{Module} * (op maybe to null) .

vars O O MI Y : Oid .
var Atts : AttributeSet .
var QIL : QidList .
var Str : String .
vars T T : Term .
vars Ty Ty : Type .
var N : Nat .
var RP? : [ResultPair] .
var M : Module .
var M? : Maybe{Module} .
vars QI? : Maybe{Qid} .
vars QI MN : Qid .
var EqS : EquationSet .

MiniMaude objects are represented using the following declarations.

sort MiniMaude .
subsort MiniMaude < Cid .
op MiniMaude : -> MiniMaude .
op mi:_ : Maybe{Oid} -> Attribute [prec 20 gather (&)] . ---- meta-interpreter
op mn:_ : Maybe{Qid} -> Attribute [prec 20 gather (&)] . ---- default module name
op in:_ : QidList -> Attribute [prec 20 gather (&)] . ---- accumulated input
op st:_ : Nat -> Attribute [prec 20 gather (&)] . ---- state

Several messages are used for intermediate steps.

op processInput : Oid Term -> Msg .
op pendingBubbles : Oid Term -> Msg .
op parsedEquations : Oid EquationSet -> Msg .
op processReduce : Oid [ResultPair] -> Msg .

The MiniMaude environment may be initiated using the minimaude constants, with it an interpreter is created and a banner is sent to the output stream.

op o : -> Oid .
op minimaude : -> Configuration .

eq minimaude
= <>
< o : MiniMaude | mi: null, mn: null, in: nil, st: 0 >
write(stdout, o, "’\n\t MiniMaude Execution Environment\n")
createInterpreter(interpreterManager, o, none) .

Once the message is written and the meta-interpreter created, the MINI-MAUDE-SYNTAX module is inserted in the meta-interpreter. The second argument of the createdInterpreter message is, as usual, the sender (interpreterManager in this case).

rl < O : MiniMaude | mi: null, st: 0, Atts >
wrote(O, O’)
createdInterpreter(O, Y, MI)
=> < O : MiniMaude | mi: MI, st: 1, Atts >
insertModule(MI, O, upModule(’MINI-MAUDE-SYNTAX, true)) .

Once the module is inserted, a getLine message is sent to the stdin object.

rl < O : MiniMaude | mi: MI, st: 1, Atts >
insertedModule(O, O’)
=> < O : MiniMaude | mi: MI, st: 2, Atts >
getLine(stdin, O, "minimaude> ") .

When the user introduces some inputs, the stdin object responds with a gotLine message with the string entered. The user is expected to write quit or q to leave the environment. If the input is one of these, a goodbye message is sent to the stdout object and the meta-interpreter is killed. Otherwise, an attempt is made to parse the input. Note that some previous inputs may be stored in the in attribute, so the message to the meta-interpreter to parse the input includes the entire Qid list.

rl < O : MiniMaude | mi: MI, in: QIL, st: 2, Atts >
gotLine(O, O’, Str)
=> if tokenize(Str) == quit or tokenize(Str) == q
then < O : MiniMaude | mi: MI, in: nil, st: 3, Atts >
write(stdout, o, "goodbye\n")
quit(MI, O)
else < O : MiniMaude | mi: MI, in: QIL tokenize(Str), st: 4, Atts >
parseTerm(MI, O, MINI-MAUDE-SYNTAX, none, QIL tokenize(Str), Input)
fi .

If a quit message was sent to the meta-interpreter, it would respond with a bye message. This is the final rule, which terminates the execution.

rl < O : MiniMaude | mi: MI, st: 3, Atts >
wrote(O, O’)
bye(O, MI)
=> none .

If the parse succeeded, the meta-interpreter responds with a parsedTerm message that includes a term of sort ResultPair. This term in that pair is sent in a processInput message.

rl < O : MiniMaude | mi: MI, in: QIL, st: 4, Atts >
parsedTerm(O, MI, {T, Ty})
=> < O : MiniMaude | mi: MI, in: nil, st: 6, Atts >
processInput(O, T) .

If the parse failed, the parsedTerm message from the meta-interpreter includes a noParse term with the position at which the parsing failed. If the position is the end of the input it means that the input was incomplete, and in that case that partial input is added to the current input and additional text is requested from the user. If the error was in some other position, an error message is sent.

rl < O : MiniMaude | mi: MI, in: QIL, st: 4, Atts >
parsedTerm(O, MI, noParse(N))
=> if N == size(QIL)
then < O : MiniMaude | mi: MI, in: QIL, st: 2, Atts >
getLine(stdin, O, "> ")
else < O : MiniMaude | mi: MI, in: nil, st: 5, Atts >
write(stdout, o, "Parse error\n")
fi .

The response may also be informing about an ambiguity. Although more precise information might be given to the user, we have simplified the error message.

rl < O : MiniMaude | mi: MI, in: QIL, st: 4, Atts >
parsedTerm(O, MI, ambiguity({T, Ty}, {T’, Ty’}))
=> < O : MiniMaude | mi: MI, in: nil, st: 5, Atts >
write(stdout, o, "Ambiguous input\n") .

The processInput message may correspond to a functional module or to a reduce command. In the first case, if the input contains a valid signature, such a module is inserted in the meta-interpreter. The input is kept in a pendingBubbles message for later processing.

rl < O : MiniMaude | mi: MI, mn: QI?, st: 6, Atts >
processInput(O, fmod_is_endfm[’token[T], T’])
=> if extractSignature(’fmod_is_endfm[’token[T], T’]) :: Module
then < O : MiniMaude | mi: MI, mn: downTerm(T, default-name), st: 7, Atts >
insertModule(MI, O, extractSignature(’fmod_is_endfm[’token[T], T’]))
pendingBubbles(O, T’)
else < O : MiniMaude | mi: MI, mn: QI?, st: 5, Atts >
write(stdout, o, "Parse error\n")
fi .

Once the signature is inserted, the MiniMaude object requests the flattened module. If the module contains importations of previously entered modules, the entire module must be used for the processing of the bubbles in the top module.

rl < O : MiniMaude | mi: MI, mn: QI, st: 7, Atts >
insertedModule(O, MI)
=> < O : MiniMaude | mi: MI, mn: QI, st: 8, Atts >
showModule(MI, O, QI, true) .

The retrieved flattened module is then used to process the bubbles in the equations of the module. If the processing fails, an error message is shown to the user. If it succeeded, the top module is requested so that the equations can be added to it.

rl < O : MiniMaude | mi: MI, mn: QI, st: 8, Atts >
showingModule(O, MI, M)
pendingBubbles(O, T)
=> if solveBubblesAux(T, M) :: EquationSet
then < O : MiniMaude | mi: MI, mn: QI, st: 9, Atts >
parsedEquations(O, solveBubblesAux(T, M))
showModule(MI, O, QI, false)
else < O : MiniMaude | mi: MI, mn: QI, st: 5, Atts >
write(stdout, o, "Parse error\n")
fi .

The top module is inserted in the meta-interpreter once the processed equations are added to it.

rl < O : MiniMaude | mi: MI, mn: QI, st: 9, Atts >
showingModule(O, MI, M)
parsedEquations(O, EqS)
=> < O : MiniMaude | mi: MI, mn: QI, st: 10, Atts >
insertModule(MI, O, addEquations(M, EqS)) .

When the insertion is completed with success, the user is informed.

rl < O : MiniMaude | mi: MI, st: 10, Atts >
insertedModule(O, MI)
=> < O : MiniMaude | mi: MI, st: 5, Atts >
write(stdout, O, "Module loaded successfully\n") .

As can be seen in Figure 19.1, state 5 is the one to which the object returns every time an operation concludes, either with a failure or success, after notifying the user, and then requesting further inputs.

rl < O : MiniMaude | mi: MI, st: 5, Atts >
wrote(O, O’)
=> < O : MiniMaude | mi: MI, st: 2, Atts >
getLine(stdin, O, "minimaude> ") .

The input may also correspond to a reduce command. The following rule handles the case in which a command is introduced but there is no previous module inserted on which the command can be evaluated.

rl < O : MiniMaude | mn: null, st: 6, Atts >
processInput(O, reduce_.[T])
=> < O : MiniMaude | mn: null, st: 5, Atts >
write(stdout, o, "No module in the system\n") .

If there is a previous module, the term to be reduced must first be parsed.

rl < O : MiniMaude | mi: MI, mn: MN, st: 6, Atts >
processInput(O, reduce_.[’bubble[T]])
=> < O : MiniMaude | mi: MI, mn: MN, st: 11, Atts >
parseTerm(MI, O, MN, none, downTerm(T, nil), anyType) .

The parsing of the term may result in success or failure. In the first case, a reduceTerm message is sent to the meta-interpreter. In the second case, an error message is given.

rl < O : MiniMaude | mi: MI, mn: MN, st: 11, Atts >
parsedTerm(O, MI, {T, Ty})
=> < O : MiniMaude | mi: MI, mn: MN, st: 12, Atts >
reduceTerm(MI, O, MN, T) .

rl < O : MiniMaude | mi: MI, mn: MN, st: 11, Atts >
parsedTerm(O, MI, noParse(N))
=> < O : MiniMaude | mi: MI, st: 5, Atts >
write(stdout, o, "Parse error\n") .

Once the simplification command is completed, the meta-interpreter sends back a reducedTerm message with the result of the execution. Before showing the result to the user, the pretty-printing of the term must be requested to the meta-interpreter.

rl < O : MiniMaude | mi: MI, mn: MN, st: 12, Atts >
reducedTerm(O, MI, N, T, Ty)
=> < O : MiniMaude | mi: MI, mn: MN, st: 13, Atts >
reducedTerm(O, MI, N, T, Ty)
printTerm(MI, O, MN, none, T, mixfix flat format number rat) .

rl < O : MiniMaude | mi: MI, st: 13, Atts >
reducedTerm(O, MI, N, T, Ty)
printedTerm(O, MI, QIL)
=> < O : MiniMaude | mi: MI, st: 5, Atts >
write(stdout, o, "result " + string(Ty) + ": " + printTokens(QIL) + "\n") .

We can run the environment with the minimaude configuration.

Maude> erew minimaude .
erewrite in MINI-MAUDE-META-INTERPRETER : minimaude .

MiniMaude Execution Environment

First, let us introduce a simple example, the NAT3 module already used in Section 18.3.

> fmod NAT3 is
> sort Nat3 .
> op s_ : Nat3 -> Nat3 .
> op 0 : -> Nat3 .
> eq s s s 0 = 0 .
> endfm
Module loaded successfully

We can execute a simple command on that module as follows.

minimaude> reduce s s s s 0 .
result Nat3: s 0

A more interesting module refers to the previous one, extending it with a plus operation.

minimaude> fmod NAT3+ is
> including NAT3 .
> op _+_ : Nat3 Nat3 -> Nat3 .
> eq 0 + N:Nat3 = N:Nat3 .
> eq s N:Nat3 + M:Nat3 = s (N:Nat3 + M:Nat3) .
> endfm
Module loaded successfully

minimaude> reduce s s 0 + s 0 .
result Nat3: 0

If wrong inputs are inserted, an error message is provided.

minimaude> reduce foo .
Parse error

We can finally exit the environment with a q command.

minimaude> q
rewrites: 643 in 10ms cpu (128883ms real) (62885 rewrites/second)
result Portal: <>