{-# 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}