metaXapply

The (partial) operation metaXapply 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, a natural number, a Bound value, and another natural number.

The operation $\texttt{metaXapply(}\overline{\mathcal{R}}\texttt{, } \overline{t}\texttt{, }\overline{l}\texttt{, }\sigma\texttt{, }n\texttt{, }b\texttt{, }m\texttt{)}$ is evaluated as the function metaApply but using extension (see Section 4.8) and in any possible position, not only at the top. The arguments $n$ and $b$ can be used to localize the part of the term where the rule application can take place:

• $n$ is the lower bound on depth in terms of nested operators, and should be set to 0 to start searching from the top, while
• the Bound argument $b$ indicates the upper bound, and should be set to unbounded to have no cut off.

Notice that nested occurrences of an operator with the assoc attribute are counted as a single operator for depth purposes, that is, matching takes place on the flattened term (see Section 4.8). The same idea applies to iter operators (see section 4.4.2): a whole stack of an iter operator counts as a single operator. Furthermore, because of matching with extension, the solution may have an extra layer, as illustrated in the matching examples at the end of Section 11.4.5.

The last Nat argument $m$ in $\texttt{metaXapply(}\overline{\mathcal{R}}\texttt{, } \overline{t}\texttt{, }\overline{l}\texttt{, }\sigma\texttt{, }n\texttt{, }b\texttt{, }m\texttt{)}$, as in the case of the operation metaApply, is the solution number, used to enumerate multiple solutions. The first solution is 0, and they should again be generated in order for efficiency.

The result of metaXapply has an additional component, giving the context (a term with a single ``hole'', represented []) inside the given term $t$, where the rewriting has taken place. The sort CTermList represents lists of terms with exactly one ``hole,'' that is, exactly one term of sort Context, the rest being of sort Term. The sort GTermList is the supersort of CTermList and TermList needed for the assoc attribute to make sense.

  sorts Context CTermList GTermList  .
  subsort Context < CTermList .
  subsorts TermList CTermList < GTermList .
  op [] : -> Context [ctor] .
  op _,_ : TermList CTermList -> CTermList 
       [ctor assoc gather (e E) prec 120] .
  op _,_ : CTermList TermList -> CTermList 
       [ctor assoc gather (e E) prec 120] .
  op _[_] : Qid CTermList -> Context [ctor] .

  sorts Result4Tuple Result4Tuple? .
  subsort Result4Tuple < Result4Tuple? .
  op {_,_,_,_} : Term Type Substitution Context -> Result4Tuple 
       [ctor] .
  op failure : -> Result4Tuple? [ctor] .

  op metaXapply :
       Module Term Qid Substitution Nat Bound Nat ~> Result4Tuple?
       [special (...)] .

Appropriate selectors extract from the result 4-tuples their four components:

  op getTerm : Result4Tuple -> Term .
  op getType : Result4Tuple -> Type .
  op getSubstitution : Result4Tuple -> Substitution .
  op getContext : Result4Tuple -> Context .

As an example, we can force at the metalevel the rewriting of the term $ q in the module VENDING-MACHINE so that only the rule buy-c is used (compare with the last metaApply example).

  Maude> reduce in META-LEVEL :
           metaXapply(upModule('VENDING-MACHINE, false),
             '__['q.Coin, '$.Coin], 'buy-c, none, 0, unbounded, 0) .
  result Result4Tuple: 
    {'__['q.Coin, 'c.Item], 'Marking, none, '__['q.Coin, []]}

Notice the fragment '__['q.Coin, []] of the result, providing the context where the rule has been applied. Since this is the only possible solution, if we request the ``next'' solution (by increasing to 1 the last argument), the result will be a failure.

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