{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, GADTs #-} module Main where -------------------------------------------------------------------------- -- imports import Test.QuickCheck import Test.QuickCheck.Poly import Data.List ( sort , nub , (\\) ) import Data.Maybe ( fromJust ) import Control.Monad ( liftM , liftM2 ) -------------------------------------------------------------------------- -- skew heaps data Heap a = Node a (Heap a) (Heap a) | Nil deriving ( Eq, Ord, Show ) empty :: Heap a empty = Nil isEmpty :: Heap a -> Bool isEmpty Nil = True isEmpty _ = False unit :: a -> Heap a unit x = Node x empty empty size :: Heap a -> Int size Nil = 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 Nil = Nothing removeMin (Node x h1 h2) = Just (x, h1 `merge` h2) merge :: Ord a => Heap a -> Heap a -> Heap a h1 `merge` Nil = h1 Nil `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 [p] [] = p merging (p:q:ps) qs = merging ps ((p`merge`q):qs) merging ps qs = merging (ps ++ reverse qs) [] toList :: Heap a -> [a] toList h = toList' [h] where toList' [] = [] toList' (Nil : hs) = toList' hs toList' (Node x h1 h2 : hs) = x : toList' (h1:h2:hs) toSortedList :: Ord a => Heap a -> [a] toSortedList Nil = [] toSortedList (Node x h1 h2) = x : toSortedList (h1 `merge` h2) -------------------------------------------------------------------------- -- heap programs data HeapP a = Empty | Unit a | Insert a (HeapP a) | SafeRemoveMin (HeapP a) | Merge (HeapP a) (HeapP a) | FromList [a] deriving (Show) safeRemoveMin :: Ord a => Heap a -> Heap a safeRemoveMin h = case removeMin h of Nothing -> empty -- arbitrary choice Just (_,h) -> h heap :: Ord a => HeapP a -> Heap a heap Empty = empty heap (Unit x) = unit x heap (Insert x p) = insert x (heap p) heap (SafeRemoveMin p) = safeRemoveMin (heap p) heap (Merge p q) = heap p `merge` heap q heap (FromList xs) = fromList xs instance (Ord a, Arbitrary a) => Arbitrary (HeapP a) where arbitrary = sized arbHeapP where arbHeapP s = frequency [ (1, do return Empty) , (1, do x <- arbitrary return (Unit x)) , (s, do x <- arbitrary p <- arbHeapP s1 return (Insert x p)) , (s, do p <- arbHeapP s1 return (SafeRemoveMin p)) , (s, do p <- arbHeapP s2 q <- arbHeapP s2 return (Merge p q)) , (1, do xs <- arbitrary return (FromList xs)) ] where s1 = s-1 s2 = s`div`2 shrink Empty = [] shrink (Unit x) = [ Unit x' | x' <- shrink x ] shrink (FromList xs) = [ Unit x | x <- xs ] ++ [ FromList xs' | xs' <- shrink xs ] shrink p = [ FromList (toList (heap p)) ] ++ case p of Insert x p -> [ p ] ++ [ Insert x p' | p' <- shrink p ] ++ [ Insert x' p | x' <- shrink x ] SafeRemoveMin p -> [ p ] ++ [ SafeRemoveMin p' | p' <- shrink p ] Merge p q -> [ p, q ] ++ [ Merge p' q | p' <- shrink p ] ++ [ Merge p q' | q' <- shrink q ] data HeapPP a = HeapPP (HeapP a) (Heap a) deriving (Show) instance (Ord a, Arbitrary a) => Arbitrary (HeapPP a) where arbitrary = do p <- arbitrary return (HeapPP p (heap p)) shrink (HeapPP p _) = [ HeapPP p' (heap p') | p' <- shrink p ] -------------------------------------------------------------------------- -- properties data Context a where Context :: Eq b => (Heap a -> b) -> Context a instance (Ord a, Arbitrary a) => Arbitrary (Context a) where arbitrary = do f <- sized arbContext let vec h = (size h, toSortedList h, isEmpty h) return (Context (vec . f)) where arbContext s = frequency [ (1, do return id) , (s, do x <- arbitrary f <- arbContext (s-1) return (insert x . f)) , (s, do f <- arbContext (s-1) return (safeRemoveMin . f)) , (s, do HeapPP _ h <- arbitrary f <- arbContext (s`div`2) elements [ (h `merge`) . f, (`merge` h) . f ]) ] instance Show (Context a) where show _ = "*" (=~) :: Heap Char -> Heap Char -> Property --h1 =~ h2 = sort (toList h1) == sort (toList h2) --h1 =~ h2 = property (nub (sort (toList h1)) == nub (sort (toList h2))) -- bug! h1 =~ h2 = property (\(Context c) -> c h1 == c h2) {- The normal form is: insert x1 (insert x2 (... empty)...) where x1 <= x2 <= ... -} -- heap creating operations prop_Unit x = unit x =~ insert x empty prop_RemoveMin_Empty = removeMin (empty :: Heap OrdA) == Nothing prop_RemoveMin_Insert1 x = removeMin (insert x empty :: Heap OrdA) == Just (x, empty) prop_RemoveMin_Insert2 x y (HeapPP _ h) = removeMin (insert x (insert y h)) ==~ (insert (max x y) `maph` removeMin (insert (min x y) h)) where f `maph` Just (x,h) = Just (x, f h) f `maph` Nothing = Nothing Nothing ==~ Nothing = property True Just (x,h1) ==~ Just (y,h2) = x==y .&&. h1 =~ h2 prop_InsertSwap x y (HeapPP _ h) = insert x (insert y h) =~ insert y (insert x h) prop_MergeInsertLeft x (HeapPP _ h1) (HeapPP _ h2) = (insert x h1 `merge` h2) =~ insert x (h1 `merge` h2) prop_MergeInsertRight x (HeapPP _ h1) (HeapPP _ h2) = (h1 `merge` insert x h2) =~ insert x (h1 `merge` h2) -- heap observing operations prop_Size_Empty = size empty == 0 prop_Size_Insert x (HeapPP _ (h :: Heap OrdA)) = size (insert x h) == 1 + size h prop_ToList_Empty = toList empty == ([] :: [OrdA]) prop_ToList_Insert x (HeapPP _ (h :: Heap OrdA)) = sort (toList (insert x h)) == sort (x : toList h) prop_ToSortedList (HeapPP _ (h :: Heap OrdA)) = toSortedList h == sort (toList h) -------------------------------------------------------------------------- -- main return [] main = \$(quickCheckAll) -------------------------------------------------------------------------- -- the end.