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      =  find x l
  | a < x      =  find x r
  | otherwise  =  True

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 (insert x l) r
  | a < x      =  Node a l (insert x r)
  | otherwise  =  Node a l r

delete :: Ord a => a -> Tree a -> Tree a
delete x Empty = Empty
delete x (Node a l r)
  | x < a      =  Node a (delete x l) r
  | a < x      =  Node a l (delete x r)
  | otherwise  =  combine l 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') = delMin r

-- delMin t = (leftmost/minimal element of t, t without that element)
delMin :: Tree a -> (a, Tree a)
delMin (Node a Empty r)  = (a, r)
delMin (Node a l     r)  = (m, Node a l' r)  where (m,l') = delMin l


-- for QuickCheck: test data generator for Trees
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))]

prop_insert :: Int -> Int -> Tree Int -> Bool
prop_insert x y t =
  find x (insert y t) == (x == y || find x t)

-- Note that Int can be problematic:
prop_delete :: Int -> Int -> Tree Int -> Bool
prop_delete x y t =
  find x (delete y t) == (x /= y && find x t)