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