on 7afa310 help sign in
Idris-dev/libs/base/Data/SortedSet.idr
28 lines 866 B history raw
1module Data.SortedSet
3import Data.SortedMap
5-- TODO: add intersection, union, difference
7data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
9empty : SortedSet k
10empty = SetWrapper Data.SortedMap.empty
12insert : Ord k => k -> SortedSet k -> SortedSet k
13insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
15delete : Ord k => k -> SortedSet k -> SortedSet k
16delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
18contains : Ord k => k -> SortedSet k -> Bool
19contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
21fromList : Ord k => List k -> SortedSet k
22fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
24toList : SortedSet k -> List k
25toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
27instance Foldable SortedSet where
28 foldr f e xs = foldr f e (Data.SortedSet.toList xs)