This chapter explains how to use the facilities provided by the predefined modules META-LEVEL, STD-STREAM, and LEXICAL 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 STD-STREAM module can be used to handle the input/output and to maintain the persistent state of the language environment or tool.1
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 the datatype of its commands and other constructs by means of a signature Signπ«.
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: insert $ and insert q for inserting a dollar or a quarter in the machine; show basket and show credit for showing the items already bought or the remaining credit; and buy__(s) for buying a number of pieces of the same item.
fmod VENDING-MACHINE-GRAMMAR is
protecting VENDING-MACHINE-SIGNATURE .
protecting NAT .
sort Action .
op insert $ : -> Action .
op insert q : -> Action .
op show basket : -> Action .
op show credit : -> Action .
op buy__(s) : Nat Item -> Action .
endfm
The interaction with the standard IO streams is performed using objects and messages. The next step is therefore to define the objects that will keep the state of the system and will interact with the IO streams. Our goal is to have a loop between the system and the user in which the vending machine asks for input, and then, depending on the specific action, performs one task or another, and gives its response to the user.
In the module VENDING-MACHINE-IO below, we introduce the necessary declarations to use objects of a class VM with attributes action, to keep the last action requested from the user (inserting a coin, showing information about the remaining credit or the items already bought, or buying one or more items), and marking, to keep the state of the machine (the marking of the vending machine, that is, the remaining credit plus the items already bought). The constants vm and idle are introduced for convenience to denote the identifier of the vending machine object and to denote the idle action in which the system is waiting for input from the user once the actual action is processed.
mod VENDING-MACHINE-IO is
including STD-STREAM .
including VENDING-MACHINE-GRAMMAR .
protecting BUYING-STRATS .
protecting CONVERSION .
protecting LEXICAL .
sort VM .
subsort VM < Cid .
op VM : -> VM .
op action :_ : Action -> Attribute .
op marking :_ : Marking -> Attribute .
op vm : -> Oid .
op idle : -> Action .
To operate on the system we introduce two further constants: VM-GRAMMAR represents the module in which the input from the user is going to be parsed, the above VENDING-MACHINE-GRAMMAR; the vending machine configuration is used to initialize the system, and it includes the portal to interact with standard streams, the vm object, initially with null marking and action idle, and a first write message to show the user that the machine is started.
op VM-GRAMMAR : -> Module .
eq VM-GRAMMAR = upModule(βVENDING-MACHINE-GRAMMAR, false) .
op vending machine : -> Configuration .
eq vending machine
= <>
< vm : VM | marking : null, action : idle >
write(stdout, vm, "\n\t Vending machine\n") .
The interaction with the user is then handled by the following two rules. Once a write message is processed, the output stream sends back a wrote message, which is used to request an action from the user, who is prompted with a > character. When the user hits the return key, the stream object sends the input in a gotLine message. In the rule below, we expect either a "quit" that will finish the interaction, a valid input in the VM-GRAMMAR grammar, or a non-valid input. In the first case, a goodbye message is shown and the interaction terminates (note that the object is removed from the state). If there is an invalid input, an error message is shown and the interaction continues. If the input is valid in the VM-GRAMMAR grammar, the corresponding action is placed in the action attribute of the VM object for further processing. Note the use of the tokenize function2 to tokenize the input, which is received as a string, before parsing it. 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 17.6.1).
vars O Oβ : Oid .
var Str : String .
var Atts : AttributeSet .
var X : VM .
rl < O : X | Atts >
wrote(O, Oβ)
=> < O : X | Atts >
getLine(stdin, O, "> ") .
rl < O : X | action : idle, Atts >
gotLine(O, Oβ, Str)
=> if Str == "quit"
then write(stdout, O, "goodbye\n")
else if metaParse(VM-GRAMMAR, tokenize(Str), βAction) :: ResultPair
then < O : X |
action : downTerm(
getTerm(
metaParse(VM-GRAMMAR, tokenize(Str), βAction)),
idle),
Atts >
else < O : X | action : idle, Atts >
write(stdout, O, "Invalid input\n")
fi
fi .
The processing of the valid inputs, the actions, is performed by several rewriting rules, modeling the changes produced in the state of the vending machine by the actions requested by the client. 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 17.7. Recall that BUYING-STRATS includes the META-LEVEL module.
var A : Action .
var I : Item .
var C : Coin .
var M : Marking .
vars QIL QILβ QILββ : QidList .
var N : Nat .
For the show basket and show credit actions, the following rules extract the information about the remaining credit or the items already bought, and send a write message with the corresponding information. 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 17.6.1 ).
op showBasket : Marking -> QidList .
eq showBasket(I M)
= metaPrettyPrint(upModule(βVENDING-MACHINE-SIGNATURE, false), upTerm(I))
showBasket(M) .
eq showBasket(C M) = showBasket(M) .
eq showBasket(null) = nil .
op showCredit : Marking -> QidList .
eq showCredit(C M)
= metaPrettyPrint(upModule(βVENDING-MACHINE-SIGNATURE, false), upTerm(C))
showCredit(M) .
eq showCredit(I M) = showCredit(M) .
eq showCredit(null) = nil .
rl < O : X | action : show basket, marking : M, Atts >
=> < O : X | action : idle, marking : M, Atts >
write(stdout, O, "basket: " + printTokens(showBasket(M)) + "\n") .
rl < O : X | action : show credit, marking : M, Atts >
=> < O : X | action : idle, marking : M, Atts >
write(stdout, O, "credit: " + printTokens(showCredit(M)) + "\n") .
The following rules 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 17.7) 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.
rl < O : X | action : insert q, marking : M, Atts >
=> < O : X | action : idle,
marking : downTerm(insertCoin(βadd-q, upTerm(M)), null), Atts >
write(stdout, O, "one quarter introduced\n") .
rl < O : X | action : insert $, marking : M, Atts >
=> < O : X | action : idle,
marking : downTerm(insertCoin(βadd-$, upTerm(M)), null), Atts >
write(stdout, O, "one dollar introduced\n") .
The last two rules implement the actions of buying one or more items. The strategy onlyNitems defined in the module BUYING-STRATS (see Section 17.7) 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.
rl < O : X | action : (buy N c (s)), marking : M, Atts >
=> < O : X | action : idle,
marking : downTerm(onlyNitems(upTerm(M), βbuy-c, N), null), Atts >
write(stdout, O, string(N, 10) + " cakes bought\n") .
rl < O : X | action : (buy N a (s)), marking : M, Atts >
=> < O : X | action : idle,
marking : downTerm(onlyNitems(upTerm(M), βbuy-a, N), null),Atts >
write(stdout, O, string(N, 10) + " apples bought\n") .
endm
With the above definitions, we can now illustrate the basic interaction with the vending machine. Once the VENDING-MACHINE-IO module has been entered, we can initiate the execution using the erewrite command and the vending machine constant.
Once the machine interface has been initialized, we can input any data by writing it after the prompt. For example,
We can terminate the interface by introducing the quit action.
The example presented in the previous two sections is a toy example to illustrate the basic features of a possible interaction loop with the system. However, the most interesting applications of the STD-STREAM 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 we can use a similar approach to handle the input/output and maintaining the persistent state of the object language interpreter or tool.
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 datatype for β-modules, as well as auxiliary declarations for commands and other constructs, by means of a signature Signβ. 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: (1) what we may call the top-level syntax of the language, and (2) the user-definable syntax introduced in each module. The bubble datatype 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 [40, 41].
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 datatypes by parameterizing their definition. Thus, for example, a bubble of length one, which we call a token, can be defined as follows:
sort Token .
op token : Qid -> Token
[special (id-hook Bubble (1 1)
op-hook qidSymbol (<Qids> : ~> Qid))] .
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.
op bubble : QidList -> Bubble
[special
(id-hook Bubble (1 -1)
op-hook qidListSymbol (__ : QidList QidList ~> QidList)
op-hook qidSymbol (<Qids> : ~> Qid)
id-hook Exclude (.))] .
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. In general, the syntax Exclude (I1 I2β¦Ik) is used to exclude identifiers I1,I2,β¦,Ik inside tokens.
We can, for example, declare the sort NeTokenList with constructor neTokenList as a list of identifiers, of any length greater or equal than one, excluding the identifier β->β with the following declarations.
op neTokenList : QidList -> NeTokenList
[special
(id-hook Bubble (1 -1)
op-hook qidListSymbol (__ : QidList QidList ~> QidList)
op-hook qidSymbol (<Qids> : ~> Qid)
id-hook Exclude ( -> ))] .
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.
fmod MINI-MAUDE-SYNTAX is
protecting QID-LIST .
sorts Token Bubble NeTokenList .
op token : Qid -> Token
[special
(id-hook Bubble (1 1)
op-hook qidSymbol (<Qids> : ~> Qid))] .
op bubble : QidList -> Bubble
[special
(id-hook Bubble (1 -1)
op-hook qidListSymbol (__ : QidList QidList ~> QidList)
op-hook qidSymbol (<Qids> : ~> Qid)
id-hook Exclude (.))] .
op neTokenList : QidList -> NeTokenList
[special
(id-hook Bubble (1 -1)
op-hook qidListSymbol (__ : QidList QidList ~> QidList)
op-hook qidSymbol (<Qids> : ~> Qid)
id-hook Exclude (->))] .
sorts Decl DeclList PreModule Input Command .
subsort Decl < DeclList .
subsorts Module Command < Input .
op including_. : Token -> Decl . --- including declaration
op sort_. : Token -> Decl . --- sort declaration
op op_: ->_. : Token Token -> Decl . --- operator declaration
op op_:_->_. : Token NeTokenList Token -> Decl .
op eq_=_. : Bubble Bubble -> Decl . --- equation declaration
--- functional module
op fmod_is_endfm : Token DeclList -> PreModule .
op __ : DeclList DeclList -> DeclList [assoc gather(e E)] .
--- reduce command
op reduce_. : Bubble -> Command .
endfm
Notice how we explicitly declare operators that correspond to part of 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. Notice also that not all terms of sort PreModule represent valid 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. We sometimes refer to modules with bubbles as premodules.
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.
Maude> red in META-LEVEL :
metaParse(upModule(βMINI-MAUDE-SYNTAX, false),
βfmod βNAT3 βis
βsort βNat3 β.
βop βs_ β: βNat3 β-> βNat3 β.
βop β0 β: β-> βNat3 β.
βeq βs βs βs β0 β= β0 β.
βendfm,
βPreModule) .
We get the following term of sort ResultPair as a result:
result ResultPair:
{βfmod_is_endfm[βNAT3,
β__[βsort_.[βNat3],
β__[βop_:_->_.[βs_, βNat3, βNat3],
β__[βop_:_->_.[β0, βNat3],
βeq_=_.[βsβsβsβ0, β0]]],
βPreModule}
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.
result ResultPair: {
βfmod_is_endfm[βtoken[ββNAT3.Qid],
β__[βsort_.[βtoken[ββNat3.Qid]],
β__[βop_:_->_.[βtoken[ββs_.Qid],
βneTokenList[ββNat3.Qid],
βtoken[ββNat3.Qid]],
β__[βop_:β->_.[βtoken[ββ0.Qid], βtoken[ββNat3.Qid]],
βeq_=_.[βbubble[β__[ββs.Qid, ββs.Qid, ββs.Qid,ββ0.Qid]],
βbubble[ββ0.Qid]]]]]],
βPreModule}
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, operator, and importation declarations. A homonymous function is used to recursively handle each declaration and add it to the module carried along as second argument. 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 processModule 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:
fmod MINI-MAUDE is
protecting META-LEVEL .
vars T T1 T2 T3 : Term .
vars TL TLβ : TermList .
var QI : Qid .
var QIL : QidList .
var F : Qid .
var M : Module .
var I : Import .
vars IL : ImportList .
var S : Sort .
vars SS : SortSet .
var SsS : SubsortDeclSet .
var OD : OpDecl .
var ODS : OpDeclSet .
var MbS : MembAxSet .
vars EqS EqSβ : EquationSet .
op processModule : Term ~> FModule .
eq processModule(T) = solveBubbles(T, extractSignature(T)) .
---- extractSignature
op extractSignature : Term ~> FModule .
op extractSignature : Term FModule ~> FModule .
eq extractSignature(βfmod_is_endfm[βtoken[QI], T])
= extractSignature(T,
fmod downTerm(QI, βerror) is nil sorts none . none none none none endfm) .
eq extractSignature(β__[T1, T2], M)
= extractSignature(T2, extractSignature(T1, M)) .
eq extractSignature(βsort_.[βtoken[T]], M) = addSort(M, downTerm(T, βerror)) .
eq extractSignature(βop_:_->_.[βtoken[T1], βneTokenList[TL], βtoken[T2]], M)
= addOpDecl(M,
op downTerm(T1, βerror) : downTerm(TL, nil) -> downTerm(T2, βerror) [none] .) .
eq extractSignature(βop_:β->_.[βtoken[T1], βtoken[T2]], M)
= addOpDecl(M, (op downTerm(T1, βerror) : nil -> downTerm(T2, βerror) [none] .)) .
eq extractSignature(βincluding_.[βtoken[T]], M)
= addImport(M, including downTerm(T, βerror) .) .
eq extractSignature(T, M) = M [owise] .
---- solveBubbles
op solveBubbles : Term FModule ~> FModule .
op solveBubblesAux : Term FModule ~> EquationSet .
eq solveBubbles(βfmod_is_endfm[βtoken[QI], T], M)
= addEquations(M, solveBubblesAux(T, M)) .
eq solveBubblesAux(βeq_=_.[T1, T2], M)
= (eq getTerm(processTerm(T1, M)) = getTerm(processTerm(T2, M)) [none] .) .
eq solveBubblesAux(β__[βeq_=_.[T1, T2], T3], M)
= (eq getTerm(processTerm(T1, M)) = getTerm(processTerm(T2, M)) [none] .
solveBubblesAux(T3, M)) .
ceq solveBubblesAux(β__[F[TL], T2], M)
= solveBubblesAux(T2, M)
if F =/= βeq_=_. .
ceq solveBubblesAux(F[TL], M)
= none
if F =/= β__ /\ F =/= βeq_=_. .
op processTerm : Term Module ~> ResultPair .
eq processTerm(βbubble[T], M)
= metaParse(M, downTerm(T, nil), anyType) .
op addSort : FModule Sort -> FModule .
eq addSort(fmod QI is IL sorts SS . SsS ODS MbS EqS endfm, S)
= fmod QI is IL sorts SS ; S . SsS ODS MbS EqS endfm .
op addOpDecl : FModule OpDecl -> FModule .
eq addOpDecl(fmod QI is IL sorts SS . SsS ODS MbS EqS endfm, OD)
= fmod QI is IL sorts SS . SsS (OD ODS) MbS EqS endfm .
op addImport : FModule Import -> FModule .
eq addImport(fmod QI is IL sorts SS . SsS ODS MbS EqS endfm, I)
= fmod QI is IL I sorts SS . SsS ODS MbS EqS endfm .
op addEquations : FModule EquationSet -> FModule .
eq addEquations(fmod QI is IL sorts SS . SsS ODS MbS EqS endfm, EqSβ)
= fmod QI is IL sorts SS . SsS ODS MbS (EqS EqSβ) endfm .
endfm
We have then the following reductions:
Maude> red in MINI-MAUDE :
extractSignature(
getTerm(metaParse(upModule(βMINI-MAUDE-SYNTAX, false),
βfmod βNAT3 βis
βop βs_ β: βNat3 β-> βNat3 β.
βsort βNat3 β.
βop β0 β: β-> βNat3 β.
βeq βs βs βs β0 β= β0 β.
βendfm,
βPreModule))) .
result FModule: fmod βNAT3 is
nil
sorts βNat3 .
none
op β0 : nil -> βNat3 [none] .
op βs_ : βNat3 -> βNat3 [none] .
none
none
endfm
Maude> red in MINI-MAUDE :
processModule(
getTerm(metaParse(upModule(βMINI-MAUDE-SYNTAX, false),
βfmod βNAT3 βis
βsort βNat3 β.
βop βs_ β: βNat3 β-> βNat3 β.
βop β0 β: β-> βNat3 β.
βeq βs βs βs β0 β= β0 β.
βendfm,
βPreModule))) .
result FModule: fmod βNAT3 is
nil
sorts βNat3 .
none
op β0 : nil -> βNat3 [none] .
op βs_ : βNat3 -> βNat3 [none] .
none
eq βs_[βs_[βs_[β0.Nat3]]] = β0.Nat3 [none] .
endfm
Maude> red in MINI-MAUDE :
processModule(
getTerm(metaParse(upModule(βMINI-MAUDE-SYNTAX, false),
βfmod βNAT3 βis
βsort βNat3 β.
βop βs_ β: βNat3 β-> βNat3 β.
βop β0 β: β-> βNat3 β.
βeq βs βs βs βN:Nat3 β= βN:Nat3 β.
βendfm,
βPreModule))) .
result FModule: fmod βNAT3 is
nil
sorts βNat3 .
none
op β0 : nil -> βNat3 [none] .
op βs_ : βNat3 -> βNat3 [none] .
none
eq βs_[βs_[βs_[βN:Nat3]]] = βN:Nat3 [none] .
endfm
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.
mod LOOP-MODE is
protecting QID-LIST .
sorts State System .
op [_,_,_] : QidList State QidList -> System [ctor special (...)] .
endm
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 is no longer maintained. The support for communication with external objects (see Section 9) makes it possible to develop more general and flexible solutions for dealing with input/output.
Since with the loop object 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.3 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.4 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.