agda/test/Internal/Utils/Bag.hs

{-# LANGUAGE TemplateHaskell #-}

module Internal.Utils.Bag ( tests ) where

import Agda.Utils.Bag

import Data.Functor.Identity
import qualified Data.List as List
import qualified Data.Set as Set

import Prelude hiding ( map )

import Internal.Helpers

------------------------------------------------------------------------
-- * Properties
------------------------------------------------------------------------

instance (Ord a, Arbitrary a) => Arbitrary (Bag a) where
  arbitrary = fromList <$> arbitrary

prop_count_empty :: Ord a => a -> Bool
prop_count_empty a = count a empty == 0

prop_count_singleton :: Ord a => a -> Bool
prop_count_singleton a = count a (singleton a) == 1

prop_count_insert :: Ord a => a -> Bag a -> Bool
prop_count_insert a b = count a (insert a b) == 1 + count a b

prop_size_union :: Ord a => Bag a -> Bag a -> Bool
prop_size_union b c = size (b `union` c) == size b + size c

prop_size_fromList :: Ord a => [a] -> Bool
prop_size_fromList l = size (fromList l) == length l

prop_fromList_toList :: Ord a => Bag a -> Bool
prop_fromList_toList b = fromList (toList b) == b

prop_toList_fromList :: Ord a => [a] -> Bool
prop_toList_fromList l = toList (fromList l) == List.sort l

prop_keys_fromList :: Ord a => [a] -> Bool
prop_keys_fromList l = keys (fromList l) == Set.toList (Set.fromList l)

prop_nonempty_groups :: Bag a -> Bool
prop_nonempty_groups b = all (not . List.null) $ groups b

prop_map_id :: Ord a => Bag a -> Bool
prop_map_id b = map id b == b

prop_map_compose :: (Ord b, Ord c) =>
                    (b -> c) -> (a -> b) -> Bag a -> Bool
prop_map_compose f g b = map f (map g b) == map (f . g) b

prop_traverse_id :: Ord a => Bag a -> Bool
prop_traverse_id b = traverse' Identity b == Identity b

------------------------------------------------------------------------
-- * All tests
------------------------------------------------------------------------

-- Template Haskell hack to make the following $allProperties work
-- under ghc-7.8.
return [] -- KEEP!

-- | All tests as collected by 'allProperties'.
--
-- Using 'allProperties' is convenient and superior to the manual
-- enumeration of tests, since the name of the property is added
-- automatically.

tests :: TestTree
tests = testProperties "Internal.Utils.Bag" $allProperties