binarytree.hs

import QuickSpec hiding (insert)
import Test.QuickCheck hiding (insert,(==>))
import Data.Function (on)
import Data.List (isSubsequenceOf)

data BT a = Null | Fork (BT a) a (BT a)
            deriving (Show)

instance (Eq a, Ord a) => Eq (BT a) where
  (==) = (==) `on` toList

instance (Eq a, Ord a) => Ord (BT a) where
  (<=) = isSubsequenceOf `on` toList

insert :: Ord a => a -> BT a -> BT a
insert x Null             = Fork Null x Null
insert x t@(Fork t1 y t2) = case compare x y of
                            LT -> Fork (insert x t1) y t2
                            EQ -> t
                            GT -> Fork t1 y (insert x t2)

delete :: Ord a => a -> BT a -> BT a
delete x Null = Null
delete x t@(Fork t1 y t2) = case compare x y of
                            LT -> Fork (delete x t1) y t2
                            EQ -> graft t1 t2
                            GT -> Fork t1 y (delete x t2)

isIn :: Ord a => a -> BT a -> Bool
isIn x t = x `elem` toList t

graft :: Ord a => BT a -> BT a -> BT a
graft Null           t = t
graft (Fork t1 x t2) t = Fork t1 x (graft t2 t)

toList :: Ord a => BT a -> [a]
toList Null           = []
toList (Fork t1 x t2) = toList t1 ++ [x] ++ toList t2

fromList :: Ord a => [a] -> BT a
fromList = foldr insert Null

{-
fromList :: Ord a => [a] -> BT a
fromList [] = Null
fromList xs = Fork (fromList ys) x (fromList zs)
  where
  (x:ys,zs) = deal xs

deal :: [a] -> ([a],[a])
deal []     = ([],[])
deal (x:xs) = (x:ys,zs)
  where
  (zs,ys) = deal xs
-}

isSearch :: Ord a => BT a -> Bool
isSearch = strictlyOrdered . toList

ordered :: Ord a => [a] -> Bool
ordered [] = True
ordered xs = and (zipWith (<=) xs $ tail xs)

strictlyOrdered :: Ord a => [a] -> Bool
strictlyOrdered [] = True
strictlyOrdered xs = and (zipWith (<) xs $ tail xs)

-- | truncate tiers of values in the presence of one empty size
--
-- truncateT [[x,y],[z,w],[],[],[],...] == [[x,y],[z,w]]
truncateT :: [[a]] -> [[a]]
truncateT ([]:xss) = []
truncateT (xs:xss) = xs:truncateT xss
truncateT xss = xss

instance (Ord a, Arbitrary a) => Arbitrary (BT a) where
  arbitrary = sized arbtree
    where
    arbtree 0 = return Null
    arbtree n = oneof
      [ return Null
      , (Fork <$> arbtree (n `div` 2) <*> arbitrary <*> arbtree (n `div` 2))
        `suchThat` isSearch
      ]

type Item = Int

main = quickSpec signature
  { maxTermSize = Just 9
  , maxTests = Just 2000
-- the maximum number of tests above needs to be 2000,
-- otherwise the law `isIn x t1 ==> isIn x (insert y t1) = True`
-- does not appear in the output (which is mainly what I want with this
-- benchmark).  Even so, it works only about 2/3 of the time.
  , constants =
      [ constant "Null" (Null :: BT Item)
      , constant "insert" (insert :: Item -> BT Item -> BT Item)
      , constant "delete" (delete :: Item -> BT Item -> BT Item)
      , constant "isIn" (isIn :: Item -> BT Item -> Bool)
--    , constant "<="  ((<=) :: Item -> Item -> Bool)
--    , constant "<="  ((<=) :: BT Item -> BT Item -> Bool)
--    , constant "/="  ((/=) :: Item -> Item -> Bool)
--    , constant "ordered" (ordered :: [Item] -> Bool)
--    , constant "strictlyOrdered" (strictlyOrdered :: [Item] -> Bool)
--    , constant "toList" (toList :: BT Item -> [Item])
--    , constant "fromList" (fromList :: [Item] -> BT Item)
--    , constant "isSearch" (isSearch :: BT Item -> Bool)
--    , constant "[]" ([]::[Item])
      , constant "==>" ((==>) :: Bool -> Bool -> Bool)
      , constant "True" True
      , constant "False" False
      ]
  , instances =
      [ baseType (undefined :: BT Item)
      , baseTypeNames ["t1","t2","t3"] (undefined :: BT Item)
      ]
  }

(==>) :: Bool -> Bool -> Bool
False ==> _ = True
True  ==> p = p