Maude-help mailing list

[gcaltais <gcaltais AT info.uaic.ro>]

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