{-# LANGUAGE TemplateHaskell #-}
--
-- Testing binary search trees for key-value associations
--
-- Video: "How to specify it", J. Hughes
-- https://youtu.be/G0NUOst-53U
--
module BSTTests where

import BST
import Test.QuickCheck

-- Arbitrary instance for BSTs
-- generator and shrinking
instance (Ord k, Arbitrary k, Arbitrary v) =>
         Arbitrary (BST k v) where
  arbitrary = do
    kvs <- arbitrary
    return (fromList kvs)
  shrink = shrinkTree

-- shrinking function
shrinkTree :: (Arbitrary v, Arbitrary k) => BST k v -> [BST k v]
shrinkTree Leaf = []
shrinkTree (Branch k v left right)
  = [Leaf, left, right] ++
    [Branch k v left' right | left'<-shrinkTree left] ++
    [Branch k v left right' | right'<-shrinkTree right] ++
    -- [Branch k' v left right | k' <- shrink k] ++  -- WRONG
    [Branch k v' left right | v'<-shrink v]


-- * properties

type Key = Int
type Val = Int
type Tree = BST Key Val

-- | check the search tree invariant
-- on every branch:
-- the key is smaller than every key on the right
-- and greater than every key on the left
-- NB: this test the simplest specification but inefficient
-- (quadratic on the tree size)
--
valid :: Tree -> Bool
valid Leaf
  = True
valid (Branch k v left right)
  = all (<k) (keys left) &&
    all (k<) (keys right) &&
    valid left && valid right


-- * test the generator
prop_generator_valid :: Tree -> Bool
prop_generator_valid t = valid t


-- * test the shrinking function
prop_shrink_valid :: Tree -> Bool
prop_shrink_valid t = all valid (shrink t)


prop_insert :: Key -> Val -> Tree -> Bool
prop_insert k v t = valid (insert k v t)

prop_delete :: Key -> Tree -> Bool
prop_delete k t = valid (delete k t)

prop_find_occurs :: Key -> Val -> Tree -> Bool
prop_find_occurs k v t
  = find k (insert k v t) ==  Just v  -- occurs by construction

prop_find_not_occurs :: Key -> Tree -> Bool
prop_find_not_occurs k t
  = find k (delete k t) == Nothing   -- doesn't occur by construction


-- * test postconditions

-- * insert postcondition
prop_insert_pos :: Key -> Key -> Val -> Tree -> Property
prop_insert_pos k' k v t =
  find k' (insert k v t)
  ===
  if k == k' then Just v else find k' t


-- * delete postcondition
prop_delete_pos :: Key -> Val -> Tree -> Property
prop_delete_pos k' k t
  = find k' (delete k t)
    ===
    if k==k' then Nothing else find k' t

-------
return []
runTests = $quickCheckAll