1{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, GADTs #-} 2module Main where 3 4-------------------------------------------------------------------------- 5-- imports 6 7import Test.QuickCheck 8import Test.QuickCheck.Poly 9 10import Data.List 11 ( sort 12 , nub 13 , (\\) 14 ) 15 16import Data.Maybe 17 ( fromJust 18 ) 19 20import Control.Monad 21 ( liftM 22 , liftM2 23 ) 24 25-------------------------------------------------------------------------- 26-- skew heaps 27 28data Heap a 29 = Node a (Heap a) (Heap a) 30 | Nil 31 deriving ( Eq, Ord, Show ) 32 33empty :: Heap a 34empty = Nil 35 36isEmpty :: Heap a -> Bool 37isEmpty Nil = True 38isEmpty _ = False 39 40unit :: a -> Heap a 41unit x = Node x empty empty 42 43size :: Heap a -> Int 44size Nil = 0 45size (Node _ h1 h2) = 1 + size h1 + size h2 46 47insert :: Ord a => a -> Heap a -> Heap a 48insert x h = unit x `merge` h 49 50removeMin :: Ord a => Heap a -> Maybe (a, Heap a) 51removeMin Nil = Nothing 52removeMin (Node x h1 h2) = Just (x, h1 `merge` h2) 53 54merge :: Ord a => Heap a -> Heap a -> Heap a 55h1 `merge` Nil = h1 56Nil `merge` h2 = h2 57h1@(Node x h11 h12) `merge` h2@(Node y h21 h22) 58 | x <= y = Node x (h12 `merge` h2) h11 59 | otherwise = Node y (h22 `merge` h1) h21 60 61fromList :: Ord a => [a] -> Heap a 62fromList xs = merging [ unit x | x <- xs ] [] 63 where 64 merging [] [] = empty 65 merging [p] [] = p 66 merging (p:q:ps) qs = merging ps ((p`merge`q):qs) 67 merging ps qs = merging (ps ++ reverse qs) [] 68 69toList :: Heap a -> [a] 70toList h = toList' [h] 71 where 72 toList' [] = [] 73 toList' (Nil : hs) = toList' hs 74 toList' (Node x h1 h2 : hs) = x : toList' (h1:h2:hs) 75 76toSortedList :: Ord a => Heap a -> [a] 77toSortedList Nil = [] 78toSortedList (Node x h1 h2) = x : toSortedList (h1 `merge` h2) 79 80-------------------------------------------------------------------------- 81-- heap programs 82 83data HeapP a 84 = Empty 85 | Unit a 86 | Insert a (HeapP a) 87 | SafeRemoveMin (HeapP a) 88 | Merge (HeapP a) (HeapP a) 89 | FromList [a] 90 deriving (Show) 91 92safeRemoveMin :: Ord a => Heap a -> Heap a 93safeRemoveMin h = case removeMin h of 94 Nothing -> empty -- arbitrary choice 95 Just (_,h) -> h 96 97heap :: Ord a => HeapP a -> Heap a 98heap Empty = empty 99heap (Unit x) = unit x 100heap (Insert x p) = insert x (heap p) 101heap (SafeRemoveMin p) = safeRemoveMin (heap p) 102heap (Merge p q) = heap p `merge` heap q 103heap (FromList xs) = fromList xs 104 105instance (Ord a, Arbitrary a) => Arbitrary (HeapP a) where 106 arbitrary = sized arbHeapP 107 where 108 arbHeapP s = 109 frequency 110 [ (1, do return Empty) 111 , (1, do x <- arbitrary 112 return (Unit x)) 113 , (s, do x <- arbitrary 114 p <- arbHeapP s1 115 return (Insert x p)) 116 , (s, do p <- arbHeapP s1 117 return (SafeRemoveMin p)) 118 , (s, do p <- arbHeapP s2 119 q <- arbHeapP s2 120 return (Merge p q)) 121 , (1, do xs <- arbitrary 122 return (FromList xs)) 123 ] 124 where 125 s1 = s-1 126 s2 = s`div`2 127 128 129 shrink Empty = [] 130 shrink (Unit x) = [ Unit x' | x' <- shrink x ] 131 shrink (FromList xs) = [ Unit x | x <- xs ] 132 ++ [ FromList xs' | xs' <- shrink xs ] 133 shrink p = 134 [ FromList (toList (heap p)) ] ++ 135 case p of 136 Insert x p -> [ p ] 137 ++ [ Insert x p' | p' <- shrink p ] 138 ++ [ Insert x' p | x' <- shrink x ] 139 SafeRemoveMin p -> [ p ] 140 ++ [ SafeRemoveMin p' | p' <- shrink p ] 141 Merge p q -> [ p, q ] 142 ++ [ Merge p' q | p' <- shrink p ] 143 ++ [ Merge p q' | q' <- shrink q ] 144 145data HeapPP a = HeapPP (HeapP a) (Heap a) 146 deriving (Show) 147 148instance (Ord a, Arbitrary a) => Arbitrary (HeapPP a) where 149 arbitrary = 150 do p <- arbitrary 151 return (HeapPP p (heap p)) 152 153 shrink (HeapPP p _) = 154 [ HeapPP p' (heap p') | p' <- shrink p ] 155 156-------------------------------------------------------------------------- 157-- properties 158 159data Context a where 160 Context :: Eq b => (Heap a -> b) -> Context a 161 162instance (Ord a, Arbitrary a) => Arbitrary (Context a) where 163 arbitrary = 164 do f <- sized arbContext 165 let vec h = (size h, toSortedList h, isEmpty h) 166 return (Context (vec . f)) 167 where 168 arbContext s = 169 frequency 170 [ (1, do return id) 171 , (s, do x <- arbitrary 172 f <- arbContext (s-1) 173 return (insert x . f)) 174 , (s, do f <- arbContext (s-1) 175 return (safeRemoveMin . f)) 176 , (s, do HeapPP _ h <- arbitrary 177 f <- arbContext (s`div`2) 178 elements [ (h `merge`) . f, (`merge` h) . f ]) 179 ] 180 181instance Show (Context a) where 182 show _ = "*" 183 184(=~) :: Heap Char -> Heap Char -> Property 185--h1 =~ h2 = sort (toList h1) == sort (toList h2) 186--h1 =~ h2 = property (nub (sort (toList h1)) == nub (sort (toList h2))) -- bug! 187h1 =~ h2 = property (\(Context c) -> c h1 == c h2) 188 189{- 190The normal form is: 191 192 insert x1 (insert x2 (... empty)...) 193 194where x1 <= x2 <= ... 195-} 196 197-- heap creating operations 198 199prop_Unit x = 200 unit x =~ insert x empty 201 202prop_RemoveMin_Empty = 203 removeMin (empty :: Heap OrdA) == Nothing 204 205prop_RemoveMin_Insert1 x = 206 removeMin (insert x empty :: Heap OrdA) == Just (x, empty) 207 208prop_RemoveMin_Insert2 x y (HeapPP _ h) = 209 removeMin (insert x (insert y h)) ==~ 210 (insert (max x y) `maph` removeMin (insert (min x y) h)) 211 where 212 f `maph` Just (x,h) = Just (x, f h) 213 f `maph` Nothing = Nothing 214 215 Nothing ==~ Nothing = property True 216 Just (x,h1) ==~ Just (y,h2) = x==y .&&. h1 =~ h2 217 218prop_InsertSwap x y (HeapPP _ h) = 219 insert x (insert y h) =~ insert y (insert x h) 220 221prop_MergeInsertLeft x (HeapPP _ h1) (HeapPP _ h2) = 222 (insert x h1 `merge` h2) =~ insert x (h1 `merge` h2) 223 224prop_MergeInsertRight x (HeapPP _ h1) (HeapPP _ h2) = 225 (h1 `merge` insert x h2) =~ insert x (h1 `merge` h2) 226 227-- heap observing operations 228 229prop_Size_Empty = 230 size empty == 0 231 232prop_Size_Insert x (HeapPP _ (h :: Heap OrdA)) = 233 size (insert x h) == 1 + size h 234 235prop_ToList_Empty = 236 toList empty == ([] :: [OrdA]) 237 238prop_ToList_Insert x (HeapPP _ (h :: Heap OrdA)) = 239 sort (toList (insert x h)) == sort (x : toList h) 240 241prop_ToSortedList (HeapPP _ (h :: Heap OrdA)) = 242 toSortedList h == sort (toList h) 243 244-------------------------------------------------------------------------- 245-- main 246 247return [] 248main = $(quickCheckAll) 249 250-------------------------------------------------------------------------- 251-- the end. 252 253 254 255