A Core Maude module, such as those presented in previous sections, can be entered in Full Maude by enclosing it in parentheses. For example, the module PATH given in Section 2.1 can be entered to Full Maude as follows.
Maude> (fmod PATH is
protecting MACHINE-INT .
sorts Edge Path Path? Node .
subsorts Edge < Path < Path? .
ops n1 n2 n3 n4 n5 : -> Node .
ops a b c d e : -> Edge .
op _;_ : Path? Path? -> Path? [assoc] .
ops source target : Path -> Node .
op length : Path -> MachineInt .
var E : Edge .
var P : Path .
cmb E ; P : Path if target(E) == source(P) .
ceq source(E ; P) = source(E) if E ; P : Path .
ceq target(P ; E) = target(E) if P ; E : Path .
eq length(E) = 1 .
ceq length(E ; P) = 1 + length(P) if E ; P : Path .
eq source(a) = n1 .
eq target(a) = n2 .
eq source(b) = n1 .
eq target(b) = n3 .
eq source(c) = n3 .
eq target(c) = n4 .
eq source(d) = n4 .
eq target(d) = n2 .
eq source(e) = n2 .
eq target(e) = n5 .
endfm)
As in Core Maude, we can enter any module or command by writing it directly after the prompt, or by having it in a file and then using the in command of Core Maude. Also as in Core Maude, we can write several Full Maude modules or commands in a file and then enter all of them with a single in command; but each of the modules or commands has to be enclosed in parentheses. In Full Maude, in addition to functional and system modules and some of the Core Maude commands, we can enter object-oriented modules, parameterized modules, theories, views and some additional commands. We discuss all these concepts in the coming sections.
As we will discuss in Section 3.4, we can do some reduction or rewriting using a syntax for commands such as that of Core Maude, although with some minor differences that will be explained in Section 3.4.
Maude> (red b ; c ; d .) Result Path? : b ; c ; d Maude> (red length(b ; c ; d) .) Result NzMachineInt : 3 Maude> (red a ; b ; c .) Result Path? : a ; b ; c Maude> (red source(a ; b ; c) .) Result errorSort(Node) : source(a ; b ; c) Maude> (red target(a ; b ; c) .) Result errorSort(Node) : target(a ; b ; c) Maude> (red length(a ; b ; c) .) Result errorSort(MachineInt) : length(a ; b ; c)
In the rest of this chapter we describe the syntax of Full Maude giving the declarations of sorts, subsort relations, and operators included in the actual module used in the parsing of the inputs to Full Maude. We use the techniques described in Section 2.7.6 to parse these inputs. In addition to the declarations for Token, Bubble, and NeTokenList introduced in Section 2.7.6, we need to add declarations for two new kinds of tokens, namely ViewToken and SortToken. These two sorts are just particular cases of tokens which exclude several identifiers.
op viewToken : Qid -> ViewToken
[special
(id-hook Bubble (1 1)
op-hook qidBaseSymbol (<Qids> : -> Qid)
id-hook Exclude (assoc associative
comm commutative
idem idempotent))] .
op sortToken : Qid -> SortToken
[special
(id-hook Bubble (1 1)
op-hook qidBaseSymbol (<Qids> : -> Qid)
id-hook Exclude ([ ] < to : , . ( )))] .
The basic syntax for the declarations of sorts, subsort relations, and operations in Full Maude modules is given by the following declarations27.
subsorts SortToken < Sort < SortList . subsort Attr < AttrList . op __ : SortList SortList -> SortList [assoc] . op sort_. : SortList -> SortDecl . op sorts_. : SortList -> SortDecl . op _<_ : SortList SortList -> SubsortRel . op _<_ : SortList SubsortRel -> SubsortRel . op subsort_. : SubsortRel -> SubsortDecl . op subsorts_. : SubsortRel -> SubsortDecl . op assoc : -> Attr . op comm : -> Attr . op id:_ : Bubble -> Attr . op left id:_ : Bubble -> Attr . op right id:_ : Bubble -> Attr . op strat(_) : NeTokenList -> AttrList . op prec_ : Token -> Attr . op gather(_) : NeTokenList -> Attr . op idem : -> Attr . op __ : AttrList AttrList -> AttrList [assoc] . op op_: ->_. : Token Sort -> OpDecl . op op_: ->_[_]. : Token Sort AttrList -> OpDecl . op op_:_->_. : Token SortList Sort -> OpDecl . op op_:_->_[_]. : Token SortList Sort AttrList -> OpDecl . op ops_: ->_. : NeTokenList Sort -> OpDecl . op ops_: ->_[_]. : NeTokenList Sort AttrList -> OpDecl . op ops_:_->_. : NeTokenList SortList Sort -> OpDecl . op ops_:_->_[_]. : NeTokenList SortList Sort AttrList -> OpDecl .
Full Maude supports, not only module hierachies, that is, acyclic graphs of module importations, as discussed in Section 2.3 for Core Maude, but also parameterized programming techniques in the OBJ3 style. In particular, Full Maude supports importations in including and protecting modes, not only for user-defined modules, but, as we will see in Section 3.5.4, for module expressions as well. The syntax for importation declarations is as follows.
subsort Token < ModExp . op including_. : ModExp -> ImportDecl . op protecting_. : ModExp -> ImportDecl .The syntax for the declaration of variables, membership axioms, equations, and rules is the following.
op vars_:_. : NeTokenList Sort -> VarDecl . op var_:_. : NeTokenList Sort -> VarDecl . op mb_:_. : Bubble Sort -> MembAxDecl . op cmb_:_if_. : Bubble Sort Bubble -> MembAxDecl . op eq_=_. : Bubble Bubble -> EquationDecl . op ceq_=_if_. : Bubble Bubble Bubble -> EquationDecl . op rl[_]:_=>_. : Token Bubble Bubble -> RuleDecl . op crl[_]:_=>_if_. : Token Bubble Bubble Bubble -> RuleDecl .Finally, the top syntax for functional and system modules is given by the following declarations.
subsort VarDecl < VarDeclList .
op __ : VarDeclList VarDeclList -> VarDeclList [assoc] .
subsorts ImportDecl SortDecl SubsortDecl OpDecl
MembAxDecl EquationDecl VarDeclList < FDeclList .
op __ : FDeclList FDeclList -> FDeclList [assoc] .
subsorts RuleDecl FDeclList < SDeclList .
op __ : SDeclList SDeclList -> SDeclList [assoc] .
subsort Token < ModuleName .
op fmod_is_endfm : ModuleName FDeclList -> PreModule .
op mod_is_endm : ModuleName SDeclList -> PreModule .