metaReduce

The (partial) operation metaReduce takes as arguments the metarepresentation of a module $\mathcal{R}$ and the metarepresentation of a term $t$.

  sort ResultPair .
  op {_,_} : Term Type -> ResultPair [ctor] .
  op metaReduce : Module Term ~> ResultPair [special (...)] .

When $t$ is a term in $\mathcal{R}$, $\texttt{metaReduce(}\overline{\mathcal{R}}\texttt{,}\overline{t}\texttt{)}$ returns the metarepresentation of the canonical form of $t$, using the equations in $\mathcal{R}$, together with the metarepresentation of its corresponding sort or kind. The reduction strategy used by metaReduce coincides with that of the reduce command (see Sections 4.9 and 16.2).

As said above, in general, when either the first argument of metaReduce is a term of sort Module but not a correct metarepresentation $\overline{\mathcal{R}}$ of an object module $\mathcal{R}$, or the second argument is not the correct metarepresentation $\overline{t}$ of a term $t$ in $\mathcal{R}$, the operation metaReduce is undefined, that is, the term metaReduce(u,v) does not reduce and it does not get evaluated to a term of sort ResultPair, but only to an expression in the kind [ResultPair].

Appropriate selectors extract from the result pairs their two components:

  op getTerm : ResultPair -> Term .
  op getType : ResultPair -> Type .

Using metaReduce we can simulate at the metalevel the primes computation example at the end of Section 4.4.7.

  Maude> reduce in META-LEVEL :
           metaReduce(upModule('SIEVE, false),
             'show_upto_['primes.NatList, 's_^10['0.Zero]]) .
  result ResultPair:
    {'_._['s_^2['0.Zero], 's_^3['0.Zero], 's_^5['0.Zero],
          's_^7['0.Zero], 's_^11['0.Zero], 's_^13['0.Zero],
          's_^17['0.Zero], 's_^19['0.Zero], 's_^23['0.Zero],
          's_^29['0.Zero]],
     'IntList}

We can also insert a new element into an empty map of the type declared in the module PARMODEX at the end of Section 11.3 as follows:

  Maude> red in META-LEVEL :
           metaReduce(
             fmod 'PARMODEX{'X :: 'TRIV} is
               including 'MAP{'String, 'X} .
               sorts 'Foo .
               none
               none
               none
               none
             endfm,
             'insert['"foo".String, 'A:X$Elt, 
                     'empty.Map`{String`,X`}]) .
  result ResultPair: 
    {'_|->_['"foo".String,'A:X$Elt],'Entry`{String`,X`}}

Notice that the module expression 'MAP{'String, 'X} has a bound parameter X, which appears also in the sort X$Elt in the on-the-fly declaration of the variable A:X$Elt.