Maude-help mailing list

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

Dear all,

I would like to have priorities between rules.

The motivation is some calculation of upper bound,
with some basic rules and some better one.

A minimal running example is the following:
-------------------------------------------
mod RULE-PREC is
 protecting STRING .
 sorts S T .
 subsort T < S .

 var s : S .
 var t : T .

 op Name _ : S -> String .
 op doS : -> S .
 op doT : -> T .

*** Equational version
*** eq [NameS] : Name s = "sort-s"  .
*** eq [NameT] : Name t = "sort-t"  .

*** Rule version
 rl [NameS] : Name s => "sort-s" . 
 rl [NameT] : Name t => "sort-t" .                 
endm    

rew Name doS .
rew Name doT .
-------------------------------------------

I would like 'Name doS' to become "sort-s" and 'name doT'
to become "sort-t". But the code, as given there,
rewrite 'Name doT' in "sort-s", which is true, but not
the more accurate.

I have found two hacks, but I was wondering if there i a better way.

a) Changing rule orders
  If I change the order of rule [NameS] and [NameT] in the source
file, it works. But, in my real problem, S and T are in different
modules.

b) Using equations and the [owise] attribute
  I can use equations instead of rules, and set the [owise]
attribute to equation [NameS]. It works (that is what I am using),
but it is not scalable: with a sort U, subsort of T, it fails.


Is there any other (and better) way ?


Marc Boyer
--
Marc Boyer                  INPT - ENSEEIHT - Dép. Télécoms & Réseaux
Tel: (33)  5.61.58.80.21                                     IRIT-IRT
Fax: (33)  5.61.58.80.14                              2, rue Camichel
http://www.enseeiht.fr/~boyer/                 31071 TOULOUSE Cedex 7