The following module provides some operations that involve both lists and sets; since these data types are not affected by the new operations, both of them are imported in protecting mode.
fmod LIST-AND-SET{X :: TRIV} is
protecting LIST{X} .
protecting SET{X} .
var E : X$Elt .
vars A L : List{X} .
var S : Set{X} .
The operation makeSet transforms a list into a set, that is,
it forgets the order between the elements and its repetitions; operationally,
it simply transforms the constructors nil and __ for lists
into the constructors empty and _,_ for sets, but this is
done in an efficient way by using an auxiliary operator $makeSet
with an accumulator argument that allows a tail-recursive definition
by structural induction on the list given as first argument.
Notice that both operators are overloaded to take into account in their
declarations whether their arguments are empty or not.
op makeSet : List{X} -> Set{X} .
op makeSet : NeList{X} -> NeSet{X} .
eq makeSet(L) = $makeSet(L, empty) .
op $makeSet : List{X} Set{X} -> Set{X} .
op $makeSet : NeList{X} Set{X} -> NeSet{X} .
op $makeSet : List{X} NeSet{X} -> NeSet{X} .
eq $makeSet(nil, S) = S .
eq $makeSet(E L, S) = $makeSet(L, (E, S)) .
An inverse operation makeList that transforms a set into a list will be seen in Section 7.12.7, because it only makes sense when we have additional information to put the elements of the set in a sequence in a univocally defined way.
The operations filter and filterOut take a list and a set as arguments, and return the list formed by those elements of the given list that belong and that do not belong, respectively, to the given set, in their original order. Again, both are defined by means of auxiliary operations with accumulator arguments allowing efficient tail-recursive definitions.
op filter : List{X} Set{X} -> List{X} .
eq filter(L, S) = $filter(L, S, nil) .
op $filter : List{X} Set{X} List{X} -> List{X} .
eq $filter(nil, S, A) = A .
eq $filter(E L, S, A)
= $filter(L, S, if E in S then A E else A fi) .
op filterOut : List{X} Set{X} -> List{X} .
eq filterOut(L, S) = $filterOut(L, S, nil) .
op $filterOut : List{X} Set{X} List{X} -> List{X} .
eq $filterOut(nil, S, A) = A .
eq $filterOut(E L, S, A)
= $filterOut(L, S, if E in S then A else A E fi) .
endfm
For illustration, we consider the following instantiation and some reductions.
fmod INT-LIST-AND-SET is
pr LIST-AND-SET{Int} .
endfm
Maude> red in INT-LIST-AND-SET : filter((1 -1 1 -2 1), (1, 2)) .
result NeList{Int}: 1 1 1
Maude> red filterOut((1 -1 1 -2 1), (1, 2)) .
result NeList{Int}: -1 -2
Maude> red makeSet(1 -1 1 -2 1) .
result NeSet{Int}: 1, -1, -2