metaRewrite

The (partial) operation metaRewrite takes as arguments the metarepresentation of a module $\mathcal{R}$, the metarepresentation of a term $t$, and a value $b$ of the sort Bound, i.e., either a natural number or the constant unbounded.

  sort Bound .
  subsort Nat < Bound .
  op unbounded :-> Bound [ctor] .
  op metaRewrite : Module Term Bound ~> ResultPair [special (...)] .

The operation metaRewrite is entirely analogous to metaReduce, but instead of using only the equational part of a module it now uses both the equations and the rules to rewrite the term. The reduction strategy used by metaRewrite coincides with that of the rewrite command (see Sections 5.4 and 16.2). That is, the result of $\texttt{metaRewrite(}\overline{\mathcal{R}}\texttt{, }\overline{t}\texttt{, }b\texttt{)}$ is the metarepresentation of the term obtained from $t$ after at most $b$ applications of the rules in $\mathcal{R}$ using the rewrite strategy, together with the metarepresentation of its corresponding sort or kind. When the value unbounded is given as the third argument, no bound is imposed to the number of rewrites, and rewriting proceeds to the bitter end.

Using metaRewrite we can redo at the metalevel the examples in Section 5.4.

  Maude> reduce in META-LEVEL :
           metaRewrite(upModule('VENDING-MACHINE, false),
             '__['$.Coin, '__['$.Coin, '__['q.Coin, 'q.Coin]]], 1) .
  result ResultPair: 
    {'__['$.Coin, '$.Coin, 'q.Coin, 'q.Coin, 'q.Coin], 'Marking}

  Maude> reduce in META-LEVEL :
           metaRewrite(upModule('VENDING-MACHINE, false),
             '__['$.Coin, '__['$.Coin, '__['q.Coin, 'q.Coin]]], 2) .
  result ResultPair:
    {'__['$.Coin, '$.Coin, '$.Coin, 'q.Coin, 'q.Coin, 'q.Coin], 
         'Marking}