module Agda.Utils.Bag where
import Prelude hiding (null, map)
import Control.Applicative hiding (empty)
import Text.Show.Functions ()
import Data.Foldable (Foldable(foldMap))
import Data.Functor.Identity
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid
import qualified Data.Set as Set
import Data.Traversable
import Agda.Utils.Functor
import Agda.Utils.QuickCheck
#include "undefined.h"
import Agda.Utils.Impossible
newtype Bag a = Bag { bag :: Map a [a] }
deriving (Eq, Ord)
null :: Bag a -> Bool
null = Map.null . bag
size :: Bag a -> Int
size = getSum . foldMap (Sum . length) . bag
(!) :: Ord a => Bag a -> a -> [a]
Bag b ! a = Map.findWithDefault [] a b
member :: Ord a => a -> Bag a -> Bool
member a = not . notMember a
notMember :: Ord a => a -> Bag a -> Bool
notMember a b = List.null (b ! a)
count :: Ord a => a -> Bag a -> Int
count a b = length (b ! a)
empty :: Bag a
empty = Bag $ Map.empty
singleton :: a -> Bag a
singleton a = Bag $ Map.singleton a [a]
union :: Ord a => Bag a -> Bag a -> Bag a
union (Bag b) (Bag c) = Bag $ Map.unionWith (++) b c
unions :: Ord a => [Bag a] -> Bag a
unions = Bag . Map.unionsWith (++) . List.map bag
insert :: Ord a => a -> Bag a -> Bag a
insert a = Bag . Map.insertWith (++) a [a] . bag
fromList :: Ord a => [a] -> Bag a
fromList = Bag . Map.fromListWith (++) . List.map (\ a -> (a,[a]))
groups :: Bag a -> [[a]]
groups = Map.elems . bag
toList :: Bag a -> [a]
toList = concat . groups
keys :: Bag a -> [a]
keys = Map.keys . bag
elems :: Bag a -> [a]
elems = toList
toAscList :: Bag a -> [a]
toAscList = toList
map :: Ord b => (a -> b) -> Bag a -> Bag b
map f = Bag . Map.fromListWith (++) . List.map ff . Map.elems . bag
where
ff (a : as) = (b, b : List.map f as) where b = f a
ff [] = __IMPOSSIBLE__
traverse' :: forall a b m . (Applicative m, Ord b) =>
(a -> m b) -> Bag a -> m (Bag b)
traverse' f = (Bag . Map.fromListWith (++)) <.> traverse trav . Map.elems . bag
where
trav :: [a] -> m (b, [b])
trav (a : as) = (\ b bs -> (b, b:bs)) <$> f a <*> traverse f as
trav [] = __IMPOSSIBLE__
instance Show a => Show (Bag a) where
showsPrec _ (Bag b) = ("Agda.Utils.Bag.Bag (" ++) . showsPrec 0 b . (')':)
instance Ord a => Monoid (Bag a) where
mempty = empty
mappend = union
mconcat = unions
instance Foldable Bag where
foldMap f = foldMap f . toList
instance (Ord a, Arbitrary a) => Arbitrary (Bag a) where
arbitrary = fromList <$> arbitrary
prop_count_empty :: Ord a => a -> Bool
prop_count_empty a = count a empty == 0
prop_count_singleton :: Ord a => a -> Bool
prop_count_singleton a = count a (singleton a) == 1
prop_count_insert :: Ord a => a -> Bag a -> Bool
prop_count_insert a b = count a (insert a b) == 1 + count a b
prop_size_union :: Ord a => Bag a -> Bag a -> Bool
prop_size_union b c = size (b `union` c) == size b + size c
prop_size_fromList :: Ord a => [a] -> Bool
prop_size_fromList l = size (fromList l) == length l
prop_fromList_toList :: Ord a => Bag a -> Bool
prop_fromList_toList b = fromList (toList b) == b
prop_toList_fromList :: Ord a => [a] -> Bool
prop_toList_fromList l = toList (fromList l) == List.sort l
prop_keys_fromList :: Ord a => [a] -> Bool
prop_keys_fromList l = keys (fromList l) == Set.toList (Set.fromList l)
prop_nonempty_groups :: Bag a -> Bool
prop_nonempty_groups b = all (not . List.null) $ groups b
prop_map_id :: Ord a => Bag a -> Bool
prop_map_id b = map id b == b
prop_map_compose :: (Ord b, Ord c) =>
(b -> c) -> (a -> b) -> Bag a -> Bool
prop_map_compose f g b = map f (map g b) == map (f . g) b
prop_traverse_id :: Ord a => Bag a -> Bool
prop_traverse_id b = traverse' Identity b == Identity b
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.Favorites"
$quickCheckAll