import Control.Monad
import Test.QuickCheck

-- Example: Binary tree
data Tree a = Empty | Node a (Tree a) (Tree a)
              deriving (Eq, Show)

-- assumption: < is a linear ordering

find :: Ord a => a -> Tree a -> Bool
find _ Empty  =  False
find x (Node a l r)
  | x == a     =  True
  | x < a      =  find x l
  | otherwise  =  find x r

insert :: Ord a => a -> Tree a -> Tree a
insert x Empty  =  Node x Empty Empty
insert x (Node a l r)
  | x == a     =  Node a l r
  | x < a      =  Node a (insert x l) r
  | otherwise  =  Node a l (insert x r)

delete :: Ord a => a -> Tree a -> Tree a
delete x Empty = Empty
delete x (Node a l r)
  | x == a     =  combine l r
  | x < a      =  Node a (delete x l) r
  | otherwise  =  Node a l (delete x r)

combine :: Tree a -> Tree a -> Tree a
combine Empty r  =  r
combine l Empty  =  l
combine l r      =  Node m l r'  where (m,r') = delL r

delL :: Tree a -> (a, Tree a)
delL (Node a Empty r)  = (a, r)
delL (Node a l     r)  = (m, Node a l' r)  where (m,l') = delL l

-- allow QuickCheck to generate arbitrary values of type Tree
instance Arbitrary a => Arbitrary (Tree a) where
  arbitrary = sized tree
    where
    tree 0 = return Empty
    tree n | n > 0 = oneof [return Empty,
      liftM3 Node arbitrary (tree (n `div` 2)) (tree (n `div` 2))]

-- True or False?
prop_find_insert :: Int -> Int -> Tree Int -> Bool
prop_find_insert x y t =
  find x (insert y t) == (x==y || find x t)

-- True or False?
prop_find_delete :: Int -> Int -> Tree Int -> Bool
prop_find_delete x y t =
  find x (delete y t) == (x /= y && find x t)