module Test.Tests where

import Data.List (sort)
import Prelude hiding (null, lookup)
import Test.QuickCheck
import Test.QuickCheck.Batch

import Data.Bimap


instance (Ord a, Arbitrary a, Ord b, Arbitrary b)
    => Arbitrary (Bimap a b) where
    arbitrary = fromList `fmap` arbitrary
    coarbitrary = coarbitrary . toList


-- empty bimap has zero size
prop_size_empty = size empty == 0

-- empty bimap is null
prop_null_empty = null empty

-- when converting from a list and back, each pair in the latter
-- list was originally in the former list
-- (heh, this is probably made redundant by polymorphism)
prop_fromList_toList xs =
    let xs' = toList . fromList $ xs
    in all (flip elem xs) xs'
    where
    _ = xs :: [(Int, Integer)]

-- when converting a list to a bimap, each list element either
-- ends up in the bimap, or could conceivably have been clobbered
prop_fromList_account xs = all (\x -> isMember x || notUnique x) xs
    where
    _ = xs :: [(Int, Integer)]
    bi = fromList xs
    isMember x = x `pairMember` bi
    notUnique (x, y) = 
        ((>1) . length . filter (== x) . map fst $ xs) ||
        ((>1) . length . filter (== y) . map snd $ xs)

-- a bimap created from a list is no larger than the list
prop_fromList_size xs = (size $ fromList xs) <= length xs
    where
    _ = xs :: [(Int, Integer)]

