From 90f5a37542eafba210de57c1d67686a2ef132806 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 22 Aug 2024 21:37:02 -0400 Subject: [PATCH 01/31] Initial commit for adding a map container. --- README.md | 2 +- containers.ipkg | 4 +- src/Data/Map.idr | 674 ++++++++++++++++++++++++++++++++++++++ src/Data/Map/Internal.idr | 307 +++++++++++++++++ 4 files changed, 985 insertions(+), 2 deletions(-) create mode 100644 src/Data/Map.idr create mode 100644 src/Data/Map/Internal.idr 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..1403e35 100644 --- a/containers.ipkg +++ b/containers.ipkg @@ -7,5 +7,7 @@ sourcedir = "src" depends = base >= 0.6.0 , elab-util -modules = Data.Queue +modules = Data.Map + , Data.Map.Internal + , Data.Queue , Data.Tree diff --git a/src/Data/Map.idr b/src/Data/Map.idr new file mode 100644 index 0000000..bf65fda --- /dev/null +++ b/src/Data/Map.idr @@ -0,0 +1,674 @@ +module Data.Map + +import Data.Map.Internal + +import Control.Monad.Identity +import Data.List +import Data.String +import Derive.Prelude + +%hide Prelude.null + +%default total + +-------------------------------------------------------------------------------- +-- Creating Maps +-------------------------------------------------------------------------------- + +||| The empty map. (O)1 +public export +empty : Map k a +empty = Tip + +-------------------------------------------------------------------------------- +-- Insertion +-------------------------------------------------------------------------------- + +public 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 => + case (go orig kx x l) == l of + True => + t + False => + balanceL ky y (go orig kx x l) r + GT => + case (go orig kx x r) == r of + True => + t + False => + balanceR ky y l (go orig kx x r) + EQ => + case (x == y && orig == ky) of + True => + t + False => + Bin sz orig x l r + +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 => + case (go orig kx x l) == l of + True => + t + False => + balanceL ky y (go orig kx x l) r + GT => + case (go orig kx x r) == r of + True => + t + False => + balanceR ky y l (go orig kx x r) + EQ => + t + +public 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 + +public 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 + +public 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 +-------------------------------------------------------------------------------- + +public 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 => + case (go k l) == l of + True => + t + False => + balanceR kx x (go k l) r + GT => + case (go k r) == r of + True => + t + False => + balanceL kx x l (go k r) + EQ => + glue l r + +public 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 + +public export +adjust : Ord k => (v -> v) -> k -> Map k v -> Map k v +adjust f = adjustWithKey (\_, x => f x) + +public 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 + +public export +update : Ord k => (v -> Maybe v) -> k -> Map k v -> Map k v +update f = updateWithKey (\_, x => f x) + +public 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) + +public 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 +-------------------------------------------------------------------------------- + +public 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 + +public export +(!?) : Ord k => Map k v -> k -> Maybe v +(!?) m k = lookup k m + +public 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 + +public export +notMember : Ord k => k -> Map k v -> Bool +notMember k m = not $ member k m + +public export +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 + +public export +(!!) : Ord k => Map k v -> k -> v +(!!) m k = find k m + +public 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 + +public 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 + +public 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 + +public 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 + +public 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 +-------------------------------------------------------------------------------- + +public export +null : Map k v -> Bool +null Tip = True +null _ = False + +-------------------------------------------------------------------------------- +-- Filter +-------------------------------------------------------------------------------- + +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) + +public 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] + +public 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) + +public 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) + +public 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) + +public export +filter : Eq (Map k v) => (v -> Bool) -> Map k v -> Map k v +filter p m = filterWithKey (\_, x => p x) m + +public 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) + ) + +public 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 + +public 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 + +public 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) + +public 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) + +public export +mapMaybe : (a -> Maybe b) -> Map k a -> Map k b +mapMaybe f = mapMaybeWithKey (\_, x => f x) + +public 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)) + +public export +mapEither : (a -> Either b c) -> Map k a -> (Map k b, Map k c) +mapEither f m = mapEitherWithKey (\_, x => f x) m + +{- +-------------------------------------------------------------------------------- +-- Combine +-------------------------------------------------------------------------------- + +union : Ord k => Map k v -> Map k v -> Map k v +union t1 Tip = t1 +union t1 (Bin _ k x Tip Tip) = insert 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) | l1l2 `ptrEq` l1 && r1r2 `ptrEq` r1 -> t1 + | otherwise -> link k1 x1 l1l2 r1r2 + where !l1l2 = union l1 l2 + !r1r2 = union r1 r2 +-} + +-------------------------------------------------------------------------------- +-- Folds +-------------------------------------------------------------------------------- + +public 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 + +public 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 + +public 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 + +public 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 + +-------------------------------------------------------------------------------- +-- Traversal +-------------------------------------------------------------------------------- + +public 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) + +public 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) + +public 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') + +public 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') + +public export +mapAccumWithKey : (v -> k -> w -> (v,c)) -> v -> Map k w -> (v,Map k c) +mapAccumWithKey f a t = mapAccumL f a t + +public 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 + +-------------------------------------------------------------------------------- +-- Compose +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +-- Lists +-------------------------------------------------------------------------------- + +public export +toDescList : Map k v -> List (k,v) +toDescList Tip = [] +toDescList t@(Bin _ _ _ _ _) = foldlWithKey (\xs, k, x => (k,x) :: xs) [] t + +public 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. +public export +toList : Map k v -> List (k,v) +toList = toAscList + +-------------------------------------------------------------------------------- +-- Keys +-------------------------------------------------------------------------------- + +||| Gets the keys of the map. +public export +keys : Map k v -> List k +keys = map fst . toList + +-------------------------------------------------------------------------------- +-- Values +-------------------------------------------------------------------------------- + +||| Gets the values of the map. +||| Could contain duplicates. +public export +values : Map k v -> List v +values = map snd . toList + +-------------------------------------------------------------------------------- +-- Interfaces +-------------------------------------------------------------------------------- + +public export +Functor (Map k) where + map f m = map f m + +public export +Foldable (Map k) where + foldl f z = foldl f z . values + foldr f z = foldr f z . values + null = null diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr new file mode 100644 index 0000000..2af2d9e --- /dev/null +++ b/src/Data/Map/Internal.idr @@ -0,0 +1,307 @@ +module Data.Map.Internal + +import Data.List +import Data.String +import Derive.Prelude + +%language ElabReflection +%default total + +-------------------------------------------------------------------------------- +-- Maps +-------------------------------------------------------------------------------- + +public export +Size : Type +Size = Int + +||| 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] + +data MinView k a = MinView' k a (Map k a) + +%runElab derive "MinView" [Eq,Ord,Show] + +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 +public export +singleton : k -> a -> Map k a +singleton k x = Bin 1 k x Tip Tip + +-------------------------------------------------------------------------------- +-- Query +-------------------------------------------------------------------------------- + +public export +size : Map k v -> Int +size Tip = 0 +size (Bin sz _ _ _ _) = sz + +-------------------------------------------------------------------------------- +-- 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 : Int +delta = 3 + +ratio : Int +ratio = 2 + +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 + +public 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 + +public 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 + +public 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 + +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) + +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 + +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) + +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') + +public 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' + +public 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 + +public 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 From e9fe5b49da17200b9946b1dcd522a80364e5f71d Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 23 Aug 2024 18:00:56 -0400 Subject: [PATCH 02/31] Cleaning up and adding documentation. --- src/Data/Map.idr | 692 ++++++++++++++++++++++++++++++++++++-- src/Data/Map/Internal.idr | 19 ++ 2 files changed, 679 insertions(+), 32 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index bf65fda..5a02d7b 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1,11 +1,9 @@ +||| Finite Maps module Data.Map import Data.Map.Internal -import Control.Monad.Identity import Data.List -import Data.String -import Derive.Prelude %hide Prelude.null @@ -20,10 +18,41 @@ public export empty : Map k a empty = Tip +-------------------------------------------------------------------------------- +-- Folds +-------------------------------------------------------------------------------- + +||| Fold the values in the map using the given left-associative binary operator. O(n) +public 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) +public 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) +public 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) +public 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) public 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 @@ -73,6 +102,11 @@ insertR kx0 = go kx0 kx0 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) public export insertWith : Ord k => (v -> v -> v) -> k -> v -> Map k v -> Map k v insertWith = go @@ -88,6 +122,36 @@ insertWith = go EQ => Bin sy kx (f x y) l r +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 + +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) public export insertWithKey : Ord k => (k -> v -> v -> v) -> k -> v -> Map k v -> Map k v insertWithKey = go @@ -100,6 +164,10 @@ insertWithKey = go 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) public 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 @@ -120,6 +188,8 @@ insertLookupWithKey f0 k0 x0 = go f0 k0 x0 -- 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) public export delete : Eq (Map k v) => Eq k => Ord k => k -> Map k v -> Map k v delete = go @@ -143,6 +213,8 @@ delete = go 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) public export adjustWithKey : Ord k => (k -> v -> v) -> k -> Map k v -> Map k v adjustWithKey = go @@ -158,10 +230,16 @@ adjustWithKey = go 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) public 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) public export updateWithKey : Ord k => (k -> v -> Maybe v) -> k -> Map k v -> Map k v updateWithKey = go @@ -181,10 +259,16 @@ updateWithKey = go 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) public 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) public export updateLookupWithKey : Ord k => (k -> v -> Maybe v) -> k -> Map k v -> (Maybe v,Map k v) updateLookupWithKey f0 k0 = go f0 k0 @@ -209,6 +293,8 @@ updateLookupWithKey f0 k0 = go f0 k0 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) public export alter : Ord k => (Maybe v -> Maybe v) -> k -> Map k v -> Map k v alter = go @@ -233,6 +319,9 @@ alter = go -- 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) public export lookup : Ord k => k -> Map k v -> Maybe v lookup = go @@ -246,10 +335,13 @@ lookup = go 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) public 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) public export member : Ord k => k -> Map k v -> Bool member _ Tip = False @@ -259,10 +351,13 @@ member k (Bin _ kx _ l r) = GT => member k r EQ => True +||| Is the key not a member of the map? See also member. O(log n) public 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) public export find : Ord k => k -> Map k v -> v find _ Tip = assert_total $ idris_crash "Map.!: given key is not an element in the map" @@ -272,10 +367,15 @@ find k (Bin _ kx x l r) = 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) public export (!!) : 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) public export findWithDefault : Ord k => v -> k -> Map k v -> v findWithDefault def _ Tip = def @@ -285,6 +385,8 @@ findWithDefault def k (Bin _ kx x l r) = 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) public export lookupLT : Ord k => k -> Map k v -> Maybe (k,v) lookupLT = goNothing @@ -302,6 +404,8 @@ lookupLT = goNothing 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) public export lookupGT : Ord k => k -> Map k v -> Maybe (k,v) lookupGT = goNothing @@ -319,6 +423,8 @@ lookupGT = goNothing 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) public export lookupLE : Ord k => k -> Map k v -> Maybe (k,v) lookupLE = goNothing @@ -338,6 +444,8 @@ lookupLE = goNothing 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) public export lookupGE : Ord k => k -> Map k v -> Maybe (k,v) lookupGE = goNothing @@ -361,6 +469,7 @@ lookupGE = goNothing -- Size -------------------------------------------------------------------------------- +||| Is the map empty? O(1) public export null : Map k v -> Bool null Tip = True @@ -386,6 +495,8 @@ splitMember k0 m = go k0 m 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) public export splitRoot : Map k v -> List (Map k v) splitRoot orig = @@ -395,6 +506,8 @@ splitRoot orig = 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) public export splitLookup : Ord k => k -> Map k v -> (Map k v,Maybe v,Map k v) splitLookup k0 m = go k0 m @@ -412,6 +525,9 @@ splitLookup k0 m = go k0 m 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) public export split : Ord k => k -> Map k v -> (Map k v,Map k v) split k0 t0 = go k0 t0 @@ -429,6 +545,7 @@ split k0 t0 = go k0 t0 in (link kx x l lt,gt) EQ => (l,r) +||| Filter all keys/values that satisfy the predicate. O(n) public export filterWithKey : Eq (Map k v) => (k -> v -> Bool) -> Map k v -> Map k v filterWithKey _ Tip = Tip @@ -443,10 +560,14 @@ filterWithKey p t@(Bin _ kx x l r) = False => link2 (filterWithKey p l) (filterWithKey p r) +||| Filter all values that satisfy the predicate. O(n) public 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) public export partitionWithKey : Eq (Map k v) => (k -> v -> Bool) -> Map k v -> (Map k v,Map k v) partitionWithKey p0 t0 = go p0 t0 @@ -472,6 +593,9 @@ partitionWithKey p0 t0 = go p0 t0 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) public export takeWhileAntitone : (k -> Bool) -> Map k v -> Map k v takeWhileAntitone _ Tip = Tip @@ -482,6 +606,9 @@ takeWhileAntitone p (Bin _ kx x l 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) public export dropWhileAntitone : (k -> Bool) -> Map k v -> Map k v dropWhileAntitone _ Tip = Tip @@ -492,6 +619,9 @@ dropWhileAntitone p (Bin _ kx x l 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) public export spanAntitone : (k -> Bool) -> Map k v -> (Map k v, Map k v) spanAntitone p0 m = go p0 m @@ -507,6 +637,7 @@ spanAntitone p0 m = go p0 m let (u,v) = go p l in (u,link kx x v r) +||| Map keys/values and collect the Just results. O(n) public export mapMaybeWithKey : (k -> a -> Maybe b) -> Map k a -> Map k b mapMaybeWithKey _ Tip = Tip @@ -517,10 +648,12 @@ mapMaybeWithKey f (Bin _ kx x l r) = Nothing => link2 (mapMaybeWithKey f l) (mapMaybeWithKey f r) +||| Map values and collect the Just results. O(n) public 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) public export mapEitherWithKey : (k -> a -> Either b c) -> Map k a -> (Map k b, Map k c) mapEitherWithKey f0 t0 = go f0 t0 @@ -532,65 +665,556 @@ mapEitherWithKey f0 t0 = go f0 t0 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) public export mapEither : (a -> Either b c) -> Map k a -> (Map k b, Map k c) mapEither f m = mapEitherWithKey (\_, x => f x) m -{- +-------------------------------------------------------------------------------- +-- Submap +-------------------------------------------------------------------------------- + +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. +public 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 (==)). +public 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. +public 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 (==)). +public 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) +public export +lookupIndex : Ord k => k -> Map k v -> Maybe Int +lookupIndex = go 0 + where + go : Int -> k -> Map k a -> Maybe Int + 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) +public export +findIndex : Ord k => k -> Map k v -> Int +findIndex = go 0 + where + go : Int -> k -> Map k a -> Int + 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) +public export +elemAt : Int -> 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-(size l)-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) +public export +updateAt : (k -> v -> Maybe v) -> Int -> 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-(size l)-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) +public export +deleteAt : Int -> 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-(size l)-1) r) + EQ => + glue l r + +||| Take a given number of entries in key order, beginning +||| with the smallest keys. O(log n) +public export +take : Int -> Map k v -> Map k v +take i m = + case i >= size m of + True => + m + False => + go i m + where + go : Int -> 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 - (size l) - 1) r) + EQ => + l + +||| Drop a given number of entries in key order, beginning +||| with the smallest keys. O(log n) +public export +drop : Int -> Map k v -> Map k v +drop i m = + case i >= size m of + True => + Tip + False => + go i m + where + go : Int -> 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 - (size l) - 1) r + EQ => + insertMin kx x r + +||| Split a map at a particular index. O(log n) +public export +splitAt : Int -> 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 : Int -> 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 - (size l) - 1) r of + (rl,rr) => + (link kx x l rl,rr) + EQ => + (l,insertMin kx x r) + +-------------------------------------------------------------------------------- +-- Min/Max +-------------------------------------------------------------------------------- + +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) +public export +lookupMin : Map k v -> Maybe (k,v) +lookupMin Tip = Nothing +lookupMin (Bin _ k v l _) = Just $ lookupMinSure k v l + +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) +public 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) +public export +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) +public export +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) +public 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) +public 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) +public 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) +public export +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) +public 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) +public export +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) +public 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) +public 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) +public 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) +public 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) +public 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) +public 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 -------------------------------------------------------------------------------- -union : Ord k => Map k v -> Map k v -> Map k v -union t1 Tip = t1 -union t1 (Bin _ k x Tip Tip) = insert 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) | l1l2 `ptrEq` l1 && r1r2 `ptrEq` r1 -> t1 - | otherwise -> link k1 x1 l1l2 r1r2 - where !l1l2 = union l1 l2 - !r1r2 = union r1 r2 --} +||| The expression (union t1 t2) takes the left-biased union of t1 and t2. +||| It prefers t1 when duplicate keys are encountered. +public 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. +public 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. +public 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. +public 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. +public export +unionsWith : Foldable f => Ord k => (v -> v -> v) -> f (Map k v) -> Map k v +unionsWith f ts = foldl (unionWith f) empty ts -------------------------------------------------------------------------------- --- Folds +-- Difference -------------------------------------------------------------------------------- +||| Difference of two maps. +||| Return elements of the first map not existing in the second map. public 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 +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. public 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 +(\\) : 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. public 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 +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. public 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 +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. +public 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). +public 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. +public 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) public 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) public 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) public export mapAccumL : (v -> k -> w -> (v,c)) -> v -> Map k w -> (v,Map k c) mapAccumL _ a Tip = (a,Tip) @@ -600,6 +1224,8 @@ mapAccumL f a (Bin sx kx x l r) = (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) public export mapAccumRWithKey : (v -> k -> w -> (v,c)) -> v -> Map k w -> (v,Map k c) mapAccumRWithKey _ a Tip = (a,Tip) @@ -609,27 +1235,29 @@ mapAccumRWithKey f a (Bin sx kx x l r) = (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) public 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) public 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 --------------------------------------------------------------------------------- --- Compose --------------------------------------------------------------------------------- - -------------------------------------------------------------------------------- -- Lists -------------------------------------------------------------------------------- +||| Convert the map to a list of key/value pairs where the keys are in descending order. O(n) public 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) public export toAscList : Map k v -> List (k,v) toAscList Tip = [] diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr index 2af2d9e..eafd1e1 100644 --- a/src/Data/Map/Internal.idr +++ b/src/Data/Map/Internal.idr @@ -1,3 +1,4 @@ +||| Map Internals module Data.Map.Internal import Data.List @@ -22,10 +23,12 @@ data Map k v = Bin Size k v (Map k v) (Map k v) %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] @@ -43,6 +46,7 @@ singleton k x = Bin 1 k x Tip Tip -- Query -------------------------------------------------------------------------------- +||| The number of elements in the map. O(1) public export size : Map k v -> Int size Tip = 0 @@ -91,9 +95,11 @@ delta = 3 ratio : Int 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. public export balance : k -> v -> Map k v -> Map k v -> Map k v balance k x l r = @@ -157,6 +163,9 @@ balance k x l r = 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. public export balanceL : k -> v -> Map k v -> Map k v -> Map k v balanceL k x l r = @@ -196,6 +205,9 @@ balanceL k x l r = 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. public export balanceR : k -> v -> Map k v -> Map k v -> Map k v balanceR k x l r = @@ -235,6 +247,7 @@ balanceR k x l r = False => Bin (1+ls+rs) k x l r +public export insertMax : k -> v -> Map k v -> Map k v insertMax kx x t = case t of @@ -243,6 +256,7 @@ insertMax kx x t = Bin _ ky y l r => balanceR ky y l (insertMax kx x r) +public export insertMin : k -> v -> Map k v -> Map k v insertMin kx x t = case t of @@ -251,18 +265,21 @@ insertMin kx x t = Bin _ ky y l r => balanceL ky y (insertMin kx x l) r +public 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) +public 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). public export glue : Map k v -> Map k v -> Map k v glue Tip r = r @@ -276,6 +293,7 @@ glue l@(Bin sl kl xl ll lr) r@(Bin sr kr xr rl rr) = 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. public export link2 : Map k v -> Map k v -> Map k v link2 Tip r = r @@ -291,6 +309,7 @@ link2 l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry) = False => glue l r +||| Utility function that maintains the balance properties of the tree. public export link : k -> v -> Map k v -> Map k v -> Map k v link kx x Tip r = insertMin kx x r From 47f57276ec417b5923855204670a401a7c53fad8 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 23 Aug 2024 19:32:15 -0400 Subject: [PATCH 03/31] Removing Data.Internal.Map.idr from modules. --- containers.ipkg | 1 - 1 file changed, 1 deletion(-) diff --git a/containers.ipkg b/containers.ipkg index 1403e35..a4c0060 100644 --- a/containers.ipkg +++ b/containers.ipkg @@ -8,6 +8,5 @@ depends = base >= 0.6.0 , elab-util modules = Data.Map - , Data.Map.Internal , Data.Queue , Data.Tree From e9fd3ff40becaaa353b925ae3067047feacec28d Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 24 Aug 2024 00:35:08 -0400 Subject: [PATCH 04/31] Fixing whitespace linting, and change Ints to Nats. --- src/Data/Map.idr | 52 +++++++++++++++++++-------------------- src/Data/Map/Internal.idr | 13 +++++----- 2 files changed, 33 insertions(+), 32 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 5a02d7b..d510454 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -31,7 +31,7 @@ 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) public export foldr : (v -> w -> w) -> w -> Map k v -> w -foldr f z Tip = z +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) @@ -414,7 +414,7 @@ lookupGT = goNothing 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 + True => goJust k kx x l False => goJust k kx' x' r goNothing : k -> Map k v -> Maybe (k,v) goNothing _ Tip = Nothing @@ -729,10 +729,10 @@ isProperSubmapOf m1 m2 = isProperSubmapOfBy (==) m1 m2 ||| 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) public export -lookupIndex : Ord k => k -> Map k v -> Maybe Int +lookupIndex : Ord k => k -> Map k v -> Maybe Nat lookupIndex = go 0 where - go : Int -> k -> Map k a -> Maybe Int + go : Nat -> k -> Map k a -> Maybe Nat go _ _ Tip = Nothing go idx k (Bin _ kx _ l r) = case compare k kx of @@ -748,10 +748,10 @@ lookupIndex = go 0 ||| including, the size of the map. Calls idris_crash when the key is not ||| a member of the map. O(log n) public export -findIndex : Ord k => k -> Map k v -> Int +findIndex : Ord k => k -> Map k v -> Nat findIndex = go 0 where - go : Int -> k -> Map k a -> Int + 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 @@ -766,14 +766,14 @@ findIndex = go 0 ||| 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) public export -elemAt : Int -> Map k v -> (k,v) +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-(size l)-1) r + elemAt ((i `minus` (size l)) `minus` 1) r EQ => (kx,x) @@ -781,7 +781,7 @@ elemAt i (Bin _ kx x l r) = ||| 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) public export -updateAt : (k -> v -> Maybe v) -> Int -> Map k v -> Map k v +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" @@ -790,7 +790,7 @@ updateAt f i t = LT => balanceR kx x (updateAt f i l) r GT => - balanceL kx x l (updateAt f (i-(size l)-1) r) + balanceL kx x l (updateAt f ((i `minus` (size l)) `minus` 1) r) EQ => case f kx x of Just x' => @@ -802,7 +802,7 @@ updateAt f i t = ||| 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) public export -deleteAt : Int -> Map k v -> Map k v +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" @@ -811,14 +811,14 @@ deleteAt i t = LT => balanceR kx x (deleteAt i l) r GT => - balanceL kx x l (deleteAt (i-(size l)-1) r) + 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) public export -take : Int -> Map k v -> Map k v +take : Nat -> Map k v -> Map k v take i m = case i >= size m of True => @@ -826,7 +826,7 @@ take i m = False => go i m where - go : Int -> Map k v -> Map k v + go : Nat -> Map k v -> Map k v go _ Tip = Tip go i (Bin _ kx x l r) = case i <= 0 of @@ -837,14 +837,14 @@ take i m = LT => go i l GT => - link kx x l (go (i - (size l) - 1) r) + 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) public export -drop : Int -> Map k v -> Map k v +drop : Nat -> Map k v -> Map k v drop i m = case i >= size m of True => @@ -852,7 +852,7 @@ drop i m = False => go i m where - go : Int -> Map k v -> Map k v + go : Nat -> Map k v -> Map k v go _ Tip = Tip go i (Bin _ kx x l r) = case i <= 0 of @@ -863,13 +863,13 @@ drop i m = LT => link kx x (go i l) r GT => - go (i - (size l) - 1) r + go ((i `minus` (size l)) `minus` 1) r EQ => insertMin kx x r ||| Split a map at a particular index. O(log n) public export -splitAt : Int -> Map k v -> (Map k v, Map k v) +splitAt : Nat -> Map k v -> (Map k v, Map k v) splitAt i m = case i >= size m of True => @@ -877,7 +877,7 @@ splitAt i m = False => go i m where - go : Int -> Map k v -> (Map k v,Map k v) + 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 @@ -890,7 +890,7 @@ splitAt i m = (ll,lr) => (ll,link kx x lr r) GT => - case go (i - (size l) - 1) r of + case go ((i `minus` (size l)) `minus` 1) r of (rl,rr) => (link kx x l rl,rr) EQ => @@ -1087,7 +1087,7 @@ unionWithKey f (Bin _ k1 x1 l1 r1) t2 = 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. +||| The union of a list of maps. public 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 @@ -1147,7 +1147,7 @@ public 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 = +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) @@ -1190,7 +1190,7 @@ disjoint (Bin _ k _ l r) t = ||| O(n * log(m)), where m is the size of the first argument. public export compose : Ord b => Map b c -> Map a b -> Map a c -compose bc ab = +compose bc ab = case null bc of True => empty @@ -1297,6 +1297,6 @@ Functor (Map k) where public export Foldable (Map k) where - foldl f z = foldl f z . values - foldr f z = foldr f z . values + foldl f z = foldl f z . values + foldr f z = foldr f z . values null = null diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr index eafd1e1..d740cf6 100644 --- a/src/Data/Map/Internal.idr +++ b/src/Data/Map/Internal.idr @@ -14,7 +14,7 @@ import Derive.Prelude public export Size : Type -Size = Int +Size = Nat ||| A finite map from keys k to values v. public export @@ -48,9 +48,10 @@ singleton k x = Bin 1 k x Tip Tip ||| The number of elements in the map. O(1) public export -size : Map k v -> Int -size Tip = 0 -size (Bin sz _ _ _ _) = sz +size : Map k v -> Nat +size Tip = 0 +size (Bin Z _ _ _ _) = 0 +size (Bin (S n) _ _ _ _) = n -------------------------------------------------------------------------------- -- Map Internals @@ -89,10 +90,10 @@ size (Bin sz _ _ _ _) = sz is larger, we currently use delta=3. -} -delta : Int +delta : Nat delta = 3 -ratio : Int +ratio : Nat ratio = 2 ||| The bin constructor maintains the size of the tree. From 8346347ebff36f0dd94cea6de6e699a2a040446b Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 29 Aug 2024 16:11:13 -0400 Subject: [PATCH 05/31] Adding fromList function. --- src/Data/Map.idr | 60 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index d510454..b413d22 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -3,6 +3,7 @@ module Data.Map import Data.Map.Internal +import Data.Bits import Data.List %hide Prelude.null @@ -1251,6 +1252,65 @@ mapAccum f a m = mapAccumWithKey (\a', _, x' => f a' x') a m -- Lists -------------------------------------------------------------------------------- +||| Build a map from a list of key/value pairs. See also fromAscList. +||| 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)) +public export +partial +fromList : Eq (Map k v) => Eq v => Ord k => List (k,v) -> Map k v +fromList [] = Tip +fromList [(kx, x)] = Bin 1 kx x Tip Tip +fromList ((kx0, x0) :: xs0) = + case not_ordered kx0 xs0 of + True => + fromList' (Bin 1 kx0 x0 Tip Tip) xs0 + False => + go 1 (Bin 1 kx0 x0 Tip Tip) xs0 + where + not_ordered : k -> List (k,v) -> Bool + not_ordered _ [] = False + not_ordered kx ((ky,_) :: _) = kx >= ky + fromList' : Map k v -> List (k,v) -> Map k v + fromList' t0 xs = foldl ins t0 xs + where + ins : Map k v -> (k,v) -> Map k v + ins t (k,x) = insert k x t + create : Nat -> List (k,v) -> (Map k v,List (k,v),List (k,v)) + create _ [] = (Tip, [], []) + create Z _ = (Tip, [], []) + create (S k) xs@((kx, x) :: xss) = + case k == 1 of + True => + case not_ordered kx xss of + True => + (Bin 1 kx x Tip Tip, [], xss) + False => + (Bin 1 kx x Tip Tip, xss, []) + False => + case create (the Nat (cast (the Int (cast k) `shiftR` 1))) xs of + res@(_, [], _) => res + (l, [(ky, y)], zs) => (insertMax ky y l, [], zs) + (l, ys@((ky, y) :: yss), _) => + case not_ordered ky yss of + True => + (l, [], ys) + False => + let (r, zs, ws) = create (the Nat (cast (the Int (cast k) `shiftR` 1))) yss + in (link ky y l r, zs, ws) + go : Nat -> Map k v -> List (k,v) -> Map k v + go _ t [] = t + go Z t _ = t + go _ t [(kx, x)] = insertMax kx x t + go (S k) l xs@((kx, x) :: xss) = + case not_ordered kx xss of + True => + fromList' l xs + False => + case create k xss of + (r, ys, []) => go (the Nat (cast (the Int (cast k) `shiftL` 1))) (link kx x l r) ys + (r, _, ys) => fromList' (link kx x l r) ys + ||| Convert the map to a list of key/value pairs where the keys are in descending order. O(n) public export toDescList : Map k v -> List (k,v) From c36e3e0a873865eabb138b48d0ce34c286eb6fe1 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 29 Aug 2024 17:42:45 -0400 Subject: [PATCH 06/31] Updating containers.ipkg with Data.Map.Internal module, and adding show interface for Map k v. --- containers.ipkg | 1 + src/Data/Map.idr | 7 ++++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/containers.ipkg b/containers.ipkg index a4c0060..1403e35 100644 --- a/containers.ipkg +++ b/containers.ipkg @@ -8,5 +8,6 @@ depends = base >= 0.6.0 , elab-util modules = Data.Map + , Data.Map.Internal , Data.Queue , Data.Tree diff --git a/src/Data/Map.idr b/src/Data/Map.idr index b413d22..7177f4c 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1,12 +1,13 @@ ||| Finite Maps module Data.Map -import Data.Map.Internal +import public Data.Map.Internal import Data.Bits import Data.List %hide Prelude.null +%hide Prelude.toList %default total @@ -1360,3 +1361,7 @@ Foldable (Map k) where foldl f z = foldl f z . values foldr f z = foldr f z . values null = null + +public export +Show k => Show v => Show (Map k v) where + show = show . toList From 05607515e923a976cd536f2e3270211ee82690f2 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 4 Sep 2024 21:17:24 -0400 Subject: [PATCH 07/31] Reordering pragmas at top of src/Data/Map/Internal.idr and removing unnecessary Show implementation for Map k v. --- src/Data/Map.idr | 4 ---- src/Data/Map/Internal.idr | 2 +- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 7177f4c..9da5e10 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1361,7 +1361,3 @@ Foldable (Map k) where foldl f z = foldl f z . values foldr f z = foldr f z . values null = null - -public export -Show k => Show v => Show (Map k v) where - show = show . toList diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr index d740cf6..459254b 100644 --- a/src/Data/Map/Internal.idr +++ b/src/Data/Map/Internal.idr @@ -5,8 +5,8 @@ import Data.List import Data.String import Derive.Prelude -%language ElabReflection %default total +%language ElabReflection -------------------------------------------------------------------------------- -- Maps From 0cf19b1fe2bccca1f9f6f775e19f8abc2baa615b Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 4 Sep 2024 21:49:43 -0400 Subject: [PATCH 08/31] Making fromList total. --- src/Data/Map.idr | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 9da5e10..d18770d 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1258,7 +1258,7 @@ mapAccum f a m = mapAccumWithKey (\a', _, x' => f a' x') a m ||| for the key is retained. ||| If the keys of the list are ordered, a linear-time implementation is used. O(n * log(n)) public export -partial +total fromList : Eq (Map k v) => Eq v => Ord k => List (k,v) -> Map k v fromList [] = Tip fromList [(kx, x)] = Bin 1 kx x Tip Tip @@ -1289,7 +1289,7 @@ fromList ((kx0, x0) :: xs0) = False => (Bin 1 kx x Tip Tip, xss, []) False => - case create (the Nat (cast (the Int (cast k) `shiftR` 1))) xs of + case assert_total (create (the Nat (cast (the Int (cast k) `shiftR` 1))) xs) of res@(_, [], _) => res (l, [(ky, y)], zs) => (insertMax ky y l, [], zs) (l, ys@((ky, y) :: yss), _) => @@ -1297,7 +1297,7 @@ fromList ((kx0, x0) :: xs0) = True => (l, [], ys) False => - let (r, zs, ws) = create (the Nat (cast (the Int (cast k) `shiftR` 1))) yss + let (r, zs, ws) = assert_total (create (the Nat (cast (the Int (cast k) `shiftR` 1))) yss) in (link ky y l r, zs, ws) go : Nat -> Map k v -> List (k,v) -> Map k v go _ t [] = t @@ -1308,8 +1308,8 @@ fromList ((kx0, x0) :: xs0) = True => fromList' l xs False => - case create k xss of - (r, ys, []) => go (the Nat (cast (the Int (cast k) `shiftL` 1))) (link kx x l r) ys + case assert_total (create k xss) of + (r, ys, []) => assert_total (go (the Nat (cast (the Int (cast k) `shiftL` 1))) (link kx x l r) ys) (r, _, ys) => fromList' (link kx x l r) ys ||| Convert the map to a list of key/value pairs where the keys are in descending order. O(n) From a282eb82920ae755daa6505392a3e6118ae560d8 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 10 Sep 2024 17:54:00 -0400 Subject: [PATCH 09/31] Fixing export modifiers and adding custom show implementations. --- src/Data/Map.idr | 205 +++++++++++++++++++++++++---------------------- 1 file changed, 110 insertions(+), 95 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index d18770d..a16d0b7 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -16,7 +16,7 @@ import Data.List -------------------------------------------------------------------------------- ||| The empty map. (O)1 -public export +export empty : Map k a empty = Tip @@ -25,25 +25,25 @@ empty = Tip -------------------------------------------------------------------------------- ||| Fold the values in the map using the given left-associative binary operator. O(n) -public export +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) -public export +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) -public export +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) -public export +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 @@ -55,7 +55,7 @@ foldrWithKey f z (Bin _ kx x l r) = foldrWithKey f (f kx x (foldrWithKey f z r)) ||| 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) -public export +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 @@ -109,7 +109,7 @@ insertR kx0 = go kx0 kx0 ||| 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) -public export +export insertWith : Ord k => (v -> v -> v) -> k -> v -> Map k v -> Map k v insertWith = go where @@ -154,7 +154,7 @@ insertWithKeyR = go ||| 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) -public export +export insertWithKey : Ord k => (k -> v -> v -> v) -> k -> v -> Map k v -> Map k v insertWithKey = go where @@ -170,7 +170,7 @@ insertWithKey = go ||| 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) -public export +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 @@ -192,7 +192,7 @@ insertLookupWithKey f0 k0 x0 = go f0 k0 x0 ||| 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) -public export +export delete : Eq (Map k v) => Eq k => Ord k => k -> Map k v -> Map k v delete = go where @@ -217,7 +217,7 @@ delete = go ||| 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) -public export +export adjustWithKey : Ord k => (k -> v -> v) -> k -> Map k v -> Map k v adjustWithKey = go where @@ -234,7 +234,7 @@ adjustWithKey = go ||| 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) -public export +export adjust : Ord k => (v -> v) -> k -> Map k v -> Map k v adjust f = adjustWithKey (\_, x => f x) @@ -242,7 +242,7 @@ adjust f = adjustWithKey (\_, x => f x) ||| 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) -public export +export updateWithKey : Ord k => (k -> v -> Maybe v) -> k -> Map k v -> Map k v updateWithKey = go where @@ -264,14 +264,14 @@ updateWithKey = go ||| 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) -public export +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) -public export +export updateLookupWithKey : Ord k => (k -> v -> Maybe v) -> k -> Map k v -> (Maybe v,Map k v) updateLookupWithKey f0 k0 = go f0 k0 where @@ -297,7 +297,7 @@ updateLookupWithKey f0 k0 = go f0 k0 ||| 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) -public export +export alter : Ord k => (Maybe v -> Maybe v) -> k -> Map k v -> Map k v alter = go where @@ -324,7 +324,7 @@ alter = go ||| 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) -public export +export lookup : Ord k => k -> Map k v -> Maybe v lookup = go where @@ -339,12 +339,12 @@ lookup = go ||| Find the value at a key. ||| Returns Nothing when the element can not be found. O(log n) -public export +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) -public export +export member : Ord k => k -> Map k v -> Bool member _ Tip = False member k (Bin _ kx _ l r) = @@ -354,13 +354,13 @@ member k (Bin _ kx _ l r) = EQ => True ||| Is the key not a member of the map? See also member. O(log n) -public export +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) -public export +export 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) = @@ -371,14 +371,14 @@ find k (Bin _ kx x l r) = ||| Find the value at a key. ||| Calls idris_crash when the element can not be found. O(log n) -public export +export (!!) : 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) -public export +export findWithDefault : Ord k => v -> k -> Map k v -> v findWithDefault def _ Tip = def findWithDefault def k (Bin _ kx x l r) = @@ -389,7 +389,7 @@ findWithDefault def k (Bin _ kx x l r) = ||| Find largest key smaller than the given one and return the ||| corresponding (key, value) pair. O(log n) -public export +export lookupLT : Ord k => k -> Map k v -> Maybe (k,v) lookupLT = goNothing where @@ -408,7 +408,7 @@ lookupLT = goNothing ||| Find smallest key greater than the given one and return the ||| corresponding (key, value) pair. O(log n) -public export +export lookupGT : Ord k => k -> Map k v -> Maybe (k,v) lookupGT = goNothing where @@ -427,7 +427,7 @@ lookupGT = goNothing ||| Find largest key smaller or equal to the given one and return ||| the corresponding (key, value) pair. O(log n) -public export +export lookupLE : Ord k => k -> Map k v -> Maybe (k,v) lookupLE = goNothing where @@ -448,7 +448,7 @@ lookupLE = goNothing ||| Find smallest key greater or equal to the given one and return ||| the corresponding (key, value) pair. O(log n) -public export +export lookupGE : Ord k => k -> Map k v -> Maybe (k,v) lookupGE = goNothing where @@ -472,7 +472,7 @@ lookupGE = goNothing -------------------------------------------------------------------------------- ||| Is the map empty? O(1) -public export +export null : Map k v -> Bool null Tip = True null _ = False @@ -499,7 +499,7 @@ splitMember k0 m = go k0 m ||| 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) -public export +export splitRoot : Map k v -> List (Map k v) splitRoot orig = case orig of @@ -510,7 +510,7 @@ splitRoot orig = ||| The expression (splitLookup k map) splits a map just ||| like split but also returns lookup k map. O(log n) -public export +export splitLookup : Ord k => k -> Map k v -> (Map k v,Maybe v,Map k v) splitLookup k0 m = go k0 m where @@ -530,7 +530,7 @@ splitLookup k0 m = go k0 m ||| 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) -public export +export split : Ord k => k -> Map k v -> (Map k v,Map k v) split k0 t0 = go k0 t0 where @@ -548,7 +548,7 @@ split k0 t0 = go k0 t0 EQ => (l,r) ||| Filter all keys/values that satisfy the predicate. O(n) -public export +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) = @@ -563,14 +563,14 @@ filterWithKey p t@(Bin _ kx x l r) = link2 (filterWithKey p l) (filterWithKey p r) ||| Filter all values that satisfy the predicate. O(n) -public export +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) -public export +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 @@ -598,7 +598,7 @@ partitionWithKey p0 t0 = go p0 t0 ||| 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) -public export +export takeWhileAntitone : (k -> Bool) -> Map k v -> Map k v takeWhileAntitone _ Tip = Tip takeWhileAntitone p (Bin _ kx x l r) = @@ -611,7 +611,7 @@ takeWhileAntitone p (Bin _ kx x l r) = ||| 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) -public export +export dropWhileAntitone : (k -> Bool) -> Map k v -> Map k v dropWhileAntitone _ Tip = Tip dropWhileAntitone p (Bin _ kx x l r) = @@ -624,7 +624,7 @@ dropWhileAntitone p (Bin _ kx x 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) -public export +export spanAntitone : (k -> Bool) -> Map k v -> (Map k v, Map k v) spanAntitone p0 m = go p0 m where @@ -640,7 +640,7 @@ spanAntitone p0 m = go p0 m in (u,link kx x v r) ||| Map keys/values and collect the Just results. O(n) -public export +export mapMaybeWithKey : (k -> a -> Maybe b) -> Map k a -> Map k b mapMaybeWithKey _ Tip = Tip mapMaybeWithKey f (Bin _ kx x l r) = @@ -651,12 +651,12 @@ mapMaybeWithKey f (Bin _ kx x l r) = link2 (mapMaybeWithKey f l) (mapMaybeWithKey f r) ||| Map values and collect the Just results. O(n) -public export +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) -public export +export mapEitherWithKey : (k -> a -> Either b c) -> Map k a -> (Map k b, Map k c) mapEitherWithKey f0 t0 = go f0 t0 where @@ -668,7 +668,7 @@ mapEitherWithKey f0 t0 = go f0 t0 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) -public export +export mapEither : (a -> Either b c) -> Map k a -> (Map k b, Map k c) mapEither f m = mapEitherWithKey (\_, x => f x) m @@ -699,12 +699,12 @@ submap' f (Bin _ kx x l r) t = ||| 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. -public export +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 (==)). -public export +export isSubmapOf : Eq v => Ord k => Map k v -> Map k v -> Bool isSubmapOf m1 m2 = isSubmapOfBy (==) m1 m2 @@ -713,13 +713,13 @@ isSubmapOf m1 m2 = isSubmapOfBy (==) m1 m2 ||| 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. -public export +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 (==)). -public export +export isProperSubmapOf : Eq v => Ord k => Map k v -> Map k v -> Bool isProperSubmapOf m1 m2 = isProperSubmapOfBy (==) m1 m2 @@ -730,7 +730,7 @@ isProperSubmapOf m1 m2 = isProperSubmapOfBy (==) m1 m2 ||| 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) -public export +export lookupIndex : Ord k => k -> Map k v -> Maybe Nat lookupIndex = go 0 where @@ -749,7 +749,7 @@ lookupIndex = go 0 ||| 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) -public export +export findIndex : Ord k => k -> Map k v -> Nat findIndex = go 0 where @@ -767,7 +767,7 @@ findIndex = go 0 ||| 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) -public export +export 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) = @@ -782,7 +782,7 @@ elemAt i (Bin _ kx x l r) = ||| 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) -public export +export updateAt : (k -> v -> Maybe v) -> Nat -> Map k v -> Map k v updateAt f i t = case t of @@ -803,7 +803,7 @@ updateAt f i t = ||| 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) -public export +export deleteAt : Nat -> Map k v -> Map k v deleteAt i t = case t of @@ -819,7 +819,7 @@ deleteAt i t = ||| Take a given number of entries in key order, beginning ||| with the smallest keys. O(log n) -public export +export take : Nat -> Map k v -> Map k v take i m = case i >= size m of @@ -845,7 +845,7 @@ take i m = ||| Drop a given number of entries in key order, beginning ||| with the smallest keys. O(log n) -public export +export drop : Nat -> Map k v -> Map k v drop i m = case i >= size m of @@ -870,7 +870,7 @@ drop i m = insertMin kx x r ||| Split a map at a particular index. O(log n) -public export +export splitAt : Nat -> Map k v -> (Map k v, Map k v) splitAt i m = case i >= size m of @@ -907,7 +907,7 @@ 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) -public export +export lookupMin : Map k v -> Maybe (k,v) lookupMin Tip = Nothing lookupMin (Bin _ k v l _) = Just $ lookupMinSure k v l @@ -917,13 +917,13 @@ 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) -public export +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) -public export +export findMin : Map k v -> (k,v) findMin t = case lookupMin t of @@ -931,7 +931,7 @@ findMin t = 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) -public export +export findMax : Map k v -> (k,v) findMax t = case lookupMax t of @@ -939,14 +939,14 @@ findMax t = 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) -public export +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) -public export +export deleteMax : Map k v -> Map k v deleteMax Tip = Tip deleteMax (Bin _ _ _ l Tip) = l @@ -954,7 +954,7 @@ 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) -public export +export minViewWithKey : Map k v -> Maybe ((k,v),Map k v) minViewWithKey Tip = Nothing minViewWithKey (Bin _ k x l r) = @@ -964,7 +964,7 @@ minViewWithKey (Bin _ k x l r) = ((km,xm),t) ||| Delete and find the minimal element. O(log n) -public export +export deleteFindMin : Map k v -> ((k,v),Map k v) deleteFindMin t = case minViewWithKey t of @@ -973,7 +973,7 @@ deleteFindMin t = ||| 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) -public export +export maxViewWithKey : Map k v -> Maybe ((k,v),Map k v) maxViewWithKey Tip = Nothing maxViewWithKey (Bin _ k x l r) = @@ -983,7 +983,7 @@ maxViewWithKey (Bin _ k x l r) = ((km,xm),t) ||| Delete and find the maximal element. O(log n) -public export +export deleteFindMax : Map k v -> ((k,v),Map k v) deleteFindMax t = case maxViewWithKey t of @@ -991,7 +991,7 @@ deleteFindMax t = 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) -public export +export updateMinWithKey : (k -> v -> Maybe v) -> Map k v -> Map k v updateMinWithKey _ Tip = Tip updateMinWithKey f (Bin sx kx x Tip r) = @@ -1002,12 +1002,12 @@ updateMinWithKey f (Bin _ kx x l r) = balanceR kx x (updateMinWithKey f l) r ||| Update the value at the minimal key. O(log n) -public export +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) -public export +export updateMaxWithKey : (k -> v -> Maybe v) -> Map k v -> Map k v updateMaxWithKey _ Tip = Tip updateMaxWithKey f (Bin sx kx x l Tip) = @@ -1018,13 +1018,13 @@ updateMaxWithKey f (Bin _ kx x l r) = balanceL kx x l (updateMaxWithKey f r) ||| Update the value at the maximal key. O(log n) -public export +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) -public export +export minView : Map k v -> Maybe (v,Map k v) minView t = case minViewWithKey t of @@ -1033,7 +1033,7 @@ minView 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) -public export +export maxView : Map k v -> Maybe (v,Map k v) maxView t = case maxViewWithKey t of @@ -1046,7 +1046,7 @@ maxView t = ||| The expression (union t1 t2) takes the left-biased union of t1 and t2. ||| It prefers t1 when duplicate keys are encountered. -public export +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 @@ -1062,7 +1062,7 @@ union t1@(Bin _ k1 x1 l1 r1) t2 = link k1 x1 (union l1 l2) (union r1 r2) ||| Union with a combining function. -public export +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 @@ -1076,7 +1076,7 @@ unionWith f (Bin _ k1 x1 l1 r1) t2 = Just x2 => link k1 (f x1 x2) (unionWith f l1 l2) (unionWith f r1 r2) ||| Union with a combining function. -public export +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 @@ -1090,12 +1090,12 @@ unionWithKey f (Bin _ k1 x1 l1 r1) t2 = Just x2 => link k1 (f k1 x1 x2) (unionWithKey f l1 l2) (unionWithKey f r1 r2) ||| The union of a list of maps. -public export +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. -public export +export unionsWith : Foldable f => Ord k => (v -> v -> v) -> f (Map k v) -> Map k v unionsWith f ts = foldl (unionWith f) empty ts @@ -1105,7 +1105,7 @@ unionsWith f ts = foldl (unionWith f) empty ts ||| Difference of two maps. ||| Return elements of the first map not existing in the second map. -public export +export difference : Ord k => Map k a -> Map k b -> Map k a difference Tip _ = Tip difference t1 Tip = t1 @@ -1119,7 +1119,7 @@ difference t1 (Bin _ k _ l2 r2) = link2 (difference l1 l2) (difference r1 r2) ||| Same as difference. -public export +export (\\) : Ord k => Map k a -> Map k b -> Map k a m1 \\ m2 = difference m1 m2 @@ -1129,7 +1129,7 @@ m1 \\ m2 = difference m1 m2 ||| Intersection of two maps. ||| Return data in the first map for the keys existing in both maps. -public export +export intersection : Eq (Map k a) => Ord k => Map k a -> Map k b -> Map k a intersection Tip _ = Tip intersection _ Tip = Tip @@ -1145,7 +1145,7 @@ intersection t1@(Bin _ k x l1 r1) t2 = link2 (intersection l1 l2) (intersection r1 r2) ||| Intersection with a combining function. -public export +export intersectionWith : Ord k => (a -> b -> c) -> Map k a -> Map k b -> Map k c intersectionWith f Tip _ = Tip intersectionWith f _ Tip = Tip @@ -1157,7 +1157,7 @@ intersectionWith f (Bin _ k x1 l1 r1) t2 = link2 (intersectionWith f l1 l2) (intersectionWith f r1 r2) ||| Intersection with a combining function. -public export +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 @@ -1174,7 +1174,7 @@ intersectionWithKey f (Bin _ k x1 l1 r1) t2 = ||| Check whether the key sets of two ||| maps are disjoint (i.e., their intersection is empty). -public export +export disjoint : Ord k => Map k a -> Map k b -> Bool disjoint Tip _ = True disjoint _ Tip = True @@ -1190,7 +1190,7 @@ disjoint (Bin _ k _ l r) t = ||| 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. -public export +export compose : Ord b => Map b c -> Map a b -> Map a c compose bc ab = case null bc of @@ -1204,20 +1204,20 @@ compose bc ab = -------------------------------------------------------------------------------- ||| Map a function over all values in the map. O(n) -public export +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) -public export +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) -public export +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) = @@ -1228,7 +1228,7 @@ mapAccumL f a (Bin sx kx x l r) = ||| The function mapAccumRWithKey threads an accumulating ||| argument through the map in descending order of keys. O(n) -public export +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) = @@ -1239,13 +1239,13 @@ mapAccumRWithKey f a (Bin sx kx x l r) = ||| The function mapAccumWithKey threads an accumulating ||| argument through the map in ascending order of keys. O(n) -public export +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) -public export +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 @@ -1257,7 +1257,7 @@ mapAccum f a m = mapAccumWithKey (\a', _, x' => f a' x') a m ||| 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)) -public export +export total fromList : Eq (Map k v) => Eq v => Ord k => List (k,v) -> Map k v fromList [] = Tip @@ -1313,19 +1313,19 @@ fromList ((kx0, x0) :: xs0) = (r, _, ys) => fromList' (link kx x l r) ys ||| Convert the map to a list of key/value pairs where the keys are in descending order. O(n) -public export +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) -public export +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. -public export +export toList : Map k v -> List (k,v) toList = toAscList @@ -1334,7 +1334,7 @@ toList = toAscList -------------------------------------------------------------------------------- ||| Gets the keys of the map. -public export +export keys : Map k v -> List k keys = map fst . toList @@ -1344,7 +1344,7 @@ keys = map fst . toList ||| Gets the values of the map. ||| Could contain duplicates. -public export +export values : Map k v -> List v values = map snd . toList @@ -1352,12 +1352,27 @@ values = map snd . toList -- Interfaces -------------------------------------------------------------------------------- -public export +export Functor (Map k) where map f m = map f m -public export +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 = show . toList From dfa0eaadcb93af1f966457befab360e80bcdb145 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 13 Sep 2024 15:34:44 -0400 Subject: [PATCH 10/31] Adding terminating (via structural recursion) version of fromList, and fixing size function. --- src/Data/Map.idr | 127 ++++++++++++++++++++------------------ src/Data/Map/Internal.idr | 36 ++++++----- 2 files changed, 88 insertions(+), 75 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index a16d0b7..3520342 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -17,7 +17,7 @@ import Data.List ||| The empty map. (O)1 export -empty : Map k a +empty : Map k v empty = Tip -------------------------------------------------------------------------------- @@ -1253,65 +1253,6 @@ mapAccum f a m = mapAccumWithKey (\a', _, x' => f a' x') a m -- Lists -------------------------------------------------------------------------------- -||| Build a map from a list of key/value pairs. See also fromAscList. -||| 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 -total -fromList : Eq (Map k v) => Eq v => Ord k => List (k,v) -> Map k v -fromList [] = Tip -fromList [(kx, x)] = Bin 1 kx x Tip Tip -fromList ((kx0, x0) :: xs0) = - case not_ordered kx0 xs0 of - True => - fromList' (Bin 1 kx0 x0 Tip Tip) xs0 - False => - go 1 (Bin 1 kx0 x0 Tip Tip) xs0 - where - not_ordered : k -> List (k,v) -> Bool - not_ordered _ [] = False - not_ordered kx ((ky,_) :: _) = kx >= ky - fromList' : Map k v -> List (k,v) -> Map k v - fromList' t0 xs = foldl ins t0 xs - where - ins : Map k v -> (k,v) -> Map k v - ins t (k,x) = insert k x t - create : Nat -> List (k,v) -> (Map k v,List (k,v),List (k,v)) - create _ [] = (Tip, [], []) - create Z _ = (Tip, [], []) - create (S k) xs@((kx, x) :: xss) = - case k == 1 of - True => - case not_ordered kx xss of - True => - (Bin 1 kx x Tip Tip, [], xss) - False => - (Bin 1 kx x Tip Tip, xss, []) - False => - case assert_total (create (the Nat (cast (the Int (cast k) `shiftR` 1))) xs) of - res@(_, [], _) => res - (l, [(ky, y)], zs) => (insertMax ky y l, [], zs) - (l, ys@((ky, y) :: yss), _) => - case not_ordered ky yss of - True => - (l, [], ys) - False => - let (r, zs, ws) = assert_total (create (the Nat (cast (the Int (cast k) `shiftR` 1))) yss) - in (link ky y l r, zs, ws) - go : Nat -> Map k v -> List (k,v) -> Map k v - go _ t [] = t - go Z t _ = t - go _ t [(kx, x)] = insertMax kx x t - go (S k) l xs@((kx, x) :: xss) = - case not_ordered kx xss of - True => - fromList' l xs - False => - case assert_total (create k xss) of - (r, ys, []) => assert_total (go (the Nat (cast (the Int (cast k) `shiftL` 1))) (link kx x l r) ys) - (r, _, ys) => fromList' (link kx x l r) ys - ||| 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) @@ -1329,6 +1270,72 @@ export toList : Map k v -> List (k,v) toList = toAscList +||| Build a map from a list of key/value pairs. See also fromAscList. +||| 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 +total +fromList : Eq (Map k v) => Ord k => Eq v => List (k, v) -> Map k v +fromList [] = Tip +fromList [(kx, x)] = Bin 1 kx x Tip Tip +fromList ((kx0, x0) :: xs0) = + if not_ordered kx0 xs0 then + fromList' (Bin 1 kx0 x0 Tip Tip) xs0 + else + go (Bin 1 kx0 x0 Tip Tip) xs0 + where + -- Helper function to calculate the size of a tree + sizeTree : Map k v -> Nat + sizeTree Tip = 0 + sizeTree (Bin sz _ _ _ _) = sz + -- Rotate the tree to the right to balance + rotateRight : Map k v -> Map k v + rotateRight (Bin _ kx x (Bin _ kl xl lll llr) right) = + Bin (sizeTree lll + sizeTree llr + sizeTree right + 2) kl xl lll (Bin (sizeTree llr + sizeTree right + 1) kx x llr right) + rotateRight t = t + -- Rotate the tree to the left to balance + rotateLeft : Map k v -> Map k v + rotateLeft (Bin _ kx x left (Bin _ kr xr rll rlr)) = + Bin (sizeTree left + sizeTree rll + sizeTree rlr + 2) kr xr (Bin (sizeTree left + sizeTree rll + 1) kx x left rll) rlr + rotateLeft t = t + -- Balance the tree based on its size + balanceTree : Map k v -> Map k v + balanceTree Tip = Tip + balanceTree t@(Bin sz k v left right) = + let diff = minus (sizeTree left) (sizeTree right) in + if diff > 1 then + rotateRight t + else if diff < -1 then + rotateLeft t + else + t + -- Check if the keys are not ordered + not_ordered : k -> List (k,v) -> Bool + not_ordered _ [] = False + not_ordered kx ((ky, _) :: _) = kx >= ky + -- Insert elements into the map using 'insert', avoiding sequential insertions + fromList' : Map k v -> List (k, v) -> Map k v + fromList' t0 xs = foldl (\t, (k, x) => balanceTree (insert k x t)) t0 xs + -- Create function with rebalancing to prevent skewed trees + create : Map k v -> List (k, v) -> Map k v + create acc [] = acc + create acc ((kx, x) :: xs) = + if not_ordered kx xs then + fromList' (insert kx x acc) xs + else + create (balanceTree (insert kx x acc)) xs + -- Recursive function using structural recursion on the input list + go : Map k v -> List (k,v) -> Map k v + go acc [] = acc + go acc [(kx, x)] = insertMax kx x acc + go acc ((kx, x) :: xs) = + if not_ordered kx xs then + fromList' acc ((kx, x) :: xs) + else + let newAcc = balanceTree (insert kx x acc) in + go newAcc xs + -------------------------------------------------------------------------------- -- Keys -------------------------------------------------------------------------------- diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr index 459254b..29fa52a 100644 --- a/src/Data/Map/Internal.idr +++ b/src/Data/Map/Internal.idr @@ -38,7 +38,7 @@ data MaxView k a = MaxView' k a (Map k a) -------------------------------------------------------------------------------- ||| Wrap a single value in a map -public export +export singleton : k -> a -> Map k a singleton k x = Bin 1 k x Tip Tip @@ -47,11 +47,17 @@ singleton k x = Bin 1 k x Tip Tip -------------------------------------------------------------------------------- ||| The number of elements in the map. O(1) -public export +export +size : Map k v -> Nat +size Tip = 0 +size (Bin _ _ _ l r) = 1 + size l + size r +{- +export size : Map k v -> Nat -size Tip = 0 -size (Bin Z _ _ _ _) = 0 -size (Bin (S n) _ _ _ _) = n +size Tip = 0 +size (Bin Z _ _ _ _) = 0 +size (Bin (S n) kx x l r) = n + 1 +-} -------------------------------------------------------------------------------- -- Map Internals @@ -101,7 +107,7 @@ 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. -public export +export balance : k -> v -> Map k v -> Map k v -> Map k v balance k x l r = case l of @@ -167,7 +173,7 @@ balance 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. -public export +export balanceL : k -> v -> Map k v -> Map k v -> Map k v balanceL k x l r = case r of @@ -209,7 +215,7 @@ balanceL 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. -public export +export balanceR : k -> v -> Map k v -> Map k v -> Map k v balanceR k x l r = case l of @@ -248,7 +254,7 @@ balanceR k x l r = False => Bin (1+ls+rs) k x l r -public export +export insertMax : k -> v -> Map k v -> Map k v insertMax kx x t = case t of @@ -257,7 +263,7 @@ insertMax kx x t = Bin _ ky y l r => balanceR ky y l (insertMax kx x r) -public export +export insertMin : k -> v -> Map k v -> Map k v insertMin kx x t = case t of @@ -266,14 +272,14 @@ insertMin kx x t = Bin _ ky y l r => balanceL ky y (insertMin kx x l) r -public export +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) -public export +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) = @@ -281,7 +287,7 @@ maxViewSure k x l (Bin _ kr xr rl rr) = 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). -public export +export glue : Map k v -> Map k v -> Map k v glue Tip r = r glue l Tip = l @@ -295,7 +301,7 @@ glue l@(Bin sl kl xl ll lr) r@(Bin sr kr xr rl rr) = in balanceL km m l r' ||| Utility function that maintains the balance properties of the tree. -public export +export link2 : Map k v -> Map k v -> Map k v link2 Tip r = r link2 l Tip = l @@ -311,7 +317,7 @@ link2 l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry) = glue l r ||| Utility function that maintains the balance properties of the tree. -public export +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 From 75ccfafb9aa5399c6fbe9372af1c2a0f1775b2ad Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 13 Sep 2024 15:43:44 -0400 Subject: [PATCH 11/31] Cleaning up fromList function. --- src/Data/Map.idr | 81 ++++++++++++++++++++++++++++-------------------- 1 file changed, 47 insertions(+), 34 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 3520342..63d7535 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1275,66 +1275,79 @@ toList = toAscList ||| for the key is retained. ||| If the keys of the list are ordered, a linear-time implementation is used. O(n * log(n)) export -total fromList : Eq (Map k v) => Ord k => Eq v => List (k, v) -> Map k v -fromList [] = Tip -fromList [(kx, x)] = Bin 1 kx x Tip Tip +fromList [] = Tip +fromList [(kx, x)] = Bin 1 kx x Tip Tip fromList ((kx0, x0) :: xs0) = - if not_ordered kx0 xs0 then - fromList' (Bin 1 kx0 x0 Tip Tip) xs0 - else - go (Bin 1 kx0 x0 Tip Tip) xs0 + case not_ordered kx0 xs0 of + True => + fromList' (Bin 1 kx0 x0 Tip Tip) xs0 + False => + go (Bin 1 kx0 x0 Tip Tip) xs0 where -- Helper function to calculate the size of a tree sizeTree : Map k v -> Nat - sizeTree Tip = 0 + sizeTree Tip = 0 sizeTree (Bin sz _ _ _ _) = sz -- Rotate the tree to the right to balance rotateRight : Map k v -> Map k v rotateRight (Bin _ kx x (Bin _ kl xl lll llr) right) = - Bin (sizeTree lll + sizeTree llr + sizeTree right + 2) kl xl lll (Bin (sizeTree llr + sizeTree right + 1) kx x llr right) - rotateRight t = t + Bin (sizeTree lll + sizeTree llr + sizeTree right + 2) + kl + xl + lll + (Bin (sizeTree llr + sizeTree right + 1) kx x llr right) + rotateRight t = t -- Rotate the tree to the left to balance rotateLeft : Map k v -> Map k v rotateLeft (Bin _ kx x left (Bin _ kr xr rll rlr)) = - Bin (sizeTree left + sizeTree rll + sizeTree rlr + 2) kr xr (Bin (sizeTree left + sizeTree rll + 1) kx x left rll) rlr - rotateLeft t = t + Bin (sizeTree left + sizeTree rll + sizeTree rlr + 2) + kr + xr + (Bin (sizeTree left + sizeTree rll + 1) kx x left rll) + rlr + rotateLeft t = t -- Balance the tree based on its size balanceTree : Map k v -> Map k v - balanceTree Tip = Tip + balanceTree Tip = Tip balanceTree t@(Bin sz k v left right) = - let diff = minus (sizeTree left) (sizeTree right) in - if diff > 1 then - rotateRight t - else if diff < -1 then - rotateLeft t - else - t + let diff = minus (sizeTree left) (sizeTree right) + in case diff > 1 of + True => + rotateRight t + False => + case diff < -1 of + True => + rotateLeft t + False => + t -- Check if the keys are not ordered not_ordered : k -> List (k,v) -> Bool - not_ordered _ [] = False + not_ordered _ [] = False not_ordered kx ((ky, _) :: _) = kx >= ky -- Insert elements into the map using 'insert', avoiding sequential insertions fromList' : Map k v -> List (k, v) -> Map k v fromList' t0 xs = foldl (\t, (k, x) => balanceTree (insert k x t)) t0 xs -- Create function with rebalancing to prevent skewed trees create : Map k v -> List (k, v) -> Map k v - create acc [] = acc + create acc [] = acc create acc ((kx, x) :: xs) = - if not_ordered kx xs then - fromList' (insert kx x acc) xs - else - create (balanceTree (insert kx x acc)) xs + case not_ordered kx xs of + True => + fromList' (insert kx x acc) xs + False => + create (balanceTree (insert kx x acc)) xs -- Recursive function using structural recursion on the input list go : Map k v -> List (k,v) -> Map k v - go acc [] = acc - go acc [(kx, x)] = insertMax kx x acc - go acc ((kx, x) :: xs) = - if not_ordered kx xs then - fromList' acc ((kx, x) :: xs) - else - let newAcc = balanceTree (insert kx x acc) in - go newAcc xs + go acc [] = acc + go acc [(kx, x)] = insertMax kx x acc + go acc l@((kx, x) :: xs) = + case not_ordered kx xs of + True => + fromList' acc l + False => + let newAcc = balanceTree (insert kx x acc) + in go newAcc xs -------------------------------------------------------------------------------- -- Keys From 6f15af02afa00e23cb1c4e19769168c3ea3bb788 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 13 Sep 2024 15:45:50 -0400 Subject: [PATCH 12/31] Removing unnecessary code for size function. --- src/Data/Map/Internal.idr | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr index 29fa52a..a98cefd 100644 --- a/src/Data/Map/Internal.idr +++ b/src/Data/Map/Internal.idr @@ -50,14 +50,7 @@ singleton k x = Bin 1 k x Tip Tip export size : Map k v -> Nat size Tip = 0 -size (Bin _ _ _ l r) = 1 + size l + size r -{- -export -size : Map k v -> Nat -size Tip = 0 -size (Bin Z _ _ _ _) = 0 -size (Bin (S n) kx x l r) = n + 1 --} +size (Bin _ _ _ l r) = 1 + size l + size r -------------------------------------------------------------------------------- -- Map Internals From 3b321f565da95c1e7fa238ecd494463fdbe5e6e6 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 14 Sep 2024 09:04:03 -0400 Subject: [PATCH 13/31] Adding more performant fromList implementation. --- src/Data/Map.idr | 111 +++++++++++++++++------------------------------ 1 file changed, 39 insertions(+), 72 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 63d7535..a800790 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -5,6 +5,7 @@ import public Data.Map.Internal import Data.Bits import Data.List +import Data.List1 %hide Prelude.null %hide Prelude.toList @@ -1270,84 +1271,50 @@ export toList : Map k v -> List (k,v) toList = toAscList -||| Build a map from a list of key/value pairs. See also fromAscList. +||| 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 -fromList : Eq (Map k v) => Ord k => Eq v => List (k, v) -> Map k v -fromList [] = Tip -fromList [(kx, x)] = Bin 1 kx x Tip Tip -fromList ((kx0, x0) :: xs0) = - case not_ordered kx0 xs0 of - True => - fromList' (Bin 1 kx0 x0 Tip Tip) xs0 - False => - go (Bin 1 kx0 x0 Tip Tip) xs0 +fromList : Ord (k, v) => Ord k => List (k, v) -> Map k v +fromList [] = Tip +fromList xs = buildBalancedTree (convertToList1 (sort xs)) where - -- Helper function to calculate the size of a tree + -- Calculate the size of a tree sizeTree : Map k v -> Nat - sizeTree Tip = 0 + sizeTree Tip = 0 sizeTree (Bin sz _ _ _ _) = sz - -- Rotate the tree to the right to balance - rotateRight : Map k v -> Map k v - rotateRight (Bin _ kx x (Bin _ kl xl lll llr) right) = - Bin (sizeTree lll + sizeTree llr + sizeTree right + 2) - kl - xl - lll - (Bin (sizeTree llr + sizeTree right + 1) kx x llr right) - rotateRight t = t - -- Rotate the tree to the left to balance - rotateLeft : Map k v -> Map k v - rotateLeft (Bin _ kx x left (Bin _ kr xr rll rlr)) = - Bin (sizeTree left + sizeTree rll + sizeTree rlr + 2) - kr - xr - (Bin (sizeTree left + sizeTree rll + 1) kx x left rll) - rlr - rotateLeft t = t - -- Balance the tree based on its size - balanceTree : Map k v -> Map k v - balanceTree Tip = Tip - balanceTree t@(Bin sz k v left right) = - let diff = minus (sizeTree left) (sizeTree right) - in case diff > 1 of - True => - rotateRight t - False => - case diff < -1 of - True => - rotateLeft t - False => - t - -- Check if the keys are not ordered - not_ordered : k -> List (k,v) -> Bool - not_ordered _ [] = False - not_ordered kx ((ky, _) :: _) = kx >= ky - -- Insert elements into the map using 'insert', avoiding sequential insertions - fromList' : Map k v -> List (k, v) -> Map k v - fromList' t0 xs = foldl (\t, (k, x) => balanceTree (insert k x t)) t0 xs - -- Create function with rebalancing to prevent skewed trees - create : Map k v -> List (k, v) -> Map k v - create acc [] = acc - create acc ((kx, x) :: xs) = - case not_ordered kx xs of - True => - fromList' (insert kx x acc) xs - False => - create (balanceTree (insert kx x acc)) xs - -- Recursive function using structural recursion on the input list - go : Map k v -> List (k,v) -> Map k v - go acc [] = acc - go acc [(kx, x)] = insertMax kx x acc - go acc l@((kx, x) :: xs) = - case not_ordered kx xs of - True => - fromList' acc l - False => - let newAcc = balanceTree (insert kx x acc) - in go newAcc xs + -- 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 -> Map k v + linkRootWithSubtrees (kx, x) left right = + let newSize = sizeTree left + sizeTree right + 1 + in Bin newSize kx x left right + -- Split a non-empty list into left, middle, and right parts + splitList : List1 (k, v) -> (List (k, v), (k, v), List (k, v)) + splitList l@(x ::: xs) = + let len = length l + 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) + -- Build a balanced tree from a non-empty list + buildBalancedTree : List1 (k, v) -> Map k v + buildBalancedTree ((kx, x) ::: []) = Bin 1 kx x Tip Tip + buildBalancedTree l@(x ::: xs) = + let (left, root, right) = splitList l + leftTree = case left of + [] => Tip + _ => assert_total $ buildBalancedTree (convertToList1 left) + rightTree = case right of + [] => Tip + _ => assert_total $ buildBalancedTree (convertToList1 right) + in linkRootWithSubtrees root leftTree rightTree -------------------------------------------------------------------------------- -- Keys @@ -1384,7 +1351,7 @@ Foldable (Map k) where private Show k => Show v => Show (List (k, v)) where - show xs = "[" ++ show' xs ++ "]" + show xs = "fromList " ++ "[" ++ show' xs ++ "]" where show'' : (k, v) -> String show'' (k, v) = "(" ++ show k ++ ", " ++ show v ++ ")" From 85f5a5391939ac6ebf0e72f68943b1908e64fb8b Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 14 Sep 2024 09:36:30 -0400 Subject: [PATCH 14/31] Further optimizing fromList implementation. --- src/Data/Map.idr | 49 +++++++++++++++++++++++++++--------------------- 1 file changed, 28 insertions(+), 21 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index a800790..a027893 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1275,11 +1275,14 @@ toList = toAscList ||| 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 fromList : Ord (k, v) => Ord k => List (k, v) -> Map k v fromList [] = Tip -fromList xs = buildBalancedTree (convertToList1 (sort xs)) +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 @@ -1290,31 +1293,35 @@ fromList xs = buildBalancedTree (convertToList1 (sort xs)) 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 -> Map k v - linkRootWithSubtrees (kx, x) left right = - let newSize = sizeTree left + sizeTree right + 1 - in Bin newSize kx x left right + 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) -> (List (k, v), (k, v), List (k, v)) - splitList l@(x ::: xs) = - let len = length l - half = len `div` 2 + 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) + [] => + 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) -> Map k v - buildBalancedTree ((kx, x) ::: []) = Bin 1 kx x Tip Tip - buildBalancedTree l@(x ::: xs) = - let (left, root, right) = splitList l + 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) + [] => + Tip + _ => + assert_total $ buildBalancedTree (convertToList1 left) (length left) rightTree = case right of - [] => Tip - _ => assert_total $ buildBalancedTree (convertToList1 right) - in linkRootWithSubtrees root leftTree rightTree + [] => + Tip + _ => + assert_total $ buildBalancedTree (convertToList1 right) (length right) + in linkRootWithSubtrees root leftTree rightTree totalSize -------------------------------------------------------------------------------- -- Keys From 2845075d976581703d3dd61eda0e5e778525c656 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 14 Sep 2024 10:28:21 -0400 Subject: [PATCH 15/31] Adding export modifiers for functions missing them. --- src/Data/Map.idr | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index a027893..32e7925 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -83,6 +83,7 @@ insert kx0 vx0 m = go kx0 kx0 vx0 m 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 @@ -125,6 +126,7 @@ insertWith = go 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 @@ -139,6 +141,7 @@ insertWithR = go 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 @@ -482,6 +485,7 @@ 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 @@ -677,6 +681,7 @@ 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 @@ -903,6 +908,7 @@ splitAt i m = -- 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 @@ -913,6 +919,7 @@ 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 From d669756ee2f340f297d991f39195c7132b71a370 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 14 Sep 2024 11:25:07 -0400 Subject: [PATCH 16/31] Altering show interface. --- src/Data/Map.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 32e7925..9371dfe 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1365,7 +1365,7 @@ Foldable (Map k) where private Show k => Show v => Show (List (k, v)) where - show xs = "fromList " ++ "[" ++ show' xs ++ "]" + show xs = "[" ++ show' xs ++ "]" where show'' : (k, v) -> String show'' (k, v) = "(" ++ show k ++ ", " ++ show v ++ ")" @@ -1376,4 +1376,4 @@ Show k => Show v => Show (List (k, v)) where export Show (List (k, v)) => Show (Map k v) where - show = show . toList + show m = "fromList " ++ (show $ toList m) From 4a2537248f53e1a117ed6667fe92acca16a7aba5 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 14 Sep 2024 18:40:12 -0400 Subject: [PATCH 17/31] Adding profiling for map. --- profile/profile.ipkg | 11 +++ profile/src/Main.idr | 226 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 237 insertions(+) create mode 100644 profile/profile.ipkg create mode 100644 profile/src/Main.idr diff --git a/profile/profile.ipkg b/profile/profile.ipkg new file mode 100644 index 0000000..97c5460 --- /dev/null +++ b/profile/profile.ipkg @@ -0,0 +1,11 @@ +package containers-profile + +authors = "stefan-hoeck" +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..005c74b --- /dev/null +++ b/profile/src/Main.idr @@ -0,0 +1,226 @@ +module Main + +import Data.List +import Data.Map as M +import Data.SortedMap as SM +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] + +insertMap : Nat -> Map Nat Nat +insertMap n = do + let m = M.fromList $ map (\x => (x,plus x 1)) [0..n] + let m = M.insert 1 2 m + let m = M.insert 3 4 m + let m = M.insert 4 5 m + let m = M.insert 6 7 m + let m = M.insert 8 9 m + let m = M.insert 10 11 m + let m = M.insert 12 13 m + let m = M.insert 14 15 m + let m = M.insert 16 17 m + M.insert 18 19 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 1 2 m + let m = SM.insert 3 4 m + let m = SM.insert 4 5 m + let m = SM.insert 6 7 m + let m = SM.insert 8 9 m + let m = SM.insert 10 11 m + let m = SM.insert 12 13 m + let m = SM.insert 14 15 m + let m = SM.insert 16 17 m + SM.insert 18 19 m + +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 + +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 + +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 + +bench : Benchmark Void +bench = Group "map" + [ 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 "insertMap" + [ Single "10" (basic insertMap 0) + ] + , Group "insertSortedMap" + [ Single "10" (basic insertSortedMap 0) + ] + , Group "deleteMap" + [ Single "10" (basic deleteMap 9) + ] + , Group "deleteSortedMap" + [ Single "10" (basic deleteSortedMap 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 "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) + ] + ] + +main : IO () +main = do + runDefault (const True) Details show bench From ae3499573fcebb312be32c3650cc06ef968d7df6 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 14 Sep 2024 18:55:32 -0400 Subject: [PATCH 18/31] Updating authors section of containers.ipkg and profile.ipkg. --- containers.ipkg | 2 +- profile/profile.ipkg | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/containers.ipkg b/containers.ipkg index 1403e35..035dcbb 100644 --- a/containers.ipkg +++ b/containers.ipkg @@ -1,6 +1,6 @@ package containers -authors = "stefan-hoeck" +authors = "stefan-hoeck and matthew-mosior" brief = "Basic Tree and Queue data structures" version = 0.6.0 sourcedir = "src" diff --git a/profile/profile.ipkg b/profile/profile.ipkg index 97c5460..ad2f28f 100644 --- a/profile/profile.ipkg +++ b/profile/profile.ipkg @@ -1,6 +1,6 @@ package containers-profile -authors = "stefan-hoeck" +authors = "stefan-hoeck and matthew-mosior" version = 0.7.0 sourcedir = "src" depends = containers From 75b9604536b3f15332a10804299b792455329011 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 17 Sep 2024 10:45:53 -0400 Subject: [PATCH 19/31] Updating insert/delete profiling cases. --- profile/src/Main.idr | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/profile/src/Main.idr b/profile/src/Main.idr index 005c74b..0ff3620 100644 --- a/profile/src/Main.idr +++ b/profile/src/Main.idr @@ -19,30 +19,30 @@ createSortedMap n = SM.fromList $ map (\x => (x,plus x 1)) [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 1 2 m - let m = M.insert 3 4 m - let m = M.insert 4 5 m - let m = M.insert 6 7 m - let m = M.insert 8 9 m - let m = M.insert 10 11 m - let m = M.insert 12 13 m - let m = M.insert 14 15 m - let m = M.insert 16 17 m - M.insert 18 19 m + 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 1 2 m - let m = SM.insert 3 4 m - let m = SM.insert 4 5 m - let m = SM.insert 6 7 m - let m = SM.insert 8 9 m - let m = SM.insert 10 11 m - let m = SM.insert 12 13 m - let m = SM.insert 14 15 m - let m = SM.insert 16 17 m - SM.insert 18 19 m + 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 deleteMap : Nat -> Map Nat Nat deleteMap n = do From 86afed2655cee0d035212bd2444018436c47015f Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 11:31:22 -0400 Subject: [PATCH 20/31] Adding internals for Set implementation. --- src/Data/Set/Internal.idr | 236 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 236 insertions(+) create mode 100644 src/Data/Set/Internal.idr diff --git a/src/Data/Set/Internal.idr b/src/Data/Set/Internal.idr new file mode 100644 index 0000000..af97843 --- /dev/null +++ b/src/Data/Set/Internal.idr @@ -0,0 +1,236 @@ +||| 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 + +-------------------------------------------------------------------------------- +-- Creating Sets +-------------------------------------------------------------------------------- + +||| Wrap a single value in a map +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. +-} + +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 From 256efbf252394ae22697834f73b4ff0a2b7eeb11 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 11:33:42 -0400 Subject: [PATCH 21/31] Adding punctuation for documentation of map and set singleton functions. --- src/Data/Map/Internal.idr | 2 +- src/Data/Set/Internal.idr | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr index a98cefd..20ed75a 100644 --- a/src/Data/Map/Internal.idr +++ b/src/Data/Map/Internal.idr @@ -37,7 +37,7 @@ data MaxView k a = MaxView' k a (Map k a) -- Creating Maps -------------------------------------------------------------------------------- -||| Wrap a single value in a map +||| Wrap a single value in a map. export singleton : k -> a -> Map k a singleton k x = Bin 1 k x Tip Tip diff --git a/src/Data/Set/Internal.idr b/src/Data/Set/Internal.idr index af97843..424dcb9 100644 --- a/src/Data/Set/Internal.idr +++ b/src/Data/Set/Internal.idr @@ -25,7 +25,7 @@ data Set a = Bin Size a (Set a) (Set a) -- Creating Sets -------------------------------------------------------------------------------- -||| Wrap a single value in a map +||| Wrap a single value in a set. export singleton : a -> Set a singleton x = Bin 1 x Tip Tip From ba8e09fc2a470e04339379edd6002a759507edde Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 11:36:07 -0400 Subject: [PATCH 22/31] Updating containers.ipkg to include Data.Set.Internal. --- containers.ipkg | 1 + 1 file changed, 1 insertion(+) diff --git a/containers.ipkg b/containers.ipkg index 035dcbb..5da8aa3 100644 --- a/containers.ipkg +++ b/containers.ipkg @@ -9,5 +9,6 @@ depends = base >= 0.6.0 modules = Data.Map , Data.Map.Internal + , Data.Set.Internal , Data.Queue , Data.Tree From f59b2351a2fbf1747d5ccdb53ece0df02f20f84f Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 19:43:57 -0400 Subject: [PATCH 23/31] Completing implementation for Set, small doc fix to Map, adding Data.Set to containers.ipkg. --- containers.ipkg | 1 + src/Data/Map.idr | 13 +- src/Data/Set.idr | 822 ++++++++++++++++++++++++++++++++++++++ src/Data/Set/Internal.idr | 1 + 4 files changed, 831 insertions(+), 6 deletions(-) create mode 100644 src/Data/Set.idr diff --git a/containers.ipkg b/containers.ipkg index 5da8aa3..037c0ec 100644 --- a/containers.ipkg +++ b/containers.ipkg @@ -9,6 +9,7 @@ depends = base >= 0.6.0 modules = Data.Map , Data.Map.Internal + , Data.Set , Data.Set.Internal , Data.Queue , Data.Tree diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 9371dfe..d8dbffe 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1285,15 +1285,16 @@ toList = toAscList export 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) +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 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) diff --git a/src/Data/Set.idr b/src/Data/Set.idr new file mode 100644 index 0000000..c14142a --- /dev/null +++ b/src/Data/Set.idr @@ -0,0 +1,822 @@ +||| 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 => + case (go orig x l) == l of + True => + t + False => + balanceL y (go orig x l) r + GT => + case (go orig x r) == r of + True => + t + False => + balanceR y l (go orig x 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 => + case (go orig x l) == l of + True => + t + False => + balanceL y (go orig x l) r + GT => + case (go orig x r) == r of + True => + t + False => + balanceR y l (go orig x 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 => + case (go x l) == l of + True => + t + False => + balanceR y (go x l) r + GT => + case (go x r) == r of + True => + t + False => + balanceL y l (go x 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 +-------------------------------------------------------------------------------- + +private +||| Merges two trees. +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 +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 +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 +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 +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 +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 +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 +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 = + case split x t2 of + (l2,r2) => + case (union l1 l2) == l1 && (union r1 r2) == r1 of + True => + t1 + False => + link x (union l1 l2) (union r1 r2) + +-------------------------------------------------------------------------------- +-- 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) = + case split x t1 of + (l1,r1) => + case size (difference l1 l2) + size (difference r1 r2) == size t1 of + True => + t1 + False => + merge (difference l1 l2) (difference r1 r2) + +||| 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 = + case splitMember x t2 of + (l2,True,r2) => + case (intersection l1 l2) == l1 && (intersection r1 r2) == r1 of + True => + t1 + False => + link x (intersection l1 l2) (intersection r1 r2) + (l2,False,r2) => + merge (intersection l1 l2) (intersection r1 r2) + +-------------------------------------------------------------------------------- +-- 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 +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 index 424dcb9..536eacb 100644 --- a/src/Data/Set/Internal.idr +++ b/src/Data/Set/Internal.idr @@ -77,6 +77,7 @@ size (Bin _ _ l r) = 1 + size l + size r is larger, we currently use delta=3. -} +export delta : Nat delta = 3 From 9aa5b72e3ce00aa2907a7b0b4a355ff893862d63 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 19:53:39 -0400 Subject: [PATCH 24/31] Adding initial set profiling. --- profile/src/Main.idr | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/profile/src/Main.idr b/profile/src/Main.idr index 0ff3620..d7934be 100644 --- a/profile/src/Main.idr +++ b/profile/src/Main.idr @@ -3,6 +3,8 @@ 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 @@ -16,6 +18,12 @@ 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 $ map (\x => x) [0..n] + +createSortedSet : Nat -> SortedSet Nat +createSortedSet n = SS.fromList $ map (\x => x) [0..n] + insertMap : Nat -> Map Nat Nat insertMap n = do let m = M.fromList $ map (\x => (x,plus x 1)) [0..n] @@ -167,7 +175,7 @@ valuesSortedMap n = do SM.values m bench : Benchmark Void -bench = Group "map" +bench = Group "containers" [ Group "List" [ Single "1" (basic createList 0) , Single "100" (basic createList 99) @@ -183,6 +191,16 @@ bench = Group "map" , 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) ] From 89497b1730af23b0f8386ec850bb33cfe696163c Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 20:03:24 -0400 Subject: [PATCH 25/31] Adding elab reflection derived interfaces for Set. --- src/Data/Set/Internal.idr | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Data/Set/Internal.idr b/src/Data/Set/Internal.idr index 536eacb..2e97a75 100644 --- a/src/Data/Set/Internal.idr +++ b/src/Data/Set/Internal.idr @@ -21,6 +21,8 @@ public export data Set a = Bin Size a (Set a) (Set a) | Tip +%runElab derive "Set" [Eq,Ord,Show] + -------------------------------------------------------------------------------- -- Creating Sets -------------------------------------------------------------------------------- From 93fead51510457fe99e01d0a5c9c8db780d40735 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 20:07:45 -0400 Subject: [PATCH 26/31] Fixing small doc issue with merge. --- src/Data/Set.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Set.idr b/src/Data/Set.idr index c14142a..fdda984 100644 --- a/src/Data/Set.idr +++ b/src/Data/Set.idr @@ -306,8 +306,8 @@ disjoint (Bin _ x l r) t = -- Merge -------------------------------------------------------------------------------- -private ||| Merges two trees. +private merge : Set a -> Set a -> Set a merge Tip r = r merge l Tip = l From 851e587908e1378d6c9699ab85e8ce3d09d78c6f Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 20:35:49 -0400 Subject: [PATCH 27/31] Adding final (for now) profiling cases. --- profile/src/Main.idr | 127 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 125 insertions(+), 2 deletions(-) diff --git a/profile/src/Main.idr b/profile/src/Main.idr index d7934be..f3682a7 100644 --- a/profile/src/Main.idr +++ b/profile/src/Main.idr @@ -19,10 +19,10 @@ 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 $ map (\x => x) [0..n] +createSet n = S.fromList [0..n] createSortedSet : Nat -> SortedSet Nat -createSortedSet n = SS.fromList $ map (\x => x) [0..n] +createSortedSet n = SS.fromList [0..n] insertMap : Nat -> Map Nat Nat insertMap n = do @@ -52,6 +52,34 @@ insertSortedMap n = do 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] @@ -80,6 +108,35 @@ deleteSortedMap n = do 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] @@ -174,6 +231,42 @@ 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" @@ -207,12 +300,24 @@ bench = Group "containers" , 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) ] @@ -237,6 +342,24 @@ bench = Group "containers" , 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 () From a6112126a964db5862190386cf71254305e16c33 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 18 Sep 2024 21:11:28 -0400 Subject: [PATCH 28/31] Adding member (contains) profiling, and optimizing intersection, union, and difference. --- profile/src/Main.idr | 36 +++++++++++++++++++++++++++++++ src/Data/Set.idr | 51 ++++++++++++++++++++++++-------------------- 2 files changed, 64 insertions(+), 23 deletions(-) diff --git a/profile/src/Main.idr b/profile/src/Main.idr index f3682a7..58e9b21 100644 --- a/profile/src/Main.idr +++ b/profile/src/Main.idr @@ -211,6 +211,36 @@ lookupSortedMap n = do 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] @@ -330,6 +360,12 @@ bench = Group "containers" , 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) ] diff --git a/src/Data/Set.idr b/src/Data/Set.idr index fdda984..1bc1dd6 100644 --- a/src/Data/Set.idr +++ b/src/Data/Set.idr @@ -663,13 +663,14 @@ 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 = - case split x t2 of - (l2,r2) => - case (union l1 l2) == l1 && (union r1 r2) == r1 of - True => - t1 - False => - link x (union l1 l2) (union r1 r2) + 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 @@ -682,13 +683,14 @@ difference : Ord a => Set a -> Set a -> Set a difference Tip _ = Tip difference t1 Tip = t1 difference t1 (Bin _ x l2 r2) = - case split x t1 of - (l1,r1) => - case size (difference l1 l2) + size (difference r1 r2) == size t1 of - True => - t1 - False => - merge (difference l1 l2) (difference r1 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 @@ -706,15 +708,18 @@ 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 = - case splitMember x t2 of - (l2,True,r2) => - case (intersection l1 l2) == l1 && (intersection r1 r2) == r1 of - True => - t1 - False => - link x (intersection l1 l2) (intersection r1 r2) - (l2,False,r2) => - merge (intersection l1 l2) (intersection r1 r2) + 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 From 4128c3a46eced66266862f9fd947da1396fd588c Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 19 Sep 2024 09:08:33 -0400 Subject: [PATCH 29/31] Adding last optimizations to Map and Set insert and delete. --- src/Data/Map.idr | 66 ++++++++++++++++++++++++++---------------------- src/Data/Set.idr | 66 ++++++++++++++++++++++++++---------------------- 2 files changed, 72 insertions(+), 60 deletions(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index d8dbffe..469c1c6 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -65,17 +65,19 @@ insert kx0 vx0 m = go kx0 kx0 vx0 m go orig kx x t@(Bin sz ky y l r) = case compare kx ky of LT => - case (go orig kx x l) == l of - True => - t - False => - balanceL ky y (go orig kx x l) r + let l' = go orig kx x l + in case l' == l of + True => + t + False => + balanceL ky y l' r GT => - case (go orig kx x r) == r of - True => - t - False => - balanceR ky y l (go orig kx x r) + 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 => @@ -92,17 +94,19 @@ insertR kx0 = go kx0 kx0 go orig kx x t@(Bin _ ky y l r) = case compare kx ky of LT => - case (go orig kx x l) == l of - True => - t - False => - balanceL ky y (go orig kx x l) r + let l' = go orig kx x l + in case l' == l of + True => + t + False => + balanceL ky y l' r GT => - case (go orig kx x r) == r of - True => - t - False => - balanceR ky y l (go orig kx x r) + let r' = go orig kx x r + in case r' == r of + True => + t + False => + balanceR ky y l r' EQ => t @@ -205,17 +209,19 @@ delete = go go k t@(Bin _ kx x l r) = case compare k kx of LT => - case (go k l) == l of - True => - t - False => - balanceR kx x (go k l) r + let l' = go k l + in case l' == l of + True => + t + False => + balanceR kx x l' r GT => - case (go k r) == r of - True => - t - False => - balanceL kx x l (go k r) + let r' = go k r + in case r' == r of + True => + t + False => + balanceL kx x l r' EQ => glue l r diff --git a/src/Data/Set.idr b/src/Data/Set.idr index 1bc1dd6..b148005 100644 --- a/src/Data/Set.idr +++ b/src/Data/Set.idr @@ -54,17 +54,19 @@ insert x0 s = go x0 x0 s go orig x t@(Bin sz y l r) = case compare x y of LT => - case (go orig x l) == l of - True => - t - False => - balanceL y (go orig x l) r + let l' = go orig x l + in case l' == l of + True => + t + False => + balanceL y l' r GT => - case (go orig x r) == r of - True => - t - False => - balanceR y l (go orig x r) + let r' = go orig x r + in case r' == r of + True => + t + False => + balanceR y l r' EQ => case orig == y of True => @@ -81,17 +83,19 @@ insertR x0 s = go x0 x0 s go orig x t@(Bin _ y l r) = case compare x y of LT => - case (go orig x l) == l of - True => - t - False => - balanceL y (go orig x l) r + let l' = go orig x l + in case l' == l of + True => + t + False => + balanceL y l' r GT => - case (go orig x r) == r of - True => - t - False => - balanceR y l (go orig x r) + let r' = go orig x r + in case r' == r of + True => + t + False => + balanceR y l r' EQ => t @@ -110,17 +114,19 @@ delete = go go x t@(Bin _ y l r) = case compare x y of LT => - case (go x l) == l of - True => - t - False => - balanceR y (go x l) r + let l' = go x l + in case l' == l of + True => + t + False => + balanceR y l' r GT => - case (go x r) == r of - True => - t - False => - balanceL y l (go x r) + let r' = go x r + in case r' == r of + True => + t + False => + balanceL y l r' EQ => glue l r From 5586d97076f82737095fabdf825fc00cadfea433 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 19 Sep 2024 09:17:02 -0400 Subject: [PATCH 30/31] Adding partial annotations to non-total functions. --- src/Data/Map.idr | 11 +++++++++++ src/Data/Set.idr | 10 +++++++++- 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 469c1c6..52bfb3c 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -371,6 +371,7 @@ 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) = @@ -382,6 +383,7 @@ find k (Bin _ kx x l r) = ||| 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 @@ -762,6 +764,7 @@ lookupIndex = go 0 ||| 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 @@ -780,6 +783,7 @@ findIndex = go 0 ||| 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) = @@ -795,6 +799,7 @@ elemAt i (Bin _ kx x l r) = ||| 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 @@ -816,6 +821,7 @@ updateAt f i t = ||| 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 @@ -938,6 +944,7 @@ 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 @@ -946,6 +953,7 @@ findMin t = ||| 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 @@ -979,6 +987,7 @@ minViewWithKey (Bin _ k x l r) = ||| 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 @@ -998,6 +1007,7 @@ maxViewWithKey (Bin _ k x l r) = ||| 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 @@ -1289,6 +1299,7 @@ toList = toAscList ||| 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 = diff --git a/src/Data/Set.idr b/src/Data/Set.idr index b148005..c66f0e2 100644 --- a/src/Data/Set.idr +++ b/src/Data/Set.idr @@ -441,6 +441,7 @@ lookupIndex = go 0 ||| 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 @@ -459,6 +460,7 @@ findIndex = go 0 ||| 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) = @@ -474,6 +476,7 @@ elemAt i (Bin _ x l r) = ||| 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 @@ -596,14 +599,16 @@ 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 + 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 @@ -634,6 +639,7 @@ minView (Bin _ 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 @@ -650,6 +656,7 @@ maxView (Bin _ 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 @@ -753,6 +760,7 @@ toList = toAscList ||| 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 = From 953a4ce59b4f3789fa0d5d28e8a7d63d2bd7e34d Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 19 Sep 2024 09:35:36 -0400 Subject: [PATCH 31/31] Fixing linting issues. --- profile/src/Main.idr | 2 +- src/Data/Map.idr | 2 +- src/Data/Map/Internal.idr | 2 +- src/Data/Set.idr | 6 +++--- src/Data/Set/Internal.idr | 4 ++-- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/profile/src/Main.idr b/profile/src/Main.idr index 58e9b21..36c8005 100644 --- a/profile/src/Main.idr +++ b/profile/src/Main.idr @@ -323,7 +323,7 @@ bench = Group "containers" [ Single "1" (basic createSortedSet 0) , Single "100" (basic createSortedSet 99) , Single "1000" (basic createSortedSet 999) - ] + ] , Group "insertMap" [ Single "10" (basic insertMap 0) ] diff --git a/src/Data/Map.idr b/src/Data/Map.idr index 52bfb3c..8c12221 100644 --- a/src/Data/Map.idr +++ b/src/Data/Map.idr @@ -1329,7 +1329,7 @@ fromList xs = in case rest of [] => assert_total $ idris_crash "Unexpected empty list" - (middle :: right) => + (middle :: right) => (left, middle, right, len) -- Build a balanced tree from a non-empty list buildBalancedTree : List1 (k, v) -> Nat -> Map k v diff --git a/src/Data/Map/Internal.idr b/src/Data/Map/Internal.idr index 20ed75a..0f80f60 100644 --- a/src/Data/Map/Internal.idr +++ b/src/Data/Map/Internal.idr @@ -50,7 +50,7 @@ singleton k x = Bin 1 k x Tip Tip export size : Map k v -> Nat size Tip = 0 -size (Bin _ _ _ l r) = 1 + size l + size r +size (Bin _ _ _ l r) = 1 + size l + size r -------------------------------------------------------------------------------- -- Map Internals diff --git a/src/Data/Set.idr b/src/Data/Set.idr index c66f0e2..05ea9d5 100644 --- a/src/Data/Set.idr +++ b/src/Data/Set.idr @@ -603,7 +603,7 @@ partial findMin : Set a -> a findMin t = case lookupMin t of - Just r => r + 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) @@ -724,7 +724,7 @@ 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 + in case x' of True => case l1l2 == l1 && r1r2 == r1 of True => @@ -790,7 +790,7 @@ fromList xs = in case rest of [] => assert_total $ idris_crash "Unexpected empty list" - (middle :: right) => + (middle :: right) => (left, middle, right, len) -- Build a balanced tree from a non-empty list buildBalancedTree : List1 a -> Nat -> Set a diff --git a/src/Data/Set/Internal.idr b/src/Data/Set/Internal.idr index 2e97a75..9a990e6 100644 --- a/src/Data/Set/Internal.idr +++ b/src/Data/Set/Internal.idr @@ -40,7 +40,7 @@ singleton x = Bin 1 x Tip Tip export size : Set a -> Nat size Tip = 0 -size (Bin _ _ l r) = 1 + size l + size r +size (Bin _ _ l r) = 1 + size l + size r -------------------------------------------------------------------------------- -- Set Internals @@ -197,7 +197,7 @@ 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, l') => (xm, balanceR x l' r) export