[Maude-users] Is EquationSet < Set{Equation} ?

[Steven Eker]

Hi Santiago,

The support for using parameterized module instantiations for NatList,
QidList and QidSet was done because it was fairly easy (but not
entirely straightforward - look at the intricate sort declarations
needed for _;_ on TypeSets, __ on TypeLists and _;_ on TypeListSet -
these operators come from QidList and QidSet). In fact one of your examples, 
SortSet, is actually a subsort of QidSet and so you could use the set 
operators on it.

There are 3 other kinds of list:

TermList
ImportList
HookList

and 8 other kinds of set:

SubsortDeclSet
AttrSet
RenamingSet
OpDeclSet
MembAxSet
EquationSet
RuleSet
PrintOptionSet

Also Conditions and Traces look like lists and Substitutions look like
sets so you might want to treat them this way. For each of these 14
data types we would need a view from TRIV to some module which would
mean dividing up the 3 modules that currently make up the metalevel
into smaller pieces. With all the extra operations the metalevel would
be much bulkier. Getting sort declarations to be preregular and ctor
consistant for TermLists declared in this way might be tricky because
they are already rather intricate.

Currently it is fairly easy to change EquationSet to be a list, for
example, because there are no other operators, in fact  you could just
remove the comm attribute in a pinch; if it were a renamed
instantiation of SET this would not be so easy.

This is not to say it cannot or should not be done. It's just that it
can't be done lightly or without significant effort and thus was not
done for 2.2.

Steven


On Friday 27 January 2006 13:29, Santiago Escobar wrote:
> Hi,
>
> I have a question about Maude version 2.2.
>
> Old sorts like NatList, QidList, and QidSet are indeed renamings for the
> new List{Nat}, List{Qid} and Set{Qid}.
> However, the sorts in the meta-level modules have not been renamed to
> new sorts and I wonder why.
> That is, sorts  EquationSet, SortSet, or TypeList in META-TERM are not
> renamings of Set{Equation}, Set{Sort} and List{Term}.
>
> Is there any reason for this?
> Because now operators such as "_in_" or "_occurs_" cannot be reused for
> EquationSet or TypeList and have to be typed again.
>
> This seems very strange, since Full Maude version 2.1.1 already included
> sorts Set<Equation>, Set<Sort> and List<Type>.
> Well, their extended versions Set<EEquation>, Set<ESort> and List<EType>.
>
> Many thanks,
> Santiago