metaApply

The (partial) operation metaApply takes as arguments the metarepresentation of a module, the metarepresentation of a term, the metarepresentation of a rule label, the metarepresentation of a set of assignments (possibly empty) defining a partial substitution, and a natural number.

  sorts Assignment Substitution .
  subsort Assignment < Substitution .
  op _<-_ : Variable Term -> Assignment [ctor prec 63] .
  op none : -> Substitution [ctor] .
  op _;_ : Substitution Substitution -> Substitution 
       [assoc comm id: none prec 65] .

  sort ResultTriple ResultTriple? .
  subsort ResultTriple < ResultTriple? .
  op {_,_,_} : Term Type Substitution -> ResultTriple [ctor] .
  op failure : -> ResultTriple? [ctor] .
  op metaApply : Module Term Qid Substitution Nat ~> ResultTriple? 
       [special (...)] .

The operation $\texttt{metaApply(}\overline{\mathcal{R}}\texttt{, }\overline{t}\texttt{, }\overline{l}\texttt{, }\sigma\texttt{, }n\texttt{)}$ is evaluated as follows:

1. the term $t$ is first fully reduced using the equations in $\mathcal{R}$;
2. the resulting term is matched at the top against all rules with label $l$ in $\mathcal{R}$ partially instantiated with $\sigma$, with matches that fail to satisfy the condition of their rule discarded;
3. the first $n$ successful matches are discarded; if there is an $(n +1)$th match, its rule is applied using that match and the steps 4 and 5 below are taken; otherwise failure is returned;
4. the term resulting from applying the given rule with the $(n +1)$th match is fully reduced using the equations in $\mathcal{R}$;
5. the triple formed by the metarepresentation of the resulting fully reduced term, the metarepresentation of its corresponding sort or kind, and the metarepresentation of the substitution used in the reduction is returned.

The failure value should not be confused with the ``undefined'' value for the metaApply operation. As already mentioned before for descent functions in general, this operation is partial because it does not make sense on some nonvalid arguments that are terms of the appropriate sort but are not correct metarepresentations. However, even if all arguments are valid in this sense, the intended rule application may fail, either because there is no match or because the match does not satisfy the corresponding rule condition, and then failure is used to represent this situation, which is important to distinguish from ill-formed invocations, for example, for error recovery purposes.

Note also that, according to the information in step 3 above, the last argument of metaApply is a natural number used to enumerate (starting from 0) all the possible solutions of the intended rule application. For efficiency, the different solutions should be generated in order, that is, starting with the argument 0 and increasing it until a failure is obtained, indicating that there are no more solutions.

Appropriate selectors extract from the result triples their three components:

  op getTerm : ResultTriple -> Term .
  op getType : ResultTriple -> Type .
  op getSubstitution : ResultTriple -> Substitution .

As an example, we can force at the metalevel the rewriting of the term $ in the module VENDING-MACHINE, so that only the rule buy-c is used, and only once.

  Maude> reduce in META-LEVEL :
           metaApply(upModule('VENDING-MACHINE, false), 
             '$.Coin, 'buy-c, none, 0) .
  result ResultTriple: {'c.Item, 'Item, none}

Similarly, we can force the rewriting of the same term so that this time only the rule add-$ is applied.

  Maude> reduce in META-LEVEL :
           metaApply(upModule('VENDING-MACHINE, false), 
             '$.Coin, 'add-$, none, 0) .
  result ResultTriple:
    {'__['$.Coin, '$.Coin], 'Marking, 'M:Marking <- '$.Coin}

However, using metaApply, we cannot force the term q $ to be rewritten with the rule buy-c, since its lefthand side, $, does not match (without extension) this term. In this case, we should use instead the metaXapply operation described below.

  Maude> reduce in META-LEVEL :
           metaApply(upModule('VENDING-MACHINE, false),
             '__['q.Coin, '$.Coin], 'buy-c, none, 0) .
  result ResultTriple?: (failure).ResultTriple?