0 | module Data.SortedMap.Extra
 1 |
 2 | import Data.List
 3 | import Data.SortedMap
 4 |
 5 | import public Syntax.IHateParens
 6 |
 7 | %default total
 8 |
 9 | export
10 | mapMaybe : Ord k => (a -> Maybe b) -> SortedMap k a -> SortedMap k b
11 | mapMaybe f = SortedMap.fromList . mapMaybe (\(k, a) => (k,) <$> f a) . SortedMap.toList
12 |
13 | export
14 | mapWithKey : Ord k => (k -> a -> b) -> SortedMap k a -> SortedMap k b
15 | mapWithKey f = fromList . map (\(k, x) => (k, f k x)) . SortedMap.toList
16 |
17 | public export %inline
18 | mapWithKey' : Ord k => SortedMap k a -> (k -> a -> b) -> SortedMap k b
19 | mapWithKey' = flip mapWithKey
20 |
21 | ----------------------------------------------------------
22 | --- Properties of collections (most actually unproved) ---
23 | ----------------------------------------------------------
24 |
25 | export
26 | mapAsList : (f : v -> w) -> (m : SortedMap k v) -> (map f m).asList === map (mapSnd f) m.asList
27 | mapAsList f m = believe_me $ Refl {x=Z}
28 |
29 | export
30 | mapSize : (f : v -> w) -> (m : SortedMap k v) -> (map f m).size = m.size
31 | mapSize f m = rewrite mapAsList f m in lengthMap _
32 |
33 | export
34 | keySetSize : (m : SortedMap k v) -> (keySet m).size = m.size
35 | keySetSize m = believe_me $ Refl {x=Z}
36 |
37 | export
38 | keysThruAsList : (m : SortedMap k v) -> keys m === (Builtin.fst <$> m.asList)
39 | keysThruAsList m = believe_me $ Refl {x=Z}
40 |