Maude-help mailing list

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

Hi,

Both of your problems arise from the source - Maude considers two operators 
to 
be subsort polymorphically overloaded (i.e. essentially the same operator) if 
they have the same name and their corresponding sorts lie in the same kind.
It has to be this way for sort computations to work.

Now for example, Var < Exp, Var < List{Var} and Exp < List{Exp} so List{Var} 
and List{Exp} are in the same kind (in fact I see you have actually added an 
extra subsort declaration). Thus all of your operators on lists end up 
subsort polymorphically overloaded which is what I'm guessing you wanted. The 
advisories are because you are essentially bashing together operators from 
List{Var} and List{Exp} that were originally unrelated. It's not an error as 
such - it is considered a slightly dubious thing to do, but now that we have 
parameterized modules it's not that unreasonable.

Bashing together the operations from Bag{Cond} and List{Var} is not such a 
good idea - in fact when they have different attributes it is not allowed 
since an operators attributes usually cannot depend on the sorts of the 
arguments (ctor is a special case that has very special handling).

I would suggest you make the operator names for the various containers 
distinct.

Steven

On Monday 08 December 2008 05:46, Juan Ignacio Perna wrote:
> 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