%% $Id: SetOps.oz,v 1.3 2009/01/10 19:26:15 leavens Exp $ %% Sets %% AUTHOR: Gary T. Leavens %% Representation: %% ::= empty | set( T) declare fun {FoldSet S F V} %% ENSURES: Result is the fold of F on S with V as base value case S of set(Es E) then {F E {FoldSet Es F V}} else V end end fun {EmptySet} %% ENSURES: Result is the empty set empty end fun {AsSet L} %% ENSURES: Result is a set containing exactly the distinct elements of L {FoldR L fun {$ X R} {Add R X} end empty} end fun {AsList S} %% ENSURES: Result is a list containing exactly the elements of S {FoldSet S fun {$ X R} X|R end nil} end fun {IsEmpty S} %% ENSURES: Result is true if S is empty case S of empty then true else false end end fun {Size S} %% ENSURES: Result is the number of distinct elements in S {FoldSet S fun {$ _ N} 1+N end 0} end fun {Choose set(_ E)} %% ENSURES: Result is an element of the argument E end fun {IsMember S X} %% ENSURES: Result is true if X a member of S {FoldSet S fun {$ E R} R orelse X == E end false} end fun {IsSubset S1 S2} %% ENSURES: Result is true if S1 is a (not necessarily proper) subset of S2 {FoldSet S1 fun {$ X R} R andthen {IsMember S2 X} end true} end fun {Equal S1 S2} %% ENSURES: Result is true if S1 and S2 are equal {Size S1} == {Size S2} andthen {IsSubset S1 S2} end fun {Add S X} %% ENSURES: Result is a set containing and all the elements of S and also X if {IsMember S X} then S else set(S X) end end fun {Remove S X} %% ENSRUES: Result contains all the elements of S except X {FoldSet S fun {$ E R} if X==E then R else set(R E) end end empty} end fun {Union S1 S2} %% ENSURES: Result contains just the elements of S1 and S2 {FoldSet S1 fun {$ E R} {Add R E} end S2} end fun {Minus S1 S2} %% ENSURES: Result contains just the elements of S1 that are not in S2 {FoldSet S1 fun {$ E R} if {IsMember S2 E} then R else {Add R E} end end empty} end fun {Intersect S1 S2} %% ENSURES: Result contains just the elements of S1 that are also in S2 {FoldSet S1 fun {$ E R} if {IsMember S2 E} then {Add R E} else R end end empty} end fun {UnionList Sets} %% ENSURES: Result contains just the elements of all the sets in Sets {FoldR Sets Union empty} end