RBTreeTest.hs

{-# LANGUAGE TemplateHaskell #-}
module RBTreeTest where

import           RBTree

import           Test.Target

type E = Char
type T = RBTree E

-- liquidTests :: [(String, Test)]
liquidTests = [ ('add,    T (add :: E -> T -> T))
              , ('remove, T (remove :: E -> T -> T))
              ]

-- liquidTests_bad :: [(String, Test)]
liquidTests_bad = [ ('add,    T (add_bad :: E -> T -> T))
                  , ('remove, T (remove_bad :: E -> T -> T))
                  ]

remove_bad x t = makeBlack (del_bad x t)

del_bad x Leaf           = Leaf
del_bad x (Node _ y a b) = case compare x y of
   EQ -> append_bad y a b
   LT -> case a of
           Leaf         -> Node R y Leaf b
           Node B _ _ _ -> lbalS y (del_bad x a) b
           _            -> let t = Node R y (del_bad x a) b in t
   GT -> case b of
           Leaf         -> Node R y a Leaf
           Node B _ _ _ -> rbalS y a (del_bad x b)
           _            -> Node R y a (del_bad x b)

append_bad :: a -> RBTree a -> RBTree a -> RBTree a
append_bad _ Leaf r                               = r
append_bad _ l Leaf                               = l
append_bad piv (Node R lx ll lr) (Node R rx rl rr)  = case append_bad piv lr rl of
                                                    --Node R x lr' rl' -> Node R x (Node R lx ll lr') (Node R rx rl' rr)
                                                    lrl              -> Node R lx ll (Node R rx lrl rr)
append_bad piv (Node B lx ll lr) (Node B rx rl rr)  = case append_bad piv lr rl of
                                                    --Node R x lr' rl' -> Node R x (Node B lx ll lr') (Node B rx rl' rr)
                                                    lrl              -> lbalS lx ll (Node B rx lrl rr)
append_bad piv l@(Node B _ _ _) (Node R rx rl rr)   = Node R rx (append_bad piv l rl) rr
append_bad piv l@(Node R lx ll lr) r@(Node B _ _ _) = Node R lx ll (append_bad piv lr r)

add_bad x s = ins x s