-- a monotone bimap can be reconstituted via fromAscPairList
prop_fromAscPairList_reconstitute xs = and
    [ (not . isBottom) bi'
    , valid bi'
    , (bi == bi')
    ]
    where
    xs' = zip (sort $ map fst xs) (sort $ map snd xs)
    bi :: Bimap Int Integer
    bi = fromList xs'
    bi' = fromAscPairList . toAscList $ bi

-- fromAscPairList will never produce an invalid bimap
prop_fromAscPairList_check xs = or
    [ isBottom bi
    , valid bi
    ]
    where
    bi :: Bimap Int Integer
    bi = fromAscPairList xs

-- if a pair is a member of the bimap, then both elements are present
-- and associated with each other
prop_pairMember bi k v =
    ((k, v) `pairMember` bi) == and
        [ k `member`  bi
        , v `memberR` bi
        , lookup  k bi == Just v
        , lookupR v bi == Just k
        ]
    where
    _ = bi :: Bimap Int Integer

-- an inserted pair ends up in the bimap
prop_insert_member bi k v = (k, v) `pairMember` (insert k v bi)
    where
    _ = bi :: Bimap Int Integer

-- if we insert a pair with an existing value, the old value's twin
-- is no longer in the bimap
prop_clobberL bi b' =
    (not . null $ bi) && (b' `notMemberR` bi)
    ==>
    (a, b) `pairNotMember` insert a b' bi
    where
    (a, b) = head . toList $ bi :: (Int, Integer)

prop_clobberR bi a' =
    (not . null $ bi) && (a' `notMember` bi)
    ==>
    (a, b) `pairNotMember` insert a' b bi
    where
    (a, b) = head . toList $ bi :: (Int, Integer)

-- if we politely insert two members, neither of which is present,
-- then the two are successfully associated
prop_tryInsert_member bi k v = (k, v) `neitherMember` bi ==>
    pairMember (k, v) (tryInsert k v bi)
    where
    _ = bi :: Bimap Int Integer
    neitherMember (k, v) bi = k `notMember` bi && v `notMemberR` bi

-- polite insertion will never remove existing associations
prop_tryInsert_not_clobber bi k v =
    all (flip pairMember $ tryInsert k v bi) (toList bi)
    where
    _ = bi :: Bimap Int Integer

-- an arbitrary bimap is valid
prop_valid bi = valid bi
    where
    _ = bi :: Bimap Int Integer

-- if x maps to y, then y maps to x
prop_member_twin bi = flip all (toList bi) $ \(x, y) -> and
    [ (bi !  x) `memberR` bi
    , (bi !> y) `member`  bi
    ]
    where
    _ = bi :: Bimap Int Integer

-- deleting an element removes it from the map
prop_delete bi = flip all (toList bi) $ \(x, y) -> and
    [ x `notMember`  delete  x bi
    , y `notMemberR` deleteR y bi
    ]
    where
    _ = bi :: Bimap Int Integer

-- deleting an element removes its twin from the map
prop_delete_twin bi = flip all (toList bi) $ \(x, y) -> and
    [ (bi !  x) `notMemberR` delete  x bi
    , (bi !> y) `notMember`  deleteR y bi
    ]
    where
    _ = bi :: Bimap Int Integer

-- a singleton bimap is valid, has one association, and the two
-- given values map to each other
prop_singleton x y = let bi = singleton x y in and
    [ valid bi
    , (x, y) `pairMember` bi
    , (bi !  x) == y
    , (bi !> y) == x
    , size bi == 1
    ]
    where
    _ = (x, y) :: (Int, Integer)

-- twist is its own inverse
prop_twist_twist bi =
    bi == (twist . twist $ bi)
    where
    _ = bi :: Bimap Int Integer

-- the property (fromList == fromAList . reverse) only holds
-- if either the left or right values are all distinct
prop_fromList_fromAList xs = and
    [ fromList  ys == fromAList rys
    , fromList rys == fromAList  ys
    ]
    where
    ys = xs `zip` [1..] :: [(Int, Integer)]
    rys = reverse ys

swap (x, y) = (y, x)

-- deleteFindMin and deleteMin agree
prop_deleteMin_is_delete bi = not (null bi) ==>
    snd (deleteFindMin bi) == deleteMin bi
    where
    _ = bi :: Bimap Int Integer

-- deleteFindMin and findMin agree
prop_deleteMin_is_find bi = not (null bi) ==>
    fst (deleteFindMin bi) == findMin bi
    where
    _ = bi :: Bimap Int Integer

-- elements removed by deleteFindMin are no longer in the bimap
prop_deleteMin_deletes bi = not (null bi) ==>
    fst (deleteFindMin bi) `pairNotMember` snd (deleteFindMin bi)
    where
    _ = bi :: Bimap Int Integer

-- findMin finds a member of the map
prop_findMin_member bi = not (null bi) ==>
    findMin bi `pairMember` bi
    where
    _ = bi :: Bimap Int Integer

-- the minimum of a singleton bimap is its contents
prop_singleton_is_findMin x y = findMin bi == (x, y)
    where
    bi :: Bimap Int Integer
    bi = singleton x y

-- deleting the minimum of a singleton leaves it empty
prop_singleton_deleteMin_empty x y = null (deleteMin bi)
    where
    bi :: Bimap Int Integer
    bi = singleton x y

-- the minimum of a bimap is <= all other elements
prop_findMin_is_minimal bi = all (\ (a, _) -> a >= x) lst
    where
    lst = toList bi
    _ = bi :: Bimap Int Integer
    x = fst . findMin $ bi

prop_deleteMinR_is_delete bi = not (null bi) ==>
    snd (deleteFindMinR bi) == deleteMinR bi 
    where
    _ = bi :: Bimap Int Integer

prop_deleteMinR_is_find bi = not (null bi) ==>
    fst (deleteFindMinR bi) == findMinR bi 
    where
    _ = bi :: Bimap Int Integer

prop_deleteMinR_deletes bi = not (null bi) ==>
    (swap . fst) (deleteFindMinR bi) `pairNotMember` snd (deleteFindMinR bi)
    where
    _ = bi :: Bimap Int Integer

prop_findMinR_member bi = not (null bi) ==>
    swap (findMinR bi) `pairMember` bi
    where
    _ = bi :: Bimap Int Integer
        
prop_singleton_is_findMinR x y = findMinR bi == (y, x)
    where
    bi :: Bimap Int Integer
    bi = singleton x y

prop_singleton_deleteMinR_empty x y = null (deleteMinR bi)
    where
    bi :: Bimap Int Integer
    bi = singleton x y

prop_findMinR_is_minimal bi = all (\ (_, b) -> b >= y) lst
    where
    lst = toList bi
    _ = bi :: Bimap Int Integer
    y = fst . findMinR $ bi

prop_deleteMax_is_delete bi = not (null bi) ==>
    snd (deleteFindMax bi) == deleteMax bi
    where
    _ = bi :: Bimap Int Integer

prop_deleteMax_is_find bi = not (null bi) ==>
    fst (deleteFindMax bi) == findMax bi
    where
    _ = bi :: Bimap Int Integer

prop_deleteMax_deletes bi = not (null bi) ==>
    fst (deleteFindMax bi) `pairNotMember` snd (deleteFindMax bi)
    where
    _ = bi :: Bimap Int Integer

prop_findMax_member bi = not (null bi) ==>
    findMax bi `pairMember` bi
    where
    _ = bi :: Bimap Int Integer
        
prop_singleton_is_findMax x y = findMax bi == (x, y)
    where
    bi :: Bimap Int Integer
    bi = singleton x y

prop_singleton_deleteMax_empty x y = null (deleteMax bi)
    where
    bi :: Bimap Int Integer
    bi = singleton x y

prop_findMax_is_maximal bi = all (\ (a, _) -> a <= x) lst
    where
    lst = toList bi
    _ = bi :: Bimap Int Integer
    x = fst . findMax $ bi

prop_deleteMaxR_is_delete bi = not (null bi) ==>
    snd (deleteFindMaxR bi) == deleteMaxR bi 
    where
    _ = bi :: Bimap Int Integer

prop_deleteMaxR_is_find bi = not (null bi) ==>
    fst (deleteFindMaxR bi) == findMaxR bi
    where
    _ = bi :: Bimap Int Integer

prop_deleteMaxR_deletes bi = not (null bi) ==>
    (swap . fst) (deleteFindMaxR bi) `pairNotMember` snd (deleteFindMaxR bi)
    where
    _ = bi :: Bimap Int Integer

prop_findMaxR_member bi = not (null bi) ==>
    swap (findMaxR bi) `pairMember` bi
    where
    _ = bi :: Bimap Int Integer
        
prop_singleton_is_findMaxR x y = findMaxR bi == (y, x)
    where
    bi :: Bimap Int Integer
    bi = singleton x y

prop_singleton_deleteMaxR_empty x y = null (deleteMaxR bi)
    where
    bi :: Bimap Int Integer
    bi = singleton x y

prop_findMaxR_is_maximal bi = all (\ (_, b) -> b <= y) lst
    where
    lst = toList bi
    _ = bi :: Bimap Int Integer
    y = fst . findMaxR $ bi

prop_deleteMin_is_valid bi = not (null bi) ==>
    valid (deleteMin bi)
    where
    _ = bi :: Bimap Int Integer

prop_deleteFindMin_is_valid bi = not (null bi) ==>
    valid (snd $ deleteFindMin bi)
    where
    _ = bi :: Bimap Int Integer

prop_deleteMinR_is_valid bi = not (null bi) ==>
    valid (deleteMinR bi)
    where
    _ = bi :: Bimap Int Integer

prop_deleteFindMinR_is_valid bi = not (null bi) ==>
    valid (snd $ deleteFindMinR bi)
    where
    _ = bi :: Bimap Int Integer

prop_deleteMax_is_valid bi = not (null bi) ==>
    valid (deleteMax bi)
    where
    _ = bi :: Bimap Int Integer

prop_deleteFindMax_is_valid bi = not (null bi) ==>
    valid (snd $ deleteFindMax bi)
    where
    _ = bi :: Bimap Int Integer

prop_deleteMaxR_is_valid bi = not (null bi) ==>
    valid (deleteMaxR bi)
    where
    _ = bi :: Bimap Int Integer

prop_deleteFindMaxR_is_valid bi = not (null bi) ==>
    valid (snd $ deleteFindMaxR bi)
    where
    _ = bi :: Bimap Int Integer