Portability | MPTC, FD, undecidable instances |
---|---|
Stability | experimental |
Maintainer | jeanphilippe.bernardy; google mail. |
The purpose of this module is twofold:
- Check instances of the classes in the collection framework.
- 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.
- 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)]
- foldable_properties :: forall c a. (Arbitrary c, Arbitrary a, Show a, Show c, Eq c, Eq a, Foldable c a) => c -> [(Property, String)]
- collection_properties :: forall c i. (CoArbitrary i, Arbitrary c, Arbitrary i, Show i, Show c, Eq c, Eq i, Collection c i) => c -> [(Property, String)]
- map_properties :: forall m k v. (CoArbitrary v, CoArbitrary k, Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Map m k v) => m -> [(Property, String)]
- 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)]
- 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)]
- map_fold_properties :: forall m k v. (CoArbitrary 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)]
- 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)]
- 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)]
- sequence_properties :: forall s a. (Arbitrary s, Arbitrary a, Show s, Show a, Eq s, Eq a, Sequence s a) => s -> [(Property, String)]
- indexed_properties :: forall m k v. (CoArbitrary 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_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)]
Documentation
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)]Source
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
foldable_properties :: forall c a. (Arbitrary c, Arbitrary a, Show a, Show c, Eq c, Eq a, Foldable c a) => c -> [(Property, String)]Source
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
collection_properties :: forall c i. (CoArbitrary i, Arbitrary c, Arbitrary i, Show i, Show c, Eq c, Eq i, Collection c i) => c -> [(Property, String)]Source
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)
map_properties :: forall m k v. (CoArbitrary v, CoArbitrary k, Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Map m k v) => m -> [(Property, String)]Source
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
- isProperSubmapBy
isProperSubmapBy f m1 m2 <==> isSubmapBy f m1 m2 && m1 /= m2
- 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
- properSubset
isProperSubset m1 m2 <==> isProperSubmapBy (\_ _ -> 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_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)]Source
map_unfold_properties returns the following properties:
- mempty
mempty == empty
- insert
insert (k,v) m == insertWith (\x _ -> x) k v 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)]Source
set_unfold_properties returns the following properties:
- mempty
mempty == empty
- insert
insert k m == insertWith (\x _->x) k () m
map_fold_properties :: forall m k v. (CoArbitrary 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)]Source
map_fold_properties returns the following properties:
- foldable
maybeToList (lookup k m) == map snd (List.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)
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)]Source
set_fold_properties returns the following properties:
- foldable
maybeToList (lookup k m) == map (const ()) (List.filter (== k) (toList m))
- size
sizeExcept (alter f k m) == sizeExcept m where sizeExcept m = size m - maybe 0 (const 1) (lookup k m)
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)]Source
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}
sequence_properties :: forall s a. (Arbitrary s, Arbitrary a, Show s, Show a, Eq s, Eq a, Sequence s a) => s -> [(Property, String)]Source
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
indexed_properties :: forall m k v. (CoArbitrary v, Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Indexed m k v) => m -> [(Property, String)]Source
indexed_properties returns the following properties:
- adjust
k `inDomain` m ==> index k (adjust f k m) == f (index k m)
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)]Source
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