on master help sign in
Re-added the changes, one hour of trying to rebase should be enough :P
5b70287Synthetica9
libs/contrib/Data/SortedMap.idr+51−1
@@ -1,6 +1,6 @@
1module Data.SortedMap
1module Data.SortedMap
2
2
3−-- TODO: write merge and split
3+-- TODO: write split
4
4
5private
5private
6data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
6data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
@@ -214,6 +214,9 @@ insert k v (M _ t) =
214 Left t' => (M _ t')
214 Left t' => (M _ t')
215 Right t' => (M _ t')
215 Right t' => (M _ t')
216
216
217+insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
218+insertFrom = flip $ foldl $ flip $ uncurry insert
219+
217export
220export
218delete : k -> SortedMap k v -> SortedMap k v
221delete : k -> SortedMap k v -> SortedMap k v
219delete _ Empty = Empty
222delete _ Empty = Empty
@@ -235,6 +238,16 @@ toList : SortedMap k v -> List (k, v)
235toList Empty = []
238toList Empty = []
236toList (M _ t) = treeToList t
239toList (M _ t) = treeToList t
237
240
241+||| Gets the keys of the map.
242+export
243+keys : SortedMap k v -> List k
244+keys = map fst . toList
245+
246+||| Gets the values of the map. Could contain duplicates.
247+export
248+values : SortedMap k v -> List v
249+values = map snd . toList
250+
238treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
251treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
239treeMap f (Leaf k v) = Leaf k (f v)
252treeMap f (Leaf k v) = Leaf k (f v)
240treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
253treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
@@ -245,3 +258,40 @@ export
245implementation Functor (SortedMap k) where
258implementation Functor (SortedMap k) where
246 map _ Empty = Empty
259 map _ Empty = Empty
247 map f (M n t) = M _ (treeMap f t)
260 map f (M n t) = M _ (treeMap f t)
261+
262+||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
263+||| Uses the ordering of the first map given.
264+export
265+mergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k v
266+mergeWith f x y = insertFrom inserted x where
267+ inserted : List (k, v)
268+ inserted = do
269+ (k, v) <- toList y
270+ let v' = (maybe id f $ lookup k x) v
271+ pure (k, v')
272+
273+||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
274+||| Uses mergeWith internally, so the ordering of the left map is kept.
275+export
276+merge : Semigroup v => SortedMap k v -> SortedMap k v -> SortedMap k v
277+merge = mergeWith (<+>)
278+
279+||| Left-biased merge, also keeps the ordering specified by the left map.
280+export
281+mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v
282+mergeLeft = mergeWith const
283+
284+-- TODO: is this the right variant of merge to use for this? I think it is, but
285+-- I could also see the advantages of using `mergeLeft`. The current approach is
286+-- strictly more powerful I believe, because `mergeLeft` can be emulated with
287+-- the `First` monoid. However, this does require more code to do the same
288+-- thing.
289+export
290+Semigroup v => Semigroup (SortedMap k v) where
291+ (<+>) = merge
292+
293+||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
294+||| However, semantically, it should be equal.
295+export
296+(Ord k, Semigroup v) => Monoid (SortedMap k v) where
297+ neutral = empty
libs/contrib/Data/SortedSet.idr+3−1
@@ -29,7 +29,6 @@ export
29toList : SortedSet k -> List k
29toList : SortedSet k -> List k
30toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
30toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
31
31
32−export
33Foldable SortedSet where
32Foldable SortedSet where
34 foldr f e xs = foldr f e (Data.SortedSet.toList xs)
33 foldr f e xs = foldr f e (Data.SortedSet.toList xs)
35
34
@@ -60,3 +59,6 @@ Ord k => Semigroup (SortedSet k) where
60export
59export
61Ord k => Monoid (SortedSet k) where
60Ord k => Monoid (SortedSet k) where
62 neutral = empty
61 neutral = empty
62+
63+keySet : SortedMap k v -> SortedSet k
64+keySet = SetWrapper . map (const ())