[ base ] Harmonise Sorted* in base and compiler's lib

This is done to be able to replace the second one with the first one
after the next compiler's release

CHANGELOG_NEXT.md

@@ -95,6 +95,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Typst files can be compiled as Literate Idris
 
+* `min` was renamed to `leftMost` in `Libraries.Data.Sorted{Map|Set}` in order
+  to be defined as in `base`.
+
 ### Backend changes
 
 #### RefC Backend
@@ -246,6 +249,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Deprecated `toList` function in favor of `Prelude.toList` in `Data.SortedSet`.
 
+* Several functions like `pop`, `differenceMap` and `toSortedMap` were added to `Data.Sorted{Map|Set}`
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.

libs/base/Data/SortedMap.idr

@@ -189,6 +189,11 @@ rightMost : SortedMap key val -> Maybe (key,val)
 rightMost = map unDPair . rightMost . unM
 
 
+||| Pops the leftmost key and corresponding value from the map
+export
+pop : SortedMap k v -> Maybe ((k, v), SortedMap k v)
+pop = map (bimap unDPair M) . pop . unM
+
 export
 (Show k, Show v) => Show (SortedMap k v) where
    show m = "fromList " ++ (show $ toList m)

libs/base/Data/SortedMap/Dependent.idr

@@ -451,6 +451,13 @@ rightMost : SortedDMap k v -> Maybe (x : k ** v x)
 rightMost Empty = Nothing
 rightMost (M _ t) = Just $ treeRightMost t
 
+||| Pops the leftmost key and corresponding value from the map
+export
+pop : SortedDMap k v -> Maybe ((x : k ** v x), SortedDMap k v)
+pop m = do
+  kv@(k ** _) <- leftMost m
+  pure (kv, delete k m)
+
 export
 (Show k, {x : k} -> Show (v x)) => Show (SortedDMap k v) where
    show m = "fromList " ++ (show $ toList m)

libs/base/Data/SortedSet.idr

@@ -113,6 +113,29 @@ namespace Dependent
   keySet : SortedDMap k v -> SortedSet k
   keySet = SetWrapper . cast . map (const ())
 
+||| Removes all given keys from the given map
+export
+differenceMap : SortedMap k v -> SortedSet k -> SortedMap k v
+differenceMap x y = foldr delete x y
+
+||| Leaves only given keys in the given map
+export
+intersectionMap : SortedMap k v -> SortedSet k -> SortedMap k v
+intersectionMap x y = differenceMap x (keySet $ differenceMap x y)
+
 export
 singleton : Ord k => k -> SortedSet k
 singleton = insert' empty
+
+export %inline
+toSortedMap : SortedSet k -> SortedMap k ()
+toSortedMap (SetWrapper m) = m
+
+export %inline
+fromSortedMap : SortedMap k () -> SortedSet k
+fromSortedMap = SetWrapper
+
+||| Pops the leftmost element from the set
+export
+pop : SortedSet k -> Maybe (k, SortedSet k)
+pop (SetWrapper m) = bimap fst fromSortedMap <$> pop m

src/Libraries/Data/SortedMap.idr

@@ -1,3 +1,4 @@
+-- Remove as soon as 0.8.0 (or greater) is released
 module Libraries.Data.SortedMap
 
 %default total
@@ -324,20 +325,20 @@ adjust k f m =
     Nothing => m
     Just v => insert k (f v) m
 
-treeMin : Tree n k v o -> (k, v)
-treeMin (Leaf k v) = (k, v)
-treeMin (Branch2 t _ _) = treeMin t
-treeMin (Branch3 t _ _ _ _) = treeMin t
+treeLeftMost : Tree n k v o -> (k, v)
+treeLeftMost (Leaf k v) = (k, v)
+treeLeftMost (Branch2 t _ _) = treeLeftMost t
+treeLeftMost (Branch3 t _ _ _ _) = treeLeftMost t
 
 export
-min : SortedMap k v -> Maybe (k, v)
-min Empty = Nothing
-min (M _ t) = Just (treeMin t)
+leftMost : SortedMap k v -> Maybe (k, v)
+leftMost Empty = Nothing
+leftMost (M _ t) = Just $ treeLeftMost t
 
 export
 pop : SortedMap k v -> Maybe ((k, v), SortedMap k v)
 pop m = do
-  (k, v) <- min m
+  (k, v) <- leftMost m
   pure ((k, v), delete k m)
 
 export

src/Libraries/Data/SortedSet.idr

@@ -1,3 +1,4 @@
+-- Remove as soon as 0.8.0 (or greater) is released
 module Libraries.Data.SortedSet
 
 import Data.Maybe
@@ -97,9 +98,10 @@ export
 toSortedMap : SortedSet k -> SortedMap k ()
 toSortedMap (SetWrapper m) = m
 
+||| Returns the leftmost (least) value
 export
-min : SortedSet k -> Maybe k
-min (SetWrapper m) = fst <$> min m
+leftMost : SortedSet k -> Maybe k
+leftMost (SetWrapper m) = fst <$> leftMost m
 
 export
 pop : SortedSet k -> Maybe (k, SortedSet k)