[Maude-help] metaReduce functionality

[Francisco Duran]

Hi Chucky,

There is no way to trace the application of equations at the metalevel. 
But you can transform your equations into rules, by hand or using a 
transformation function, and then use metaApply, metaXapply and so on to 
trace/guide your execution.

Paco


Chucky Ellison escribió:
> 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
> _______________________________________________
> Maude-help mailing list
> Maude-help at maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help
> 
>