Maude-help mailing list

[Michael Katelman <katelman AT uiuc.edu>]

On Fri, May 27, 2011 at 9:14 AM, Iago Abal 
<iago.abal AT gmail.com>
 wrote:
> 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 see; and, unfortunately, I can't think of an elegant solution.
Although I would certainly discourage this, I suppose it should still
be *possible* to apply something similar to (1).

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

This seems very sensible to me.

Sorry for not being able to provide something more helpful.

-Mike

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