Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

Dear Pierre,

You are welcome.

Regarding your question, it's your choice. I don't think one way is  
"cleaner" than the other.

BTW, consider the following definition of getSubst:

    eq getSubst((V <- T ; Sub), V) = T .
    eq getSubst(Sub, V)
        = none ------------------ how can it return none ?
        [owise] .

Paco

El 18/12/2008, a las 15:26, Pierre Fourès escribió:

> 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