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.
