The Full Maude system is defined as a Core Maude module. That is, the entire semantics of Full Maude is defined and executed in Core Maude. The full definition of the Full Maude system, including the definition of all the internal functions implementing the system can be found in [19]. In particular, the grammar of the Full Maude language, that a user should follow to enter modules and commands, is itself a functional submodule of the overall Full Maude system specification. This allows giving the following specification of the Full Maude grammar in a form more perspicuous in certain ways than the corresponding BNF grammar form.
fmod SIGNS&VIEW-EXPRS is
sorts Token NeTokenList Bubble
SortToken Sort SortList SortDecl
ViewToken ViewExp
SubsortRel SubsortDecl
OpDecl Attr AttrList Hook HookList .
subsorts SortToken < Sort < SortList .
subsort ViewToken < ViewExp .
subsort Attr < AttrList .
subsort Hook < HookList .
op ((_)) : Token -> Token .
*** extended sorts
op _[_] : Sort ViewExp -> Sort [prec 40] .
op __ : SortList SortList -> SortList [assoc] .
op _,_ : ViewExp ViewExp -> ViewExp [assoc] .
*** sort declaration
op sorts_. : SortList -> SortDecl .
op sort_. : SortList -> SortDecl .
*** subsort declaration
op subsort_. : SubsortRel -> SubsortDecl .
op subsorts_. : SubsortRel -> SubsortDecl .
op _<_ : SortList SortList -> SubsortRel .
op _<_ : SortList SubsortRel -> SubsortRel .
*** operator attributes
op __ : AttrList AttrList -> AttrList [assoc] .
op assoc : -> Attr .
op associative : -> Attr .
op comm : -> Attr .
op commutative : -> Attr .
op id:_ : Bubble -> Attr .
op identity:_ : Bubble -> Attr .
op left id:_ : Bubble -> Attr .
op left identity:_ : Bubble -> Attr .
op right id:_ : Bubble -> Attr .
op right identity:_ : Bubble -> Attr .
op strat(_) : NeTokenList -> AttrList .
op strategy(_) : NeTokenList -> AttrList .
op prec_ : Token -> Attr .
op precedence_ : Token -> Attr .
op gather(_) : NeTokenList -> Attr .
op gathering(_) : NeTokenList -> Attr .
op idem : -> Attr .
op idempotent : -> Attr .
op special(_) : HookList -> Attr .
op __ : HookList HookList -> HookList [assoc] .
op id-hook_ : Token -> Hook .
op id-hook_(_) : Token NeTokenList -> Hook .
op op-hook_(_:_->_) : Token Token NeTokenList Token -> Hook .
op op-hook_(_: ->_) : Token Token Token -> Hook .
op term-hook_(_) : Token Bubble -> Hook .
*** operator declaration
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 .
endfm
fmod F&S-MODS&THS is
including SIGNS&VIEW-EXPRS .
sorts FDeclList SDeclList PreModule
ImportDecl ModExp Parameter ParameterList
ModuleName EquationDecl RuleDecl MembAxDecl
VarDecl VarDeclList .
subsort Parameter < ParameterList .
subsorts Token < ModExp ModuleName .
subsort VarDecl < VarDeclList .
subsorts VarDecl ImportDecl SortDecl SubsortDecl
OpDecl MembAxDecl EquationDecl VarDeclList < FDeclList .
subsorts RuleDecl FDeclList < SDeclList .
*** variable declaration
op vars_:_. : NeTokenList Sort -> VarDecl .
op var_:_. : NeTokenList Sort -> VarDecl .
*** membership axiom declaration
op mb_:_. : Bubble Sort -> MembAxDecl .
op cmb_:_if_. : Bubble Sort Bubble -> MembAxDecl .
*** equation declaration
op eq_=_. : Bubble Bubble -> EquationDecl .
op ceq_=_if_. : Bubble Bubble Bubble -> EquationDecl .
*** rule declaration
op rl[_] :_=>_. : Token Bubble Bubble -> RuleDecl .
op crl[_]:_=>_if_. : Token Bubble Bubble Bubble -> RuleDecl .
*** importation declaration
op including_. : ModExp -> ImportDecl .
op inc_. : ModExp -> ImportDecl .
op protecting_. : ModExp -> ImportDecl .
op pr_. : ModExp -> ImportDecl .
*** parameterized module interface
op _::_ : Token ModExp -> Parameter [prec 40 gather (e &)] .
op _,_ : ParameterList ParameterList -> ParameterList [assoc] .
op _[_] : Token ParameterList -> ModuleName .
*** declaration list
op __ : VarDeclList VarDeclList -> VarDeclList [assoc] .
op __ : SDeclList SDeclList -> SDeclList [assoc] .
op __ : FDeclList FDeclList -> FDeclList [assoc] .
*** functional and system module and theory
op fmod_is_endfm : ModuleName FDeclList -> PreModule .
op mod_is_endm : ModuleName SDeclList -> PreModule .
op fth_is_endfth : ModuleName FDeclList -> PreModule .
op th_is_endth : ModuleName SDeclList -> PreModule .
endfm
fmod OO-MODS&THS is
including F&S-MODS&THS .
sorts ClassDecl AttrDecl AttrDeclList
SubclassDecl MsgDecl ODeclList .
subsorts SDeclList MsgDecl SubclassDecl ClassDecl < ODeclList .
subsort AttrDecl < AttrDeclList .
*** object-oriented module and theory
op omod_is_endom : ModuleName ODeclList -> PreModule .
op oth_is_endoth : ModuleName ODeclList -> PreModule .
*** class declaration
op class_|_. : Sort AttrDeclList -> ClassDecl .
op class_. : Sort -> ClassDecl .
op _,_ : AttrDeclList AttrDeclList -> AttrDeclList [assoc] .
op _:_ : Token Sort -> AttrDecl [prec 40] .
*** subclass declaration
op subclass_. : SubsortRel -> SubclassDecl .
op subclasses_. : SubsortRel -> SubclassDecl .
op _<_ : SortList SortList -> SubsortRel .
op _<_ : SortList SubsortRel -> SubsortRel .
*** message declaration
op msg_:_->_. : Token SortList Sort -> MsgDecl .
op msgs_:_->_. : NeTokenList SortList Sort -> MsgDecl .
endfm
fmod MOD-EXPRS is
including OO-MODS&THS .
sorts Map MapList .
subsort Map < MapList .
*** module expression
op _*(_) : ModExp MapList -> ModExp .
op _[_] : ModExp ViewExp -> ModExp .
*** renaming maps
op op_to_ : Token Token -> Map .
op op_:_->_to_ : Token SortList Sort Token -> Map .
op op_: ->_to_ : Token Sort Token -> Map .
op op_to_[_] : Token Token AttrList -> Map .
op op_:_->_to_[_] : Token SortList Sort Token AttrList -> Map .
op op_: ->_to_[_] : Token Sort Token AttrList -> Map .
op sort_to_ : Sort Sort -> Map .
op label_to_ : Token Token -> Map .
op class_to_ : Sort Sort -> Map .
op attr_._to_ : Token Sort Token -> Map .
op msg_to_ : Token Token -> Map .
op msg_:_->_to_ : Token SortList Sort Token -> Map .
op msg_: ->_to_ : Token Sort Token -> Map .
op _,_ : MapList MapList -> MapList [assoc prec 42] .
endfm
fmod VIEWS is
including OO-MODS&THS .
sorts ViewDecl ViewDeclList PreView .
subsorts VarDecl < ViewDecl < ViewDeclList .
subsort VarDeclList < ViewDeclList .
*** view maps
op op_to term_. : Bubble Bubble -> ViewDecl .
op op_to_. : Token Token -> ViewDecl .
op op_:_->_to_. : Token SortList Sort Token -> ViewDecl .
op op_: ->_to_. : Token Sort Token -> ViewDecl .
op sort_to_. : Sort Sort -> ViewDecl .
op class_to_. : Sort Sort -> ViewDecl .
op attr_._to_. : Token Sort Token -> ViewDecl .
op msg_to_. : Token Token -> ViewDecl .
op msg_:_->_to_. : Token SortList Sort Token -> ViewDecl .
op msg_: ->_to_. : Token Sort Token -> ViewDecl .
*** view
op view_from_to_is_endv :
ViewToken ModExp ModExp ViewDeclList -> PreView .
op __ : ViewDeclList ViewDeclList -> ViewDeclList [assoc] .
endfm
fmod COMMANDS is
including MOD-EXPRS .
sorts PreCommand .
*** down function
op down_:_ : ModExp PreCommand -> PreCommand .
*** reduce command
op red_. : Bubble -> PreCommand .
op red-in_:_. : ModExp Bubble -> PreCommand .
op reduce_. : Bubble -> PreCommand .
op reduce-in_:_. : ModExp Bubble -> PreCommand .
*** rewrite command
op rew_. : Bubble -> PreCommand .
op rew[_]_. : Token Bubble -> PreCommand .
op rew-in_:_. : ModExp Bubble -> PreCommand .
op rew-in[_]_:_. : Token ModExp Bubble -> PreCommand .
op rewrite_. : Bubble -> PreCommand .
op rewrite[_]_. : Token Bubble -> PreCommand .
op rewrite-in_:_. : ModExp Bubble -> PreCommand .
op rewrite-in[_]_:_. : Token ModExp Bubble -> PreCommand .
*** select command
op select_. : ModExp -> PreCommand .
*** show commands
op show module . : -> PreCommand .
op show module_. : ModExp -> PreCommand .
op show all . : -> PreCommand .
op show all_. : ModExp -> PreCommand .
op show sorts . : -> PreCommand .
op show sorts_. : ModExp -> PreCommand .
op show ops . : -> PreCommand .
op show ops_. : ModExp -> PreCommand .
op show vars . : -> PreCommand .
op show vars_. : ModExp -> PreCommand .
op show mbs . : -> PreCommand .
op show mbs_. : ModExp -> PreCommand .
op show eqns . : -> PreCommand .
op show eqns_. : ModExp -> PreCommand .
op show rls . : -> PreCommand .
op show rls_. : ModExp -> PreCommand .
op show view_. : ViewExp -> PreCommand .
op show modules . : -> PreCommand .
op show views . : -> PreCommand .
endfm
fmod FULL-MAUDE-SIGN is
including VIEWS .
including COMMANDS .
endfm