Maude-help mailing list

[Michael Katelman <katelman AT uiuc.edu>]

Note that if you were using equations instead of rules, you could do
what you are asking for with the "strat" attribute.

On Fri, May 27, 2011 at 11:03 AM, Michael Katelman 
<katelman AT uiuc.edu>
 wrote:
> 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
>>
>