Maude-help mailing list

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

I don't see what is your problem.

Please, try

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 .
  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) .

Cheers,

Paco

El 15/12/2008, a las 14:46, Pierre Fourès escribió:

> Hi,
>
> I'm currently using metaXmatch and I would appreciate some help with  
> the use of getContext.
>
> The maude manual discuss by the end of page 291 (numbered as 279)  
> about the getContext selector (available for both metaXapply and  
> metaXmatch). The provided result includes a single "hole" where the  
> rewriting has taken place. This "hole" is represented by [] and is a  
> term of the Context's sort.
>
> I'm looking forward to replace it with an other term. I thought  
> about an equation taking this Context term and a replacing Term to  
> producing a new Term. It could look something like : op newTerm :  
> Context Term -> Term .
>
> In a trivial example, getContext produces the following : result  
> Context: '`[_`,_`,_`]['null.Marking,'nullTransition.Trans,[]]
> My point would be to replace the previous result with : result  
> Context: '`[_`,_`,_`]['null.Marking,'nullTransition.Trans,  
> 'nullThread.Thread]
>
> Unfortunately I can't figure out how to replace the [] at its  
> precise position. I'm sure I'm missing something obvious, could  
> someone put me back on track ?
>
>
> In advance, thanks for your help,
> Regards,
> Pierre Fourès
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help