As yet another example of user-defined strategies in Maude, we specify in an extension of the module STRATEGY a meta-interpreter for modules that only contain rules that are Church-Rosser and terminating (no equations are declared and none of the operators have attributes). For the sake of simplicity, we assume that all the rules are labeled any.
fmod META-INTERPRETER is protecting STRATEGY . sorts Position . subsorts MachineInt < Position . op emptyPos : -> Position . op pos : Position Position -> Position [assoc] . op nullPos : -> Position . op getSubterm : Term Position -> Term . op getSubtermAux : TermList Position -> Term . op replace : Term Term Position -> Term . op replaceAux : TermList Term Position -> Term . op nextPosition : Term Position -> Position . op nextPositionUp : Term Position -> Position . var P : Position . var N : MachineInt . var F G X Y L S : Qid . var T T' T1 T1' : Term . var TL TL' : TermList . eq pos(emptyPos, P) = P .
We first define some auxiliary functions needed to find the positions in a term. Positions are represented at the metalevel as pos-lists of natural numbers, and emptyPos is the empty position. We denote by |¯p¯| the representation of a position p in the module META-INTERPRETER.
The function getSubterm( |¯t¯| , |¯p¯| ) returns the term |¯t|p¯| , if p is a valid position in t; otherwise, it returns error*.
eq getSubterm(F, N) = error* . eq getSubterm({F}S, N) = error* . eq getSubterm(F[TL], N) = getSubtermAux(TL, N) . eq getSubterm(F, pos(N, P)) = error* . eq getSubterm({F}S, pos(N, P)) = error* . eq getSubterm(F[TL], pos(N, P)) = getSubterm(getSubtermAux(TL, N), P) . eq getSubtermAux((T, TL), N) = if N == 1 then T else getSubtermAux(TL, (N - 1)) fi . eq getSubtermAux(T, N) = if N == 1 then T else error* fi .
The function nextPosition( |¯t¯| , |¯p¯| ) returns the next position in the tree defined by the term t, according to a top-down leftmost-innermost strategy. If all positions have already been considered, the function nextPosition returns nullPos.
eq nextPosition(T, P) = if getSubterm(T, pos(P, 1)) == error* then nextPositionUp(T, P) else pos(P, 1) fi . eq nextPositionUp(T, emptyPos) = nullPos . eq nextPositionUp(T, N) = if getSubterm(T, (N + 1)) == error* then nullPos else (N + 1) fi . eq nextPositionUp(T, pos(P, N)) = if getSubterm(T, pos(P, (N + 1))) == error* then nextPositionUp(T, P) else pos(P, (N + 1)) fi .
The function replace( |¯t¯| , |¯t'¯| , |¯p¯| ) returns the term |¯t[t']p¯| .
eq replace(T, T', emptyPos) = T' . eq replace(F, T', N) = error* . eq replace({F}S, T', N) = error* . eq replace(F[TL], T', N) = F[replaceAux(TL, T', N)] . eq replace(F, T', pos(N, P)) = error* . eq replace({F}S, T', pos(N, P)) = error* . eq replace(F[TL], T', pos(N, P)) = F[replaceAux(TL, T', pos(N, P))] . eq replaceAux((T, TL), T', N) = if N == 1 then (T', TL) else (T, replaceAux(TL, T', (N - 1))) fi . eq replaceAux(T, T', N) = if N == 1 then T' else error* fi . eq replaceAux((T, TL), T', pos(N, P)) = if N == 1 then (replace(T, T', P), TL) else (T, replaceAux(TL, T', pos((N - 1), P))) fi . eq replaceAux(T, T', pos(N, P)) = if N == 1 then replace(T, T', P) else error* fi .
Finally, we introduce the strategy metaInterpreter that specifies the Maude interpreter for functional modules17, that is, for any valid module M and any term t in that module, rewInWith( |¯M¯| , |¯t¯| , nilBindingList, metaInterpreter) returns rewInWith( |¯M¯| , |¯t'¯| , nilBindingList, idle), where t' is the canonical form of t with respect to M.
op metaInterpreter : -> Strategy . op applyInPRedex : Position -> Strategy . var M : Module . eq rewInWith(M, T, nilBindingList, metaInterpreter) = rewInWith(M, T, nilBindingList, orelse(and(applyInPRedex(emptyPos), metaInterpreter), idle)) .
The auxiliary strategy applyInPRedex( |¯p¯| ) specifies an interpreter that only applies once a rule to a term t at position p or at any position "after" p in t (traversing the tree defined by t with a top-down leftmost-innermost strategy).
eq rewInWith(M, T, nilBindingList, applyInPRedex(P)) = if P =/= nullPos then (if meta-apply(M, getSubterm(T, P), 'any, none, 0) == {error*, none} then rewInWith(M, T, nilBindingList, applyInPRedex(nextPosition(T, P))) else rewInWith(M, replace(T, extTerm( meta-apply(M, getSubterm(T, P), 'any, none, 0)), P), nilBindingList, idle) fi) else failure fi .
As an example, consider the following module NAT-TREE:
mod NAT-TREE is sorts Nat Tree . subsort Nat < Tree . op 0 : -> Nat . op s_ : Nat -> Nat . op _+_ : Nat Nat -> Nat . vars N M : Nat . rl [any]: (N + 0) => N . rl [any]: (0 + N) => N . rl [any]: (s N + s M) => s s (N + M) . op _^_ : Tree Tree -> Tree . op rev : Tree -> Tree . vars T T' : Tree . rl [any]: rev(N) => N . rl [any]: rev(T ^ T') => (rev(T') ^ rev(T)) . endm
Thus, in the module NAT-TREE, the tree
is represented by the term
(((s 0 + s s 0) ^ s 0) ^ (0 ^ (s 0 + s 0))).
We extend the modulo META-INTERPRETER with the equation
op NAT-TREE : -> Module . eq NAT-TREE = (mod 'NAT-TREE is including 'BOOL . sorts ('Nat ; 'Tree) . subsort 'Nat < 'Tree . op '0 : nil -> 'Nat [none] . op 's_ : 'Nat -> 'Nat [none] . op '_+_ : ('Nat 'Nat) -> 'Nat [none] . op '_^_ : ('Tree 'Tree) -> 'Tree [none] . op 'rev : 'Tree -> 'Tree [none] . var 'N : 'Nat . var 'M : 'Nat . var 'T : 'Tree . var 'T' : 'Tree . none none rl ['any]: '_+_['N, {'0}'Nat] => 'N . rl ['any]: '_+_[{'0}'Nat, 'N] => 'N . rl ['any]: '_+_['s_['N], 's_['M]] => 's_['s_['_+_['N, 'M]]] . rl ['any]: 'rev['N] => 'N . rl ['any]: 'rev['_^_['T, 'T']] => '_^_['rev['T'], 'rev['T]] . endm) .
The result of computing the strategy metaInterpreter on the metarepresentation of the operation of reversing the above tree is the following
Maude> rew rewInWith(NAT-TREE, 'rev['_^_['_^_['_+_['s_[{'0}'Nat], 's_['s_[{'0}'Nat]]], 's_[{'0}'Nat]], '_^_[{'0}'Nat, '_+_['s_[{'0}'Nat], 's_[{'0}'Nat]]]]], nilBindingList, metaInterpreter) . result StrategyExpression: rewInWith(NAT-TREE, '_^_['_^_['s_['s_[{'0}'Nat]],{'0}'Nat], '_^_['s_[{'0}'Nat],'s_['s_['s_[{'0}'Nat]]]]], nilBindingList, idle)
Thus, the result is the meta-representation of the tree
that is, the meta-representation of the original tree reversed after all its leaves have been evaluated.