As explained for Core Maude in Section 2.3, in Full Maude we can use keywords protecting and including, or pr and inc in abbreviated form, to define structured specifications. All the predefined modules introduced in Section 2.4, plus the module META-LEVEL, are also available in Full Maude31. As we will explain in Section 3.5, Full Maude supports not only the importation of modules, but the importation of module expressions as well.
In metalevel computations it is very convenient to be able to refer by name to the meta-representations of modules already entered into the system. To make this possible, Full Maude allows importation declarations of the form protecting META-LEVEL[Id_1,..., Id_n] . where Id1,...,Idn is a list of names of user-defined modules. With this declaration, new constants Id1,...,Idn of sort Module are declared, and equations making each constant Idi equal to the metalevel representation of the module with name Idi declared previously by the user, for i=1...n, are added. Thus, we can first enter the module.
(fmod NAT is
sort Nat .
op 0 : -> Nat .
op s_ : Nat -> Nat .
op _+_ : Nat Nat -> Nat [assoc comm id: 0] .
var N M : Nat .
eq s N + s M = s s (N + M) .
endfm)
and then we can declare a module that protects META-LEVEL[NAT]
and defines a function to extract the set of operator declarations
of a functional module as follows.
(fmod META-NAT is
protecting META-LEVEL[NAT] .
op getOpDeclSet : FModule -> OpDeclSet .
var QI : Qid .
var IL : ImportList .
var SD : SortDecl .
var SSDS : SubsortDeclSet .
var ODS : OpDeclSet .
var VDS : VarDeclSet .
var MAS : MembAxSet .
var EqS : EquationSet .
eq getOpDeclSet(fmod QI is IL SD SSDS ODS VDS MAS EqS endfm)
= ODS .
endfm)
Then we can apply this function to the constant NAT, which in META-NAT has been declared to be equal to the meta-representation of the above module NAT, as follows.
Maude> (red getOpDeclSet(NAT) .)
Result OpDeclSet :
op '0 : nil -> 'Nat [none] .
op '_+_ : 'Nat 'Nat -> 'Nat [assoc comm id({'0}'Nat)] .
op 's_ : 'Nat -> 'Nat [none] .
We can also use the descent functions as discussed in Section 2.5.5.
Maude> (red meta-reduce(NAT, '_+_[{'0}'Nat, 's_[{'0}'Nat]]) .)
Result Term : 's_[{'0}'Nat]
Note that we have written the actual meta-representation of the term
0 + s 0 instead of using the more intuitive notation
|¯0 + s 0¯| used in Section 2.5.5.
However, in Full Maude, we can use the up function to avoid the
cumbersome task of explicitly writing the meta-representation of a term or the
meta-representation of a module. For example, to obtain the
meta-representation of a term as s 0 in the module NAT,
which we denote by |¯s 0¯| , we can write
Maude> (red up(NAT, s 0) .)
Result Term : 's_[{'0}'Nat]
Thus, instead of explicitly writing the meta-representation
|¯0 + s 0¯| in the above reduction we can write
Maude> (red meta-reduce(NAT, up(NAT, 0 + s 0)) .)
Result Term : 's_[{'0}'Nat]
Note that the module name is the first argument of the up function, with
the term of that module to be meta-represented as the second argument. Since
the same term can be parsed in different ways in different modules, and
therefore can have different meta-representations depending on the module in
which it is considered, the module to which the term belongs has to be used to
obtain the correct meta-representation. Note also that the above reduction only
makes sense at the metalevel, that is, in a module importing the module
META-LEVEL.
The up function also gives us a second way of accessing the meta-representation of any module in the database. Evaluating in any module importing the module META-LEVEL the up function with the name of any module in the database as argument we obtain the meta-representation of such a module. Thus, assuming that the previous module NAT has been entered in Full Maude, and therefore is in the database, we can get its meta-representation, which we denote by |¯NAT¯| , as follows.
Maude> (red up(NAT) .)
Result FModule :
fmod 'NAT is
nil
sorts 'Nat .
none
op '0 : nil -> 'Nat [none] .
op '_+_ : 'Nat 'Nat -> 'Nat [assoc comm id({'0}'Nat)] .
op 's_ : 'Nat -> 'Nat [none] .
var 'M : 'Nat .
var 'N : 'Nat .
none
eq '_+_['s_['N], 's_['M]] = 's_['s_['_+_['N, 'M]]].
endfm
This facility can be used to write reductions of terms as
those presented in Section 2.5.5, for example of
meta-reduce( |¯NAT¯| ,
|¯s s 0 + s s s 0¯| ),
as follows.
Maude> (red meta-reduce(up(NAT), up(NAT, s s 0 + s s s 0)) .)
Result Term : 's_['s_['s_['s_['s_[{'0}'Nat]]]]]
The result of a metalevel computation that may use several levels of reflection can be a term or module meta-represented one or more times, which may be hard to read. Therefore, to display the output in a more readable form we can use the down command, which is in a sense inverse to up, since it gives us back the term from its meta-representation. The down command takes two arguments. The first argument is the name of the module to which the term to be returned belongs. The meta-representation of the desired output term should be the result of the command given as second argument. The syntax of the down command is as follows.
op down_:_ : ModExp PreCommand -> PreCommand .Thus, we can give the following command.
Maude> (down NAT :
red-in META-NAT :
meta-reduce(NAT, up(NAT, 0 + s 0)) .)
Result Nat : s 0
Notice that this is equivalent to what we wrote in
section 2.5.5 as
Maude> red meta-reduce( |¯NAT¯| , |¯s 0 + 0¯| ) . result Term: |¯s 0¯|
The use of up and down can be iterated with as many levels of reflection as we wish. For example, in a module
(fmod META-META-NAT is
protecting META-LEVEL[META-NAT] .
endfm)
we can give the command
Maude> (down NAT :
down META-NAT :
red meta-reduce(META-NAT,
up(META-NAT,
meta-reduce(NAT,
up(NAT, 0 + s 0)))) .)
Result Nat : s 0
This is equivalent to what we would have written using the overline notation
as
Maude> red meta-reduce( |¯META-NAT¯| , |¯meta-reduce( |¯NAT¯| , |¯s 0 + 0¯| )¯| ) . result Term: |¯ |¯s 0¯| ¯|