, the first thing we need to do is to
define the language for interaction. This can be done by defining a data type Sign
for commands
and other constructs.
This chapter explains how to use the facilities provided by the predefined modules META-LEVEL and LOOP-MODE for constructing user interfaces and metalanguage applications, in which Maude is used not only to define a domain-specific language or tool, but also to build an environment for the given language or tool. In such applications, the LOOP-MODE module can be used to handle the input/output and to maintain the persistent state of the language environment or tool.
Using object-oriented concepts, we specify in Maude a general input/output facility provided by the LOOP-MODE module shown below, which extends the module QID-LIST (see Section 7.10), into a generic read-eval-print loop.
The operator [_,_,_] can be seen as an object—that we call the loop object—with an input stream (the first argument), an output stream (the third argument), and a state (given by its second argument). This read-eval-print loop provided by LOOP-MODE is a simple mechanism that may not be maintained in future versions, because the support for communication with external objects (see Section 8.4) makes it possible to develop more general and flexible solutions for dealing with input/output in future releases.
Since in the current release only one input stream is supported (the current terminal), the way to distinguish the input passed to the loop object from the input passed to the Maude system—either modules or commands—is by enclosing them in parentheses. When something enclosed in parentheses is written after the Maude prompt, it is converted into a list of quoted identifiers. This is done by the system by first breaking the input stream into a sequence of Maude identifiers (see Section 3.1) and then converting each of these identifiers into a quoted identifier by putting a quote in front of it, and appending the results into a list of quoted identifiers, which is then placed in the first slot of the loop object. The output is handled in the reverse way, that is, the list of quoted identifiers placed in the third slot of the loop object is displayed on the terminal after applying the inverse process of “unquoting” each of the identifiers in the list. However, the output stream is not cleared at the time when the output is printed; it is instead cleared when the next input is entered. We can think of the input and output events as implicit rewrites that transfer—in a slightly modified, quoted or unquoted form—the input and output data between two objects, namely the loop object and the “user” or “terminal” object.
Besides having input and output streams, terms of sort System give us the possibility of maintaining a state in their second component. This state has been declared in a completely generic way. In fact, the sort State in LOOP-MODE does not have any constructors. This gives complete flexibility for defining the terms we want to have for representing the state of the loop in each particular application. In this way, we can use this input/output facility not only for building user interfaces for applications written in Maude, but also for uses of Maude as a metalanguage, where the object language being implemented may be completely different from Maude. For each such tool or language the nature of the state of the system may be completely different. We can tailor the State sort to any such application by importing LOOP-MODE in a module in which we define the state structure and the rewrite rules for changing the state and interacting with the loop.
In order to generate in Maude an interface for an application , the first thing we need to do is to
define the language for interaction. This can be done by defining a data type Sign for commands
and other constructs.
As a running example for this chapter, we will specify a basic interface for the vending machine introduced in Section 5.1. First, we define in the module VENDING-MACHINE-GRAMMAR a language for interacting with the vending machine. The signature of this module extends the signature of VENDING-MACHINE-SIGNATURE with operators to represent the valid actions, namely: $ and q for inserting a dollar or a quarter in the machine; showBasket and showCredit for showing the items already bought or the remaining credit; buy1Apple and buy1Cake for buying an apple or a cake; and buy_:_ for buying a number of pieces of the same item.
Next, we define in an extension of the LOOP-MODE module the terms of sort State representing the state of the loop for this application. In the module VENDING-MACHINE-INTERFACE below, we define this state as a triple: its first component is the next action requested by the client (inserting a coin, showing information about the remaining credit or the items already bought, or buying one or more items); its second component is the current state of the machine (the marking of the vending machine, that is, the remaining credit plus the items already bought); and its third component represents the response of the machine to the last action requested by the client. The response of the vending machine will have the form of a message, which can be represented as a list of quoted identifiers. The constant init denotes the initial state of the whole system, including the empty input and output streams and the “empty” initial state of the vending machine.
Now we define in this module, using rewrite rules, the interaction of the state of the vending machine with the loop—and, consequently, with the client—and the changes produced in the state of the vending machine by the actions requested by the client. As explained before, the client will request an action by enclosing the text in parentheses, which will then be converted into a list of quoted identifiers and placed in the first slot of the loop object. The rule in detects when a valid request has been introduced by the user and, if the vending machine is idle, passes it as the next action to be attempted. To define the interaction of the state of the vending machine with the client, we can use the strategies introduced in the BUYING-STRATS module described in Section 11.6. Recall that BUYING-STRATS includes the META-LEVEL module.
In the rule in below, the operation metaParse checks whether the input stream corresponds to a term of sort Action. If this is the case, metaParse returns the metarepresentation of that term, which is then “moved down” using the META-LEVEL function downTerm (see Section 11.5.1), and is placed in the action slot of the State triple; otherwise, an error message is placed in its output.
For the other direction of the interaction, the rule out detects when the vending machine has a response to be output and, in that case, it places it in the output slot of the loop object.
Next, we define the effects of the different actions on the state of the vending machine. The rules showBasket and showCredit extract the information about the remaining credit or the items already bought, and place it in the output slot of the state; the rule out will then take care of moving it to the output slot of the loop object. In the definitions of the auxiliary functions showBasket and showCredit, the operation metaPrettyPrint takes the metarepresentation of a coin or an item, and returns the list of quoted identifiers that encode the list of tokens produced by pretty-printing the coin or the item in the module VENDING-MACHINE-SIGNATURE. Coins and items, and, more generally, markings of a vending machine are metarepresented using the META-LEVEL function upTerm (see Section 11.5.1).
The rules labeled insertCoin implement the actions of inserting a dollar or a quarter in the vending machine. The strategy insertCoin defined in the module BUYING-STRATS (see Section 11.6) is used to produce the corresponding change in the current marking of the vending machine. Since strategies are applied at the metalevel, both the marking of the vending machine and the coin to be inserted must be first metarepresented using again the META-LEVEL function upTerm.
The rules buy1Cake, buy1Apple, and buyNitems implement the actions of buying one or more items. The strategy onlyNitems defined in the module BUYING-STRATS (see Section 11.6) is used to produce the corresponding change in the current marking of the vending machine. Again, since strategies are applied at the metalevel, the marking of the vending machine must be first metarepresented.
We illustrate the basic ideas of using the loop with a sample session with the interface for the vending machine. Once the VENDING-MACHINE-INTERFACE module has been entered, we must first initialize the loop by setting its initial state by means of the loop command.
We can inspect the state of the loop with the continue command, abbreviated cont, as follows:
Once the loop has been initialized, we can input any data by writing it after the prompt enclosed in parentheses. For example,
Note that, as already mentioned, the data in the output stream remains there after being printed; it is removed at the time of the next input event.
The example presented in the previous sections is a toy example to illustrate the basic features of the LOOP-MODE module. 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. Full Maude (see Chapter 15) is entirely implemented in Maude using the methodology explained in this section.
In order to generate in Maude an environment for a language 
, including the case of a language
with user-definable syntax, the first thing we need to do is to define the syntax for -modules. This
can be done by defining a data type Sign
for -modules, and with auxiliary declarations for
commands and other constructs. Maude provides great flexibility to do this, thanks to
its mixfix front-end and to the use of bubbles (any non-empty list of Maude identifiers).
The intuition behind bubbles is that they correspond to pieces of a module in a language
that can only be parsed once the grammar introduced by the signature of the module is
available.
The idea is that, for a language that allows modules with user-definable syntax—as it is the case for Maude itself—it is natural to see its syntax as a combined syntax at two different levels: what we may call the top-level syntax of the language, and the user-definable syntax introduced in each module. The bubble data type allows us to reflect this duality of levels in the syntax definition by encapsulating portions of (as yet unparsed) text in the user-definable syntax. Similar ideas have been exploited using ASF+SDF [32, 33].
To illustrate this concept, suppose that we want to define the syntax of Maude in Maude. Consider the following Maude module:
Notice that the lists of characters inside the boxes are not part of the top level syntax of Maude and therefore should be treated as bubbles until they are parsed. In fact, they can only be parsed with the grammar associated with the signature of the module NAT3. In this sense, we say that the syntax for Maude modules is a combination of two levels of syntax. The term s s s 0, for example, has to be parsed in the grammar associated with the signature of NAT3. The definition of the syntax of Maude in Maude must reflect this duality of syntax levels.
So far, we have talked about bubbles in a generic way. In fact, there can be many different kinds of bubbles. In Maude we can define different types of bubbles as built-in data types by parameterizing their definition. Thus, for example, a bubble of length one, which we call a token, can be defined as follows:
Any name can be used to define a bubble sort. It is the special attribute
in its constructor declaration that makes the sort Token a bubble sort. The second argument of the id-hook special attribute indicates the minimum and maximum length of such bubbles as lists of identifiers. Therefore, Token has only bubbles of size 1. To specify a bubble of any length we would use the pair of values 1 and -1. The operator used in the declaration of the bubble, in this case the operator token, is a bubble constructor that represents tokens in terms of their quoted form. For example, the token abc123 is represented as token(’abc123).
We can define bubbles of any length, that is, non-empty sequences of Maude identifiers, with the following declarations.
In this case, the system will represent the bubble as a list of quoted identifiers under the constructor bubble. For example, the bubble ab cd ef is represented as bubble(’ab ’cd ’ef).
Different types of bubbles can be defined using the id-hook special attribute Exclude, which takes as parameter a list of identifiers to be excluded from the given bubble, that is, the bubble being defined cannot contain such identifiers. We can, for example, declare the sort NeTokenList with constructor neTokenList as a list of identifiers, of any length greater than one, excluding the identifier ‘.’ with the following declarations.
In general, the syntax Exclude (I1 I2…Ik) is used to exclude identifiers I1,I2,…,Ik inside tokens.
We are now ready to give the signature to parse modules such as NAT3 above. The following module MINI-MAUDE-SYNTAX uses the above definitions of sorts Token, Bubble and NeTokenList to define the syntax of a sublanguage of Maude, namely, many-sorted, unconditional, functional modules, in which the declarations of sorts and operators have to be done one at a time, no attributes are supported for operators, and variables must be declared on-the-fly.
Notice how we explicitly declare operators that correspond to the top-level syntax of Maude, and how we represent as terms of sort Bubble those pieces of the module—namely, terms in equations—that can only be parsed afterwards with the user-defined syntax. The name of the sort PreModule reflects the fact that not all terms of this sort do actually represent Maude modules. In particular, for a term of sort PreModule to represent a Maude module all the bubbles must be correctly parsed as terms in the module’s user-defined syntax.
As an example, we can call the operation metaParse, from module META-LEVEL, with the metarepresentation of the module MINI-MAUDE-SYNTAX and the previous module NAT3 transformed into a list of quoted identifiers.
We get the following term of sort ResultPair as a result:
Of course, Maude does not return these boxes. Instead, the system returns the bubbles using their constructor form as specified in their corresponding declarations. For example, the bubbles ’Nat3 and ’s ’s ’s ’0 are represented, respectively, as token(’Nat3) and bubble(’s ’s ’s ’0). Maude returns them metarepresented. The result given by Maude is therefore the following.
The first component of the result pair is a metaterm of sort Term. To convert this term into a term of sort FModule is now straightforward. As already mentioned, we first have to extract from the term the module’s signature. For this, we can use an equationally defined function
that goes along the term metarepresenting the premodule looking for sort and operator declarations; these are obtained by means of auxiliary operations extractSorts and extractOpDecls, respectively. Notice that the operation extractSignature is partial, because it is not well defined for metaterms of sort Term that do not metarepresent terms of sort PreModule in MINI-MAUDE-SYNTAX.
Once we have extracted the signature of the module—expressed as a functional module with no equations and no membership axioms—we can then build terms of sort EquationSet with an equationally defined operation solveBubbles (also partial) that recursively replaces each bubble in an equation with the result of calling metaParse with the already extracted signature and with the quoted identifier form of the bubble.
Finally, the partial operation processPreModule takes a term and, if it metarepresents a term of sort PreModule in MINI-MAUDE-SYNTAX, and, furthermore, the solveBubbles function succeeds in parsing the bubbles in equations as terms, then it returns a term of sort FModule.
The complete specification of these operations is as follows:
We have then the following reductions: