Up

As in Core Maude, in Full Maude we can use the upModule and upTerm functions to avoid the cumbersome task of explicitly writing, respectively, the metarepresentation of a module or the metarepresentation of a term in a given module. The Full Maude upModule function takes as a single argument the name of a module and returns its metarepresentation;^14.4 upTerm takes two arguments, the name of a module and a term in such a module, and returns the corresponding metarepresentation of the term.

Therefore, by evaluating in any module importing the module META-LEVEL the upModule function with the name of any module in the system--either in Core Maude or in Full Maude--as argument, we obtain the metarepresentation of such a module. For example, assuming that the previous module NAT-PLUS has been entered into Full Maude, and therefore it is in its database, we can get its metarepresentation, which we denoted by $\overline{\texttt{NAT-PLUS}}$, as follows:

  Maude> (red in META-LEVEL : upModule(NAT-PLUS) .)
  result FModule :
    fmod 'NAT-PLUS is
    nil
    sorts 'Bool ; 'Nat .
    none
    op '0 : nil -> 'Nat [none] .
    op '_+_ : 'Nat 'Nat -> 'Nat [assoc comm id('0.Nat)] .
    ...

We can use the metarepresentation obtained in this way in any place where a term of sort Module is expected. For example, we can apply the function getOps in META-LEVEL (see Section 11.3) to upModule(NAT-PLUS) as follows:

  Maude> (red in META-LEVEL : getOps(upModule(NAT-PLUS)) .)
  result OpDeclSet :
    op '0 : nil -> 'Nat [none] .
    op '_+_ : 'Nat 'Nat -> 'Nat [assoc comm id('0.Nat)] .
    op '_=/=_ : 'Universal 'Universal -> 'Bool
         [poly(1 2)
          prec(51)
          special(
            id-hook('EqualitySymbol,nil)
            term-hook('equalTerm,'false.Bool)
            term-hook('notEqualTerm,'true.Bool))] .
    ...

Similarly, we can use it with descent functions as discussed in Section 11.4.

  Maude> (red in META-LEVEL :
            metaReduce(upModule(NAT-PLUS), '_+_['0.Nat, 's_['0.Nat]]) .)
  result ResultPair :
    {'s_['0.Nat],'Nat}

But, instead of explicitly writing the metarepresentation $\overline{\texttt{0 + s 0}}$ in the above reduction we can also make good use of the upTerm function, that allows us to get the metarepresentation of a term in a given module.

  Maude> (red in META-LEVEL :
            metaReduce(upModule(NAT-PLUS), upTerm(NAT-PLUS, 0 + s 0)) .)
  result ResultPair :
    {'s_['0.Nat], 'Nat}

As another example, to obtain the metarepresentation of the term s 0 in the module NAT-PLUS above, which we denoted by $\overline{\texttt{s 0}}$, we can write

  Maude> (red in META-LEVEL : upTerm(NAT-PLUS, s 0) .)
  result GroundTerm :
    's_['0.Nat]

The module name is the first argument of the upTerm function, with the term of that module to be metarepresented as the second argument. Since the same term can be parsed in different ways in different modules, and therefore can have different metarepresentations depending on the module in which it is considered, the module to which the term belongs has to be used to obtain the correct metarepresentation. Note also that the above reduction only makes sense at the metalevel, that is, either in the META-LEVEL module itself or in a module importing it.