[Maude-help] Priorities between rules

[Marc Boyer]

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