Maude-help mailing list

[Marc Boyer <Marc.Boyer AT onera.fr>]

Le 27/05/2011 16:14, Iago Abal a écrit :
> Thanks for your response Michael.
>
> I was able to apply (1) in some cases which solved my problem partially,
> unfortunately it is not applicable in every situation. For instance, I
> have a language with let-in expressions, and a rule to unfold a let-in
> rl [unfold-def] : let x := X in P => unfold(x,X,P) .
> I would like to prevent any application of unfold-def whenever there is
> any other rule that can be applied. This is very important for me since
> I am working with programs that are huge when every definition is
> unfolded, so it is needed to just unfold a bit, simplify most you can,
> unfold some few definitions more, ...

Perhaps could you play with equations and rules ? Equations are applied
before rules.

> Of course ideally I would like
> Maude to be aware of the concept of "definition"/common subterm, but I
> think it is not the case (Am I wrong?)!

  maude is somehow aware of "common subterm" inside a simple rule. That 
is to say, with a rule like

  eq f(x) = g(x) + g(x) .

the reduction of g(x) is done only once.

 Another point of view of the notion of "common subterm" is the [memo] 
attribute.


Regards,
  Marc Boyer
--
Marc Boyer, Ingenieur de recherche                              ONERA
Tel: (33)  5.62.25.26.36                                         DTIM
Fax: (33)  5.62.25.26.52                          2, av Edouard Belin
http://www.onera.fr/staff/marc-boyer/          31055 TOULOUSE Cedex 4