metaFrewrite

Position fair rewriting, which was described in Section 5.4, is metarepresented by the operation metaFrewrite. This (partial) operation takes as arguments the metarepresentation of a module, the metarepresentation of a term, a value of sort Bound, and a natural number.

  op metaFrewrite : Module Term Bound Nat ~> ResultPair 
       [special (...)] .

The reduction strategy used by metaFrewrite coincides with that of the frewrite command in Maude, except that a final (semantic) sort calculation is performed at the end in order to produce a correct ResultPair. That is, $\texttt{frewrite(}\overline{\mathcal{R}}\texttt{, }\overline{t}\texttt{, }b\texttt{, }n\texttt{)}$ results in the metarepresentation of the term obtained from $t$ after at most $b$ applications of the rules in $\mathcal{R}$ using the frewrite strategy, with at most $n$ rewrites at each entitled position on each traversal of a subject term, 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.

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

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

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