{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Utils.Cluster
( cluster
, cluster'
, cluster1
, cluster1'
) where
import Control.Monad
import Data.Equivalence.Monad ( runEquivT, equateAll, classDesc )
import Data.List.NonEmpty ( NonEmpty(..), nonEmpty, toList )
import Data.Maybe ( fromMaybe )
import qualified Data.Map.Strict as MapS
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 = forall a b. (NonEmpty a -> NonEmpty b) -> [a] -> [b]
liftList1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c a.
Ord c =>
(a -> NonEmpty c) -> NonEmpty a -> NonEmpty (NonEmpty a)
cluster1
cluster' :: Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' :: forall c a. Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' = forall a b. (NonEmpty a -> NonEmpty b) -> [a] -> [b]
liftList1 forall c a.
Ord c =>
NonEmpty (a, NonEmpty c) -> NonEmpty (NonEmpty a)
cluster1'
liftList1 :: (NonEmpty a -> NonEmpty b) -> [a] -> [b]
liftList1 :: forall a b. (NonEmpty a -> NonEmpty b) -> [a] -> [b]
liftList1 NonEmpty a -> NonEmpty b
f = \case
[] -> []
a
a : [a]
as -> forall a. NonEmpty a -> [a]
toList forall a b. (a -> b) -> a -> b
$ NonEmpty a -> NonEmpty b
f forall a b. (a -> b) -> a -> b
$ a
a forall a. a -> [a] -> NonEmpty a
:| [a]
as
cluster1 :: Ord c => (a -> NonEmpty c) -> NonEmpty a -> NonEmpty (NonEmpty a)
cluster1 :: forall c a.
Ord c =>
(a -> NonEmpty c) -> NonEmpty a -> NonEmpty (NonEmpty a)
cluster1 a -> NonEmpty c
f NonEmpty a
as = forall c a.
Ord c =>
NonEmpty (a, NonEmpty c) -> NonEmpty (NonEmpty a)
cluster1' forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ a
a -> (a
a, a -> NonEmpty c
f a
a)) NonEmpty a
as
cluster1' :: Ord c => NonEmpty (a, NonEmpty c) -> NonEmpty (NonEmpty a)
cluster1' :: forall c a.
Ord c =>
NonEmpty (a, NonEmpty c) -> NonEmpty (NonEmpty a)
cluster1' NonEmpty (a, NonEmpty c)
acs = forall a. Fail a -> a
runFail_ forall a b. (a -> b) -> a -> b
$ 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 forall a. a -> a
id forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ NonEmpty (a, NonEmpty c)
acs forall a b. (a -> b) -> a -> b
$ \ (a
_, c
c :| [c]
cs) -> forall c v d (m :: * -> *). MonadEquiv c v d m => [v] -> m ()
equateAll forall a b. (a -> b) -> a -> b
$ c
cforall a. a -> [a] -> [a]
:[c]
cs
NonEmpty (Map c (NonEmpty a))
cas <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM NonEmpty (a, NonEmpty c)
acs forall a b. (a -> b) -> a -> b
$ \ (a
a, c
c :| [c]
_) -> forall c v d (m :: * -> *). MonadEquiv c v d m => v -> m d
classDesc c
c forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ c
k -> forall k a. k -> a -> Map k a
MapS.singleton c
k (forall el coll. Singleton el coll => el -> coll
singleton a
a)
let m :: Map c (NonEmpty a)
m = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
MapS.unionsWith forall a. Semigroup a => a -> a -> a
(<>) NonEmpty (Map c (NonEmpty a))
cas
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => [Char] -> a
error [Char]
"impossibility at Agda.Utils.Cluster.cluster'") forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe (NonEmpty a)
nonEmpty forall a b. (a -> b) -> a -> b
$
forall k a. Map k a -> [a]
MapS.elems Map c (NonEmpty a)
m