module Agda.Utils.ListT.Tests (tests) where
import Control.Applicative
import Data.Functor.Identity
import Test.QuickCheck
import Text.Show.Functions
import Agda.Utils.ListT
type List = ListT Identity
foldList :: (a -> b -> b) -> b -> List a -> b
foldList cons nil l = runIdentity $ foldListT c (Identity nil) l
where c a = Identity . cons a . runIdentity
fromList :: [a] -> List a
fromList = foldr consListT nilListT
toList :: List a -> [a]
toList = foldList (:) []
prop_concat xxs = toList (concatListT (fromList (map fromList xxs))) == concat xxs
prop_idiom fs xs = toList (fromList fs <*> fromList xs) == (fs <*> xs)
prop_concatMap f xs = toList (fromList . f =<< fromList xs) == (f =<< xs)
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.Permutation"
$quickCheckAll