collections-0.3.1: Data/Collections/Properties.hs
{-# OPTIONS_GHC -fglasgow-exts #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Collections
-- Copyright : (c) Jean-Philippe Bernardy, 2006
-- License : BSD3
-- Maintainer : jeanphilippe.bernardy; google mail.
-- Stability : experimental
-- Portability : MPTC, FD, undecidable instances
--
-- The purpose of this module is twofold:
--
-- (1) Check instances of the classes in the collection framework.
--
-- (2) Give those classes more formal semantics.
--
-- Therefore, this acts as a contract between the collections users and implementers.
--
-- Each function in this module returns a list of @(property_name, propterty)@
-- for a given class (or set of classes). Each function is parameterized on the
-- type of
-- the collection to check, so a value witnessing the type must be passed. This
-- value is guaranteed not to be evaluated, so it can always be 'undefined'.
--
-- These properties allow to verify, with a high degree of confidence, that
-- instances of the classes defined in 'Data.Collections' satisfy
-- the prescribed properties.
--
-- You will note that properties depend on the 'Eq' class. This means that
--
-- * properties are verified up-to 'Eq' equivalence.
--
-- * Infinite structures and other @bottom@s are not testable with this module.
--
-- For convenience, this module provides an instance of @'Arbitrary' ('Maybe' a)@.
module Data.Collections.Properties
(
unfoldable_properties,
foldable_properties,
collection_properties,
map_properties,
map_unfold_properties,
set_unfold_properties,
map_fold_properties,
set_fold_properties,
indexed_map_properties,
sequence_properties,
indexed_properties,
indexed_sequence_properties
) where
--
-- The documentation in this module is mostly generated from the function definitions,
-- see tools/AnnotateProps.hs.
-- TODO:
--
-- + interactions with other classes (mainly Functor)
-- + see if prop_foldable could be defined better.
-- + array
import Prelude hiding (null, foldr, lookup, concatMap, concat, and, drop, take, reverse, elem, notElem, all, any, filter)
import Control.Monad
import Data.Collections
import Data.Collections.Foldable as Foldable
import Data.Maybe
import Data.Monoid
import qualified Data.List as List
import Test.QuickCheck
import qualified Data.Collections as C
infix 1 <==>
infix 1 <==
{-
-- no longer needed since this is in quickcheck now
instance Arbitrary a => Arbitrary (Maybe a)
where arbitrary = do test <- arbitrary
if test
then return Nothing
else return Just `ap` arbitrary
coarbitrary Nothing = variant 0
coarbitrary (Just x) = variant 1 . coarbitrary x
-}
instance Show (a->b) where
show _ = "<func>"
-- | Logic equivalence
(<==>) :: Bool -> Bool -> Bool
(<==>) x y = x == y
(<==) = flip (==>)
-- | foldable_properties returns the following properties:
--
-- [/size/]
--
-- > size c == foldr (const (+1)) 0 c
--
-- [/null/]
--
-- > null c <==> all (const False) c
--
-- [/isSingleton/]
--
-- > isSingleton c <==> size c == 1
--
-- [/eq_elem/]
--
-- > c1 == c2 ==> elem x c1 == elem x c2 -- note that the order of folding is not enforced, and that the converse is not true
foldable_properties :: forall c a. (Arbitrary c, Arbitrary a,
Show a, Show c,
Eq c, Eq a,
Foldable c a) => c -> [(Property,String)]
foldable_properties _ = [(property prop_size,"size"), (property prop_null,"null"), (property prop_isSingleton,"isSingleton"), (property prop_eq_elem,"eq_elem")]
where size = C.size :: c -> Int
null = C.null :: c -> Bool
foldr = C.foldr :: (a -> b -> b) -> b -> c -> b
toList = C.toList :: c -> [a]
elem = C.elem :: a -> c -> Bool
prop_size c = size c == foldr (const (+1)) 0 c
prop_null c = null c <==> all (const False) c
prop_isSingleton c = isSingleton c <==> size c == 1
prop_eq_elem c1 c2 x = c1 == c2 ==> elem x c1 == elem x c2 -- note that the order of folding is not enforced, and that the converse is not true
-- | unfoldable_properties returns the following properties:
--
-- [/singleton/]
--
-- > singleton a == insert a empty
--
-- [/insertMany/]
--
-- > insertMany l c == Foldable.foldr insert c l
--
-- [/insertManySorted/]
--
-- > insertManySorted l c == Foldable.foldr insert c l
-- > where l = List.sort l0
unfoldable_properties :: forall c a. (Arbitrary c, Arbitrary a,
Ord a, Show a, Show c,
Eq c, Eq a,
Unfoldable c a) => c -> [(Property,String)]
unfoldable_properties _ = [(property prop_singleton,"singleton"), (property prop_insertMany,"insertMany"), (property prop_insertManySorted,"insertManySorted")]
where empty = C.empty :: c
insert = C.insert :: a -> c -> c
singleton = C.singleton :: a -> c
prop_singleton a = singleton a == insert a empty
prop_insertMany c (l::[a]) = insertMany l c == Foldable.foldr insert c l
prop_insertManySorted c (l0::[a]) = insertManySorted l c == Foldable.foldr insert c l
where l = List.sort l0
-- | collection_properties returns the following properties:
--
-- [/collection/]
--
-- > foldr insert empty c == c
--
-- [/empty/]
--
-- > null empty
--
-- [/insert1/]
--
-- > a `elem` (insert a c) -- insert puts the element in the collection
--
-- [/insert2/]
--
-- > a /= a' ==> (a' `elem` c <== a' `elem` (insert a c)) -- insert does not insert other elements
--
-- [/insert3/]
--
-- > let c' = insert a c in x `elem` c && y `elem` c ==> x `elem` c' || y `elem` c' -- insert alters at most one element
--
-- [/filter/]
--
-- > (a `elem` filter f c) <==> ((a `elem` c) && f a)
collection_properties :: forall c i. (Arbitrary c, Arbitrary i,
Show i, Show c,
Eq c, Eq i,
Collection c i) => c -> [(Property,String)]
collection_properties _ = [(property prop_collection,"collection"), (property prop_empty,"empty"), (property prop_insert1,"insert1"), (property prop_insert2,"insert2"), (property prop_insert3,"insert3"), (property prop_filter,"filter")]
where empty = C.empty :: c
foldr = C.foldr :: (i -> b -> b) -> b -> c -> b
filter = C.filter :: (i -> Bool) -> c -> c
insert = C.insert :: i -> c -> c
prop_collection c = foldr insert empty c == c
prop_empty = null empty
prop_insert1 a c = a `elem` (insert a c) -- insert puts the element in the collection
prop_insert2 a a' c = a /= a' ==> (a' `elem` c <== a' `elem` (insert a c)) -- insert does not insert other elements
prop_insert3 a x y c = let c' = insert a c in x `elem` c && y `elem` c ==> x `elem` c' || y `elem` c' -- insert alters at most one element
--NOTE: This leaves the door open to insert actually 'removing' an element.
prop_filter f c a = (a `elem` filter f c) <==> ((a `elem` c) && f a)
-- | map_properties returns the following properties:
--
-- [/alter/]
--
-- > lookup k (alter f k m) == f (lookup k m)
--
-- [/mapWithKey/]
--
-- > lookup k (mapWithKey f m) == fmap (f k) (lookup k m)
--
-- [/unionWith/]
--
-- > lookup k (unionWith f m1 m2) == case (lookup k m1, lookup k m2) of
-- > (Nothing,Nothing) -> Nothing
-- > (Just x, Nothing) -> Just x
-- > (Nothing,Just x) -> Just x
-- > (Just x, Just y) -> Just (f x y)
--
-- [/intersectionWith/]
--
-- > lookup k (intersectionWith f m1 m2) == case (lookup k m1, lookup k m2) of
-- > (Just x, Just y) -> Just (f x y)
-- > _ -> Nothing
--
-- [/differenceWith/]
--
-- > lookup k (differenceWith f m1 m2) == case (lookup k m1, lookup k m2) of
-- > (Just x, Nothing) -> Just x
-- > (Just x, Just y) -> f x y
-- > (Nothing, _) -> Nothing
--
-- [/isSubmapBy/]
--
-- > isSubmapBy f m1 m2 <==> differenceWith (\x y->if f x y then Nothing else Just v) m1 m2 == mempty
--
-- [/insertWith/]
--
-- > insertWith f k a m == alter (\x -> Just $ case x of {Nothing->a;Just a' -> f a a'}) k m
--
-- [/fromFoldableWith/]
--
-- > fromFoldableWith f l == foldr (uncurry (insertWith f)) mempty l
--
-- [/delete/]
--
-- > delete k m == alter (const Nothing) k m
--
-- [/member/]
--
-- > member k m <==> isJust (lookup k m)
--
-- [/union/]
--
-- > union m1 m2 == unionWith const m1 m2
--
-- [/intersection/]
--
-- > intersection m1 m2 == intersectionWith const m1 m2
--
-- [/difference/]
--
-- > difference m1 m2 == differenceWith (\_ _ -> Nothing) m1 m2
--
-- [/subset/]
--
-- > isSubset m1 m2 <==> isSubmapBy (\_ _ -> True) m1 m2
--
-- [/mempty/]
--
-- > lookup k mempty == Nothing
--
-- [/mappend/]
--
-- > mappend m1 m2 == union m1 m2
--
-- [/eq_lookup/]
--
-- > c1 == c2 ==> lookup x c1 == lookup x c2 -- should really be: c1 == c2 <==> forall x. lookup x c1 == lookup x c2
map_properties :: forall m k v. (Arbitrary m, Arbitrary k, Arbitrary v,
Show k, Show v, Show m,
Eq m, Eq v,
Map m k v
) => m -> [(Property,String)]
map_properties _ = [(property prop_alter,"alter"), (property prop_mapWithKey,"mapWithKey"), (property prop_unionWith,"unionWith"), (property prop_intersectionWith,"intersectionWith"), (property prop_differenceWith,"differenceWith"), (property prop_isSubmapBy,"isSubmapBy"), (property prop_insertWith,"insertWith"), (property prop_fromFoldableWith,"fromFoldableWith"), (property prop_delete,"delete"), (property prop_member,"member"), (property prop_union,"union"), (property prop_intersection,"intersection"), (property prop_difference,"difference"), (property prop_subset,"subset"), (property prop_mempty,"mempty"), (property prop_mappend,"mappend"), (property prop_eq_lookup,"eq_lookup")]
where
-- empty = C.empty :: m
-- singleton = C.singleton :: i -> m
-- size = C.size :: m -> Int
alter = C.alter :: (Maybe v -> Maybe v) -> k -> m -> m
lookup = C.lookup :: k -> m -> Maybe v
isSubset = C.isSubset :: m -> m -> Bool
unionWith = C.unionWith :: (v -> v -> v) -> m -> m -> m
union = C.union :: m -> m -> m
intersectionWith = C.intersectionWith :: (v -> v -> v) -> m -> m -> m
differenceWith = C.differenceWith :: (v -> v -> Maybe v) -> m -> m -> m
fromFoldableWith = C.fromFoldableWith :: (v -> v -> v) -> [(k,v)] -> m
prop_alter f k m = lookup k (alter f k m) == f (lookup k m)
prop_mapWithKey f k m = lookup k (mapWithKey f m) == fmap (f k) (lookup k m)
prop_unionWith f k m1 m2 = lookup k (unionWith f m1 m2) == case (lookup k m1, lookup k m2) of
(Nothing,Nothing) -> Nothing
(Just x, Nothing) -> Just x
(Nothing,Just x) -> Just x
(Just x, Just y) -> Just (f x y)
prop_intersectionWith f k m1 m2 = lookup k (intersectionWith f m1 m2) == case (lookup k m1, lookup k m2) of
(Just x, Just y) -> Just (f x y)
_ -> Nothing
prop_differenceWith f k m1 m2 = lookup k (differenceWith f m1 m2) == case (lookup k m1, lookup k m2) of
(Just x, Nothing) -> Just x
(Just x, Just y) -> f x y
(Nothing, _) -> Nothing
prop_isSubmapBy f m1 m2 v = isSubmapBy f m1 m2 <==> differenceWith (\x y->if f x y then Nothing else Just v) m1 m2 == mempty
prop_insertWith f k a m = insertWith f k a m == alter (\x -> Just $ case x of {Nothing->a;Just a' -> f a a'}) k m
prop_fromFoldableWith f l = fromFoldableWith f l == foldr (uncurry (insertWith f)) mempty l
prop_delete k m = delete k m == alter (const Nothing) k m
prop_member k m = member k m <==> isJust (lookup k m)
prop_union m1 m2 = union m1 m2 == unionWith const m1 m2
prop_intersection m1 m2 = intersection m1 m2 == intersectionWith const m1 m2
prop_difference m1 m2 = difference m1 m2 == differenceWith (\_ _ -> Nothing) m1 m2
prop_subset m1 m2 = isSubset m1 m2 <==> isSubmapBy (\_ _ -> True) m1 m2
prop_mempty k = lookup k mempty == Nothing
prop_mappend m1 m2 = mappend m1 m2 == union m1 m2
prop_eq_lookup x c1 c2 = c1 == c2 ==> lookup x c1 == lookup x c2 -- should really be: c1 == c2 <==> forall x. lookup x c1 == lookup x c2
--prop_eq' c1 c2 = c1 == c2 <==> forAll (\x -> lookup x c1 == lookup x c2)
count :: Foldable f a => (a -> Bool) -> f -> Int
count p = getSum . foldMap (\x->Sum $ if p x then 1 else 0)
-- | map_unfold_properties returns the following properties:
--
-- [/mempty/]
--
-- > mempty == empty
--
-- [/insert/]
--
-- > insert (k,v) m == insertWith (\x _ -> x) k v m
map_unfold_properties :: forall m k v. (Arbitrary m, Arbitrary k, Arbitrary v,
Show k, Show v, Show m,
Eq m, Eq v, Eq k,
Map m k v,
Collection m (k,v)
) => m -> [(Property,String)]
map_unfold_properties _ = [(property prop_mempty,"mempty"), (property prop_insert,"insert")]
where
empty = C.empty :: m
-- singleton = C.singleton :: i -> m
-- size = C.size :: m -> Int
alter = C.alter :: (Maybe v -> Maybe v) -> k -> m -> m
lookup = C.lookup :: k -> m -> Maybe v
insertWith = C.insertWith :: (v -> v -> v) -> k -> v -> m -> m
toList = C.toList :: m -> [(k,v)]
prop_mempty = mempty == empty
prop_insert k v m = insert (k,v) m == insertWith (\x _ -> x) k v m
-- | map_fold_properties returns the following properties:
--
-- [/foldable/]
--
-- > maybeToList (lookup k m) == map snd (filter ((== k) . fst) (toList m))
--
-- [/size/]
--
-- > sizeExcept (alter f k m) == sizeExcept m
-- > where sizeExcept m = size m - maybe 0 (const 1) (lookup k m)
map_fold_properties :: forall m k v. (Arbitrary m, Arbitrary k, Arbitrary v,
Show k, Show v, Show m,
Eq m, Eq v, Eq k,
Map m k v,
Collection m (k,v)
) => m -> [(Property,String)]
map_fold_properties _ = [(property prop_foldable,"foldable"), (property prop_size,"size")]
where
empty = C.empty :: m
-- singleton = C.singleton :: i -> m
-- size = C.size :: m -> Int
alter = C.alter :: (Maybe v -> Maybe v) -> k -> m -> m
lookup = C.lookup :: k -> m -> Maybe v
insertWith = C.insertWith :: (v -> v -> v) -> k -> v -> m -> m
toList = C.toList :: m -> [(k,v)]
prop_foldable k m = maybeToList (lookup k m) == map snd (filter ((== k) . fst) (toList m))
prop_size f k m = sizeExcept (alter f k m) == sizeExcept m
where sizeExcept m = size m - maybe 0 (const 1) (lookup k m)
-- | set_unfold_properties returns the following properties:
--
-- [/mempty/]
--
-- > mempty == empty
--
-- [/insert/]
--
-- > insert k m == insertWith (\x _->x) k () m
set_unfold_properties :: forall m k. (Arbitrary m, Arbitrary k,
Show k, Show m,
Eq m, Eq k,
Map m k (),
Unfoldable m k
) => m -> [(Property,String)]
set_unfold_properties _ = [(property prop_mempty,"mempty"), (property prop_insert,"insert")]
where
empty = C.empty :: m
insertWith = C.insertWith :: (() -> () -> ()) -> k -> () -> m -> m
prop_mempty = mempty == empty
prop_insert k m = insert k m == insertWith (\x _->x) k () m
-- | set_fold_properties returns the following properties:
--
-- [/foldable/]
--
-- > maybeToList (lookup k m) == map (const ()) (filter (== k) (toList m))
--
-- [/size/]
--
-- > sizeExcept (alter f k m) == sizeExcept m
-- > where sizeExcept m = size m - maybe 0 (const 1) (lookup k m)
set_fold_properties :: forall m k. (Arbitrary m, Arbitrary k,
Show k, Show m,
Eq m, Eq k,
Map m k (),
Foldable m k
) => m -> [(Property,String)]
set_fold_properties _ = [(property prop_foldable,"foldable"), (property prop_size,"size")]
where
-- singleton = C.singleton :: i -> m
-- size = C.size :: m -> Int
alter = C.alter :: (Maybe () -> Maybe ()) -> k -> m -> m
member = C.member :: k -> m -> Bool
lookup = C.lookup :: k -> m -> Maybe ()
prop_foldable k m = maybeToList (lookup k m) == map (const ()) (filter (== k) (toList m))
prop_size f k m = sizeExcept (alter f k m) == sizeExcept m
where sizeExcept m = size m - maybe 0 (const 1) (lookup k m)
-- | indexed_properties returns the following properties:
--
-- [/adjust/]
--
-- > k `inDomain` m ==> index k (adjust f k m) == f (index k m)
indexed_properties :: forall m k v. (Arbitrary m, Arbitrary k, Arbitrary v,
Show k, Show v, Show m,
Eq m, Eq v,
Indexed m k v
) => m -> [(Property,String)]
indexed_properties _ = [(property prop_adjust,"adjust")]
where adjust = C.adjust :: (v -> v) -> k -> m -> m
prop_adjust f k m = k `inDomain` m ==> index k (adjust f k m) == f (index k m)
-- | sequence_properties returns the following properties:
--
-- [/fold0/]
--
-- > foldMap f empty == mempty
--
-- [/fold1/]
--
-- > foldMap f (x <| s) == f x `mappend` foldMap f s
--
-- [/fold2/]
--
-- > foldMap f (s |> x) == foldMap f s `mappend` f x
--
-- [/fold3/]
--
-- > foldMap f (s >< t) == foldMap f s `mappend` foldMap f t
--
-- [/front0/]
--
-- > front empty == Nothing
--
-- [/front1/]
--
-- > front (x <| s) == Just (x,s)
--
-- [/front2/]
--
-- > front (s |> x) == case front s of {Nothing -> Just (x, empty); Just (x',s') -> Just (x', s' |> x)}
--
-- [/front3/]
--
-- > front (s >< t) == case front s of {Nothing -> front t; Just (x',s') -> Just (x', s' >< t)}
--
-- [/back0/]
--
-- > back empty == Nothing
--
-- [/back1/]
--
-- > back (s |> x) == Just (s,x)
--
-- [/back2/]
--
-- > back (x <| s) == case back s of {Nothing -> Just (empty, x); Just (s',x') -> Just (x <| s', x')}
--
-- [/back3/]
--
-- > back (t >< s) == case back s of {Nothing -> back t; Just (s',x') -> Just (t >< s', x')}
--
-- [/drop1/]
--
-- > drop 0 s == s
--
-- [/drop2/]
--
-- > n>0 ==> drop (n+1) s == case front (drop n s) of Nothing -> empty; Just (_,s') -> s'
--
-- [/take1/]
--
-- > take 0 s == empty
--
-- [/take2/]
--
-- > n>0 ==> take (n+1) s == case front s of Nothing -> empty; Just (x,s') -> x <| take n s'
--
-- [/reverse/]
--
-- > foldMap f (reverse s) == getDual (foldMap (Dual . f) s)
--
-- [/mempty/]
--
-- > mempty == empty
--
-- [/eq_fold/]
--
-- > s1 == s2 ==> foldMap f s1 == foldMap f s2
sequence_properties :: forall s a . (Arbitrary s, Arbitrary a,
Show s, Show a,
Eq s, Eq a,
Sequence s a
) => s -> [(Property,String)]
sequence_properties _ = [(property prop_fold0,"fold0"), (property prop_fold1,"fold1"), (property prop_fold2,"fold2"), (property prop_fold3,"fold3"), (property prop_front0,"front0"), (property prop_front1,"front1"), (property prop_front2,"front2"), (property prop_front3,"front3"), (property prop_back0,"back0"), (property prop_back1,"back1"), (property prop_back2,"back2"), (property prop_back3,"back3"), (property prop_drop1,"drop1"), (property prop_drop2,"drop2"), (property prop_take1,"take1"), (property prop_take2,"take2"), (property prop_reverse,"reverse"), (property prop_mempty,"mempty"), (property prop_eq_fold,"eq_fold")]
where
empty = C.empty :: s
front = C.front :: s -> Maybe (a,s)
back = C.back :: s -> Maybe (s,a)
-- size = C.size :: s -> Int
drop = C.drop :: Int -> s -> s
take = C.take :: Int -> s -> s
reverse = C.reverse :: s -> s
foldMap :: forall m. Monoid m => (a -> m) -> s -> m
foldMap = C.foldMap
f :: a -> [a] -- testing this single function ensure that fold properties are ok for all monoids and functions
-- (because mappend is associative)
f = singleton
prop_fold0 = foldMap f empty == mempty
prop_fold1 s x = foldMap f (x <| s) == f x `mappend` foldMap f s
prop_fold2 s x = foldMap f (s |> x) == foldMap f s `mappend` f x
prop_fold3 s t = foldMap f (s >< t) == foldMap f s `mappend` foldMap f t
prop_front0 = front empty == Nothing
prop_front1 s x = front (x <| s) == Just (x,s)
prop_front2 s x = front (s |> x) == case front s of {Nothing -> Just (x, empty); Just (x',s') -> Just (x', s' |> x)}
prop_front3 s t = front (s >< t) == case front s of {Nothing -> front t; Just (x',s') -> Just (x', s' >< t)}
prop_back0 = back empty == Nothing
prop_back1 s x = back (s |> x) == Just (s,x)
prop_back2 s x = back (x <| s) == case back s of {Nothing -> Just (empty, x); Just (s',x') -> Just (x <| s', x')}
prop_back3 s t = back (t >< s) == case back s of {Nothing -> back t; Just (s',x') -> Just (t >< s', x')}
prop_drop1 s = drop 0 s == s
prop_drop2 s n = n>0 ==> drop (n+1) s == case front (drop n s) of Nothing -> empty; Just (_,s') -> s'
prop_take1 s = take 0 s == empty
prop_take2 s n = n>0 ==> take (n+1) s == case front s of Nothing -> empty; Just (x,s') -> x <| take n s'
prop_reverse s = foldMap f (reverse s) == getDual (foldMap (Dual . f) s)
prop_mempty = mempty == empty
prop_eq_fold s1 s2 = s1 == s2 ==> foldMap f s1 == foldMap f s2
-- | indexed_sequence_properties returns the following properties:
--
-- [/domain/]
--
-- > k `inDomain` s <==> k >= 0 && k < size s
--
-- [/left1/]
--
-- > k `inDomain` s ==> index (k+1) (x <| s) == index k s
--
-- [/left2/]
--
-- > index 0 (x <| s) == x
--
-- [/right1/]
--
-- > k `inDomain` s ==> index k (s |> x) == index k s
--
-- [/right2/]
--
-- > index (size s) (s |> x) == x
--
-- [/append1/]
--
-- > k `inDomain` t ==> index (k+size s) (s >< t) == index k t
--
-- [/append2/]
--
-- > k `inDomain` s ==> index k (s >< t) == index k s
indexed_sequence_properties :: forall s a . (Arbitrary s, Arbitrary a,
Show s, Show a,
Eq s, Eq a,
Sequence s a,
Indexed s Int a
) => s -> [(Property,String)]
indexed_sequence_properties _ = [(property prop_domain,"domain"), (property prop_left1,"left1"), (property prop_left2,"left2"), (property prop_right1,"right1"), (property prop_right2,"right2"), (property prop_append1,"append1"), (property prop_append2,"append2")]
where
index = C.index :: Int -> s -> a
(<|) = (C.<|) :: a -> s -> s
(|>) = (C.|>) :: s -> a -> s
(><) = (C.><) :: s -> s -> s
inDomain = C.inDomain :: Int -> s -> Bool
prop_domain k s = k `inDomain` s <==> k >= 0 && k < size s
prop_left1 k s x = k `inDomain` s ==> index (k+1) (x <| s) == index k s
prop_left2 s x = index 0 (x <| s) == x
prop_right1 k s x = k `inDomain` s ==> index k (s |> x) == index k s
prop_right2 s x = index (size s) (s |> x) == x
prop_append1 k s t = k `inDomain` t ==> index (k+size s) (s >< t) == index k t
prop_append2 k s t = k `inDomain` s ==> index k (s >< t) == index k s
-- | indexed_map_properties returns the following properties:
--
-- [/domain/]
--
-- > k `inDomain` m <==> k `member` m
--
-- [/index/]
--
-- > case lookup k m of {Just x -> x == index k m; _ -> True}
indexed_map_properties :: forall m k v. (Arbitrary m, Arbitrary k, Arbitrary v,
Show k, Show v, Show m,
Eq m, Eq v,
Map m k v,
Indexed m k v
) => m -> [(Property,String)]
indexed_map_properties _ = [(property prop_domain,"domain"), (property prop_index,"index")]
where
index = C.index :: k -> m -> v
inDomain = C.inDomain :: k -> m -> Bool
prop_domain k m = k `inDomain` m <==> k `member` m
prop_index k m = case lookup k m of {Just x -> x == index k m; _ -> True}