diff --git a/README.md b/README.md index c0596a7..018c411 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,2 @@ # idris2-containers -Basic Tree and Queue data types +Assorted concrete container types diff --git a/containers.ipkg b/containers.ipkg index 0d62ce8..037c0ec 100644 --- a/containers.ipkg +++ b/containers.ipkg @@ -1,11 +1,15 @@ package containers -authors = "stefan-hoeck" +authors = "stefan-hoeck and matthew-mosior" brief = "Basic Tree and Queue data structures" version = 0.6.0 sourcedir = "src" depends = base >= 0.6.0 , elab-util -modules = Data.Queue +modules = Data.Map + , Data.Map.Internal + , Data.Set + , Data.Set.Internal + , Data.Queue , Data.Tree diff --git a/profile/profile.ipkg b/profile/profile.ipkg new file mode 100644 index 0000000..ad2f28f --- /dev/null +++ b/profile/profile.ipkg @@ -0,0 +1,11 @@ +package containers-profile + +authors = "stefan-hoeck and matthew-mosior" +version = 0.7.0 +sourcedir = "src" +depends = containers + , elab-util + , profiler + +executable = "profile-containers" +main = Main diff --git a/profile/src/Main.idr b/profile/src/Main.idr new file mode 100644 index 0000000..36c8005 --- /dev/null +++ b/profile/src/Main.idr @@ -0,0 +1,403 @@ +module Main + +import Data.List +import Data.Map as M +import Data.SortedMap as SM +import Data.Set as S +import Data.SortedSet as SS +import Profile + +%default total + +createList : Nat -> List (Nat,Nat) +createList n = map (\x => (x,plus x 1)) [0..n] + +createMap : Nat -> Map Nat Nat +createMap n = M.fromList $ map (\x => (x,plus x 1)) [0..n] + +createSortedMap : Nat -> SortedMap Nat Nat +createSortedMap n = SM.fromList $ map (\x => (x,plus x 1)) [0..n] + +createSet : Nat -> Set Nat +createSet n = S.fromList [0..n] + +createSortedSet : Nat -> SortedSet Nat +createSortedSet n = SS.fromList [0..n] + +insertMap : Nat -> Map Nat Nat +insertMap n = do + let m = M.fromList $ map (\x => (x,plus x 1)) [0..n] + let m = M.insert 0 2 m + let m = M.insert 1 3 m + let m = M.insert 2 4 m + let m = M.insert 3 5 m + let m = M.insert 4 6 m + let m = M.insert 5 7 m + let m = M.insert 6 8 m + let m = M.insert 7 9 m + let m = M.insert 8 10 m + M.insert 9 11 m + +insertSortedMap : Nat -> SortedMap Nat Nat +insertSortedMap n = do + let m = SM.fromList $ map (\x => (x,plus x 1)) [0..n] + let m = SM.insert 0 2 m + let m = SM.insert 1 3 m + let m = SM.insert 2 4 m + let m = SM.insert 3 5 m + let m = SM.insert 4 6 m + let m = SM.insert 5 7 m + let m = SM.insert 6 8 m + let m = SM.insert 7 9 m + let m = SM.insert 8 10 m + SM.insert 9 11 m + +insertSet : Nat -> Set Nat +insertSet n = do + let s = S.fromList [0..n] + let s = S.insert 10 s + let s = S.insert 11 s + let s = S.insert 12 s + let s = S.insert 13 s + let s = S.insert 14 s + let s = S.insert 15 s + let s = S.insert 16 s + let s = S.insert 17 s + let s = S.insert 18 s + S.insert 19 s + +insertSortedSet : Nat -> SortedSet Nat +insertSortedSet n = do + let s = SS.fromList [0..n] + let s = SS.insert 10 s + let s = SS.insert 11 s + let s = SS.insert 12 s + let s = SS.insert 13 s + let s = SS.insert 14 s + let s = SS.insert 15 s + let s = SS.insert 16 s + let s = SS.insert 17 s + let s = SS.insert 18 s + SS.insert 19 s + +deleteMap : Nat -> Map Nat Nat +deleteMap n = do + let m = M.fromList $ map (\x => (x,plus x 1)) [0..n] + let m = M.delete 9 m + let m = M.delete 8 m + let m = M.delete 7 m + let m = M.delete 6 m + let m = M.delete 5 m + let m = M.delete 4 m + let m = M.delete 3 m + let m = M.delete 2 m + let m = M.delete 1 m + M.delete 0 m + +deleteSortedMap : Nat -> SortedMap Nat Nat +deleteSortedMap n = do + let m = SM.fromList $ map (\x => (x,plus x 1)) [0..n] + let m = SM.delete 9 m + let m = SM.delete 8 m + let m = SM.delete 7 m + let m = SM.delete 6 m + let m = SM.delete 5 m + let m = SM.delete 4 m + let m = SM.delete 3 m + let m = SM.delete 2 m + let m = SM.delete 1 m + SM.delete 0 m + + +deleteSet : Nat -> Set Nat +deleteSet n = do + let m = S.fromList [0..n] + let m = S.delete 9 m + let m = S.delete 8 m + let m = S.delete 7 m + let m = S.delete 6 m + let m = S.delete 5 m + let m = S.delete 4 m + let m = S.delete 3 m + let m = S.delete 2 m + let m = S.delete 1 m + S.delete 0 m + +deleteSortedSet : Nat -> SortedSet Nat +deleteSortedSet n = do + let m = SS.fromList [0..n] + let m = SS.delete 9 m + let m = SS.delete 8 m + let m = SS.delete 7 m + let m = SS.delete 6 m + let m = SS.delete 5 m + let m = SS.delete 4 m + let m = SS.delete 3 m + let m = SS.delete 2 m + let m = SS.delete 1 m + SS.delete 0 m + +updateMap : Nat -> Map Nat Nat +updateMap n = do + let m = M.fromList $ map (\x => (x,plus x 1)) [0..n] + let m = M.update f 0 m + let m = M.update f 1 m + let m = M.update f 2 m + let m = M.update f 3 m + let m = M.update f 4 m + let m = M.update f 5 m + let m = M.update f 6 m + let m = M.update f 7 m + let m = M.update f 8 m + M.update f 9 m + where + f : (Nat -> Maybe Nat) + f x = case x `mod` 2 == 0 of + True => + Nothing + False => + Just $ x * x + +updateSortedMap : Nat -> SortedMap Nat Nat +updateSortedMap n = do + let m = SM.fromList $ map (\x => (x,plus x 1)) [0..n] + let m = SM.update f 0 m + let m = SM.update f 1 m + let m = SM.update f 2 m + let m = SM.update f 3 m + let m = SM.update f 4 m + let m = SM.update f 5 m + let m = SM.update f 6 m + let m = SM.update f 7 m + let m = SM.update f 8 m + SM.update f 9 m + where + f : (Maybe Nat -> Maybe Nat) + f Nothing = Nothing + f (Just x) = + case x `mod` 2 == 0 of + True => + Nothing + False => + Just $ x * x + +lookupMap : Nat -> Map Nat Nat +lookupMap n = do + let m = M.fromList $ map (\x => (x,plus x 1)) [0..n] + let v = M.lookup 0 m + let v = M.lookup 1 m + let v = M.lookup 2 m + let v = M.lookup 3 m + let v = M.lookup 4 m + let v = M.lookup 5 m + let v = M.lookup 6 m + let v = M.lookup 0 m + let v = M.lookup 8 m + let v = M.lookup 9 m + m + +lookupSortedMap : Nat -> SortedMap Nat Nat +lookupSortedMap n = do + let m = SM.fromList $ map (\x => (x,plus x 1)) [0..n] + let v = SM.lookup 0 m + let v = SM.lookup 1 m + let v = SM.lookup 2 m + let v = SM.lookup 3 m + let v = SM.lookup 4 m + let v = SM.lookup 5 m + let v = SM.lookup 6 m + let v = SM.lookup 0 m + let v = SM.lookup 8 m + let v = SM.lookup 9 m + m + +memberSet : Nat -> Set Nat +memberSet n = do + let s = S.fromList [0..n] + let v = S.member 0 s + let v = S.member 1 s + let v = S.member 2 s + let v = S.member 3 s + let v = S.member 4 s + let v = S.member 5 s + let v = S.member 6 s + let v = S.member 0 s + let v = S.member 8 s + let v = S.member 9 s + s + +containsSortedSet : Nat -> SortedSet Nat +containsSortedSet n = do + let s = SS.fromList [0..n] + let v = SS.contains 0 s + let v = SS.contains 1 s + let v = SS.contains 2 s + let v = SS.contains 3 s + let v = SS.contains 4 s + let v = SS.contains 5 s + let v = SS.contains 6 s + let v = SS.contains 0 s + let v = SS.contains 8 s + let v = SS.contains 9 s + s + +keysMap : Nat -> List Nat +keysMap n = do + let m = M.fromList $ map (\x => (x,plus x 1)) [0..n] + M.keys m + +keysSortedMap : Nat -> List Nat +keysSortedMap n = do + let m = SM.fromList $ map (\x => (x,plus x 1)) [0..n] + SM.keys m + +valuesMap : Nat -> List Nat +valuesMap n = do + let m = M.fromList $ map (\x => (x,plus x 1)) [0..n] + M.values m + +valuesSortedMap : Nat -> List Nat +valuesSortedMap n = do + let m = SM.fromList $ map (\x => (x,plus x 1)) [0..n] + SM.values m + +unionSet : Nat -> Set Nat +unionSet n = do + let s = S.fromList [0..n] + let s' = S.fromList [(n `div` 2)..n] + union s s' + +unionSortedSet : Nat -> SortedSet Nat +unionSortedSet n = do + let s = SS.fromList [0..n] + let s' = SS.fromList [(n `div` 2)..n] + union s s' + +differenceSet : Nat -> Set Nat +differenceSet n = do + let s = S.fromList [0..n] + let s' = S.fromList [(n `div` 2)..n] + difference s s' + +differenceSortedSet : Nat -> SortedSet Nat +differenceSortedSet n = do + let s = SS.fromList [0..n] + let s' = SS.fromList [(n `div` 2)..n] + difference s s' + +intersectionSet : Nat -> Set Nat +intersectionSet n = do + let s = S.fromList [0..n] + let s' = S.fromList [(n `div` 2)..n] + intersection s s' + +intersectionSortedSet : Nat -> SortedSet Nat +intersectionSortedSet n = do + let s = SS.fromList [0..n] + let s' = SS.fromList [(n `div` 2)..n] + intersection s s' + +bench : Benchmark Void +bench = Group "containers" + [ Group "List" + [ Single "1" (basic createList 0) + , Single "100" (basic createList 99) + , Single "1000" (basic createList 999) + ] + , Group "fromListMap" + [ Single "1" (basic createMap 0) + , Single "100" (basic createMap 99) + , Single "1000" (basic createMap 999) + ] + , Group "fromListSortedMap" + [ Single "1" (basic createSortedMap 0) + , Single "100" (basic createSortedMap 99) + , Single "1000" (basic createSortedMap 999) + ] + , Group "fromListSet" + [ Single "1" (basic createSet 0) + , Single "100" (basic createSet 99) + , Single "1000" (basic createSet 999) + ] + , Group "fromListSortedSet" + [ Single "1" (basic createSortedSet 0) + , Single "100" (basic createSortedSet 99) + , Single "1000" (basic createSortedSet 999) + ] + , Group "insertMap" + [ Single "10" (basic insertMap 0) + ] + , Group "insertSortedMap" + [ Single "10" (basic insertSortedMap 0) + ] + , Group "insertSet" + [ Single "10" (basic insertSet 0) + ] + , Group "insertSortedSet" + [ Single "10" (basic insertSortedSet 0) + ] + , Group "deleteMap" + [ Single "10" (basic deleteMap 9) + ] + , Group "deleteSortedMap" + [ Single "10" (basic deleteSortedMap 9) + ] + , Group "deleteSet" + [ Single "10" (basic deleteSet 9) + ] + , Group "deleteSortedSet" + [ Single "10" (basic deleteSortedSet 9) + ] + , Group "updateMap" + [ Single "10" (basic updateMap 9) + ] + , Group "updateSortedMap" + [ Single "10" (basic updateSortedMap 9) + ] + , Group "lookupMap" + [ Single "10" (basic lookupMap 9) + ] + , Group "lookupSortedMap" + [ Single "10" (basic lookupSortedMap 9) + ] + , Group "memberSet" + [ Single "10" (basic memberSet 9) + ] + , Group "containsSortedSet" + [ Single "10" (basic containsSortedSet 9) + ] + , Group "keysMap" + [ Single "1000000" (basic keysMap 999999) + ] + , Group "keysSortedMap" + [ Single "1000000" (basic keysSortedMap 999999) + ] + , Group "valuesMap" + [ Single "1000000" (basic valuesMap 999999) + ] + , Group "valuesSortedMap" + [ Single "1000000" (basic valuesSortedMap 999999) + ] + , Group "unionSet" + [ Single "1000000" (basic unionSet 999999) + ] + , Group "unionSortedSet" + [ Single "1000000" (basic unionSortedSet 999999) + ] + , Group "differenceSet" + [ Single "1000" (basic differenceSet 999) + ] + , Group "differenceSortedSet" + [ Single "1000" (basic differenceSortedSet 999) + ] + , Group "intersectionSet" + [ Single "1000" (basic intersectionSet 999) + ] + , Group "intersectionSortedSet" + [ Single "1000" (basic intersectionSortedSet 999) + ] + ] + +main : IO () +main = do + runDefault (const True) Details show bench diff --git a/src/Data/Map.idr b/src/Data/Map.idr new file mode 100644 index 0000000..8c12221 --- /dev/null +++ b/src/Data/Map.idr @@ -0,0 +1,1397 @@ +||| Finite Maps +module Data.Map + +import public Data.Map.Internal + +import Data.Bits +import Data.List +import Data.List1 + +%hide Prelude.null +%hide Prelude.toList + +%default total + +-------------------------------------------------------------------------------- +-- Creating Maps +-------------------------------------------------------------------------------- + +||| The empty map. (O)1 +export +empty : Map k v +empty = Tip + +-------------------------------------------------------------------------------- +-- Folds +-------------------------------------------------------------------------------- + +||| Fold the values in the map using the given left-associative binary operator. O(n) +export +foldl : (v -> w -> v) -> v -> Map k w -> v +foldl f z Tip = z +foldl f z (Bin _ _ x l r) = foldl f (f (foldl f z l) x) r + +||| Fold the values in the map using the given right-associative binary operator. O(n) +export +foldr : (v -> w -> w) -> w -> Map k v -> w +foldr f z Tip = z +foldr f z (Bin _ _ x l r) = foldr f (f x (foldr f z r)) l + +||| Fold the keys and values in the map using the given left-associative binary operator. O(n) +export +foldlWithKey : (v -> k -> w -> v) -> v -> Map k w -> v +foldlWithKey f z Tip = z +foldlWithKey f z (Bin _ kx x l r) = foldlWithKey f (f (foldlWithKey f z l) kx x) r + +||| Fold the keys and values in the map using the given right-associative binary operator. O(n) +export +foldrWithKey : (k -> v -> w -> w) -> w -> Map k v -> w +foldrWithKey f z Tip = z +foldrWithKey f z (Bin _ kx x l r) = foldrWithKey f (f kx x (foldrWithKey f z r)) l + +-------------------------------------------------------------------------------- +-- Insertion +-------------------------------------------------------------------------------- + +||| Insert a new key and value in the map. +||| If the key is already present in the map, the associated value is +||| replaced with the supplied value. O(log n) +export +insert : Eq (Map k v) => Eq v => Ord k => k -> v -> Map k v -> Map k v +insert kx0 vx0 m = go kx0 kx0 vx0 m + where + go : k -> k -> v -> Map k v -> Map k v + go orig _ x Tip = singleton orig x + go orig kx x t@(Bin sz ky y l r) = + case compare kx ky of + LT => + let l' = go orig kx x l + in case l' == l of + True => + t + False => + balanceL ky y l' r + GT => + let r' = go orig kx x r + in case r' == r of + True => + t + False => + balanceR ky y l r' + EQ => + case (x == y && orig == ky) of + True => + t + False => + Bin sz orig x l r + +private +insertR : Eq (Map k v) => Eq v => Ord k => k -> v -> Map k v -> Map k v +insertR kx0 = go kx0 kx0 + where + go : k -> k -> v -> Map k v -> Map k v + go orig _ x Tip = singleton orig x + go orig kx x t@(Bin _ ky y l r) = + case compare kx ky of + LT => + let l' = go orig kx x l + in case l' == l of + True => + t + False => + balanceL ky y l' r + GT => + let r' = go orig kx x r + in case r' == r of + True => + t + False => + balanceR ky y l r' + EQ => + t + +||| Insert with a function, combining new value and old value. +||| insertWith f key value mp +||| will insert the pair (key, value) into mp if key does +||| not exist in the map. If the key does exist, the function will +||| insert the pair (key, f new_value old_value). O(log n) +export +insertWith : Ord k => (v -> v -> v) -> k -> v -> Map k v -> Map k v +insertWith = go + where + go : (a -> a -> a) -> k -> a -> Map k a -> Map k a + go _ kx x Tip = singleton kx x + go f kx x (Bin sy ky y l r) = + case compare kx ky of + LT => + balanceL ky y (go f kx x l) r + GT => + balanceR ky y l (go f kx x r) + EQ => + Bin sy kx (f x y) l r + +private +insertWithR : Ord k => (v -> v -> v) -> k -> v -> Map k v -> Map k v +insertWithR = go + where + go : (v -> v -> v) -> k -> v -> Map k v -> Map k v + go _ kx x Tip = singleton kx x + go f kx x (Bin sy ky y l r) = + case compare kx ky of + LT => + balanceL ky y (go f kx x l) r + GT => + balanceR ky y l (go f kx x r) + EQ => + Bin sy ky (f y x) l r + +private +insertWithKeyR : Ord k => (k -> v -> v -> v) -> k -> v -> Map k v -> Map k v +insertWithKeyR = go + where + go : (k -> v -> v -> v) -> k -> v -> Map k v -> Map k v + go _ kx x Tip = singleton kx x + go f kx x (Bin sy ky y l r) = + case compare kx ky of + LT => balanceL ky y (go f kx x l) r + GT => balanceR ky y l (go f kx x r) + EQ => Bin sy ky (f ky y x) l r + +||| Insert with a function, combining key, new value and old value. +||| insertWithKey f key value mp +||| will insert the pair (key, value) into mp if key does +||| not exist in the map. If the key does exist, the function will +||| insert the pair (key,f key new_value old_value). O(log n) +export +insertWithKey : Ord k => (k -> v -> v -> v) -> k -> v -> Map k v -> Map k v +insertWithKey = go + where + go : (k -> v -> v -> v) -> k -> v -> Map k v -> Map k v + go _ kx x Tip = singleton kx x + go f kx x (Bin sy ky y l r) = + case compare kx ky of + LT => balanceL ky y (go f kx x l) r + GT => balanceR ky y l (go f kx x r) + EQ => Bin sy kx (f kx x y) l r + +||| Combines insert operation with old value retrieval. +||| The expression (insertLookupWithKey f k x map) +||| is a pair where the first element is equal to (lookup k map) +||| and the second element equal to (insertWithKey f k x map). O(log n) +export +insertLookupWithKey : Ord k => (k -> v -> v -> v) -> k -> v -> Map k v -> (Maybe v,Map k v) +insertLookupWithKey f0 k0 x0 = go f0 k0 x0 + where + go : (k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a,Map k a) + go _ kx x Tip = (Nothing,singleton kx x) + go f kx x (Bin sy ky y l r) = + case compare kx ky of + LT => let (found,l') = go f kx x l + t' = balanceL ky y l' r + in (found,t') + GT => let (found,r') = go f kx x r + t' = balanceR ky y l r' + in (found,t') + EQ => (Just y,Bin sy kx (f kx x y) l r) + +-------------------------------------------------------------------------------- +-- Deletion/Update +-------------------------------------------------------------------------------- + +||| Delete a key and its value from the map. When the key is not +||| a member of the map, the original map is returned. O(log n) +export +delete : Eq (Map k v) => Eq k => Ord k => k -> Map k v -> Map k v +delete = go + where + go : k -> Map k v -> Map k v + go _ Tip = Tip + go k t@(Bin _ kx x l r) = + case compare k kx of + LT => + let l' = go k l + in case l' == l of + True => + t + False => + balanceR kx x l' r + GT => + let r' = go k r + in case r' == r of + True => + t + False => + balanceL kx x l r' + EQ => + glue l r + +||| Adjust a value at a specific key. When the key is not +||| a member of the map, the original map is returned. O(log n) +export +adjustWithKey : Ord k => (k -> v -> v) -> k -> Map k v -> Map k v +adjustWithKey = go + where + go : (k -> v -> v) -> k -> Map k v -> Map k v + go _ _ Tip = Tip + go f k (Bin sx kx x l r) = + case compare k kx of + LT => + Bin sx kx x (go f k l) r + GT => + Bin sx kx x l (go f k r) + EQ => + Bin sx kx (f kx x) l r + +||| Update a value at a specific key with the result of the provided function. +||| When the key is not a member of the map, the original map is returned. O(log n) +export +adjust : Ord k => (v -> v) -> k -> Map k v -> Map k v +adjust f = adjustWithKey (\_, x => f x) + +||| The expression (updateWithKey f k map) updates the +||| value x at k (if it is in the map). If (f k x) is Nothing, +||| the element is deleted. If it is (Just y), the key k is bound +||| to the new value y. O(log n) +export +updateWithKey : Ord k => (k -> v -> Maybe v) -> k -> Map k v -> Map k v +updateWithKey = go + where + go : (k -> v -> Maybe v) -> k -> Map k v -> Map k v + go _ _ Tip = Tip + go f k (Bin sx kx x l r) = + case compare k kx of + LT => + balanceR kx x (go f k l) r + GT => + balanceL kx x l (go f k r) + EQ => + case f kx x of + Just x' => + Bin sx kx x' l r + Nothing => + glue l r + +||| The expression (update f k map) updates the value x +||| at k (if it is in the map). If (f x) is Nothing, the element is +||| deleted. If it is (Just y), the key k is bound to the new value y. O(log n) +export +update : Ord k => (v -> Maybe v) -> k -> Map k v -> Map k v +update f = updateWithKey (\_, x => f x) + +||| Lookup and update. See also updateWithKey. +||| The function returns changed value, if it is updated. +||| Returns the original key value if the map entry is deleted. O(log n) +export +updateLookupWithKey : Ord k => (k -> v -> Maybe v) -> k -> Map k v -> (Maybe v,Map k v) +updateLookupWithKey f0 k0 = go f0 k0 + where + go : (k -> v -> Maybe v) -> k -> Map k v -> (Maybe v,Map k v) + go _ _ Tip = (Nothing,Tip) + go f k (Bin sx kx x l r) = + case compare k kx of + LT => + let (found,l') = go f k l + t' = balanceR kx x l' r + in (found,t') + GT => + let (found,r') = go f k r + t' = balanceL kx x l r' + in (found,t') + EQ => + case f kx x of + Just x' => + (Just x',Bin sx kx x' l r) + Nothing => + let glued = glue l r + in (Just x,glued) + +||| The expression (alter f k map) alters the value x at k, or absence thereof. +||| alter can be used to insert, delete, or update a value in a Map. O(log n) +export +alter : Ord k => (Maybe v -> Maybe v) -> k -> Map k v -> Map k v +alter = go + where + go : (Maybe v -> Maybe v) -> k -> Map k v -> Map k v + go f k Tip = + case f Nothing of + Nothing => Tip + Just x => singleton k x + go f k (Bin sx kx x l r) = + case compare k kx of + LT => + balance kx x (go f k l) r + GT => + balance kx x l (go f k r) + EQ => + case f (Just x) of + Just x' => Bin sx kx x' l r + Nothing => glue l r + +-------------------------------------------------------------------------------- +-- Query +-------------------------------------------------------------------------------- + +||| Lookup the value at a key in the map. +||| The function will return the corresponding value as (Just value), +||| or Nothing if the key isn't in the map. O(log n) +export +lookup : Ord k => k -> Map k v -> Maybe v +lookup = go + where + go : k -> Map k v -> Maybe v + go _ Tip = + Nothing + go k (Bin _ kx x l r) = + case compare k kx of + LT => go k l + GT => go k r + EQ => Just x + +||| Find the value at a key. +||| Returns Nothing when the element can not be found. O(log n) +export +(!?) : Ord k => Map k v -> k -> Maybe v +(!?) m k = lookup k m + +||| Is the key a member of the map? See also notMember. O(log n) +export +member : Ord k => k -> Map k v -> Bool +member _ Tip = False +member k (Bin _ kx _ l r) = + case compare k kx of + LT => member k l + GT => member k r + EQ => True + +||| Is the key not a member of the map? See also member. O(log n) +export +notMember : Ord k => k -> Map k v -> Bool +notMember k m = not $ member k m + +||| Find the value at a key. +||| Calls idris_crash when the element can not be found. O(log n) +export +partial +find : Ord k => k -> Map k v -> v +find _ Tip = assert_total $ idris_crash "Map.!: given key is not an element in the map" +find k (Bin _ kx x l r) = + case compare k kx of + LT => find k l + GT => find k r + EQ => x + +||| Find the value at a key. +||| Calls idris_crash when the element can not be found. O(log n) +export +partial +(!!) : Ord k => Map k v -> k -> v +(!!) m k = find k m + +||| The expression (findWithDefault def k map) returns +||| the value at key k or returns default value def +||| when the key is not in the map. O(log n) +export +findWithDefault : Ord k => v -> k -> Map k v -> v +findWithDefault def _ Tip = def +findWithDefault def k (Bin _ kx x l r) = + case compare k kx of + LT => findWithDefault def k l + GT => findWithDefault def k r + EQ => x + +||| Find largest key smaller than the given one and return the +||| corresponding (key, value) pair. O(log n) +export +lookupLT : Ord k => k -> Map k v -> Maybe (k,v) +lookupLT = goNothing + where + goJust : k -> k -> v -> Map k v -> Maybe (k,v) + goJust _ kx' x' Tip = Just (kx',x') + goJust k kx' x' (Bin _ kx x l r) = + case k <= kx of + True => goJust k kx' x' l + False => goJust k kx x r + goNothing : k -> Map k v -> Maybe (k,v) + goNothing _ Tip = Nothing + goNothing k (Bin _ kx x l r) = + case k <= kx of + True => goNothing k l + False => goJust k kx x r + +||| Find smallest key greater than the given one and return the +||| corresponding (key, value) pair. O(log n) +export +lookupGT : Ord k => k -> Map k v -> Maybe (k,v) +lookupGT = goNothing + where + goJust : k -> k -> v -> Map k v -> Maybe (k,v) + goJust _ kx' x' Tip = Just (kx',x') + goJust k kx' x' (Bin _ kx x l r) = + case k < kx of + True => goJust k kx x l + False => goJust k kx' x' r + goNothing : k -> Map k v -> Maybe (k,v) + goNothing _ Tip = Nothing + goNothing k (Bin _ kx x l r) = + case k < kx of + True => goJust k kx x l + False => goNothing k r + +||| Find largest key smaller or equal to the given one and return +||| the corresponding (key, value) pair. O(log n) +export +lookupLE : Ord k => k -> Map k v -> Maybe (k,v) +lookupLE = goNothing + where + goJust : k -> k -> v -> Map k v -> Maybe (k,v) + goJust _ kx' x' Tip = Just (kx',x') + goJust k kx' x' (Bin _ kx x l r) = + case compare k kx of + LT => goJust k kx' x' l + EQ => Just (kx,x) + GT => goJust k kx x r + goNothing : k -> Map k v -> Maybe (k,v) + goNothing _ Tip = Nothing + goNothing k (Bin _ kx x l r) = + case compare k kx of + LT => goNothing k l + EQ => Just (kx,x) + GT => goJust k kx x r + +||| Find smallest key greater or equal to the given one and return +||| the corresponding (key, value) pair. O(log n) +export +lookupGE : Ord k => k -> Map k v -> Maybe (k,v) +lookupGE = goNothing + where + goJust : k -> k -> v -> Map k v -> Maybe (k,v) + goJust _ kx' x' Tip = Just (kx',x') + goJust k kx' x' (Bin _ kx x l r) = + case compare k kx of + LT => goJust k kx x l + EQ => Just (kx,x) + GT => goJust k kx' x' r + goNothing : k -> Map k v -> Maybe (k,v) + goNothing _ Tip = Nothing + goNothing k (Bin _ kx x l r) = + case compare k kx of + LT => goJust k kx x l + EQ => Just (kx,x) + GT => goNothing k r + +-------------------------------------------------------------------------------- +-- Size +-------------------------------------------------------------------------------- + +||| Is the map empty? O(1) +export +null : Map k v -> Bool +null Tip = True +null _ = False + +-------------------------------------------------------------------------------- +-- Filter +-------------------------------------------------------------------------------- + +private +splitMember : Ord k => k -> Map k v -> (Map k v,Bool,Map k v) +splitMember k0 m = go k0 m + where + go : k -> Map k v -> (Map k v,Bool,Map k v) + go k t = + case t of + Tip => + (Tip,False,Tip) + Bin _ kx x l r => + case compare k kx of + LT => let (lt,z,gt) = go k l + in (lt,z,link kx x gt r) + GT => let (lt,z,gt) = go k r + in (link kx x l lt,z,gt) + EQ => (l,True,r) + +||| Decompose a map into pieces based on the structure of the underlying tree. +||| This function is useful for consuming a map in parallel. O(1) +export +splitRoot : Map k v -> List (Map k v) +splitRoot orig = + case orig of + Tip => + [] + Bin _ k v l r => + [l,singleton k v,r] + +||| The expression (splitLookup k map) splits a map just +||| like split but also returns lookup k map. O(log n) +export +splitLookup : Ord k => k -> Map k v -> (Map k v,Maybe v,Map k v) +splitLookup k0 m = go k0 m + where + go : k -> Map k v -> (Map k v,Maybe v,Map k v) + go k t = + case t of + Tip => + (Tip,Nothing,Tip) + Bin _ kx x l r => + case compare k kx of + LT => let (lt,z,gt) = go k l + in (lt,z,link kx x gt r) + GT => let (lt,z,gt) = go k r + in (link kx x l lt,z,gt) + EQ => (l,Just x,r) + +||| The expression (split k map) is a pair (map1,map2) where +||| the keys in map1 are smaller than k and the keys in map2 larger than k. +||| Any key equal to k is found in neither map1 nor map2. O(log n) +export +split : Ord k => k -> Map k v -> (Map k v,Map k v) +split k0 t0 = go k0 t0 + where + go : k -> Map k v -> (Map k v,Map k v) + go k t = + case t of + Tip => + (Tip,Tip) + Bin _ kx x l r => + case compare k kx of + LT => let (lt,gt) = go k l + in (lt,link kx x gt r) + GT => let (lt,gt) = go k r + in (link kx x l lt,gt) + EQ => (l,r) + +||| Filter all keys/values that satisfy the predicate. O(n) +export +filterWithKey : Eq (Map k v) => (k -> v -> Bool) -> Map k v -> Map k v +filterWithKey _ Tip = Tip +filterWithKey p t@(Bin _ kx x l r) = + case p kx x of + True => + case (filterWithKey p l) == l && (filterWithKey p r) == r of + True => + t + False => + link kx x (filterWithKey p l) (filterWithKey p r) + False => + link2 (filterWithKey p l) (filterWithKey p r) + +||| Filter all values that satisfy the predicate. O(n) +export +filter : Eq (Map k v) => (v -> Bool) -> Map k v -> Map k v +filter p m = filterWithKey (\_, x => p x) m + +||| Partition the map according to a predicate. The first +||| map contains all elements that satisfy the predicate, the second all +||| elements that fail the predicate. See also split. O(n) +export +partitionWithKey : Eq (Map k v) => (k -> v -> Bool) -> Map k v -> (Map k v,Map k v) +partitionWithKey p0 t0 = go p0 t0 + where + go : (k -> v -> Bool) -> Map k v -> (Map k v,Map k v) + go _ Tip = (Tip,Tip) + go p t@(Bin _ kx x l r) = + case p kx x of + True => + ( case (fst $ go p l) == l && (fst $ go p r) == r of + True => + t + False => + link kx x (fst $ go p l) (fst $ go p r) + , link2 (snd $ go p l) (snd $ go p r) + ) + False => + ( link2 (fst $ go p l) (fst $ go p r) + , case (snd $ go p l) == l && (snd $ go p r) == r of + True => + t + False => + link kx x (snd $ go p l) (snd $ go p r) + ) + +||| Take while a predicate on the keys holds. +||| The user is responsible for ensuring that for all keys j and k in the map, +||| j < k ==> p j >= p k. See note at spanAntitone. O(log n) +export +takeWhileAntitone : (k -> Bool) -> Map k v -> Map k v +takeWhileAntitone _ Tip = Tip +takeWhileAntitone p (Bin _ kx x l r) = + case p kx of + True => + link kx x l (takeWhileAntitone p r) + False => + takeWhileAntitone p l + +||| Drop while a predicate on the keys holds. +||| The user is responsible for ensuring that for all keys j and k in the map, +||| j < k ==> p j >= p k. See note at spanAntitone. O(log n) +export +dropWhileAntitone : (k -> Bool) -> Map k v -> Map k v +dropWhileAntitone _ Tip = Tip +dropWhileAntitone p (Bin _ kx x l r) = + case p kx of + True => + dropWhileAntitone p r + False => + link kx x (dropWhileAntitone p l) r + +||| Divide a map at the point where a predicate on the keys stops holding. +||| The user is responsible for ensuring that for all keys j and k in the map, +||| j < k ==> p j>= p k. O(log n) +export +spanAntitone : (k -> Bool) -> Map k v -> (Map k v, Map k v) +spanAntitone p0 m = go p0 m + where + go : (k -> Bool) -> Map k v -> (Map k v,Map k v) + go _ Tip = (Tip,Tip) + go p (Bin _ kx x l r) = + case p kx of + True => + let (u,v) = go p r + in (link kx x l u,v) + False => + let (u,v) = go p l + in (u,link kx x v r) + +||| Map keys/values and collect the Just results. O(n) +export +mapMaybeWithKey : (k -> a -> Maybe b) -> Map k a -> Map k b +mapMaybeWithKey _ Tip = Tip +mapMaybeWithKey f (Bin _ kx x l r) = + case f kx x of + Just y => + link kx y (mapMaybeWithKey f l) (mapMaybeWithKey f r) + Nothing => + link2 (mapMaybeWithKey f l) (mapMaybeWithKey f r) + +||| Map values and collect the Just results. O(n) +export +mapMaybe : (a -> Maybe b) -> Map k a -> Map k b +mapMaybe f = mapMaybeWithKey (\_, x => f x) + +||| Map keys/values and separate the Left and Right results. O(n) +export +mapEitherWithKey : (k -> a -> Either b c) -> Map k a -> (Map k b, Map k c) +mapEitherWithKey f0 t0 = go f0 t0 + where + go : (k -> a -> Either b c) -> Map k a -> (Map k b,Map k c) + go _ Tip = (Tip,Tip) + go f (Bin _ kx x l r) = + case f kx x of + Left y => (link kx y (fst $ go f l) (fst $ go f r),link2 (snd $ go f l) (snd $ go f r)) + Right z => (link2 (fst $ go f l) (fst $ go f r),link kx z (snd $ go f l) (snd $ go f r)) + +||| Map values and separate the Left and Right results. O(n) +export +mapEither : (a -> Either b c) -> Map k a -> (Map k b, Map k c) +mapEither f m = mapEitherWithKey (\_, x => f x) m + +-------------------------------------------------------------------------------- +-- Submap +-------------------------------------------------------------------------------- + +private +submap' : Ord a => (b -> c -> Bool) -> Map a b -> Map a c -> Bool +submap' _ Tip _ = True +submap' _ _ Tip = False +submap' f (Bin 1 kx x _ _) t = + case lookup kx t of + Just y => + f x y + Nothing => + False +submap' f (Bin _ kx x l r) t = + let (lt,found,gt) = splitLookup kx t + in case found of + Nothing => + False + Just y => + f x y && size l <= size lt + && size r <= size gt + && submap' f l lt + && submap' f r gt + +||| The expression (isSubmapOfBy f t1 t2) returns True if +||| all keys in t1 are in tree t2, and when f returns True when +||| applied to their respective values. +export +isSubmapOfBy : Ord k => (a -> b -> Bool) -> Map k a -> Map k b -> Bool +isSubmapOfBy f t1 t2 = size t1 <= size t2 && submap' f t1 t2 + +||| This function is defined as (isSubmapOf = isSubmapOfBy (==)). +export +isSubmapOf : Eq v => Ord k => Map k v -> Map k v -> Bool +isSubmapOf m1 m2 = isSubmapOfBy (==) m1 m2 + +||| Is this a proper submap? (ie. a submap but not equal). +||| The expression (isProperSubmapOfBy f m1 m2) returns True when +||| keys m1 and keys m2 are not equal, +||| all keys in m1 are in m2, and when f returns True when +||| applied to their respective values. +export +isProperSubmapOfBy : Ord k => (a -> b -> Bool) -> Map k a -> Map k b -> Bool +isProperSubmapOfBy f t1 t2 = size t1 < size t2 && submap' f t1 t2 + +||| Is this a proper submap? (ie. a submap but not equal). +||| Defined as (isProperSubmapOf = isProperSubmapOfBy (==)). +export +isProperSubmapOf : Eq v => Ord k => Map k v -> Map k v -> Bool +isProperSubmapOf m1 m2 = isProperSubmapOfBy (==) m1 m2 + +-------------------------------------------------------------------------------- +-- Indexed +-------------------------------------------------------------------------------- + +||| Lookup the index of a key, which is its zero-based index in +||| the sequence sorted by keys. The index is a number from 0 up to, but not +||| including, the size of the map. O(log n) +export +lookupIndex : Ord k => k -> Map k v -> Maybe Nat +lookupIndex = go 0 + where + go : Nat -> k -> Map k a -> Maybe Nat + go _ _ Tip = Nothing + go idx k (Bin _ kx _ l r) = + case compare k kx of + LT => + go idx k l + GT => + go (idx + size l + 1) k r + EQ => + Just $ idx + size l + +||| Return the index of a key, which is its zero-based index in +||| the sequence sorted by keys. The index is a number from 0 up to, but not +||| including, the size of the map. Calls idris_crash when the key is not +||| a member of the map. O(log n) +export +partial +findIndex : Ord k => k -> Map k v -> Nat +findIndex = go 0 + where + go : Nat -> k -> Map k a -> Nat + go _ _ Tip = assert_total $ idris_crash "Map.findIndex: element is not in the map" + go idx k (Bin _ kx _ l r) = + case compare k kx of + LT => + go idx k l + GT => + go (idx + size l + 1) k r + EQ => + idx + size l + +||| Retrieve an element by its index, i.e. by its zero-based +||| index in the sequence sorted by keys. If the index is out of range (less +||| than zero, greater or equal to size of the map), idris_crash is called. O(log n) +export +partial +elemAt : Nat -> Map k v -> (k,v) +elemAt _ Tip = assert_total $ idris_crash "Map.elemAt: index out of range" +elemAt i (Bin _ kx x l r) = + case compare i (size l) of + LT => + elemAt i l + GT => + elemAt ((i `minus` (size l)) `minus` 1) r + EQ => + (kx,x) + +||| Update the element at index, i.e. by its zero-based index in +||| the sequence sorted by keys. If the index is out of range (less than zero, +||| greater or equal to size of the map), idris_crash is called. O(log n) +export +partial +updateAt : (k -> v -> Maybe v) -> Nat -> Map k v -> Map k v +updateAt f i t = + case t of + Tip => assert_total $ idris_crash "Map.updateAt: index out of range" + Bin sx kx x l r => + case compare i (size l) of + LT => + balanceR kx x (updateAt f i l) r + GT => + balanceL kx x l (updateAt f ((i `minus` (size l)) `minus` 1) r) + EQ => + case f kx x of + Just x' => + Bin sx kx x' l r + Nothing => + glue l r + +||| Delete the element at index, i.e. by its zero-based index in +||| the sequence sorted by keys. If the index is out of range (less than zero, +||| greater or equal to size of the map), idris_crash is called. O(log n) +export +partial +deleteAt : Nat -> Map k v -> Map k v +deleteAt i t = + case t of + Tip => assert_total $ idris_crash "Map.deleteAt: index out of range" + Bin _ kx x l r => + case compare i (size l) of + LT => + balanceR kx x (deleteAt i l) r + GT => + balanceL kx x l (deleteAt ((i `minus` (size l)) `minus` 1) r) + EQ => + glue l r + +||| Take a given number of entries in key order, beginning +||| with the smallest keys. O(log n) +export +take : Nat -> Map k v -> Map k v +take i m = + case i >= size m of + True => + m + False => + go i m + where + go : Nat -> Map k v -> Map k v + go _ Tip = Tip + go i (Bin _ kx x l r) = + case i <= 0 of + True => + Tip + False => + case compare i (size l) of + LT => + go i l + GT => + link kx x l (go ((i `minus` (size l)) `minus` 1) r) + EQ => + l + +||| Drop a given number of entries in key order, beginning +||| with the smallest keys. O(log n) +export +drop : Nat -> Map k v -> Map k v +drop i m = + case i >= size m of + True => + Tip + False => + go i m + where + go : Nat -> Map k v -> Map k v + go _ Tip = Tip + go i (Bin _ kx x l r) = + case i <= 0 of + True => + m + False => + case compare i (size l) of + LT => + link kx x (go i l) r + GT => + go ((i `minus` (size l)) `minus` 1) r + EQ => + insertMin kx x r + +||| Split a map at a particular index. O(log n) +export +splitAt : Nat -> Map k v -> (Map k v, Map k v) +splitAt i m = + case i >= size m of + True => + (m,Tip) + False => + go i m + where + go : Nat -> Map k v -> (Map k v,Map k v) + go _ Tip = (Tip,Tip) + go i (Bin _ kx x l r) = + case i <= 0 of + True => + (Tip,m) + False => + case compare i (size l) of + LT => + case go i l of + (ll,lr) => + (ll,link kx x lr r) + GT => + case go ((i `minus` (size l)) `minus` 1) r of + (rl,rr) => + (link kx x l rl,rr) + EQ => + (l,insertMin kx x r) + +-------------------------------------------------------------------------------- +-- Min/Max +-------------------------------------------------------------------------------- + +private +lookupMinSure : k -> v -> Map k v -> (k,v) +lookupMinSure k v Tip = (k,v) +lookupMinSure _ _ (Bin _ k v l _) = lookupMinSure k v l + +||| The minimal key of the map. Returns Nothing if the map is empty. O(log n) +export +lookupMin : Map k v -> Maybe (k,v) +lookupMin Tip = Nothing +lookupMin (Bin _ k v l _) = Just $ lookupMinSure k v l + +private +lookupMaxSure : k -> v -> Map k v -> (k,v) +lookupMaxSure k v Tip = (k,v) +lookupMaxSure _ _ (Bin _ k v _ r) = lookupMaxSure k v r + +||| The maximal key of the map. Returns Nothing if the map is empty. O(log n) +export +lookupMax : Map k v -> Maybe (k,v) +lookupMax Tip = Nothing +lookupMax (Bin _ k v _ r) = Just $ lookupMaxSure k v r + +||| The minimal key of the map. Calls idris_crash if the map is empty. O(log n) +export +partial +findMin : Map k v -> (k,v) +findMin t = + case lookupMin t of + Just r => r + Nothing => assert_total $ idris_crash "Map.findMin: empty map has no minimal element" + +||| The maximal key of the map. Calls idris_crash if the map is empty. O(log n) +export +partial +findMax : Map k v -> (k,v) +findMax t = + case lookupMax t of + Just r => r + Nothing => assert_total $ idris_crash "Map.findMax: empty map has no maximal element" + +||| Delete the minimal key. Returns an empty map if the map is empty. O(log n) +export +deleteMin : Map k v -> Map k v +deleteMin Tip = Tip +deleteMin (Bin _ _ _ Tip r) = r +deleteMin (Bin _ kx x l r) = balanceR kx x (deleteMin l) r + +||| Delete the maximal key. Returns an empty map if the map is empty. O(log n) +export +deleteMax : Map k v -> Map k v +deleteMax Tip = Tip +deleteMax (Bin _ _ _ l Tip) = l +deleteMax (Bin _ kx x l r) = balanceL kx x l (deleteMax r) + +||| Retrieves the minimal (key,value) pair of the map, and +||| the map stripped of that element, or Nothing if passed an empty map. O(log n) +export +minViewWithKey : Map k v -> Maybe ((k,v),Map k v) +minViewWithKey Tip = Nothing +minViewWithKey (Bin _ k x l r) = + Just $ + case minViewSure k x l r of + MinView' km xm t => + ((km,xm),t) + +||| Delete and find the minimal element. O(log n) +export +partial +deleteFindMin : Map k v -> ((k,v),Map k v) +deleteFindMin t = + case minViewWithKey t of + Just res => res + Nothing => (assert_total $ idris_crash "Map.deleteFindMin: can not return the minimal element of an empty map",Tip) + +||| Retrieves the maximal (key,value) pair of the map, and +||| the map stripped of that element, or Nothing if passed an empty map. O(log n) +export +maxViewWithKey : Map k v -> Maybe ((k,v),Map k v) +maxViewWithKey Tip = Nothing +maxViewWithKey (Bin _ k x l r) = + Just $ + case maxViewSure k x l r of + MaxView' km xm t => + ((km,xm),t) + +||| Delete and find the maximal element. O(log n) +export +partial +deleteFindMax : Map k v -> ((k,v),Map k v) +deleteFindMax t = + case maxViewWithKey t of + Just res => res + Nothing => (assert_total $ idris_crash "Map.deleteFindMax: can not return the maximal element of an empty map",Tip) + +||| Update the value at the minimal key. O(log n) +export +updateMinWithKey : (k -> v -> Maybe v) -> Map k v -> Map k v +updateMinWithKey _ Tip = Tip +updateMinWithKey f (Bin sx kx x Tip r) = + case f kx x of + Nothing => r + Just x' => Bin sx kx x' Tip r +updateMinWithKey f (Bin _ kx x l r) = + balanceR kx x (updateMinWithKey f l) r + +||| Update the value at the minimal key. O(log n) +export +updateMin : (v -> Maybe v) -> Map k v -> Map k v +updateMin f m = updateMinWithKey (\_, x => f x) m + +||| Update the value at the maximal key. O(log n) +export +updateMaxWithKey : (k -> v -> Maybe v) -> Map k v -> Map k v +updateMaxWithKey _ Tip = Tip +updateMaxWithKey f (Bin sx kx x l Tip) = + case f kx x of + Nothing => l + Just x' => Bin sx kx x' l Tip +updateMaxWithKey f (Bin _ kx x l r) = + balanceL kx x l (updateMaxWithKey f r) + +||| Update the value at the maximal key. O(log n) +export +updateMax : (v -> Maybe v) -> Map k v -> Map k v +updateMax f m = updateMaxWithKey (\_, x => f x) m + +||| Retrieves the value associated with minimal key of the +||| map, and the map stripped of that element, or Nothing if passed an empty map. O(log n) +export +minView : Map k v -> Maybe (v,Map k v) +minView t = + case minViewWithKey t of + Nothing => Nothing + Just ((_,x),t') => Just (x,t') + +||| Retrieves the value associated with maximal key of the +||| map, and the map stripped of that element, or Nothing if passed an empty map. O(log n) +export +maxView : Map k v -> Maybe (v,Map k v) +maxView t = + case maxViewWithKey t of + Nothing => Nothing + Just ((_,x),t') => Just (x,t') + +-------------------------------------------------------------------------------- +-- Combine +-------------------------------------------------------------------------------- + +||| The expression (union t1 t2) takes the left-biased union of t1 and t2. +||| It prefers t1 when duplicate keys are encountered. +export +union : Eq (Map k v) => Eq v => Ord k => Map k v -> Map k v -> Map k v +union t1 Tip = t1 +union t1 (Bin _ k x Tip Tip) = insertR k x t1 +union (Bin _ k x Tip Tip) t2 = insert k x t2 +union Tip t2 = t2 +union t1@(Bin _ k1 x1 l1 r1) t2 = + case split k1 t2 of + (l2,r2) => + case (union l1 l2) == l1 && (union r1 r2) == r1 of + True => + t1 + False => + link k1 x1 (union l1 l2) (union r1 r2) + +||| Union with a combining function. +export +unionWith : Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v +unionWith _ t1 Tip = t1 +unionWith f t1 (Bin _ k x Tip Tip) = insertWithR f k x t1 +unionWith f (Bin _ k x Tip Tip) t2 = insertWith f k x t2 +unionWith _ Tip t2 = t2 +unionWith f (Bin _ k1 x1 l1 r1) t2 = + case splitLookup k1 t2 of + (l2,mb,r2) => + case mb of + Nothing => link k1 x1 (unionWith f l1 l2) (unionWith f r1 r2) + Just x2 => link k1 (f x1 x2) (unionWith f l1 l2) (unionWith f r1 r2) + +||| Union with a combining function. +export +unionWithKey : Ord k => (k -> v -> v -> v) -> Map k v -> Map k v -> Map k v +unionWithKey _ t1 Tip = t1 +unionWithKey f t1 (Bin _ k x Tip Tip) = insertWithKeyR f k x t1 +unionWithKey f (Bin _ k x Tip Tip) t2 = insertWithKey f k x t2 +unionWithKey _ Tip t2 = t2 +unionWithKey f (Bin _ k1 x1 l1 r1) t2 = + case splitLookup k1 t2 of + (l2,mb,r2) => + case mb of + Nothing => link k1 x1 (unionWithKey f l1 l2) (unionWithKey f r1 r2) + Just x2 => link k1 (f k1 x1 x2) (unionWithKey f l1 l2) (unionWithKey f r1 r2) + +||| The union of a list of maps. +export +unions : Eq (Map k v) => Eq v => Foldable f => Ord k => f (Map k v) -> Map k v +unions ts = foldl union empty ts + +||| The union of a list of maps, with a combining operation. +export +unionsWith : Foldable f => Ord k => (v -> v -> v) -> f (Map k v) -> Map k v +unionsWith f ts = foldl (unionWith f) empty ts + +-------------------------------------------------------------------------------- +-- Difference +-------------------------------------------------------------------------------- + +||| Difference of two maps. +||| Return elements of the first map not existing in the second map. +export +difference : Ord k => Map k a -> Map k b -> Map k a +difference Tip _ = Tip +difference t1 Tip = t1 +difference t1 (Bin _ k _ l2 r2) = + case split k t1 of + (l1,r1) => + case size (difference l1 l2) + size (difference r1 r2) == size t1 of + True => + t1 + False => + link2 (difference l1 l2) (difference r1 r2) + +||| Same as difference. +export +(\\) : Ord k => Map k a -> Map k b -> Map k a +m1 \\ m2 = difference m1 m2 + +-------------------------------------------------------------------------------- +-- Intersection +-------------------------------------------------------------------------------- + +||| Intersection of two maps. +||| Return data in the first map for the keys existing in both maps. +export +intersection : Eq (Map k a) => Ord k => Map k a -> Map k b -> Map k a +intersection Tip _ = Tip +intersection _ Tip = Tip +intersection t1@(Bin _ k x l1 r1) t2 = + case splitMember k t2 of + (l2,True,r2) => + case (intersection l1 l2) == l1 && (intersection r1 r2) == r1 of + True => + t1 + False => + link k x (intersection l1 l2) (intersection r1 r2) + (l2,False,r2) => + link2 (intersection l1 l2) (intersection r1 r2) + +||| Intersection with a combining function. +export +intersectionWith : Ord k => (a -> b -> c) -> Map k a -> Map k b -> Map k c +intersectionWith f Tip _ = Tip +intersectionWith f _ Tip = Tip +intersectionWith f (Bin _ k x1 l1 r1) t2 = + case splitLookup k t2 of + (l2,Just x2,r2) => + link k (f x1 x2) (intersectionWith f l1 l2) (intersectionWith f r1 r2) + (l2,Nothing,r2) => + link2 (intersectionWith f l1 l2) (intersectionWith f r1 r2) + +||| Intersection with a combining function. +export +intersectionWithKey : Ord k => (k -> a -> b -> c) -> Map k a -> Map k b -> Map k c +intersectionWithKey f Tip _ = Tip +intersectionWithKey f _ Tip = Tip +intersectionWithKey f (Bin _ k x1 l1 r1) t2 = + case splitLookup k t2 of + (l2,Just x2,r2) => + link k (f k x1 x2) (intersectionWithKey f l1 l2) (intersectionWithKey f r1 r2) + (l2,Nothing,r2) => + link2 (intersectionWithKey f l1 l2) (intersectionWithKey f r1 r2) + +-------------------------------------------------------------------------------- +-- Disjoint +-------------------------------------------------------------------------------- + +||| Check whether the key sets of two +||| maps are disjoint (i.e., their intersection is empty). +export +disjoint : Ord k => Map k a -> Map k b -> Bool +disjoint Tip _ = True +disjoint _ Tip = True +disjoint (Bin 1 k _ _ _) t = k `notMember` t +disjoint (Bin _ k _ l r) t = + let (lt,found,gt) = splitMember k t + in not found && disjoint l lt && disjoint r gt + +-------------------------------------------------------------------------------- +-- Compose +-------------------------------------------------------------------------------- + +||| Relate the keys of one map to the values of +||| the other, by using the values of the former as keys for lookups in the latter. +||| O(n * log(m)), where m is the size of the first argument. +export +compose : Ord b => Map b c -> Map a b -> Map a c +compose bc ab = + case null bc of + True => + empty + False => + mapMaybe ((!?) bc) ab + +-------------------------------------------------------------------------------- +-- Traversal +-------------------------------------------------------------------------------- + +||| Map a function over all values in the map. O(n) +export +map : (v -> w) -> Map k v -> Map k w +map _ Tip = Tip +map f (Bin sx kx x l r) = Bin sx kx (f x) (map f l) (map f r) + +||| Map a function over all values in the map. O(n) +export +mapWithKey : (k -> v -> w) -> Map k v -> Map k w +mapWithKey _ Tip = Tip +mapWithKey f (Bin sx kx x l r) = Bin sx kx (f kx x) (mapWithKey f l) (mapWithKey f r) + +||| The function mapAccumL threads an accumulating +||| argument through the map in ascending order of keys. O(n) +export +mapAccumL : (v -> k -> w -> (v,c)) -> v -> Map k w -> (v,Map k c) +mapAccumL _ a Tip = (a,Tip) +mapAccumL f a (Bin sx kx x l r) = + let (a1,l') = mapAccumL f a l + (a2,x') = f a1 kx x + (a3,r') = mapAccumL f a2 r + in (a3,Bin sx kx x' l' r') + +||| The function mapAccumRWithKey threads an accumulating +||| argument through the map in descending order of keys. O(n) +export +mapAccumRWithKey : (v -> k -> w -> (v,c)) -> v -> Map k w -> (v,Map k c) +mapAccumRWithKey _ a Tip = (a,Tip) +mapAccumRWithKey f a (Bin sx kx x l r) = + let (a1,r') = mapAccumRWithKey f a r + (a2,x') = f a1 kx x + (a3,l') = mapAccumRWithKey f a2 l + in (a3,Bin sx kx x' l' r') + +||| The function mapAccumWithKey threads an accumulating +||| argument through the map in ascending order of keys. O(n) +export +mapAccumWithKey : (v -> k -> w -> (v,c)) -> v -> Map k w -> (v,Map k c) +mapAccumWithKey f a t = mapAccumL f a t + +||| The function mapAccum threads an accumulating +||| argument through the map in ascending order of keys. O(n) +export +mapAccum : (v -> w -> (v,c)) -> v -> Map k w -> (v,Map k c) +mapAccum f a m = mapAccumWithKey (\a', _, x' => f a' x') a m + +-------------------------------------------------------------------------------- +-- Lists +-------------------------------------------------------------------------------- + +||| Convert the map to a list of key/value pairs where the keys are in descending order. O(n) +export +toDescList : Map k v -> List (k,v) +toDescList Tip = [] +toDescList t@(Bin _ _ _ _ _) = foldlWithKey (\xs, k, x => (k,x) :: xs) [] t + +||| Convert the map to a list of key/value pairs where the keys are in ascending order. O(n) +export +toAscList : Map k v -> List (k,v) +toAscList Tip = [] +toAscList t@(Bin _ _ _ _ _) = foldrWithKey (\k, x, xs => (k,x) :: xs) [] t + +||| Convert the map to a list of key/value pairs. +export +toList : Map k v -> List (k,v) +toList = toAscList + +||| Build a map from a list of key/value pairs. +||| If the list contains more than one value for the same key, the last value +||| for the key is retained. +||| If the keys of the list are ordered, a linear-time implementation is used. O(n * log(n)) +export +partial +fromList : Ord (k, v) => Ord k => List (k, v) -> Map k v +fromList [] = Tip +fromList xs = + case sorted xs of + True => + buildBalancedTree (convertToList1 xs) (length xs) + False => + buildBalancedTree (convertToList1 (sort xs)) (length xs) + where + -- Calculate the size of a tree + sizeTree : Map k v -> Nat + sizeTree Tip = 0 + sizeTree (Bin sz _ _ _ _) = sz + -- Convert a list to a List1, which requires the list to be non-empty + convertToList1 : List (k, v) -> List1 (k, v) + convertToList1 [] = assert_total $ idris_crash "Unexpected empty list" + convertToList1 (x :: xs) = x ::: xs + -- Link a root node with two subtrees + linkRootWithSubtrees : (k, v) -> Map k v -> Map k v -> Nat -> Map k v + linkRootWithSubtrees (kx, x) left right newSize = + Bin newSize kx x left right + -- Split a non-empty list into left, middle, and right parts + splitList : List1 (k, v) -> Nat -> (List (k, v), (k, v), List (k, v), Nat) + splitList l len = + let half = len `div` 2 + (left, rest) = splitAt half (forget l) + in case rest of + [] => + assert_total $ idris_crash "Unexpected empty list" + (middle :: right) => + (left, middle, right, len) + -- Build a balanced tree from a non-empty list + buildBalancedTree : List1 (k, v) -> Nat -> Map k v + buildBalancedTree ((kx, x) ::: []) _ = Bin 1 kx x Tip Tip + buildBalancedTree xs len = + let (left, root, right, totalSize) = splitList xs len + leftTree = case left of + [] => + Tip + _ => + assert_total $ buildBalancedTree (convertToList1 left) (length left) + rightTree = case right of + [] => + Tip + _ => + assert_total $ buildBalancedTree (convertToList1 right) (length right) + in linkRootWithSubtrees root leftTree rightTree totalSize + +-------------------------------------------------------------------------------- +-- Keys +-------------------------------------------------------------------------------- + +||| Gets the keys of the map. +export +keys : Map k v -> List k +keys = map fst . toList + +-------------------------------------------------------------------------------- +-- Values +-------------------------------------------------------------------------------- + +||| Gets the values of the map. +||| Could contain duplicates. +export +values : Map k v -> List v +values = map snd . toList + +-------------------------------------------------------------------------------- +-- Interfaces +-------------------------------------------------------------------------------- + +export +Functor (Map k) where + map f m = map f m + +export +Foldable (Map k) where + foldl f z = foldl f z . values + foldr f z = foldr f z . values + null = null + +private +Show k => Show v => Show (List (k, v)) where + show xs = "[" ++ show' xs ++ "]" + where + show'' : (k, v) -> String + show'' (k, v) = "(" ++ show k ++ ", " ++ show v ++ ")" + show' : List (k, v) -> String + show' Nil = "" + show' (x :: Nil) = show'' x + show' (x :: xs) = show'' x ++ ", " ++ show' xs + +export +Show (List (k, v)) => Show (Map k v) where + show m = "fromList " ++ (show $ toList m) diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr new file mode 100644 index 0000000..0f80f60 --- /dev/null +++ b/src/Data/Map/Internal.idr @@ -0,0 +1,326 @@ +||| Map Internals +module Data.Map.Internal + +import Data.List +import Data.String +import Derive.Prelude + +%default total +%language ElabReflection + +-------------------------------------------------------------------------------- +-- Maps +-------------------------------------------------------------------------------- + +public export +Size : Type +Size = Nat + +||| A finite map from keys k to values v. +public export +data Map k v = Bin Size k v (Map k v) (Map k v) + | Tip + +%runElab derive "Map" [Eq,Ord,Show] + +public export +data MinView k a = MinView' k a (Map k a) + +%runElab derive "MinView" [Eq,Ord,Show] + +public export +data MaxView k a = MaxView' k a (Map k a) + +%runElab derive "MaxView" [Eq,Ord,Show] + +-------------------------------------------------------------------------------- +-- Creating Maps +-------------------------------------------------------------------------------- + +||| Wrap a single value in a map. +export +singleton : k -> a -> Map k a +singleton k x = Bin 1 k x Tip Tip + +-------------------------------------------------------------------------------- +-- Query +-------------------------------------------------------------------------------- + +||| The number of elements in the map. O(1) +export +size : Map k v -> Nat +size Tip = 0 +size (Bin _ _ _ l r) = 1 + size l + size r + +-------------------------------------------------------------------------------- +-- Map Internals +-------------------------------------------------------------------------------- + +{- + [balance l x r] balances two trees with value x. + The sizes of the trees should balance after decreasing the + size of one of them. (a rotation). + + [delta] is the maximal relative difference between the sizes of + two trees, it corresponds with the [w] in Adams' paper. + [ratio] is the ratio between an outer and inner sibling of the + heavier subtree in an unbalanced setting. It determines + whether a double or single rotation should be performed + to restore balance. It is corresponds with the inverse + of $\alpha$ in Adam's article. + + Note that according to the Adam's paper: + - [delta] should be larger than 4.646 with a [ratio] of 2. + - [delta] should be larger than 3.745 with a [ratio] of 1.534. + + But the Adam's paper is erroneous: + - It can be proved that for delta=2 and delta>=5 there does + not exist any ratio that would work. + - Delta=4.5 and ratio=2 does not work. + + That leaves two reasonable variants, delta=3 and delta=4, + both with ratio=2. + + - A lower [delta] leads to a more 'perfectly' balanced tree. + - A higher [delta] performs less rebalancing. + + In the benchmarks, delta=3 is faster on insert operations, + and delta=4 has slightly better deletes. As the insert speedup + is larger, we currently use delta=3. +-} + +delta : Nat +delta = 3 + +ratio : Nat +ratio = 2 + +||| The bin constructor maintains the size of the tree. +bin : k -> v -> Map k v -> Map k v -> Map k v +bin k x l r = Bin (size l + size r + 1) k x l r + +||| Balances a map after the addition, deletion, or updating of a map via a new key and value. +export +balance : k -> v -> Map k v -> Map k v -> Map k v +balance k x l r = + case l of + Tip => + case r of + Tip => + Bin 1 k x Tip Tip + (Bin _ _ _ Tip Tip) => + Bin 2 k x Tip r + (Bin _ rk rx Tip rr@(Bin _ _ _ _ _)) => + Bin 3 rk rx (Bin 1 k x Tip Tip) rr + (Bin _ rk rx (Bin _ rlk rlx _ _) Tip) => + Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip) + (Bin rs rk rx rl@(Bin rls rlk rlx rll rlr) rr@(Bin rrs _ _ _ _)) => + case rls < ratio * rrs of + True => + Bin (1+rs) rk rx (Bin (1+rls) k x Tip rl) rr + False => + Bin (1+rs) rlk rlx (Bin (1+size rll) k x Tip rll) (Bin (1+rrs+size rlr) rk rx rlr rr) + (Bin ls lk lx ll lr) => + case r of + Tip => + case (ll,lr) of + (Tip, Tip) => + Bin 2 k x l Tip + (Tip, (Bin _ lrk lrx _ _)) => + Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip) + ((Bin _ _ _ _ _), Tip) => + Bin 3 lk lx ll (Bin 1 k x Tip Tip) + ((Bin lls _ _ _ _), (Bin lrs lrk lrx lrl lrr)) => + case lrs < ratio * lls of + True => + Bin (1+ls) lk lx ll (Bin (1+lrs) k x lr Tip) + False => + Bin (1+ls) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+size lrr) k x lrr Tip) + (Bin rs rk rx rl rr) => + case rs > delta * ls of + True => + case (rl,rr) of + (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _) => + case rls < ratio * rrs of + True => + Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x l rl) rr + False => + Bin (1+ls+rs) rlk rlx (Bin (1+ls+size rll) k x l rll) (Bin (1+rrs+size rlr) rk rx rlr rr) + (_,_) => + assert_total $ idris_crash "Failure in Data.Map.Internal.balance" + False => + case ls > delta * rs of + True => + case (ll,lr) of + (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr) => + case lrs < ratio * lls of + True => + Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr r) + False => + Bin (1+ls+rs) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+rs+size lrr) k x lrr r) + (_,_) => + assert_total $ idris_crash "Failure in Data.Map.Internal.balance" + False => + Bin (1+ls+rs) k x l r + +||| A specialized version of balance. +||| balanceL is called when left subtree might have been inserted to or when +||| right subtree might have been deleted from. +export +balanceL : k -> v -> Map k v -> Map k v -> Map k v +balanceL k x l r = + case r of + Tip => + case l of + Tip => + Bin 1 k x Tip Tip + (Bin _ _ _ Tip Tip) => + Bin 2 k x l Tip + (Bin _ lk lx Tip (Bin _ lrk lrx _ _)) => + Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip) + (Bin _ lk lx ll@(Bin _ _ _ _ _) Tip) => + Bin 3 lk lx ll (Bin 1 k x Tip Tip) + (Bin ls lk lx ll@(Bin lls _ _ _ _) lr@(Bin lrs lrk lrx lrl lrr)) => + case lrs < ratio * lls of + True => + Bin (1+ls) lk lx ll (Bin (1+lrs) k x lr Tip) + False => + Bin (1+ls) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+size lrr) k x lrr Tip) + (Bin rs _ _ _ _) => + case l of + Tip => + Bin (1+rs) k x Tip r + (Bin ls lk lx ll lr) => + case ls > delta * rs of + True => + case (ll,lr) of + (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr) => + case lrs < ratio * lls of + True => + Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr r) + False => + Bin (1+ls+rs) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+rs+size lrr) k x lrr r) + (_,_) => + assert_total $ idris_crash "Failure in Data.Map.Internal.balanceL" + False => + Bin (1+ls+rs) k x l r + +||| A specialized version of balance. +||| balanceR is called when right subtree might have been inserted to or when +||| left subtree might have been deleted from. +export +balanceR : k -> v -> Map k v -> Map k v -> Map k v +balanceR k x l r = + case l of + Tip => + case r of + Tip => + Bin 1 k x Tip Tip + (Bin _ _ _ Tip Tip ) => + Bin 2 k x Tip r + (Bin _ rk rx Tip rr@(Bin _ _ _ _ _)) => + Bin 3 rk rx (Bin 1 k x Tip Tip) rr + (Bin _ rk rx (Bin _ rlk rlx _ _) Tip) => + Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip) + (Bin rs rk rx rl@(Bin rls rlk rlx rll rlr) rr@(Bin rrs _ _ _ _)) => + case rls < ratio * rrs of + True => + Bin (1+rs) rk rx (Bin (1+rls) k x Tip rl) rr + False => + Bin (1+rs) rlk rlx (Bin (1+size rll) k x Tip rll) (Bin (1+rrs+size rlr) rk rx rlr rr) + (Bin ls _ _ _ _) => + case r of + Tip => + Bin (1+ls) k x l Tip + (Bin rs rk rx rl rr) => + case rs > delta * ls of + True => + case (rl,rr) of + (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _) => + case rls < ratio * rrs of + True => + Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x l rl) rr + False => + Bin (1+ls+rs) rlk rlx (Bin (1+ls+size rll) k x l rll) (Bin (1+rrs+size rlr) rk rx rlr rr) + (_,_) => + assert_total $ idris_crash "Failure in Data.Map.Internal.balanceR" + False => + Bin (1+ls+rs) k x l r + +export +insertMax : k -> v -> Map k v -> Map k v +insertMax kx x t = + case t of + Tip => + singleton kx x + Bin _ ky y l r => + balanceR ky y l (insertMax kx x r) + +export +insertMin : k -> v -> Map k v -> Map k v +insertMin kx x t = + case t of + Tip => + singleton kx x + Bin _ ky y l r => + balanceL ky y (insertMin kx x l) r + +export +minViewSure : k -> v -> Map k v -> Map k v -> MinView k v +minViewSure k x Tip r = MinView' k x r +minViewSure k x (Bin _ kl xl ll lr) r = + case minViewSure kl xl ll lr of + MinView' km xm l' => MinView' km xm (balanceR k x l' r) + +export +maxViewSure : k -> v -> Map k v -> Map k v -> MaxView k v +maxViewSure k x l Tip = MaxView' k x l +maxViewSure k x l (Bin _ kr xr rl rr) = + case maxViewSure kr xr rl rr of + MaxView' km xm r' => MaxView' km xm (balanceL k x l r') + +||| Glues two maps together (assumes that both maps are already balanced with respect to each other). +export +glue : Map k v -> Map k v -> Map k v +glue Tip r = r +glue l Tip = l +glue l@(Bin sl kl xl ll lr) r@(Bin sr kr xr rl rr) = + case sl > sr of + True => + let (MaxView' km m l') = maxViewSure kl xl ll lr + in balanceR km m l' r + False => + let (MinView' km m r') = minViewSure kr xr rl rr + in balanceL km m l r' + +||| Utility function that maintains the balance properties of the tree. +export +link2 : Map k v -> Map k v -> Map k v +link2 Tip r = r +link2 l Tip = l +link2 l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry) = + case delta * sizeL < sizeR of + True => + balanceL ky y (link2 l ly) ry + False => + case delta * sizeR < sizeL of + True => + balanceR kx x lx (link2 rx r) + False => + glue l r + +||| Utility function that maintains the balance properties of the tree. +export +link : k -> v -> Map k v -> Map k v -> Map k v +link kx x Tip r = insertMin kx x r +link kx x l Tip = insertMax kx x l +link kx x l@(Bin sizeL ky y ly ry) r@(Bin sizeR kz z lz rz) = + case delta * sizeL < sizeR of + True => + balanceL kz z (link kx x l lz) rz + False => + case delta * sizeR < sizeL of + True => + balanceR ky y ly (link kx x ry r) + False => + bin kx x l r diff --git a/src/Data/Set.idr b/src/Data/Set.idr new file mode 100644 index 0000000..05ea9d5 --- /dev/null +++ b/src/Data/Set.idr @@ -0,0 +1,841 @@ +||| Finite Sets +module Data.Set + +import public Data.Set.Internal + +import Data.Bits +import Data.List +import Data.List1 + +%hide Prelude.foldl +%hide Prelude.null +%hide Prelude.toList + +%default total + +-------------------------------------------------------------------------------- +-- Creating Sets +-------------------------------------------------------------------------------- + +||| The empty set. (O)1 +export +empty : Set a +empty = Tip + +-------------------------------------------------------------------------------- +-- Folds +-------------------------------------------------------------------------------- + +||| Fold the values in the set using the given left-associative binary operator. O(n) +export +foldl : (a -> b -> a) -> a -> Set b -> a +foldl f z Tip = z +foldl f z (Bin _ x l r) = foldl f (f (foldl f z l) x) r + +||| Fold the values in the set using the given right-associative binary operator. O(n) +export +foldr : (a -> b -> b) -> b -> Set a -> b +foldr f z Tip = z +foldr f z (Bin _ x l r) = foldr f (f x (foldr f z r)) l + +-------------------------------------------------------------------------------- +-- Insertion +-------------------------------------------------------------------------------- + +||| Insert an element in a set. +||| If the set already contains an element equal to the given value, +||| it is replaced with the new value. O(log n) +export +insert : Eq (Set a) => Eq a => Ord a => a -> Set a -> Set a +insert x0 s = go x0 x0 s + where + go : a -> a -> Set a -> Set a + go orig _ Tip = singleton orig + go orig x t@(Bin sz y l r) = + case compare x y of + LT => + let l' = go orig x l + in case l' == l of + True => + t + False => + balanceL y l' r + GT => + let r' = go orig x r + in case r' == r of + True => + t + False => + balanceR y l r' + EQ => + case orig == y of + True => + t + False => + Bin sz orig l r + +private +insertR : Eq (Set a) => Eq a => Ord a => a -> Set a -> Set a +insertR x0 s = go x0 x0 s + where + go : a -> a -> Set a -> Set a + go orig _ Tip = singleton orig + go orig x t@(Bin _ y l r) = + case compare x y of + LT => + let l' = go orig x l + in case l' == l of + True => + t + False => + balanceL y l' r + GT => + let r' = go orig x r + in case r' == r of + True => + t + False => + balanceR y l r' + EQ => + t + +-------------------------------------------------------------------------------- +-- Deletion +-------------------------------------------------------------------------------- + +||| Delete an element from a set. When the element is not +||| a member of the set, the original set is returned. O(log n) +export +delete : Eq (Set a) => Eq a => Ord a => a -> Set a -> Set a +delete = go + where + go : a -> Set a -> Set a + go _ Tip = Tip + go x t@(Bin _ y l r) = + case compare x y of + LT => + let l' = go x l + in case l' == l of + True => + t + False => + balanceR y l' r + GT => + let r' = go x r + in case r' == r of + True => + t + False => + balanceL y l r' + EQ => + glue l r + +-------------------------------------------------------------------------------- +-- Query +-------------------------------------------------------------------------------- + +||| Is the element in the set? O(log n) +export +member : Ord a => a -> Set a -> Bool +member _ Tip = False +member x (Bin _ y l r) = + case compare x y of + LT => member x l + GT => member x r + EQ => True + +||| Is the element not in the set? O(log n) +export +notMember : Ord a => a -> Set a -> Bool +notMember k m = not $ member k m + +||| Find largest element smaller than the given one. O(log n) +export +lookupLT : Ord a => a -> Set a -> Maybe a +lookupLT = goNothing + where + goJust : a -> a -> Set a -> Maybe a + goJust _ best Tip = Just best + goJust x best (Bin _ y l r) = + case x <= y of + True => goJust x best l + False => goJust x y r + goNothing : a -> Set a -> Maybe a + goNothing _ Tip = Nothing + goNothing x (Bin _ y l r) = + case x <= y of + True => goNothing x l + False => goJust x y r + +||| Find smallest element greater than the given one. O(log n) +export +lookupGT : Ord a => a -> Set a -> Maybe a +lookupGT = goNothing + where + goJust : a -> a -> Set a -> Maybe a + goJust _ best Tip = Just best + goJust x best (Bin _ y l r) = + case x < y of + True => goJust x y l + False => goJust x best r + goNothing : a -> Set a -> Maybe a + goNothing _ Tip = Nothing + goNothing x (Bin _ y l r) = + case x < y of + True => goJust x y l + False => goNothing x r + +||| Find the largest element smaller or equal to the given one. O(log n) +export +lookupLE : Ord a => a -> Set a -> Maybe a +lookupLE = goNothing + where + goJust : a -> a -> Set a -> Maybe a + goJust _ best Tip = Just best + goJust x best (Bin _ y l r) = + case compare x y of + LT => goJust x best l + EQ => Just y + GT => goJust x y r + goNothing : a -> Set a -> Maybe a + goNothing _ Tip = Nothing + goNothing x (Bin _ y l r) = + case compare x y of + LT => goNothing x l + EQ => Just y + GT => goJust x y r + +||| Find the smallest element greater or equal to the given one. O(log n) +export +lookupGE : Ord a => a -> Set a -> Maybe a +lookupGE = goNothing + where + goJust : a -> a -> Set a -> Maybe a + goJust _ best Tip = Just best + goJust x best (Bin _ y l r) = + case compare x y of + LT => goJust x y l + EQ => Just y + GT => goJust x best r + goNothing : a -> Set a -> Maybe a + goNothing _ Tip = Nothing + goNothing x (Bin _ y l r) = + case compare x y of + LT => goJust x y l + EQ => Just y + GT => goNothing x r + +||| Is the set empty? O(1) +export +null : Set a -> Bool +null Tip = True +null _ = False + +||| Performs a split but also returns whether +||| the pivot element was found in the original set. O(log n) +export +splitMember : Ord a => a -> Set a -> (Set a,Bool,Set a) +splitMember _ Tip = (Tip, False, Tip) +splitMember x (Bin _ y l r) = + case compare x y of + LT => let (lt, found, gt) = splitMember x l + gt' = link y gt r + in (lt, found, gt') + GT => let (lt, found, gt) = splitMember x r + lt' = link y l lt + in (lt', found, gt) + EQ => (l, True, r) + +||| Decompose a set into pieces based on the structure of the underlying tree. +||| This function is useful for consuming a set in parallel. O(1) +export +splitRoot : Set a -> List (Set a) +splitRoot orig = + case orig of + Tip => + [] + Bin _ v l r => + [l, singleton v, r] + +||| The expression (split x set) is a pair (set1,set2) where +||| set1 comprises the elements of set less than x and +||| set2 comprises the elements of set greater than x. O(log n) +export +split : Ord a => a -> Set a -> (Set a,Set a) +split _ Tip = (Tip, Tip) +split x (Bin _ y l r) = + case compare x y of + LT => let (lt, gt) = split x l + in (lt, link y gt r) + GT => let (lt, gt) = split x r + in (link y l lt, gt) + EQ => (l, r) + +private +isSubsetOfX : Ord a => Set a -> Set a -> Bool +isSubsetOfX Tip _ = True +isSubsetOfX _ Tip = False +isSubsetOfX (Bin 1 x _ _) t = member x t +isSubsetOfX (Bin _ x l r) t = + let (lt, found, gt) = splitMember x t + in found && + size l <= size lt && + size r <= size gt && + isSubsetOfX l lt && + isSubsetOfX r gt + +||| Indicates whether s1 is a subset of s2. +export +isSubsetOf : Ord a => Set a -> Set a -> Bool +isSubsetOf t1 t2 = + size t1 <= size t2 && isSubsetOfX t1 t2 + +||| Indicates whether s1 is a proper subset of s2. +export +isProperSubsetOf : Ord a => Set a -> Set a -> Bool +isProperSubsetOf s1 s2 = + size s1 <= size s2 && isSubsetOfX s1 s2 + +||| Check whether two sets are disjoint (i.e. their intersection is empty). +export +disjoint : Ord a => Set a -> Set a -> Bool +disjoint Tip _ = True +disjoint _ Tip = True +disjoint (Bin 1 x _ _) t = notMember x t +disjoint (Bin _ x l r) t = + let (lt, found, gt) = splitMember x t + in not found && + disjoint l lt && + disjoint r gt + +-------------------------------------------------------------------------------- +-- Merge +-------------------------------------------------------------------------------- + +||| Merges two trees. +private +merge : Set a -> Set a -> Set a +merge Tip r = r +merge l Tip = l +merge l@(Bin sizeL x lx rx) r@(Bin sizeR y ly ry) = + case delta * sizeL < sizeR of + True => + balanceL y (merge l ly) ry + False => + case delta*sizeR < sizeL of + True => + balanceR x lx (merge rx r) + False => + glue l r + +-------------------------------------------------------------------------------- +-- Filter +-------------------------------------------------------------------------------- + +||| Filter all elements that satisfy the predicate. O(n) +export +filter : Eq (Set a) => (a -> Bool) -> Set a -> Set a +filter _ Tip = Tip +filter p t@(Bin _ x l r) = + case p x of + True => + case l == (filter p l) && r == (filter p r) of + True => + t + False => + link x (filter p l) (filter p r) + False => + merge (filter p l) (filter p r) + +||| Partition the set into two sets, one with all elements +||| that satisfy the predicate and one with all elements +||| that don't satisfy the predicate. +||| See also split. +partition : Eq (Set a) => (a -> Bool) -> Set a -> (Set a,Set a) +partition _ Tip = (Tip, Tip) +partition p t@(Bin _ x l r) = + case (partition p l, partition p r) of + ((l1, l2), (r1, r2)) => + case p x of + True => + case l1 == l && r1 == r of + True => + (t, merge l2 r2) + False => + (link x l1 r1, merge l2 r2) + False => + case l2 == l && r2 == r of + True => + (merge l1 r1, t) + False => + (merge l1 r1, link x l2 r2) + +||| Take while a predicate on the keys holds. +||| The user is responsible for ensuring that for all elements j and k in the set, +||| j < k ==> p j >= p k. See note at spanAntitone. O(log n) +export +takeWhileAntitone : (a -> Bool) -> Set a -> Set a +takeWhileAntitone _ Tip = Tip +takeWhileAntitone p (Bin _ x l r) = + case p x of + True => + link x l (takeWhileAntitone p r) + False => + takeWhileAntitone p l + +||| Drop while a predicate on the keys holds. +||| The user is responsible for ensuring that for all elements j and k in the map, +||| j < k ==> p j >= p k. See note at spanAntitone. O(log n) +export +dropWhileAntitone : (a -> Bool) -> Set a -> Set a +dropWhileAntitone _ Tip = Tip +dropWhileAntitone p (Bin _ x l r) = + case p x of + True => + dropWhileAntitone p r + False => + link x (dropWhileAntitone p l) r + +||| Divide a map at the point where a predicate on the keys stops holding. +||| The user is responsible for ensuring that for all keys j and k in the map, +||| j < k ==> p j>= p k. O(log n) +export +spanAntitone : (a -> Bool) -> Set a -> (Set a,Set a) +spanAntitone p0 s = go p0 s + where + go : (a -> Bool) -> Set a -> (Set a,Set a) + go _ Tip = (Tip,Tip) + go p (Bin _ x l r) = + case p x of + True => + let (u,v) = go p r + in (link x l u,v) + False => + let (u,v) = go p l + in (u,link x v r) + +-------------------------------------------------------------------------------- +-- Indexed +-------------------------------------------------------------------------------- + +||| Lookup the index of a element, which is its zero-based index in +||| the sorted sequence of elements. The index is a number from 0 up to, but not +||| including, the size of the set. O(log n) +export +lookupIndex : Ord a => a -> Set a -> Maybe Nat +lookupIndex = go 0 + where + go : Nat -> a -> Set a -> Maybe Nat + go _ _ Tip = Nothing + go idx x (Bin _ kx l r) = + case compare x kx of + LT => + go idx x l + GT => + go (idx + size l + 1) x r + EQ => + Just $ idx + size l + +||| Return the index of an element, which is its zero-based index in +||| the sorted sequence of elements. The index is a number from 0 up to, but not +||| including, the size of the set. Calls idris_crash when the element is not +||| a member of the set. O(log n) +export +partial +findIndex : Ord a => a -> Set a -> Nat +findIndex = go 0 + where + go : Nat -> a -> Set a -> Nat + go _ _ Tip = assert_total $ idris_crash "Set.findIndex: element is not in the set" + go idx x (Bin _ kx l r) = + case compare x kx of + LT => + go idx x l + GT => + go (idx + size l + 1) x r + EQ => + idx + size l + +||| Retrieve an element by its index, i.e. by its zero-based +||| index in the sorted sequence of elements. If the index is out of range (less +||| than zero, greater or equal to size of the set), idris_crash is called. O(log n) +export +partial +elemAt : Nat -> Set a -> a +elemAt _ Tip = assert_total $ idris_crash "Set.elemAt: index out of range" +elemAt i (Bin _ x l r) = + case compare i (size l) of + LT => + elemAt i l + GT => + elemAt ((i `minus` (size l)) `minus` 1) r + EQ => + x + +||| Delete the element at index, i.e. by its zero-based index in +||| the sorted sequence of elements. If the index is out of range (less than zero, +||| greater or equal to size of the set), idris_crash is called. O(log n) +export +partial +deleteAt : Nat -> Set a -> Set a +deleteAt i t = + case t of + Tip => assert_total $ idris_crash "Set.deleteAt: index out of range" + Bin _ x l r => + case compare i (size l) of + LT => + balanceR x (deleteAt i l) r + GT => + balanceL x l (deleteAt ((i `minus` (size l)) `minus` 1) r) + EQ => + glue l r + +||| Take a given number of elements in order, beginning +||| with the smallest keys. O(log n) +export +take : Nat -> Set a -> Set a +take i s = + case i >= size s of + True => + s + False => + go i s + where + go : Nat -> Set a -> Set a + go _ Tip = Tip + go i (Bin _ x l r) = + case i <= 0 of + True => + Tip + False => + case compare i (size l) of + LT => + go i l + GT => + link x l (go ((i `minus` (size l)) `minus` 1) r) + EQ => + l + +||| Drop a given number of elements in order, beginning +||| with the smallest ones. O(log n) +export +drop : Nat -> Set a -> Set a +drop i s = + case i >= size s of + True => + Tip + False => + go i s + where + go : Nat -> Set a -> Set a + go _ Tip = Tip + go i s@(Bin _ x l r) = + case i <= 0 of + True => + s + False => + case compare i (size l) of + LT => + link x (go i l) r + GT => + go ((i `minus` (size l)) `minus` 1) r + EQ => + insertMin x r + +||| Split a set at a particular index. O(log n) +export +splitAt : Nat -> Set a -> (Set a, Set a) +splitAt i s = + case i >= size s of + True => + (s,Tip) + False => + go i s + where + go : Nat -> Set a -> (Set a,Set a) + go _ Tip = (Tip,Tip) + go i s@(Bin _ x l r) = + case i <= 0 of + True => + (Tip,s) + False => + case compare i (size l) of + LT => + case go i l of + (ll,lr) => + (ll,link x lr r) + GT => + case go ((i `minus` (size l)) `minus` 1) r of + (rl,rr) => + (link x l rl,rr) + EQ => + (l,insertMin x r) + +-------------------------------------------------------------------------------- +-- Min/Max +-------------------------------------------------------------------------------- + +private +lookupMinSure : a -> Set a -> a +lookupMinSure x Tip = x +lookupMinSure _ (Bin _ x l _) = lookupMinSure x l + +||| The minimal element of the set. Returns Nothing if the set is empty. O(log n) +export +lookupMin : Set a -> Maybe a +lookupMin Tip = Nothing +lookupMin (Bin _ x l _) = Just $ lookupMinSure x l + +private +lookupMaxSure : a -> Set a -> a +lookupMaxSure x Tip = x +lookupMaxSure _ (Bin _ x _ r) = lookupMaxSure x r + +||| The maximal element of the set. Returns Nothing if the set is empty. O(log n) +export +lookupMax : Set a -> Maybe a +lookupMax Tip = Nothing +lookupMax (Bin _ x _ r) = Just $ lookupMaxSure x r + +||| The minimal element of the set. Calls idris_crash if the set is empty. O(log n) +export +partial +findMin : Set a -> a +findMin t = + case lookupMin t of + Just r => r + Nothing => assert_total $ idris_crash "Set.findMin: empty set has no minimal element" + +||| The maximal element of the set. Calls idris_crash if the set is empty. O(log n) +export +partial +findMax : Set a -> a +findMax t = + case lookupMax t of + Just r => r + Nothing => assert_total $ idris_crash "Set.findMax: empty set has no maximal element" + +||| Delete the minimal element. Returns an empty set if the set is empty. O(log n) +export +deleteMin : Set a -> Set a +deleteMin Tip = Tip +deleteMin (Bin _ _ Tip r) = r +deleteMin (Bin _ x l r) = balanceR x (deleteMin l) r + +||| Delete the maximal element. Returns an empty set if the set is empty. O(log n) +export +deleteMax : Set a -> Set a +deleteMax Tip = Tip +deleteMax (Bin _ _ l Tip) = l +deleteMax (Bin _ x l r) = balanceL x l (deleteMax r) + +||| Retrieves the minimal element of the set, and +||| the set stripped of that element, or Nothing if passed an empty set. O(log n) +export +minView : Set a -> Maybe (a,Set a) +minView Tip = Nothing +minView (Bin _ x l r) = + Just $ minViewSure x l r + +||| Delete and find the minimal element. O(log n) +export +partial +deleteFindMin : Set a -> (a,Set a) +deleteFindMin t = + case minView t of + Just res => res + Nothing => (assert_total $ idris_crash "Set.deleteFindMin: can not return the minimal element of an empty set",Tip) + +||| Retrieves the maximal element of the set, and +||| the set stripped of that element, or Nothing if passed an empty set. O(log n) +export +maxView : Set a -> Maybe (a,Set a) +maxView Tip = Nothing +maxView (Bin _ x l r) = + Just $ maxViewSure x l r + +||| Delete and find the maximal element. O(log n) +export +partial +deleteFindMax : Set a -> (a,Set a) +deleteFindMax t = + case maxView t of + Just res => res + Nothing => (assert_total $ idris_crash "Set.deleteFindMax: can not return the maximal element of an empty set",Tip) + +-------------------------------------------------------------------------------- +-- Combine +-------------------------------------------------------------------------------- + +||| The expression (union t1 t2) takes the left-biased union of t1 and t2. +||| It prefers t1 when duplicate keys are encountered. +export +union : Eq (Set a) => Eq a => Ord a => Set a -> Set a -> Set a +union t1 Tip = t1 +union t1 (Bin 1 x _ _) = insertR x t1 +union (Bin 1 x _ _) t2 = insert x t2 +union Tip t2 = t2 +union t1@(Bin _ x l1 r1) t2 = + let (l2,r2) = split x t2 + l1l2 = union l1 l2 + r1r2 = union r1 r2 + in case l1l2 == l1 && r1r2 == r1 of + True => + t1 + False => + link x l1l2 r1r2 + +-------------------------------------------------------------------------------- +-- Difference +-------------------------------------------------------------------------------- + +||| Difference of two sets. +||| Return elements of the first set not existing in the second set. +export +difference : Ord a => Set a -> Set a -> Set a +difference Tip _ = Tip +difference t1 Tip = t1 +difference t1 (Bin _ x l2 r2) = + let (l1, r1) = split x t1 + l1l2 = difference l1 l2 + r1r2 = difference r1 r2 + in case size l1l2 + size r1r2 == size t1 of + True => + t1 + False => + merge l1l2 r1r2 + +||| Same as difference. +export +(\\) : Ord a => Set a -> Set a -> Set a +s1 \\ s2 = difference s1 s2 + +-------------------------------------------------------------------------------- +-- Intersection +-------------------------------------------------------------------------------- + +||| Intersection of two sets. +||| Return data in the first set for elements existing in both sets. +export +intersection : Eq (Set a) => Ord a => Set a -> Set a -> Set a +intersection Tip _ = Tip +intersection _ Tip = Tip +intersection t1@(Bin _ x l1 r1) t2 = + let (l2,x',r2) = splitMember x t2 + l1l2 = intersection l1 l2 + r1r2 = intersection r1 r2 + in case x' of + True => + case l1l2 == l1 && r1r2 == r1 of + True => + t1 + False => + link x l1l2 r1r2 + False => + merge l1l2 r1r2 + +-------------------------------------------------------------------------------- +-- Lists +-------------------------------------------------------------------------------- + +||| Convert the set to a list of elements where the elements are in descending order. O(n) +export +toDescList : Set a -> List a +toDescList Tip = [] +toDescList t@(Bin _ _ _ _) = foldl (\xs, x => x :: xs) [] t + +||| Convert the set to a list of elements where the elements are in ascending order. O(n) +export +toAscList : Set a -> List a +toAscList Tip = [] +toAscList t@(Bin _ _ _ _) = foldr (\x, xs => x :: xs) [] t + +||| Convert the set to a list of elements. +export +toList : Set a -> List a +toList = toAscList + +||| Build a set from a list of elements. +||| If the list contains identical element(s), +||| the last of each identical elemen is retained. +||| If the elements of the list are ordered, a linear-time implementation is used. O(n * log(n)) +export +partial +fromList : Ord a => List a -> Set a +fromList [] = Tip +fromList xs = + case sorted xs of + True => + buildBalancedTree (convertToList1 xs) (length xs) + False => + buildBalancedTree (convertToList1 (sort xs)) (length xs) + where + -- Calculate the size of a tree + sizeTree : Set a -> Nat + sizeTree Tip = 0 + sizeTree (Bin sz _ _ _) = sz + -- Convert a list to a List1, which requires the list to be non-empty + convertToList1 : List a -> List1 a + convertToList1 [] = assert_total $ idris_crash "Unexpected empty list" + convertToList1 (x :: xs) = x ::: xs + -- Link a root node with two subtrees + linkRootWithSubtrees : a -> Set a -> Set a -> Nat -> Set a + linkRootWithSubtrees x left right newSize = + Bin newSize x left right + -- Split a non-empty list into left, middle, and right parts + splitList : List1 a -> Nat -> (List a, a, List a, Nat) + splitList l len = + let half = len `div` 2 + (left, rest) = splitAt half (forget l) + in case rest of + [] => + assert_total $ idris_crash "Unexpected empty list" + (middle :: right) => + (left, middle, right, len) + -- Build a balanced tree from a non-empty list + buildBalancedTree : List1 a -> Nat -> Set a + buildBalancedTree (x ::: []) _ = Bin 1 x Tip Tip + buildBalancedTree xs len = + let (left, root, right, totalSize) = splitList xs len + leftTree = case left of + [] => + Tip + _ => + assert_total $ buildBalancedTree (convertToList1 left) (length left) + rightTree = case right of + [] => + Tip + _ => + assert_total $ buildBalancedTree (convertToList1 right) (length right) + in linkRootWithSubtrees root leftTree rightTree totalSize + +-------------------------------------------------------------------------------- +-- Map +-------------------------------------------------------------------------------- + +||| Map a function over all elements in the set. O(n) +export +map : (a -> b) -> Set a -> Set b +map _ Tip = Tip +map f (Bin sz x l r) = Bin sz (f x) (map f l) (map f r) + +-------------------------------------------------------------------------------- +-- Disjoint Union +-------------------------------------------------------------------------------- + +||| Calculate the disjoint union of two sets. O(n + m) +export +disjointUnion : Set a -> Set b -> Set (Either a b) +disjointUnion as bs = merge (map Left as) (map Right bs) + +-------------------------------------------------------------------------------- +-- Interfaces +-------------------------------------------------------------------------------- + +export +Functor Set where + map f s = map f s + +export +Show (List a) => Show (Set a) where + show s = "fromList " ++ (show $ toList s) diff --git a/src/Data/Set/Internal.idr b/src/Data/Set/Internal.idr new file mode 100644 index 0000000..9a990e6 --- /dev/null +++ b/src/Data/Set/Internal.idr @@ -0,0 +1,239 @@ +||| Set Internals +module Data.Set.Internal + +import Data.List +import Data.String +import Derive.Prelude + +%default total +%language ElabReflection + +-------------------------------------------------------------------------------- +-- Sets +-------------------------------------------------------------------------------- + +public export +Size : Type +Size = Nat + +||| A finite set of values. +public export +data Set a = Bin Size a (Set a) (Set a) + | Tip + +%runElab derive "Set" [Eq,Ord,Show] + +-------------------------------------------------------------------------------- +-- Creating Sets +-------------------------------------------------------------------------------- + +||| Wrap a single value in a set. +export +singleton : a -> Set a +singleton x = Bin 1 x Tip Tip + +-------------------------------------------------------------------------------- +-- Query +-------------------------------------------------------------------------------- + +||| The number of elements in the set. O(1) +export +size : Set a -> Nat +size Tip = 0 +size (Bin _ _ l r) = 1 + size l + size r + +-------------------------------------------------------------------------------- +-- Set Internals +-------------------------------------------------------------------------------- + +{- + [balance l x r] balances two trees with value x. + The sizes of the trees should balance after decreasing the + size of one of them. (a rotation). + + [delta] is the maximal relative difference between the sizes of + two trees, it corresponds with the [w] in Adams' paper. + [ratio] is the ratio between an outer and inner sibling of the + heavier subtree in an unbalanced setting. It determines + whether a double or single rotation should be performed + to restore balance. It is corresponds with the inverse + of $\alpha$ in Adam's article. + + Note that according to the Adam's paper: + - [delta] should be larger than 4.646 with a [ratio] of 2. + - [delta] should be larger than 3.745 with a [ratio] of 1.534. + + But the Adam's paper is erroneous: + - It can be proved that for delta=2 and delta>=5 there does + not exist any ratio that would work. + - Delta=4.5 and ratio=2 does not work. + + That leaves two reasonable variants, delta=3 and delta=4, + both with ratio=2. + + - A lower [delta] leads to a more 'perfectly' balanced tree. + - A higher [delta] performs less rebalancing. + + In the benchmarks, delta=3 is faster on insert operations, + and delta=4 has slightly better deletes. As the insert speedup + is larger, we currently use delta=3. +-} + +export +delta : Nat +delta = 3 + +ratio : Nat +ratio = 2 + +||| The bin constructor maintains the size of the tree. +bin : a -> Set a -> Set a -> Set a +bin x l r = Bin (size l + size r + 1) x l r + +||| A specialized version of balance. +||| balanceL is called when left subtree might have been inserted to or when +||| right subtree might have been deleted from. +export +balanceL : a -> Set a -> Set a -> Set a +balanceL x l r = + case r of + Tip => + case l of + Tip => + Bin 1 x Tip Tip + (Bin _ _ Tip Tip) => + Bin 2 x l Tip + (Bin _ lx Tip (Bin _ lrx _ _)) => + Bin 3 lrx (Bin 1 lx Tip Tip) (Bin 1 x Tip Tip) + (Bin _ lx ll@(Bin _ _ _ _) Tip) => + Bin 3 lx ll (Bin 1 x Tip Tip) + (Bin ls lx ll@(Bin lls _ _ _) lr@(Bin lrs lrx lrl lrr)) => + case lrs < ratio * lls of + True => + Bin (1+ls) lx ll (Bin (1+lrs) x lr Tip) + False => + Bin (1+ls) lrx (Bin (1+lls+size lrl) lx ll lrl) (Bin (1+size lrr) x lrr Tip) + (Bin rs _ _ _) => + case l of + Tip => + Bin (1+rs) x Tip r + (Bin ls lx ll lr) => + case ls > delta * rs of + True => + case (ll,lr) of + (Bin lls _ _ _, Bin lrs lrx lrl lrr) => + case lrs < ratio * lls of + True => + Bin (1+ls+rs) lx ll (Bin (1+rs+lrs) x lr r) + False => + Bin (1+ls+rs) lrx (Bin (1+lls+size lrl) lx ll lrl) (Bin (1+rs+size lrr) x lrr r) + (_,_) => + assert_total $ idris_crash "Failure in Data.Set.Internal.balanceL" + False => + Bin (1+ls+rs) x l r + +||| A specialized version of balance. +||| balanceR is called when right subtree might have been inserted to or when +||| left subtree might have been deleted from. +export +balanceR : a -> Set a -> Set a -> Set a +balanceR x l r = + case l of + Tip => + case r of + Tip => + Bin 1 x Tip Tip + (Bin _ _ Tip Tip) => + Bin 2 x Tip r + (Bin _ rx Tip rr@(Bin _ _ _ _)) => + Bin 3 rx (Bin 1 x Tip Tip) rr + (Bin _ rx (Bin _ rlx _ _) Tip) => + Bin 3 rlx (Bin 1 x Tip Tip) (Bin 1 rx Tip Tip) + (Bin rs rx rl@(Bin rls rlx rll rlr) rr@(Bin rrs _ _ _)) => + case rls < ratio * rrs of + True => + Bin (1+rs) rx (Bin (1+rls) x Tip rl) rr + False => + Bin (1+rs) rlx (Bin (1+size rll) x Tip rll) (Bin (1+rrs+size rlr) rx rlr rr) + (Bin ls _ _ _) => + case r of + Tip => + Bin (1+ls) x l Tip + (Bin rs rx rl rr) => + case rs > delta * ls of + True => + case (rl,rr) of + (Bin rls rlx rll rlr, Bin rrs _ _ _) => + case rls < ratio * rrs of + True => + Bin (1+ls+rs) rx (Bin (1+ls+rls) x l rl) rr + False => + Bin (1+ls+rs) rlx (Bin (1+ls+size rll) x l rll) (Bin (1+rrs+size rlr) rx rlr rr) + (_,_) => + assert_total $ idris_crash "Failure in Data.Set.Internal.balanceR" + False => + Bin (1+ls+rs) x l r + +export +insertMax : a -> Set a -> Set a +insertMax x t = + case t of + Tip => + singleton x + Bin _ y l r => + balanceR y l (insertMax x r) + +export +insertMin : a -> Set a -> Set a +insertMin x t = + case t of + Tip => + singleton x + Bin _ y l r => + balanceL y (insertMin x l) r + +export +minViewSure : a -> Set a -> Set a -> (a,Set a) +minViewSure x Tip r = (x,r) +minViewSure x (Bin _ xl ll lr) r = + case minViewSure xl ll lr of + (xm, l') => + (xm, balanceR x l' r) + +export +maxViewSure : a -> Set a -> Set a -> (a,Set a) +maxViewSure x l Tip = (x,l) +maxViewSure x l (Bin _ xr rl rr) = + case maxViewSure xr rl rr of + (xm, r') => + (xm, balanceL x l r') + +||| Glues two sets together (assumes that both sets are already balanced with respect to each other). +export +glue : Set a -> Set a -> Set a +glue Tip r = r +glue l Tip = l +glue l@(Bin sl xl ll lr) r@(Bin sr xr rl rr) = + case sl > sr of + True => + let (m, l') = maxViewSure xl ll lr + in balanceR m l' r + False => + let (m, r') = minViewSure xr rl rr + in balanceL m l r' + +||| Utility function that maintains the balance properties of the tree. +export +link : a -> Set a -> Set a -> Set a +link x Tip r = insertMin x r +link x l Tip = insertMax x l +link x l@(Bin sizeL y ly ry) r@(Bin sizeR z lz rz) = + case delta * sizeL < sizeR of + True => + balanceL z (link x l lz) rz + False => + case delta * sizeR < sizeL of + True => + balanceR y ly (link x ry r) + False => + bin x l r