0 | module Data.SortedSet
3 | import Data.SortedMap
4 | import Data.SortedMap.Dependent
7 | data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
10 | empty : Ord k => SortedSet k
11 | empty = SetWrapper Data.SortedMap.empty
14 | insert : k -> SortedSet k -> SortedSet k
15 | insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
17 | public export %inline
18 | insert' : SortedSet k -> k -> SortedSet k
19 | insert' = flip insert
22 | delete : k -> SortedSet k -> SortedSet k
23 | delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
25 | public export %inline
26 | delete' : SortedSet k -> k -> SortedSet k
27 | delete' = flip delete
30 | contains : k -> SortedSet k -> Bool
31 | contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
33 | public export %inline
34 | contains' : SortedSet k -> k -> Bool
35 | contains' = flip contains
38 | fromList : Ord k => List k -> SortedSet k
39 | fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
42 | Foldable SortedSet where
43 | foldr f z = foldr f z . toList
44 | foldl f z = foldl f z . toList
46 | null (SetWrapper m) = null m
48 | foldMap f = foldMap f . toList
50 | toList (SetWrapper m) = keys m
55 | public export %inline
56 | toList : SortedSet k -> List k
57 | toList = Prelude.toList
61 | union : (x, y : SortedSet k) -> SortedSet k
62 | union x y = foldr insert x y
66 | difference : (x, y : SortedSet k) -> SortedSet k
67 | difference x y = foldr delete x y
71 | symDifference : (x, y : SortedSet k) -> SortedSet k
72 | symDifference x y = union (difference x y) (difference y x)
76 | intersection : (x, y : SortedSet k) -> SortedSet k
77 | intersection x y = difference x (difference x y)
81 | leftMost : SortedSet k -> Maybe k
82 | leftMost (SetWrapper m) = fst <$> leftMost m
86 | rightMost : SortedSet k -> Maybe k
87 | rightMost (SetWrapper m) = fst <$> rightMost m
90 | Ord k => Semigroup (SortedSet k) where
94 | Ord k => Monoid (SortedSet k) where
98 | Eq k => Eq (SortedSet k) where
99 | SetWrapper x == SetWrapper y = x == y
102 | Show k => Show (SortedSet k) where
103 | show m = "fromList " ++ show (Prelude.toList m)
106 | keySet : SortedMap k v -> SortedSet k
107 | keySet = SetWrapper . map (const ())
109 | namespace Dependent
112 | keySet : SortedDMap k v -> SortedSet k
113 | keySet = SetWrapper . cast . map (const ())
117 | differenceMap : SortedMap k v -> SortedSet k -> SortedMap k v
118 | differenceMap x y = foldr delete x y
122 | intersectionMap : SortedMap k v -> SortedSet k -> SortedMap k v
123 | intersectionMap x y = differenceMap x (keySet $
differenceMap x y)
126 | singleton : Ord k => k -> SortedSet k
127 | singleton = insert' empty
130 | toSortedMap : SortedSet k -> SortedMap k ()
131 | toSortedMap (SetWrapper m) = m
134 | fromSortedMap : SortedMap k () -> SortedSet k
135 | fromSortedMap = SetWrapper
139 | pop : SortedSet k -> Maybe (k, SortedSet k)
140 | pop (SetWrapper m) = bimap fst fromSortedMap <$> pop m