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 IntMap
import Data.List
import Test.QuickCheck
import Test.QuickCheck.All
import Test.QuickCheck.Function
import Text.Show.Functions
type C = Int
cluster :: (a -> (C,[C])) -> [a] -> [[a]]
cluster f as = cluster' $ map (\ a -> (a, f a)) as
cluster' :: [(a,(C,[C]))] -> [[a]]
cluster' acs = runEquivM id const $ do
forM_ acs $ \ (_,(c,cs)) -> equateAll $ c:cs
cas <- forM acs $ \ (a,(c,_)) -> (`IntMap.singleton` [a]) <$> classDesc c
let m = IntMap.unionsWith (++) cas
return $ IntMap.elems m
prop_cluster_complete :: Fun Int (C, [C]) -> [Int] -> Bool
prop_cluster_complete (Fun _ f) as =
(`all` cluster f as) $ \ cl ->
(`all` cl) $ \ a ->
let csa = uncurry (:) $ f a in
let cl' = delete a cl in
null cl' || not (null [ (b,c) | b <- cl', c <- uncurry (:) (f b), c `elem` csa ])
prop_cluster_sound :: Fun Int (C, [C]) -> [Int] -> Bool
prop_cluster_sound (Fun _ f) as =
(`all` [ (c, d) | let cs = cluster f as, c <- cs, d <- cs, c /= d]) $ \ (c, d) ->
(`all` c) $ \ a ->
(`all` d) $ \ b ->
null $ (uncurry (:) $ f a) `intersect` (uncurry (:) $ f b)
neToList :: (a, [a]) -> [a]
neToList = uncurry (:)
isSingleton, exactlyTwo, atLeastTwo :: [a] -> Bool
isSingleton x = length x == 1
exactlyTwo x = length x == 2
atLeastTwo x = length x >= 2
prop_cluster_empty :: Bool
prop_cluster_empty =
null (cluster (const (0,[])) [])
prop_cluster_permutation :: Fun Int (C, [C]) -> [Int] -> Bool
prop_cluster_permutation (Fun _ f) as =
sort as == sort (concat (cluster f as))
prop_cluster_single :: a -> [a] -> Bool
prop_cluster_single a as =
isSingleton $ cluster (const (0,[])) $ (a:as)
prop_cluster_idem :: Fun a (C, [C]) -> a -> [a] -> Bool
prop_cluster_idem (Fun _ f) a as =
isSingleton $ cluster f $ head $ cluster f (a:as)
prop_two_clusters :: [Int] -> Bool
prop_two_clusters as =
atLeastTwo $ cluster (\ x -> (x, [x])) (1:1:as)
test :: [[String]]
test = cluster (\ (x:y:_) -> (ord x,[ord y]))
["anabel","bond","babel","hurz","furz","kurz"]
prop_test :: Bool
prop_test = test == [["anabel","bond","babel"],["hurz","furz","kurz"]]
test1 :: [[String]]
test1 = cluster (\ (x:_:_) -> (ord x,[]))
["anabel","bond","babel","hurz","furz","kurz"]
prop_test1 :: Bool
prop_test1 = test1 == [["anabel"],["bond","babel"],["furz"],["hurz"],["kurz"]]
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.Cluster"
$quickCheckAll