Down

The result of a metalevel computation, that may use several levels of reflection, can be a term or a module metarepresented 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 upTerm, since it gives us back the original term from its metarepresentation. Notice that down is not a function, but a command instead, because it is more general, taking other commands as arguments, as we are going to explain.

The down command takes two arguments. The first argument is the name of the module to which the term to be returned belongs. The metarepresentation 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:

  down $\langle$ModuleExpression$\rangle$ : $\langle$Command$\rangle$

Thus, we can give the following command.

  Maude> (down NAT-PLUS :
            red in META-LEVEL :
              getTerm(
                metaReduce(upModule(NAT-PLUS),
                           upTerm(NAT-PLUS, 0 + s 0))) .)
  result Nat :
    s 0

Notice that this is equivalent to what we may write using the overline notation as:

  Maude> red getTerm(metaReduce( , )) .
  result Term:

The use of upTerm and down can be iterated with as many levels of reflection as we wish. For example, we can give the command

  Maude> (red in META-LEVEL :
              getTerm(
                metaReduce(upModule(META-LEVEL),
                  upTerm(META-LEVEL,
                    getTerm(
                      metaReduce(upModule(NAT-PLUS),
                                 upTerm(NAT-PLUS, 0 + s 0)))))) .)
  result GroundTerm :
    '_`[_`][''s_.Sort, ''0.Nat.Constant]

This is equivalent to what we would have written using the overline notation as

  Maude> red getTerm(metaReduce( ,
                        )) .
  result Term:

We can write expressions involving simultaneously down, upModule, and upTerm:

  Maude> (down NAT-PLUS :
            down META-LEVEL :
              red in META-LEVEL : 
                  getTerm(
                    metaReduce(upModule(META-LEVEL),
                      upTerm(META-LEVEL,
                        getTerm(
                          metaReduce(upModule(NAT-PLUS),
                                     upTerm(NAT-PLUS, 0 + s 0)))))) .)
  result Nat :
    s 0

The metalevel function downTerm can also be used, but it is a Core Maude function, and therefore can only be used on Core Maude modules.

  Maude> (down NAT-PLUS :
            red in META-LEVEL :
              downTerm(
                getTerm(
                  metaReduce(upModule(META-LEVEL),
                    upTerm(META-LEVEL,
                      getTerm(
                        metaReduce(upModule(NAT-PLUS),
                                   upTerm(NAT-PLUS, 0 + s 0)))))),
                'T:Term) .)
  result Nat :
    s 0