Maude-help mailing list

[Jeff Thompson <jeff AT thefirst.org>]

When Maude reduces a term to its canonical form, which may be stored and 
used later, I'm looking for a way to keep track of the original 
unreduced term. For example:

Maude> red in NAT-LIST : 0 (1 + 2 * 3) .
result NeNatList: 0 7

I have the result structure 0 7, but I want a way to examine the 7 
(actually the constructor s_^7(0)) to find out the "provenance" 
information that it came from the original term (1 + 2 * 3).

I've been playing with LOOP-MODE to try to do this, but I'm sure it is 
not an original idea as a way of tracking history and provenance of the 
terms in a data structure. Is there a way that the original unreduced 
top-level term can be "tracked through" during the reduction so that it 
is "tacked on" somehow to the final canonical term?

Thanks for any help,
- Jeff