Maude-help mailing list

[Rubén Rafael Rubio Cuéllar <rubenrub AT ucm.es>]

Hi Ozan,

Another possibility is using the Maude strategy language. The strategy top(all) applies any rule at level 0, and a strategy can be applied on specific subterms with the matchrew combinator. For example, if your module M has two operators f of arity n and g of arity m, the following strategy atdepth(k) will apply any rule at depth at most k (or at depth exactly k if the top(all) | of the second strategy definition is removed):

smod M-STRAT is   protecting M .   protecting NAT .    strat atdepth : Nat @ Foo . var X1 : T1 . var Xn : Tn .    sd atdepth(0) := top(all) .    sd atdepth(s(N)) := top(all) | matchrew f(X1, ..., Xn) by X1 using atdepth(N) | ... | matchrew f(X1, ..., Xn) by Xn using atdepth(N) | matchrew g(X1, ..., Xm) by X1 using atdepth(N) | ... | matchrew g(X1, ..., Xm) by Xm using atdepth(N) . endsm

It can then be executed with the srewrite command, like srewrite f(...) using atdepth(3) ., that will show all the possible such rewrites.

The disadvantage is that a matchrew combinator should be written for each operator that may appear in the terms. Using generic traversals, which are available in other strategy languages but not in Maude's, the second definition could have been generically written sd atdepth(s(N)) := one(atdepth(N)) | top(all) ..

Best, Rubén.