module Agda.Utils.Cluster
( cluster
, cluster'
, tests
) where
import Control.Monad
import Data.Equivalence.Monad
import Data.Char
import Data.Functor
import qualified Data.IntMap as Map
import Data.List
import Test.QuickCheck
import Test.QuickCheck.All
import Text.Show.Functions
type C = Int
cluster :: forall a. (a -> (C,[C])) -> [a] -> [[a]]
cluster f as = cluster' $ map (\ a -> (a, f a)) as
cluster' :: forall a. [(a,(C,[C]))] -> [[a]]
cluster' acs = runEquivM id const $ do
forM acs $ \ (_,(c,cs)) -> equateAll $ c:cs
cas <- forM acs $ \ (a,(c,_)) -> (`Map.singleton` [a]) <$> classDesc c
let m = Map.unionsWith (++) cas
return $ Map.elems m
isSingleton x = length x == 1
exactlyTwo x = length x == 2
atLeastTwo x = length x >= 2
prop_cluster_empty =
null (cluster (const (0,[])) [])
prop_cluster_permutation f (as :: [Int]) =
sort as == sort (concat (cluster f as))
prop_cluster_single a as =
isSingleton $ cluster (const (0,[])) $ (a:as)
prop_cluster_idem f a as =
isSingleton $ cluster f $ head $ cluster f (a:as)
prop_two_clusters (as :: [Int]) =
atLeastTwo $ cluster (\ x -> (x, [x])) (1:1:as)
test = cluster (\ (x:y:_) -> (ord x,[ord y]))
["anabel","bond","babel","hurz","furz","kurz"]
test1 = cluster (\ (x:y:_) -> (ord x,[]))
["anabel","bond","babel","hurz","furz","kurz"]
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.Cluster"
$quickCheckAll