{-# LANGUAGE ScopedTypeVariables, TemplateHaskell #-}
module Main where
--------------------------------------------------------------------------
-- imports
import Test.QuickCheck
import Data.List
( sort
, (\\)
)
import Control.Monad
( liftM
, liftM2
)
--------------------------------------------------------------------------
-- skew heaps
data Heap a
= Node a (Heap a) (Heap a)
| Empty
deriving ( Eq, Ord, Show )
empty :: Heap a
empty = Empty
isEmpty :: Heap a -> Bool
isEmpty Empty = True
isEmpty _ = False
unit :: a -> Heap a
unit x = Node x empty empty
size :: Heap a -> Int
size Empty = 0
size (Node _ h1 h2) = 1 + size h1 + size h2
insert :: Ord a => a -> Heap a -> Heap a
insert x h = unit x `merge` h
removeMin :: Ord a => Heap a -> Maybe (a, Heap a)
removeMin Empty = Nothing
removeMin (Node x h1 h2) = Just (x, h1 `merge` h2)
merge :: Ord a => Heap a -> Heap a -> Heap a
h1 `merge` Empty = h1
Empty `merge` h2 = h2
h1@(Node x h11 h12) `merge` h2@(Node y h21 h22)
| x <= y = Node x (h12 `merge` h2) h11
| otherwise = Node y (h22 `merge` h1) h21
fromList :: Ord a => [a] -> Heap a
fromList xs = merging [ unit x | x <- xs ]
where
merging [] = empty
merging [h] = h
merging hs = merging (sweep hs)
sweep [] = []
sweep [h] = [h]
sweep (h1:h2:hs) = (h1 `merge` h2) : sweep hs
toList :: Heap a -> [a]
toList h = toList' [h]
where
toList' [] = []
toList' (Empty : hs) = toList' hs
toList' (Node x h1 h2 : hs) = x : toList' (h1:h2:hs)
toSortedList :: Ord a => Heap a -> [a]
toSortedList Empty = []
toSortedList (Node x h1 h2) = x : toList (h1 `merge` h2)
--------------------------------------------------------------------------
-- specification
invariant :: Ord a => Heap a -> Bool
invariant Empty = True
invariant (Node x h1 h2) = x <=? h1 && x <=? h2 && invariant h1 && invariant h2
(<=?) :: Ord a => a -> Heap a -> Bool
x <=? Empty = True
x <=? Node y _ _ = x <= y
(==?) :: Ord a => Heap a -> [a] -> Bool
h ==? xs = invariant h && sort (toList h) == sort xs
--------------------------------------------------------------------------
-- properties
prop_Empty =
empty ==? ([] :: [Int])
prop_IsEmpty (h :: Heap Int) =
isEmpty h == null (toList h)
prop_Unit (x :: Int) =
unit x ==? [x]
prop_Size (h :: Heap Int) =
size h == length (toList h)
prop_Insert x (h :: Heap Int) =
insert x h ==? (x : toList h)
prop_RemoveMin (h :: Heap Int) =
cover (size h > 1) 80 "non-trivial" $
case removeMin h of
Nothing -> h ==? []
Just (x,h') -> x == minimum (toList h) && h' ==? (toList h \\ [x])
prop_Merge h1 (h2 :: Heap Int) =
(h1 `merge` h2) ==? (toList h1 ++ toList h2)
prop_FromList (xs :: [Int]) =
fromList xs ==? xs
prop_ToSortedList (h :: Heap Int) =
h ==? xs && xs == sort xs
where
xs = toSortedList h
--------------------------------------------------------------------------
-- generators
instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where
arbitrary = sized (arbHeap Nothing)
where
arbHeap mx n =
frequency $
[ (1, return Empty) ] ++
[ (7, do my <- arbitrary `suchThatMaybe` ((>= mx) . Just)
case my of
Nothing -> return Empty
Just y -> liftM2 (Node y) arbHeap2 arbHeap2
where arbHeap2 = arbHeap (Just y) (n `div` 2))
| n > 0
]
--------------------------------------------------------------------------
-- main
return []
main = $quickCheckAll
--------------------------------------------------------------------------
-- the end.
{-
shrink Empty = []
shrink (Node x h1 h2) =
[ h1, h2 ]
++ [ Node x h1' h2 | h1' <- shrink h1, x <=? h1' ]
++ [ Node x h1 h2' | h2' <- shrink h2, x <=? h2' ]
++ [ Node x' h1 h2 | x' <- shrink x, x' <=? h1, x' <=? h2 ]
-}
-- toSortedList (Node x h1 h2) = x : toSortedList (h1 `merge` h2)
{-
prop_HeapIsNotSorted (h :: Heap Int) =
expectFailure $
toList h == toSortedList h
-}