[Maude-help] metaReduce functionality

[Chucky Ellison]

Hello all,

I am trying to generate some automated tests, and because of my 
particular application, I need to be able to grab intermediary states 
during the reduction of a term (aside: I am defining an abstraction 
function between two Maude theories, so I have to test it on each 
equational step in different reductions).  How can I get at this 
information?  If there were some kind of metaTrace, or depth for 
metaReduce, or metaDebugStep etc., I could get it.  I can't even write 
code to do this manually by looping through the list of equations 
because metaApply only applies to rewrite rules, not equations.

It seems like Maude's reflection system is very powerful otherwise, so I 
feel like I must be missing something obvious.  Is there any way to 
apply a single /equation/ (not a rule) at a time?  Even better would be 
to apply a single equation, letting Maude choose which equation to apply 
(ie, step).

Thanks for any help or direction you can offer,

-Chucky Ellison
UIUC FSL