{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE CPP #-}
module Agda.Utils.Cluster
( cluster
, cluster'
) where
import Control.Monad
import Data.Equivalence.Monad (runEquivT, equateAll, classDesc)
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Map.Strict as MapS
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif
import Agda.Utils.Functor
import Agda.Utils.Singleton
import Agda.Utils.Fail
cluster :: Ord c => (a -> NonEmpty c) -> [a] -> [NonEmpty a]
cluster :: forall c a. Ord c => (a -> NonEmpty c) -> [a] -> [NonEmpty a]
cluster a -> NonEmpty c
f [a]
as = [(a, NonEmpty c)] -> [NonEmpty a]
forall c a. Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' ([(a, NonEmpty c)] -> [NonEmpty a])
-> [(a, NonEmpty c)] -> [NonEmpty a]
forall a b. (a -> b) -> a -> b
$ (a -> (a, NonEmpty c)) -> [a] -> [(a, NonEmpty c)]
forall a b. (a -> b) -> [a] -> [b]
map (\ a
a -> (a
a, a -> NonEmpty c
f a
a)) [a]
as
cluster' :: Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' :: forall c a. Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' [(a, NonEmpty c)]
acs = Fail [NonEmpty a] -> [NonEmpty a]
forall a. Fail a -> a
runFail_ (Fail [NonEmpty a] -> [NonEmpty a])
-> Fail [NonEmpty a] -> [NonEmpty a]
forall a b. (a -> b) -> a -> b
$ (c -> c)
-> (c -> c -> c)
-> (forall {s}. EquivT s c c Fail [NonEmpty a])
-> Fail [NonEmpty a]
forall (m :: * -> *) v c a.
(Monad m, Applicative m) =>
(v -> c) -> (c -> c -> c) -> (forall s. EquivT s c v m a) -> m a
runEquivT c -> c
forall a. a -> a
id c -> c -> c
forall a b. a -> b -> a
const ((forall {s}. EquivT s c c Fail [NonEmpty a]) -> Fail [NonEmpty a])
-> (forall {s}. EquivT s c c Fail [NonEmpty a])
-> Fail [NonEmpty a]
forall a b. (a -> b) -> a -> b
$ do
[(a, NonEmpty c)]
-> ((a, NonEmpty c) -> EquivT s c c Fail ())
-> EquivT s c c Fail ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(a, NonEmpty c)]
acs (((a, NonEmpty c) -> EquivT s c c Fail ()) -> EquivT s c c Fail ())
-> ((a, NonEmpty c) -> EquivT s c c Fail ())
-> EquivT s c c Fail ()
forall a b. (a -> b) -> a -> b
$ \ (a
_, c
c :| [c]
cs) -> [c] -> EquivT s c c Fail ()
forall c v d (m :: * -> *). MonadEquiv c v d m => [v] -> m ()
equateAll ([c] -> EquivT s c c Fail ()) -> [c] -> EquivT s c c Fail ()
forall a b. (a -> b) -> a -> b
$ c
cc -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
cs
[Map c (NonEmpty a)]
cas <- [(a, NonEmpty c)]
-> ((a, NonEmpty c) -> EquivT s c c Fail (Map c (NonEmpty a)))
-> EquivT s c c Fail [Map c (NonEmpty a)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(a, NonEmpty c)]
acs (((a, NonEmpty c) -> EquivT s c c Fail (Map c (NonEmpty a)))
-> EquivT s c c Fail [Map c (NonEmpty a)])
-> ((a, NonEmpty c) -> EquivT s c c Fail (Map c (NonEmpty a)))
-> EquivT s c c Fail [Map c (NonEmpty a)]
forall a b. (a -> b) -> a -> b
$ \ (a
a, c
c :| [c]
_) -> c -> EquivT s c c Fail c
forall c v d (m :: * -> *). MonadEquiv c v d m => v -> m d
classDesc c
c EquivT s c c Fail c
-> (c -> Map c (NonEmpty a))
-> EquivT s c c Fail (Map c (NonEmpty a))
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ c
k -> c -> NonEmpty a -> Map c (NonEmpty a)
forall k a. k -> a -> Map k a
MapS.singleton c
k (a -> NonEmpty a
forall el coll. Singleton el coll => el -> coll
singleton a
a)
let m :: Map c (NonEmpty a)
m = (NonEmpty a -> NonEmpty a -> NonEmpty a)
-> [Map c (NonEmpty a)] -> Map c (NonEmpty a)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
MapS.unionsWith NonEmpty a -> NonEmpty a -> NonEmpty a
forall a. Semigroup a => a -> a -> a
(<>) [Map c (NonEmpty a)]
cas
[NonEmpty a] -> EquivT s c c Fail [NonEmpty a]
forall a. a -> EquivT s c c Fail a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NonEmpty a] -> EquivT s c c Fail [NonEmpty a])
-> [NonEmpty a] -> EquivT s c c Fail [NonEmpty a]
forall a b. (a -> b) -> a -> b
$ Map c (NonEmpty a) -> [NonEmpty a]
forall k a. Map k a -> [a]
MapS.elems Map c (NonEmpty a)
m