Maude-help mailing list

[Juan Ignacio Perna <jiperna AT cs.york.ac.uk>]

Hello,

I have just started using Maude and I bumped into a couple of things I 
don't know how to handle.
I have defined my own list module (I want to use comma to separate 
elements in the list) together with a set and bag modules (all these 
definitions are in the file utils.maude). This seems to compile and work 
(as far as I could test it).

After this I started defining a module of expressions (I want to embed 
another language in Maude). I defined three sorts (Var, Exp and Cond) 
and wanted to create sorts for lists of Var and Exp and a bags of Cond. 
I also did not want to write 'List{Var}' every time I wanted a list of 
variables (and so on), so my idea was to do something similar to what is 
done in the prelude for lists of naturals. My version of this is in file 
exp1.maude.

When I tried to input all these into Maude (I did: "in utils.maude" and 
then "in exp1.maude") I got this back:

Maude> in utils.maude
==========================================
fmod SET
...
fmod BAG

(so far, so good)

Maude> in exp1.maude
==========================================
fmod EXP-SORTS
==========================================
...
==========================================
fmod EXP
Advisory: "exp1.maude", line 32 (fmod EXP): operator empty has been imported
   from both "utils.maude", line 8 (fmod SET) and "utils.maude", line 8 
(fmod
   SET) with no common ancestor.
...
More 'advisory' errors like the one above
...
Warning: "utils.maude", line 68 (fmod BAG): declaration for _`,_ has 
different
   attributes from declaration on "utils.maude", line 23 (fmod LIST).
...

My questions are:

If I got it right, the first 'Advisory' message is telling me that I 
have two copies of the same operator (empty) without a super-kind.
The error seems to come from the two 'instantiations' of lists I am 
doing... What should I do here? Should I ignore this? I gave it a 
thought and I could not come up with a super-kind for the two lists (may 
be the generic, un-instantiated List{X :: Triv}, but how could I express 
this anyway?)

About the warning message, the problem seems to be that I have declared:

fmod LIST {X :: TRIV} is  ...  op _,_ : List{X} List{X} -> List{X} [ctor 
assoc id: nil prec 9] . ... endfm

and

fmod BAG {X :: TRIV} is  ... op _,_ : Bag{X} Bag{X} -> Bag{X} [ctor 
assoc comm id: emptybag prec 9] . ... endfm

Even though I am overloading the name, the properties are not the same 
for both of them, so I could not make the list of attributes equal. I 
don't really understand why the requirement of overloaded operator to 
have the same attributes (if this is the correct interpretation of this 
warning), as the situation I am in seems to be pretty common. Is this a 
bug? If it is not, is there a way round this problem? (without renaming 
the operation)?


Kind regards,

Juan
fmod EXP-SORTS is

  sorts Var Cond Exp .
  subsorts Var < Cond .
  subsorts Cond < Exp .
endfm

view Var from TRIV to EXP-SORTS is
  sort Elt to Var .
endv

view Exp from TRIV to EXP-SORTS is
  sort Elt to Exp .
endv

view Cond from TRIV to EXP-SORTS is
  sort Elt to Cond .
endv

fmod VAR-LIST is
  protecting LIST{Var} * (sort List{Var} to ListVar) .
endfm

fmod EXP-LIST is
  protecting LIST{Exp} * (sort List{Exp} to ListExp) .
endfm

fmod COND-BAG is
  protecting BAG{Cond} * (sort Bag{Cond} to BagCond) .
endfm

fmod EXP is 
  protecting EXP-SORTS .
  protecting VAR-LIST .
  protecting EXP-LIST .
  protecting COND-BAG .

  subsorts ListVar < ListExp . 
endfm 

*** Sets ***

fmod SET {X :: TRIV} is 

  sort Set{X} .
  subsorts X$Elt < Set{X} .
  
  op empty : -> Set{X} .
  op _\u_ : Set{X} Set{X} -> Set{X} [assoc comm idem id: empty prec 8] .

endfm

*** LISTS ***

fmod LIST {X :: TRIV} is

  protecting SET{X} .
  protecting NAT .

  sort List{X} .
  subsort X$Elt < List{X} .

  op nil : -> List{X} [ctor] .
  op _,_ : List{X} List{X} -> List{X} [ctor assoc id: nil prec 9] .
  op len_ : List{X} -> Nat .
  op disj_ : List{X} -> Bool [memo] .
  op notoccur : X$Elt List{X} -> Bool [memo] .
  op _++_ : List{X} List{X} -> List{X} [assoc prec 10] .
  op _-_ : List{X} List{X} -> List{X} [memo prec 10] .
  op remove : List{X} List{X} List{X} -> List{X} [memo] .
  op elts : List{X} -> Set{X} .

  vars X Y : X$Elt . 
  vars L L1 L2 : List{X} .

  eq len nil = 0 .
  eq len(X,L) = 1 + len L .
  eq notoccur(X,nil) = true .
  eq notoccur(X,(Y,L)) = (X =/= Y) and notoccur(X,L) .
  eq disj nil = true .
  eq disj (X,L) = notoccur(X,L) and (disj L) .

  eq L ++ nil = L .
  eq L1 ++ (X,L2) = if notoccur(X,L1) then (L1,X) ++ L2 
                   else (L1 ++ L2) fi .

  eq nil - L = nil .
  eq (X,L1) - L2 = if notoccur(X,L2) then (X,(L1 - L2))
                   else (L1 - L2) fi .

  eq remove(nil,nil,L) = nil . 
  eq remove((X,L),(Y,L1),L2) = 
     if notoccur(Y,L2) then (X,remove(L,L1,L2))
     else remove(L,L1,L2) fi .

  eq elts(nil) = empty .
   eq elts(X,L) =  X  \u elts(L) .

endfm

*** BAGS ***

fmod BAG {X :: TRIV} is 

  sort Bag{X} .
  subsort X$Elt < Bag{X} .
  
  op emptybag : -> Bag{X} .
  op _,_ : Bag{X} Bag{X} -> Bag{X} [ctor assoc comm id: emptybag prec 9] .
  op _-_  : Bag{X} X$Elt -> Bag{X} [memo prec 10] .   *** Remove one 
occurrence of Elt
  op _ subbag _ : Bag{X} Bag{X} -> Bool . 
  op _ psubbag _ : Bag{X} Bag{X} -> Bool . *** Proper subbag

  var a b : X$Elt .
  var A B : Bag{X} .

  eq emptybag - b = emptybag .
  eq (a,A) - b = if (a == b) then A else (a,(A - b)) fi .

  eq emptybag subbag A = true .
  eq (a,A) subbag B = if (B - a) == B then false
                       else  A subbag (B - a) fi .

  eq A psubbag B = (A subbag B) and (A =/= B) .
 
endfm