[ base ] Add unambiguous kvList function for sorted maps (idris-lan…

…g#3392)

Co-authored-by: Mathew Polzin <[email protected]>

CHANGELOG_NEXT.md

@@ -262,6 +262,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Several functions like `pop`, `differenceMap` and `toSortedMap` were added to `Data.Sorted{Map|Set}`
 
+* Added `kvList` function to `Data.SortedMap` and `Data.SortedMap.Dependent` to have an unambiguous
+  `toList` variant.
+
 * Refactored `Uninhabited` implementation for `Data.List.Elem`, `Data.List1.Elem`, `Data.SnocList.Elem` and `Data.Vect.Elem`
   so it can be used for homogeneous (===) and heterogeneous (~=~) equality.
 

libs/base/Data/SortedMap.idr

@@ -3,8 +3,6 @@ module Data.SortedMap
 import Data.SortedMap.Dependent
 import Data.Zippable
 
-%hide Prelude.toList
-
 export
 record SortedMap k v where
   constructor M
@@ -111,17 +109,22 @@ fromListWith f = flip (insertFromWith f) empty
 
 export
 toList : SortedMap k v -> List (k, v)
-toList = map unDPair . toList . unM
+toList = map unDPair . kvList . unM
+
+||| Returns a list of key-value pairs stored in this map
+public export %inline
+kvList : SortedMap k v -> List (k, v)
+kvList = toList
 
 ||| Gets the keys of the map.
 export
 keys : SortedMap k v -> List k
-keys = map fst . toList
+keys = map fst . kvList
 
 ||| Gets the values of the map. Could contain duplicates.
 export
 values : SortedMap k v -> List v
-values = map snd . toList
+values = map snd . kvList
 
 export
 implementation Functor (SortedMap k) where
@@ -142,8 +145,8 @@ implementation Traversable (SortedMap k) where
 
 export
 implementation Ord k => Zippable (SortedMap k) where
-  zipWith f mx my = fromList $ mapMaybe (\(k, x) => (k,) . f x <$> lookup k my) $ toList mx
-  zipWith3 f mx my mz = fromList $ mapMaybe (\(k, x) => (k,) .: f x <$> lookup k my <*> lookup k mz) $ toList mx
+  zipWith f mx my = fromList $ mapMaybe (\(k, x) => (k,) . f x <$> lookup k my) $ kvList mx
+  zipWith3 f mx my mz = fromList $ mapMaybe (\(k, x) => (k,) .: f x <$> lookup k my <*> lookup k mz) $ kvList mx
   unzipWith f m = let m' = map f m in (map fst m', map snd m')
   unzipWith3 f m = let m' = map f m in (map fst m', map (fst . snd) m', map (snd . snd) m')
 
@@ -154,7 +157,7 @@ mergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k v
 mergeWith f x y = insertFrom inserted x where
   inserted : List (k, v)
   inserted = do
-    (k, v) <- toList y
+    (k, v) <- kvList y
     let v' = (maybe id f $ lookup k x) v
     pure (k, v')
 
@@ -196,11 +199,11 @@ pop = map (bimap unDPair M) . pop . unM
 
 export
 (Show k, Show v) => Show (SortedMap k v) where
-   show m = "fromList " ++ (show $ toList m)
+   show m = "fromList " ++ show (kvList m)
 
 export
 (Eq k, Eq v) => Eq (SortedMap k v) where
-  (==) = (==) `on` toList
+  (==) = (==) `on` kvList
 
 -- TODO: is this the right variant of merge to use for this? I think it is, but
 -- I could also see the advantages of using `mergeLeft`. The current approach is

libs/base/Data/SortedMap/Dependent.idr

@@ -313,14 +313,19 @@ toList : SortedDMap k v -> List (x : k ** v x)
 toList Empty = []
 toList (M _ t) = treeToList t
 
+||| Returns a list of key-value pairs stored in this map
+public export %inline
+kvList : SortedDMap k v -> List (x : k ** v x)
+kvList = toList
+
 ||| Gets the keys of the map.
 export
 keys : SortedDMap k v -> List k
-keys = map fst . toList
+keys = map fst . kvList
 
 export
 values : SortedDMap k v -> List (x : k ** v x)
-values = toList
+values = kvList
 
 treeMap : ({x : k} -> a x -> b x) -> Tree n k a o -> Tree n k b o
 treeMap f (Leaf k v) = Leaf k (f v)
@@ -385,7 +390,7 @@ mergeWith : DecEq k => ({x : k} -> v x -> v x -> v x) -> SortedDMap k v -> Sorte
 mergeWith f x y = insertFrom inserted x where
   inserted : List (x : k ** v x)
   inserted = do
-    (k ** v) <- toList y
+    (k ** v) <- kvList y
     let v' = (maybe id f $ lookupPrecise k x) v
     pure (k ** v')
 
@@ -460,15 +465,15 @@ pop m = do
 
 export
 (Show k, {x : k} -> Show (v x)) => Show (SortedDMap k v) where
-   show m = "fromList " ++ (show $ toList m)
+   show m = "fromList " ++ (show $ kvList m)
 
 export
 (DecEq k, {x : k} -> Eq (v x)) => Eq (SortedDMap k v) where
-  (==) = (==) `on` toList
+  (==) = (==) `on` kvList
 
 export
 strictSubmap : DecEq k => ({x : k} -> Eq (v x)) => (sub : SortedDMap k v) -> (sup : SortedDMap k v) -> Bool
-strictSubmap sub sup = all (\(k ** v) => Just v == lookupPrecise k sup) $ toList sub
+strictSubmap sub sup = all (\(k ** v) => Just v == lookupPrecise k sup) $ kvList sub
 
 -- TODO: is this the right variant of merge to use for this? I think it is, but
 -- I could also see the advantages of using `mergeLeft`. The current approach is