Maude-help mailing list

["Pierre Fourès" <pierre.foures AT gmail.com>]

Thanks Francisco,

This was quite obvious indeed but i couldn't get my mind to work it out. I'm quite new to maude and rewriting logic and often block on easy issues. I think this was the "getContext()" who made me think like in object oriented programming and confused me while using the rewriting logic.

By the way, I now use the substituted values found by the metaXmatch instead of simply replacing the [] by 'nullThread.Thread]. I proceed quite the same way as you did and I got this :

    op getSubst : Substitution Variable -> Term .

    ceq getSubst((Sub ; Sub'), V)

      = (getSubst(Sub, V); getSubst(Sub', V))

      if Sub =/= none /\ Sub' =/= none .

    eq getSubst((V <- T), V) = T .

    eq getSubst(Sub, V) = none [owise] .

And I use it like that :  getSubst(getSubstitution(tmpMatch), 'Tb:Trans) to retrieve the value.

It works fine this way but I was wondering if it was the by way to achieve it or if it's a cleaner way to retrieve the values ?

Thanks again for unlocking me,

Regards,

Pierre Fourès.

2008/12/16 Francisco Durán <duran AT lcc.uma.es>

The important equation was missing...

fmod FOO is
 pr META-LEVEL .

 var F : Qid .
 var C : Constant .
 var V : Variable .
 vars GTL GTL' : GTermList .
 var T : Term .

 op newTerm : Context Term -> Term .
 eq newTerm(F[GTL], T) = F[newTerm(GTL, T)] .
 eq newTerm(C, T) = C .
 eq newTerm(V, T) = V .

 eq newTerm([], T) = T .

 ceq newTerm((GTL, GTL'), T)
   = (newTerm(GTL, T), newTerm(GTL', T))
   if GTL =/= empty /\ GTL' =/= empty .
endfm

red newTerm('`[_`,_`,_`]['null.Marking,'nullTransition.Trans,[]], 'nullThread.Thread) .

Paco