Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

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

One alternative to get the sorts right would be to add a LIST{D} with  
D < B C, and making List{D} < List{B} List{C}. But, although correct,  
you would still get the advisories. The advisories are given when the  
modules are imported, before completing the sort structure.

Another alternative, valid if you don't want to relate the list sorts,  
and which doesn't give any advisories, is to rename the operators when  
importing one of the modules. Try

fmod LIST-A-B-C is
 protecting LIST{B} * (op nil to nilB,
                       op __ to _._,
                       op append to appendB,
                       op head to headB,
                       op tail to tailB,
                       op last to lastB,
                       op front to frontB,
                       op occurs to occursB,
                       op reverse to reverseB,
                       op $reverse to $reverseB,
                       op size to sizeB,
                       op $size to $sizeB) .
 protecting LIST{C} .
endfm

Regards,

Paco

El 19/08/2009, a las 10:14, Marc Boyer escribió:

> Dear all,
>
> I have a problem of multiple instanciation of a LIST with two sorts,
> subsorts of a common sort.
>
> Here is a minimal example
>
> fmod SOME-SORTS is
>  sorts A B C .
>  subsort B < A .
>  subsort C < A .
> endfm
>
> view B from TRIV to SOME-SORTS is
>  sort Elt to B .
> endv
>
> view C from TRIV to SOME-SORTS is
>  sort Elt to C .
> endv
>
> fmod LIST-A-B-C is
>  protecting LIST{B} .
>  protecting LIST{C} .
> endfm
>
> Then, maude complains
> Advisory: "ListAndCommonAncestor.maude", line 26 (fmod LIST-A-B-C):  
> operator
>    nil has been imported from both "prelude.maude", line 991 (fmod
> LIST) and
>    "prelude.maude", line 991 (fmod LIST) with no common ancestor.
>
> Of course, this is a simplified example. In the application, LIST{B}  
> is
> used in one module, LIST{C} in another, and there exists a third  
> module
> which import both.
>
> Is there any solution ? I could use in both a LIST{A} (the common
> ancestor), but in this case, I losses some typing...
>
> Last detail, in the real application, there is a fort sort, D,
> which is a subsort of B and C. Any solution should allow this...
>
> Any idea ?
>
> 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
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help