Maude-help mailing list

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

Francisco Durán a écrit :
> Hi Marc,
>
> Maude assumes your modules are preregular 
> (http://maude.cs.uiuc.edu/maude2-manual/html/maude-manualch3.html#x15-350003.8), 
> which basically means that any term has a unique least sort.
>
> This is not the case in your example, since nil comes both from LIST{B} 
> and LIST{C}, with no common ancestor. And not only nil, you are probably 
> getting similar advisories for operators __, append, ...

   I understand the reason with nil, but not for other operators.
I can "expand" the module, and remove any ambiguity.

fmod SOME-SORTS is
  sorts A B C  .
  subsort B < A .
  subsort C < A .
  op b : -> B .
  op c : -> C .
  op _ + _ : B B -> B .
  op _ + _ : C C -> C .
endfm

red b + b .
red c + c .

  Maude is then able to find the sort of b + b and c + c.

Regards,
   Marc Boyer
--
Marc Boyer, Ingenieur de recherche                              ONERA
Tel: (33)  5.62.25.26.36                                         DTIM
Fax: (33)  5.62.25.26.52                          2, av Edouard Belin
http://www.onera.fr/staff/marc-boyer/          31055 TOULOUSE Cedex 4