Moving between reflection levels: upModule, upTerm, downTerm, and others

For a module $\mathcal{R}$ that has already been loaded into Maude, the operations upSorts, upSubsortDecl, upOpDecls, upMbs, upEqs, upRls, and upModule take as arguments the metarepresentation of the name of $\mathcal{R}$ and a Boolean value $b$, and return, respectively, the metarepresentations of the module $\mathcal{R}$, of its sorts, subsort declarations, operator declarations, membership axioms, equations, and rules. If the second argument of these functions is true, then the resulting metarepresentations will include the corresponding statements that $\mathcal{R}$ imports from its submodules; but if the second argument is false, the resulting metarepresentations will only contain the metarepresentations of the statements explicitly declared in $\mathcal{R}$.

  op upModule : Qid Bool ~> Module [special (...)] .
  op upSorts : Qid Bool ~> SortSet [special (...)] .
  op upSubsortDecls : Qid Bool ~> SubsortDeclSet [special (...)] .
  op upOpDecls : Qid Bool ~> OpDeclSet [special (...)] .
  op upMbs : Qid Bool ~> MembAxSet [special (...)] .
  op upEqs : Qid Bool ~> EquationSet [special (...)] .
  op upRls : Qid Bool ~> RuleSet [special (...)] .

We give below simple examples of using these functions. Note that, since BOOL is automatically imported by all modules, its equations are shown when upEqs is called with true as its second argument. For the same reason, the metarepresentation of the VENDING-MACHINE-SIGNATURE module includes an including declaration that was not explicit in that module. Here, and in the rest of this section, we assume that the modules NUMBERS and SIEVE from Chapter 4, as well as the modules VENDING-MACHINE-SIGNATURE and VENDING-MACHINE from Chapter 5, have already been loaded into Maude.

  Maude> reduce in META-LEVEL : 
           upModule('VENDING-MACHINE-SIGNATURE, false) .
  result FModule:
    fmod 'VENDING-MACHINE-SIGNATURE is
    including 'BOOL .
    sorts 'Coin ; 'Item ; 'Marking .
    subsort 'Coin < 'Marking .
    subsort 'Item < 'Marking .
    op '$ : nil -> 'Coin [format('r! 'o)] .
    op '__ : 'Marking 'Marking -> 'Marking 
          [assoc comm id('null.Marking)] .
    op 'a : nil -> 'Item [format('b! 'o)] .
    op 'c : nil -> 'Item [format('b! 'o)] .
    op 'null : nil -> 'Marking [none] .
    op 'q : nil -> 'Coin [format('r! 'o)] .
    none
    none
  endfm

  Maude> reduce in META-LEVEL : upEqs('VENDING-MACHINE, true) .
  result EquationSet:
    eq '_and_['true.Bool, 'A:Bool] = 'A:Bool [none] .
    eq '_and_['A:Bool, 'A:Bool] = 'A:Bool [none] .
    eq '_and_['A:Bool, '_xor_['B:Bool, 'C:Bool]]
      = '_xor_['_and_['A:Bool, 'B:Bool], '_and_['A:Bool, 'C:Bool]] 
      [none] .
    eq '_and_['false.Bool, 'A:Bool] = 'false.Bool [none] .
    eq '_or_['A:Bool,'B:Bool]
      = '_xor_['_and_['A:Bool, 'B:Bool],'_xor_['A:Bool, 'B:Bool]] 
      [none] .
    eq '_xor_['A:Bool, 'A:Bool] = 'false.Bool [none] .
    eq '_xor_['false.Bool, 'A:Bool] = 'A:Bool [none] .
    eq 'not_['A:Bool] = '_xor_['true.Bool, 'A:Bool] [none] .
    eq '_implies_['A:Bool, 'B:Bool]
      = 'not_['_xor_['A:Bool, '_and_['A:Bool, 'B:Bool]]] [none] .

  Maude> reduce in META-LEVEL : upEqs('VENDING-MACHINE, false) .
  result EquationSet: (none).EquationSet

  Maude> reduce in META-LEVEL : upRls('VENDING-MACHINE, true) .
  result RuleSet:
    rl '$.Coin => 'c.Item [label('buy-c)] .
    rl '$.Coin => '__['q.Coin,'a.Item] [label('buy-a)] .
    rl 'M:Marking => '__['$.Coin,'M:Marking] [label('add-$)] .
    rl 'M:Marking => '__['q.Coin,'M:Marking] [label('add-q)] .
    rl '__['q.Coin,'q.Coin,'q.Coin,'q.Coin] => '$.Coin 
      [label('change)] .

In addition to the upModule operator, there is another operator allowing the use of an already loaded module at the metalevel. This operator is defined in the module META-MODULE as follows:

  op [_] : Qid -> Module .
  eq [Q:Qid] = (th Q:Qid is including Q:Qid .
                sorts none . none none none none none endth) .

This operator is just syntactic sugar for accessing the corresponding module. Notice that the module is not moved up to the metalevel as upModule does, it is just a way of referring to it, and therefore more efficient.

The META-LEVEL module also provides a function upImports that takes as argument the metarepresentation of the name of a module $\mathcal{R}$ . When $\mathcal{R}$ is already in the Maude module database, then upImports returns the metarepresentation of its list of imported submodules. The function upImports does not take a Boolean argument, as the previous up-functions, since it is not useful to ask for the list of imported submodules of a flattened module.

  op upImports : Qid ~> ImportList [special (...)] .

Finally the META-LEVEL module introduces two polymorphic functions. The function upTerm takes a term $t$ and returns the metarepresentation of its canonical form. The function downTerm takes the metarepresentation of a term $t$ as its first argument and a term $t'$ as its second argument, and returns the canonical form of $t$, if $t$ is a term in the same kind as $t'$; otherwise, it returns the canonical form of $t'$.

  op upTerm : Universal -> Term [poly (1) special (...)] .
  op downTerm : Term Universal -> Universal 
       [poly (2 0) special (...)] .

As simple examples, we can use the function upTerm to obtain the metarepresentation of the term f(a, f(b, c)) in the module UP-DOWN-TEST below, and the function downTerm to recover the term f(a, f(b, c)) from its metarepresentation.

  fmod UP-DOWN-TEST is
    protecting META-LEVEL .
    sort Foo .
    ops a b c d : -> Foo .
    op f : Foo Foo -> Foo .
    op error : -> [Foo] .
    eq c = d .
  endfm

  Maude> reduce in UP-DOWN-TEST : upTerm(f(a, f(b, c))) .
  result GroundTerm: 'f['a.Foo,'f['b.Foo,'d.Foo]]

Notice in the previous example that the given argument has been reduced before obtaining its metarepresentation, more specifically, the subterm c has become d. In the following examples we can observe the same behavior with respect to downTerm.

  Maude> reduce in UP-DOWN-TEST : 
           downTerm('f['a.Foo,'f['b.Foo,'c.Foo]], error) .
  result Foo: f(a, f(b, d))

  Maude> reduce in UP-DOWN-TEST : 
           downTerm(upTerm(f(a, f(b, c))), error) .
  result Foo: f(a, f(b, d))

In our last example, we show the result of downTerm when its first argument does not correspond to the metarepresentation of a term in the module UP-DOWN-TEST; notice the constant e in the metarepresented term that does not correspond to a declared constant in the module.

  Maude> reduce in UP-DOWN-TEST : 
           downTerm('f['a.Foo,'f['b.Foo,'e.Foo]], error) .
  Advisory: could not find a constant e of 
            sort Foo in meta-module UP-DOWN-TEST.
  result [Foo]: error

Due to the failure in moving down the metarepresented term given as first argument, the result is the term given as second argument, namely, error, which was declared in the module UP-DOWN-TEST as a constant of kind [Foo].