on fbb201c help sign in
Idris-dev/libs/contrib/Data/SortedSet.idr
35 lines 899 B history raw
1module Data.SortedSet
3import Data.SortedMap
5-- TODO: add intersection, union, difference
7abstract
8data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
10public
11empty : Ord k => SortedSet k
12empty = SetWrapper Data.SortedMap.empty
14public
15insert : k -> SortedSet k -> SortedSet k
16insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
18public
19delete : k -> SortedSet k -> SortedSet k
20delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
22public
23contains : k -> SortedSet k -> Bool
24contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
26public
27fromList : Ord k => List k -> SortedSet k
28fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
30public
31toList : SortedSet k -> List k
32toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
34instance Foldable SortedSet where
35 foldr f e xs = foldr f e (Data.SortedSet.toList xs)