Maude-help mailing list

[Iago Abal <iago.abal AT gmail.com>]

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, ... 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?)! 

I knew (2) but I discarded it because it looks promising but immature. Moreover there is only an implementation based on full-maude providing all described features, whilst core-maude just support the most basic ones which are not enough for my needs.

Cheers,

On Thu, May 26, 2011 at 3:38 AM, Michael Katelman <katelman AT uiuc.edu> wrote:

Hi Iago,

As far as I know, what you asked for is not directly possible in
Maude. What you are talking about is imposing a "strategy" used for
rewriting.

Here are two options, (1) is probably the most sensible:

(1) modify the rules to enforce ordering: something like

rl [A] t1 => t2 .

crl [B] s1 => s2
 if ruleANotEnabled(s1) .

(2) there is an experimental strategy language implemented at the
meta-level and which *might* allow you to do what you want:

http://maude.sip.ucm.es/strategies/

-Mike

On Wed, May 25, 2011 at 5:44 PM, Iago Abal <iago.abal AT gmail.com> wrote:
> Hi all,
> I am sorry if I missed something but after some doc reading I didn't figure
> out how I could assign priorities to my rules in order to ensure that Maude
> (concretely, the rewrite command) will never try to apply a rule B if
> another rule A is applicable, in case A has higher priority than B. Is this
> possible? Is there some workaround?
>
> Thanks in advance,
> --
> Iago Abal Rivas
>

> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>
>

-- 
Iago Abal Rivas