Functional and system modules are meta-represented in a syntax very similar to their original user syntax. The main differences are that: (1) terms in equations, membership axioms, and rules are now meta-represented as we have already explained; (2) in the meta-representation of modules we follow a fixed order in introducing the different kinds of declarations for sorts, subsort relations, variables, equations, etc., whereas in the user syntax there is considerable flexibility for introducing such different declarations in an interleaved and piecemeal way; and (3) sets of identifiers--used in declarations of sorts--are represented as sets of quoted identifiers built with an associative and commutative operator _;_.
To motivate the general syntax for representing modules, we illustrate it with a simple example--namely, a module NAT for natural numbers with zero and successor and with commutative addition and multiplication operators.
fmod NAT is
sorts Zero Nat .
subsort Zero < Nat .
op 0 : -> Zero .
op s_ : Nat -> Nat .
op _+_ : Nat Nat -> Nat [comm] .
op _*_ : Nat Nat -> Nat [comm] .
vars N M : Nat .
eq 0 + N = N .
eq s N + M = s (N + M) .
eq 0 * N = 0 .
eq s N * M = M + (N * M) .
endfm
The syntax for the top-level operators representing functional and system modules is as follows
sorts FModule Module .
subsort FModule < Module .
op fmod_is_______endfm : Qid ImportList SortDecl
SubsortDeclSet OpDeclSet
VarDeclSet MembAxSet EquationSet -> FModule .
op mod_is________endm : Qid ImportList SortDecl
SubsortDeclSet OpDeclSet
VarDeclSet MembAxSet EquationSet RuleSet -> Module .
fmod 'NAT is
nil
sorts 'Zero ; 'Nat .
subsort 'Zero < 'Nat .
op '0 : nil -> 'Zero [none] .
op 's_ : 'Nat -> 'Nat [none] .
op '_+_ : 'Nat 'Nat -> 'Nat [comm] .
op '_*_ : 'Nat 'Nat -> 'Nat [comm] .
var 'N : 'Nat .
var 'M : 'Nat .
none
eq '_+_[{'0}'Nat, 'N] = 'N .
eq '_+_['s_['N], 'M] = 's_['_+_['N, 'M]] .
eq '_*_[{'0}'Nat, 'N] = {'0}'Nat .
eq '_*_['s_['N], 'M] = '_+_['N, '_*_['N, 'M]] .
endfm
of sort FModule.
Since NAT has no list of imported submodules and no membership axioms,
those fields are filled respectively by the constants nil of sort ImportList, and none of sort MembAxSet. Similarly, since the
zero and successor operators have no attributes, they have the empty set of
attributes none.
The full definition of META-LEVEL is given in Appendix D. Part of the syntax for functional and system modules is listed below. It extends in a natural way the fragment illustrated in the above example and should, for the most part, be self-explanatory by comparison with the Core Maude syntax, which is mirrored quite closely. Note that we have to represent the set of attributes of an operator. For this, sorts Attr and AttrSet are used. Such attributes may be equational axioms to rewrite modulo, syntactic attributes for parsing purposes, or attributes to link operators to built-in functions (see Sections 2.4.1 and 2.4.2).
sorts FModule Module ModuleExpression Import ImportList
MachineIntList QidSet Sort SortDecl SubsortDecl
SubsortDeclSet Attr AttrSet OpDecl OpDeclSet VarDecl
VarDeclSet Term TermList Equation EquationSet Rule
RuleSet MembAx MembAxSet Hook HookList .
subsort FModule < Module .
subsort Import < ImportList .
subsort Qid < ModuleExpression .
subsort Qid < QidList .
subsort Qid < QidSet .
subsort Qid < Sort .
subsort MachineInt < MachineIntList .
subsort SubsortDecl < SubsortDeclSet .
subsort Attr < AttrSet .
subsort OpDecl < OpDeclSet .
subsort VarDecl < VarDeclSet .
subsort Equation < EquationSet .
subsort Rule < RuleSet .
subsort MembAx < MembAxSet .
subsort Hook < HookList .
op none : -> QidSet .
op _;_ : QidSet QidSet -> QidSet [assoc comm id: none] .
op nil : -> MachineIntList .
op __ : MachineIntList MachineIntList -> MachineIntList
[assoc id: nil] .
op nil : -> ImportList .
op __ : ImportList ImportList -> ImportList [assoc id: nil] .
op including_. : ModuleExpression -> Import .
op sorts_. : QidSet -> SortDecl .
op subsort_<_. : Qid Qid -> SubsortDecl .
op none : -> SubsortDeclSet .
op __ : SubsortDeclSet SubsortDeclSet -> SubsortDeclSet
[assoc comm id: none] .
op op_:_->_[_]. : Qid QidList Qid AttrSet -> OpDecl .
op none : -> OpDeclSet .
op __ : OpDeclSet OpDeclSet -> OpDeclSet
[assoc comm id: none] .
op none : -> AttrSet .
op __ : AttrSet AttrSet -> AttrSet [assoc comm id: none] .
ops assoc comm idem : -> Attr .
ops id left-id right-id : Term -> Attr .
op strat : MachineIntList -> Attr .
op prec : MachineInt -> Attr .
op gather : QidList -> Attr .
op special : HookList -> Attr .
op __ : HookList HookList -> HookList [assoc] .
op id-hook : Qid QidList -> Hook .
op op-hook : Qid Qid QidList Qid -> Hook .
op term-hook : Qid Term -> Hook .
op var_:_. : Qid Qid -> VarDecl .
op none : -> VarDeclSet .
op __ : VarDeclSet VarDeclSet -> VarDeclSet
[assoc comm id: none] .
op mb_:_. : Term Qid -> MembAx .
op cmb_:_if_=_. : Term Qid Term Term -> MembAx .
op none : -> MembAxSet .
op __ : MembAxSet MembAxSet -> MembAxSet
[assoc comm id: none] .
op eq_=_. : Term Term -> Equation .
op ceq_=_if_=_. : Term Term Term Term -> Equation .
op none : -> EquationSet .
op __ : EquationSet EquationSet -> EquationSet
[assoc comm id: none] .
op rl[_]:_=>_. : Qid Term Term -> Rule .
op crl[_]:_=>_if_=_. : Qid Term Term Term Term -> Rule .
op none : -> RuleSet .
op __ : RuleSet RuleSet -> RuleSet [assoc comm id: none] .
Note that--just as in the case of terms--terms of sort Module can be meta-represented again, yielding then a term of sort Term, and this can be iterated an arbitrary number of times. This is in fact necessary when a metalevel computation has to operate at higher levels. A good example is the inductive theorem prover described in [12], where modules are meta-represented as terms in the inference rules for induction, but they have to be meta-meta-represented as terms of sort Term when used in strategies that control the application of the inductive inference rules. We illustrate the meta-meta-representation of modules with a simple example, namely a module TRUTH-VALUES of truth values
fmod TRUTH-VALUES is
sorts Truth .
ops t f : -> Truth .
endfm
'fmod_is_______endfm[
{''TRUTH-VALUES}'Qid,
{'nil}'ImportList,
'sorts_.[{''Truth}'Qid],
{'none}'SubsortDeclSet,
'__['op_:_->_`[_`].[
{''t}'Qid, {'nil}'QidList, {''Truth}'Qid,
{'none}'AttrSet],
'op_:_->_`[_`].[
{''f}'Qid, {'nil}'QidList, {''Truth}'Qid,
{'none}'AttrSet]],
{'none}'VarDeclSet,
{'none}'MembAxSet,
{'none}'EquationSet]