0 | module Data.List.Set
 1 |
 2 | import Data.List
 3 | import Data.SortedSet
 4 |
 5 | public export
 6 | record ListSet v where
 7 |   constructor MkListSet
 8 |   {auto eq : Eq v}
 9 |   rawValues : List v
10 |
11 | export
12 | empty : Eq v => ListSet v
13 | empty = MkListSet empty
14 |
15 | export
16 | insert : v -> ListSet v -> ListSet v
17 | insert v (MkListSet vs) = MkListSet $ v :: vs
18 |
19 | public export %inline
20 | insert' : ListSet v -> v -> ListSet v
21 | insert' = flip insert
22 |
23 | export
24 | contains : v -> ListSet v -> Bool
25 | contains v (MkListSet vs) = elem v vs
26 |
27 | public export %inline
28 | contains' : ListSet v -> v -> Bool
29 | contains' = flip contains
30 |
31 | export
32 | singleton : Eq v => v -> ListSet v
33 | singleton = MkListSet . singleton
34 |
35 | export
36 | fromList : Eq v => List v -> ListSet v
37 | fromList = MkListSet
38 |
39 | export
40 | normalise : ListSet v -> ListSet v
41 | normalise (MkListSet vs) = MkListSet $ nub vs
42 |
43 | export  %inline
44 | (.asList) : ListSet v -> List v
45 | (.asList) = rawValues . normalise
46 |
47 | ||| Set union. Keeps the equality specified by the left set.
48 | export
49 | union : (x, y : ListSet v) -> ListSet v
50 | union (MkListSet @{eq} xs) (MkListSet ys) = MkListSet @{eq} $ xs ++ ys
51 |
52 | ||| Set difference. Delete all elements in y from x.
53 | ||| Keeps the equality specified by the left set.
54 | export
55 | difference : (x, y : ListSet v) -> ListSet v
56 | difference (MkListSet @{eq} xs) (MkListSet ys) = MkListSet @{eq} $ (xs \\ ys) @{eq}
57 |
58 | ||| Set symmetric difference. Uses the union of the differences.
59 | export
60 | symDifference : (x, y : ListSet v) -> ListSet v
61 | symDifference x y = union (difference x y) (difference y x)
62 |
63 | ||| Set intersection. Implemented as the difference of the union and the symetric difference.
64 | export
65 | intersection : (x, y : ListSet v) -> ListSet v
66 | intersection x y = difference x (difference x y)
67 |
68 | public export %inline
69 | toSortedSet : Ord v => ListSet v -> SortedSet v
70 | toSortedSet = fromList . rawValues
71 |
72 | export
73 | Ord k => Semigroup (ListSet k) where
74 |   (<+>) = union
75 |
76 | export
77 | Ord k => Monoid (ListSet k) where
78 |   neutral = empty
79 |
80 | export
81 | Show k => Show (ListSet k) where
82 |    show m = "fromList " ++ show (rawValues m)
83 |
84 | export
85 | Foldable ListSet where
86 |   foldr f init = foldr f init . (.asList)
87 |   foldl f init = foldl f init . (.asList)
88 |   null $ MkListSet vs = null vs
89 |   foldlM f init = foldlM f init . (.asList)
90 |   toList = (.asList)
91 |