module StoreCheck where

import Store    
import Test.QuickCheck

instance (Eq a, Arbitrary a, Arbitrary b)=> Arbitrary (Store a b) where
  arbitrary = do
   size <- choose (0, 20)
   a <- vector size
   b <- vector size
   return (foldl (\s (a, v)-> upd s a v) empty (zip a b))

prop_read_empty :: Int-> Bool
prop_read_empty a = 
  get (empty :: Store Int Int) a == Nothing 
 
prop_read_write :: Store Int Int-> Int-> Int-> Bool
prop_read_write s a v= 
  get (upd s a v) a == Just v

prop_read_write_other :: 
  Store Int Int-> Int-> Int-> Int-> Property

prop_read_write_other s a v b= 
  a /= b ==> get (upd s a v) b == get s b

prop_write_write :: Store Int Int-> Int-> Int-> Int-> Bool
prop_write_write s a v w =
  upd (upd s a v) a w == upd s a w

prop_write_other :: 
  Store Int Int-> Int-> Int-> Int-> Int-> Property        
prop_write_other s a v b w =
  a /= b ==> upd (upd s a v) b w == upd (upd s b w) a v