Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi,

Sorry for the delay in replying.  There are two problems:

fmod TEST-MODULE is
  including LIST{Equation} .
endfm

Here the __ list constructor gets confused with the EquationSet constructor 
in 
META-MODULE.

fmod TEST-MODULE is
  including META-MODULE .
  including LIST{Constant} .
endfm

Here because META-MODULE protects QID-LIST and Constant is a subsort of Qid, 
LIST{Constant} becomes confused with QID-LIST.

My suggestion is to rename __ in LIST before instantiating LIST{Equation} and 
to use QID-LIST rather than LIST{Constant} :

fmod TEST-MODULE is 
  including QID-LIST .
  including (LIST * (op __ to _|_)){Equation} .
endfm

Actually since view Equation implicitly imports QID-LIST you could leave out 
explicitly importing it.

Steven

On Friday 11 January 2008 07:15, gcaltais wrote:
> Greetings,
>
> I encountered a problem when trying to define two lists within a certain
> module.
> In particular, there is list of constants and a list of equations. The
> related
> code is as follows:
>
> ---[---[---[---[---[---[---[---[---[---[---[
> *** File test.maude
> view Constant from TRIV to META-TERM is
>    sort Elt to Constant .
> endv
>
> view Equation from TRIV to META-MODULE is
>    sort Elt to Equation .
> endv
>
> fmod TEST-MODULE is
>
>   including LIST{Constant} .
>   including LIST{Equation} .
>
> endfm
> ---]---]---]---]---]---]---]---]---]---]---]
>
>
> When loading the example, the result is:
>
> ---[---[---[---[---[---[---[---[---[---[---[
> Maude> in test.maude
> ==========================================
>
> Reading in file: "test.maude"
> ==========================================
> view Constant
> ==========================================
> view Equation
> ==========================================
> fmod TEST-MODULE
> Warning: "prelude.maude", line 985 (fmod LIST): declaration for __ has
>     different attributes from declaration on "prelude.maude", line 1761
> (fmod
>     META-MODULE).
> Advisory: <automatic>: operator __ has been imported from both
> "prelude.maude",
>     line 1761 (fmod META-MODULE) and "prelude.maude", line 985 (fmod LIST)
> with
>     no common ancestor.
> Warning: "prelude.maude", line 985 (fmod LIST): declaration for __ has
>     different attributes from declaration on "prelude.maude", line 1761
> (fmod
>     META-MODULE).
> Warning: "prelude.maude", line 985 (fmod LIST): declaration for __ has
>     different attributes from declaration on "prelude.maude", line 1761
> (fmod
>     META-MODULE).
> Done reading in file: "test.maude"
> ---]---]---]---]---]---]---]---]---]---]---]
>
>
> I believe the problem is the multiple importation of the __ operator.
> Trying to solve the problem, I defined my own generic list:
>
> ---[---[---[---[---[---[---[---[---[---[---[
> *** This module is intended to solve the multiple imports problem
> *** when more than one kind of list are used in the same module.
> fmod NIL-LIST is
>
>   sort NilList .
>
>   op nsnil :                 -> NilList [ctor] .
>   op _.._  : NilList NilList -> NilList [ctor assoc id: nsnil prec 25] .
>
> endfm
>
> *** "Non Standard" List
> fmod NSLIST{X :: TRIV} is
>
>   including NIL-LIST .
>
>   sorts NeNsList{X} NsList{X} .
>   subsort X$Elt < NeNsList{X} < NsList{X} .
>   subsort NilList < NsList{X} .
>
>   op _.._ : NsList{X}   NsList{X}   -> NsList{X}   [ctor ditto] .
>   op _.._ : NeNsList{X} NsList{X}   -> NeNsList{X} [ctor ditto] .
>   op _.._ : NsList{X}   NeNsList{X} -> NsList{X}   [ctor ditto] .
>
> endfm
>
> view Constant from TRIV to META-TERM is
>    sort Elt to Constant .
> endv
>
> view Equation from TRIV to META-MODULE is
>    sort Elt to Equation .
> endv
>
> fmod TEST-MODULE is
>
>   including NSLIST{Constant} .
>   including NSLIST{Equation} .
>
> endfm
> ---]---]---]---]---]---]---]---]---]---]---]
>
>
> Now, when loading the example, the result is:
>
> ---[---[---[---[---[---[---[---[---[---[---[
> Maude> in test.maude
> ==========================================
>
> Reading in file: "test.maude"
> ==========================================
> fmod NIL-LIST
> ==========================================
> fmod NSLIST
> ==========================================
> view Constant
> ==========================================
> view Equation
> ==========================================
> fmod TEST-MODULE
> Advisory: "test.maude", line 37 (fmod TEST-MODULE): operator none has been
>     imported from both "prelude.maude", line 1123 (fmod SET) and
>     "prelude.maude", line 1760 (fmod META-MODULE) with no common ancestor.
> Warning: "prelude.maude", line 1761 (fmod META-MODULE): declaration for __
> has
>     different attributes from declaration on "prelude.maude", line 985
> (fmod
>     LIST).
> Advisory: "test.maude", line 37 (fmod TEST-MODULE): operator __ has been
>     imported from both "prelude.maude", line 985 (fmod LIST) and
>     "prelude.maude", line 1761 (fmod META-MODULE) with no common ancestor.
> Warning: "test.maude", line 37 (fmod TEST-MODULE): this module contains one
> or
>     more errors that could not be patched up and thus it cannot be used or
>     imported.
> Done reading in file: "test.maude"
> ---]---]---]---]---]---]---]---]---]---]---]
>
>
> Would you please help me by telling me why these warnings appear in this
> case
> and how the problem could be solved ?
>
> Thank you,
> Georgiana
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help