{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Utils.Bag where
import Prelude hiding (null, map)
import Text.Show.Functions ()
import qualified Data.List as List
import Data.List.NonEmpty ( NonEmpty, pattern (:|) )
import qualified Data.List.NonEmpty as List1
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Semigroup
import Agda.Utils.Functor
newtype Bag a = Bag
{ forall a. Bag a -> Map a (NonEmpty a)
bag :: Map a (NonEmpty a)
}
deriving (Bag a -> Bag a -> Bool
(Bag a -> Bag a -> Bool) -> (Bag a -> Bag a -> Bool) -> Eq (Bag a)
forall a. Eq a => Bag a -> Bag a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Bag a -> Bag a -> Bool
== :: Bag a -> Bag a -> Bool
$c/= :: forall a. Eq a => Bag a -> Bag a -> Bool
/= :: Bag a -> Bag a -> Bool
Eq, Eq (Bag a)
Eq (Bag a) =>
(Bag a -> Bag a -> Ordering)
-> (Bag a -> Bag a -> Bool)
-> (Bag a -> Bag a -> Bool)
-> (Bag a -> Bag a -> Bool)
-> (Bag a -> Bag a -> Bool)
-> (Bag a -> Bag a -> Bag a)
-> (Bag a -> Bag a -> Bag a)
-> Ord (Bag a)
Bag a -> Bag a -> Bool
Bag a -> Bag a -> Ordering
Bag a -> Bag a -> Bag a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Bag a)
forall a. Ord a => Bag a -> Bag a -> Bool
forall a. Ord a => Bag a -> Bag a -> Ordering
forall a. Ord a => Bag a -> Bag a -> Bag a
$ccompare :: forall a. Ord a => Bag a -> Bag a -> Ordering
compare :: Bag a -> Bag a -> Ordering
$c< :: forall a. Ord a => Bag a -> Bag a -> Bool
< :: Bag a -> Bag a -> Bool
$c<= :: forall a. Ord a => Bag a -> Bag a -> Bool
<= :: Bag a -> Bag a -> Bool
$c> :: forall a. Ord a => Bag a -> Bag a -> Bool
> :: Bag a -> Bag a -> Bool
$c>= :: forall a. Ord a => Bag a -> Bag a -> Bool
>= :: Bag a -> Bag a -> Bool
$cmax :: forall a. Ord a => Bag a -> Bag a -> Bag a
max :: Bag a -> Bag a -> Bag a
$cmin :: forall a. Ord a => Bag a -> Bag a -> Bag a
min :: Bag a -> Bag a -> Bag a
Ord)
null :: Bag a -> Bool
null :: forall a. Bag a -> Bool
null = Map a (NonEmpty a) -> Bool
forall k a. Map k a -> Bool
Map.null (Map a (NonEmpty a) -> Bool)
-> (Bag a -> Map a (NonEmpty a)) -> Bag a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> Map a (NonEmpty a)
forall a. Bag a -> Map a (NonEmpty a)
bag
size :: Bag a -> Int
size :: forall a. Bag a -> Int
size = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (Bag a -> Sum Int) -> Bag a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty a -> Sum Int) -> Map a (NonEmpty a) -> Sum Int
forall m a. Monoid m => (a -> m) -> Map a a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> Sum Int
forall a. a -> Sum a
Sum (Int -> Sum Int) -> (NonEmpty a -> Int) -> NonEmpty a -> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty a -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) (Map a (NonEmpty a) -> Sum Int)
-> (Bag a -> Map a (NonEmpty a)) -> Bag a -> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> Map a (NonEmpty a)
forall a. Bag a -> Map a (NonEmpty a)
bag
(!) :: Ord a => Bag a -> a -> [a]
! :: forall a. Ord a => Bag a -> a -> [a]
(!) (Bag Map a (NonEmpty a)
b) a
a = [a] -> (NonEmpty a -> [a]) -> Maybe (NonEmpty a) -> [a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
List1.toList (Maybe (NonEmpty a) -> [a]) -> Maybe (NonEmpty a) -> [a]
forall a b. (a -> b) -> a -> b
$ a -> Map a (NonEmpty a) -> Maybe (NonEmpty a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a Map a (NonEmpty a)
b
member :: Ord a => a -> Bag a -> Bool
member :: forall a. Ord a => a -> Bag a -> Bool
member a
a = Bool -> Bool
not (Bool -> Bool) -> (Bag a -> Bool) -> Bag a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bag a -> Bool
forall a. Ord a => a -> Bag a -> Bool
notMember a
a
notMember :: Ord a => a -> Bag a -> Bool
notMember :: forall a. Ord a => a -> Bag a -> Bool
notMember a
a Bag a
b = [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null (Bag a
b Bag a -> a -> [a]
forall a. Ord a => Bag a -> a -> [a]
! a
a)
count :: Ord a => a -> Bag a -> Int
count :: forall a. Ord a => a -> Bag a -> Int
count a
a Bag a
b = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Bag a
b Bag a -> a -> [a]
forall a. Ord a => Bag a -> a -> [a]
! a
a)
empty :: Bag a
empty :: forall a. Bag a
empty = Map a (NonEmpty a) -> Bag a
forall a. Map a (NonEmpty a) -> Bag a
Bag (Map a (NonEmpty a) -> Bag a) -> Map a (NonEmpty a) -> Bag a
forall a b. (a -> b) -> a -> b
$ Map a (NonEmpty a)
forall k a. Map k a
Map.empty
singleton :: a -> Bag a
singleton :: forall a. a -> Bag a
singleton a
a = Map a (NonEmpty a) -> Bag a
forall a. Map a (NonEmpty a) -> Bag a
Bag (Map a (NonEmpty a) -> Bag a) -> Map a (NonEmpty a) -> Bag a
forall a b. (a -> b) -> a -> b
$ a -> NonEmpty a -> Map a (NonEmpty a)
forall k a. k -> a -> Map k a
Map.singleton a
a (a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [])
union :: Ord a => Bag a -> Bag a -> Bag a
union :: forall a. Ord a => Bag a -> Bag a -> Bag a
union (Bag Map a (NonEmpty a)
b) (Bag Map a (NonEmpty a)
c) = Map a (NonEmpty a) -> Bag a
forall a. Map a (NonEmpty a) -> Bag a
Bag (Map a (NonEmpty a) -> Bag a) -> Map a (NonEmpty a) -> Bag a
forall a b. (a -> b) -> a -> b
$ (NonEmpty a -> NonEmpty a -> NonEmpty a)
-> Map a (NonEmpty a) -> Map a (NonEmpty a) -> Map a (NonEmpty a)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith NonEmpty a -> NonEmpty a -> NonEmpty a
forall a. Semigroup a => a -> a -> a
(<>) Map a (NonEmpty a)
b Map a (NonEmpty a)
c
unions :: Ord a => [Bag a] -> Bag a
unions :: forall a. Ord a => [Bag a] -> Bag a
unions = Map a (NonEmpty a) -> Bag a
forall a. Map a (NonEmpty a) -> Bag a
Bag (Map a (NonEmpty a) -> Bag a)
-> ([Bag a] -> Map a (NonEmpty a)) -> [Bag a] -> Bag a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty a -> NonEmpty a -> NonEmpty a)
-> [Map a (NonEmpty a)] -> Map a (NonEmpty a)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith NonEmpty a -> NonEmpty a -> NonEmpty a
forall a. Semigroup a => a -> a -> a
(<>) ([Map a (NonEmpty a)] -> Map a (NonEmpty a))
-> ([Bag a] -> [Map a (NonEmpty a)])
-> [Bag a]
-> Map a (NonEmpty a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bag a -> Map a (NonEmpty a)) -> [Bag a] -> [Map a (NonEmpty a)]
forall a b. (a -> b) -> [a] -> [b]
List.map Bag a -> Map a (NonEmpty a)
forall a. Bag a -> Map a (NonEmpty a)
bag
insert :: Ord a => a -> Bag a -> Bag a
insert :: forall a. Ord a => a -> Bag a -> Bag a
insert a
a = Map a (NonEmpty a) -> Bag a
forall a. Map a (NonEmpty a) -> Bag a
Bag (Map a (NonEmpty a) -> Bag a)
-> (Bag a -> Map a (NonEmpty a)) -> Bag a -> Bag a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty a -> NonEmpty a -> NonEmpty a)
-> a -> NonEmpty a -> Map a (NonEmpty a) -> Map a (NonEmpty a)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith NonEmpty a -> NonEmpty a -> NonEmpty a
forall a. Semigroup a => a -> a -> a
(<>) a
a (a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| []) (Map a (NonEmpty a) -> Map a (NonEmpty a))
-> (Bag a -> Map a (NonEmpty a)) -> Bag a -> Map a (NonEmpty a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> Map a (NonEmpty a)
forall a. Bag a -> Map a (NonEmpty a)
bag
fromList :: Ord a => [a] -> Bag a
fromList :: forall a. Ord a => [a] -> Bag a
fromList = Map a (NonEmpty a) -> Bag a
forall a. Map a (NonEmpty a) -> Bag a
Bag (Map a (NonEmpty a) -> Bag a)
-> ([a] -> Map a (NonEmpty a)) -> [a] -> Bag a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty a -> NonEmpty a -> NonEmpty a)
-> [(a, NonEmpty a)] -> Map a (NonEmpty a)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith NonEmpty a -> NonEmpty a -> NonEmpty a
forall a. Semigroup a => a -> a -> a
(<>) ([(a, NonEmpty a)] -> Map a (NonEmpty a))
-> ([a] -> [(a, NonEmpty a)]) -> [a] -> Map a (NonEmpty a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (a, NonEmpty a)) -> [a] -> [(a, NonEmpty a)]
forall a b. (a -> b) -> [a] -> [b]
List.map (\ a
a -> (a
a, a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| []))
groups :: Bag a -> [NonEmpty a]
groups :: forall a. Bag a -> [NonEmpty a]
groups = Map a (NonEmpty a) -> [NonEmpty a]
forall k a. Map k a -> [a]
Map.elems (Map a (NonEmpty a) -> [NonEmpty a])
-> (Bag a -> Map a (NonEmpty a)) -> Bag a -> [NonEmpty a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> Map a (NonEmpty a)
forall a. Bag a -> Map a (NonEmpty a)
bag
toList :: Bag a -> [a]
toList :: forall a. Bag a -> [a]
toList = (NonEmpty a -> [a]) -> [NonEmpty a] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
List1.toList ([NonEmpty a] -> [a]) -> (Bag a -> [NonEmpty a]) -> Bag a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> [NonEmpty a]
forall a. Bag a -> [NonEmpty a]
groups
keys :: Bag a -> [a]
keys :: forall a. Bag a -> [a]
keys = Map a (NonEmpty a) -> [a]
forall k a. Map k a -> [k]
Map.keys (Map a (NonEmpty a) -> [a])
-> (Bag a -> Map a (NonEmpty a)) -> Bag a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> Map a (NonEmpty a)
forall a. Bag a -> Map a (NonEmpty a)
bag
elems :: Bag a -> [a]
elems :: forall a. Bag a -> [a]
elems = Bag a -> [a]
forall a. Bag a -> [a]
toList
toAscList :: Bag a -> [a]
toAscList :: forall a. Bag a -> [a]
toAscList = Bag a -> [a]
forall a. Bag a -> [a]
toList
map :: Ord b => (a -> b) -> Bag a -> Bag b
map :: forall b a. Ord b => (a -> b) -> Bag a -> Bag b
map a -> b
f = Map b (NonEmpty b) -> Bag b
forall a. Map a (NonEmpty a) -> Bag a
Bag (Map b (NonEmpty b) -> Bag b)
-> (Bag a -> Map b (NonEmpty b)) -> Bag a -> Bag b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty b -> NonEmpty b -> NonEmpty b)
-> [(b, NonEmpty b)] -> Map b (NonEmpty b)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith NonEmpty b -> NonEmpty b -> NonEmpty b
forall a. Semigroup a => a -> a -> a
(<>) ([(b, NonEmpty b)] -> Map b (NonEmpty b))
-> (Bag a -> [(b, NonEmpty b)]) -> Bag a -> Map b (NonEmpty b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty a -> (b, NonEmpty b))
-> [NonEmpty a] -> [(b, NonEmpty b)]
forall a b. (a -> b) -> [a] -> [b]
List.map NonEmpty a -> (b, NonEmpty b)
ff ([NonEmpty a] -> [(b, NonEmpty b)])
-> (Bag a -> [NonEmpty a]) -> Bag a -> [(b, NonEmpty b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a (NonEmpty a) -> [NonEmpty a]
forall k a. Map k a -> [a]
Map.elems (Map a (NonEmpty a) -> [NonEmpty a])
-> (Bag a -> Map a (NonEmpty a)) -> Bag a -> [NonEmpty a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> Map a (NonEmpty a)
forall a. Bag a -> Map a (NonEmpty a)
bag
where
ff :: NonEmpty a -> (b, NonEmpty b)
ff (a
a :| [a]
as) = (b
b, b
b b -> [b] -> NonEmpty b
forall a. a -> [a] -> NonEmpty a
:| (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
List.map a -> b
f [a]
as) where b :: b
b = a -> b
f a
a
traverse' :: forall a b m . (Applicative m, Ord b) =>
(a -> m b) -> Bag a -> m (Bag b)
traverse' :: forall a b (m :: * -> *).
(Applicative m, Ord b) =>
(a -> m b) -> Bag a -> m (Bag b)
traverse' a -> m b
f = (Map b (NonEmpty b) -> Bag b
forall a. Map a (NonEmpty a) -> Bag a
Bag (Map b (NonEmpty b) -> Bag b)
-> ([(b, NonEmpty b)] -> Map b (NonEmpty b))
-> [(b, NonEmpty b)]
-> Bag b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty b -> NonEmpty b -> NonEmpty b)
-> [(b, NonEmpty b)] -> Map b (NonEmpty b)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith NonEmpty b -> NonEmpty b -> NonEmpty b
forall a. Semigroup a => a -> a -> a
(<>)) ([(b, NonEmpty b)] -> Bag b)
-> (Bag a -> m [(b, NonEmpty b)]) -> Bag a -> m (Bag b)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> (NonEmpty a -> m (b, NonEmpty b))
-> [NonEmpty a] -> m [(b, NonEmpty b)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse NonEmpty a -> m (b, NonEmpty b)
trav ([NonEmpty a] -> m [(b, NonEmpty b)])
-> (Bag a -> [NonEmpty a]) -> Bag a -> m [(b, NonEmpty b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a (NonEmpty a) -> [NonEmpty a]
forall k a. Map k a -> [a]
Map.elems (Map a (NonEmpty a) -> [NonEmpty a])
-> (Bag a -> Map a (NonEmpty a)) -> Bag a -> [NonEmpty a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> Map a (NonEmpty a)
forall a. Bag a -> Map a (NonEmpty a)
bag
where
trav :: NonEmpty a -> m (b, NonEmpty b)
trav :: NonEmpty a -> m (b, NonEmpty b)
trav (a
a :| [a]
as) = (\ b
b [b]
bs -> (b
b, b
b b -> [b] -> NonEmpty b
forall a. a -> [a] -> NonEmpty a
:| [b]
bs)) (b -> [b] -> (b, NonEmpty b)) -> m b -> m ([b] -> (b, NonEmpty b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a m ([b] -> (b, NonEmpty b)) -> m [b] -> m (b, NonEmpty b)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> m b) -> [a] -> m [b]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> m b
f [a]
as
instance Show a => Show (Bag a) where
showsPrec :: Int -> Bag a -> ShowS
showsPrec Int
_ (Bag Map a (NonEmpty a)
b) = (String
"Agda.Utils.Bag.Bag (" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a (NonEmpty a) -> ShowS
forall a. Show a => a -> ShowS
shows Map a (NonEmpty a)
b ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
')'Char -> ShowS
forall a. a -> [a] -> [a]
:)
instance Ord a => Semigroup (Bag a) where
<> :: Bag a -> Bag a -> Bag a
(<>) = Bag a -> Bag a -> Bag a
forall a. Ord a => Bag a -> Bag a -> Bag a
union
instance Ord a => Monoid (Bag a) where
mempty :: Bag a
mempty = Bag a
forall a. Bag a
empty
mappend :: Bag a -> Bag a -> Bag a
mappend = Bag a -> Bag a -> Bag a
forall a. Semigroup a => a -> a -> a
(<>)
mconcat :: [Bag a] -> Bag a
mconcat = [Bag a] -> Bag a
forall a. Ord a => [Bag a] -> Bag a
unions
instance Foldable Bag where
foldMap :: forall m a. Monoid m => (a -> m) -> Bag a -> m
foldMap a -> m
f = (a -> m) -> [a] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f ([a] -> m) -> (Bag a -> [a]) -> Bag a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag a -> [a]
forall a. Bag a -> [a]
toList