Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi Jeff,

You could always use the operator strategy mechanism:

fmod EVAL-WITH-HISTORY is
  pr NAT .
  sorts Expr HistPair .
  subsort Nat < Expr .
  op eval-with-history : Expr -> HistPair [strat (0)] .
  op _ evaluated to _ : Expr Nat -> HistPair [strat (2 0)].

  eq eval-with-history(E:Expr) = E:Expr evaluated to E:Expr .
endfm

red eval-with-history(1 + 2 * 3) .

Steven

On Monday 04 May 2009 01:26, Jeff Thompson wrote:
> 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
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help