import SparseCheck

-- Binary search trees

data Tree a = Empty | Node a (Tree a) (Tree a)
  deriving Show

del a Empty = Empty
del a (Node b t0 t1)
  | a < b = Node b (del a t0) t1
  | a > b = Node b t0 (del a t1)
  | otherwise = ext t0 t1

ext Empty t = t
ext (Node a t0 t1) t = Node a t0 (ext t1 t)

ord t = ord' (const True) t
  where
    ord' p Empty = True
    ord' p (Node a t0 t1) = p a && ord' (<= a) t0
                                && ord' (>= a) t1

-- Prepare data type for SparseCheck

(empty :- node) = datatype (ctr0 Empty \/ ctr3 Node)

instance Convert a => Convert (Tree a) where
  term Empty = empty
  term (Node a t0 t1) = node (term a) (term t0) (term t1)
  unterm = converter (conv0 Empty -+- conv3 Node)

-- Property

ordered t = ord (\a -> return ()) t
  where
    ord p t = caseOf t alts where
                alts (a, t0, t1) =
                      empty :-> return ()
                  :|: node a t0 t1 :-> p a & ord (|<=| a) t0
                                           & ord (|>=| a) t1

gen_ordDel a t = ordered t

prop_ordDel :: Int -> Tree Int -> Bool
prop_ordDel a t = lower ordered (del a t)

check_ordDel n = check2 n gen_ordDel prop_ordDel