1{-# LANGUAGE ScopedTypeVariables, TemplateHaskell #-}
2module Main where
3
4--------------------------------------------------------------------------
5-- imports
6
7import Test.QuickCheck
8
9import Data.List
10  ( sort
11  , (\\)
12  )
13
14import Control.Monad
15  ( liftM
16  , liftM2
17  )
18
19--------------------------------------------------------------------------
20-- skew heaps
21
22data Heap a
23  = Node a (Heap a) (Heap a)
24  | Empty
25 deriving ( Eq, Ord, Show )
26
27empty :: Heap a
28empty = Empty
29
30isEmpty :: Heap a -> Bool
31isEmpty Empty = True
32isEmpty _     = False
33
34unit :: a -> Heap a
35unit x = Node x empty empty
36
37size :: Heap a -> Int
38size Empty          = 0
39size (Node _ h1 h2) = 1 + size h1 + size h2
40
41insert :: Ord a => a -> Heap a -> Heap a
42insert x h = unit x `merge` h
43
44removeMin :: Ord a => Heap a -> Maybe (a, Heap a)
45removeMin Empty          = Nothing
46removeMin (Node x h1 h2) = Just (x, h1 `merge` h2)
47
48merge :: Ord a => Heap a -> Heap a -> Heap a
49h1    `merge` Empty = h1
50Empty `merge` h2    = h2
51h1@(Node x h11 h12) `merge` h2@(Node y h21 h22)
52  | x <= y    = Node x (h12 `merge` h2) h11
53  | otherwise = Node y (h22 `merge` h1) h21
54
55fromList :: Ord a => [a] -> Heap a
56fromList xs = merging [ unit x | x <- xs ]
57 where
58  merging []  = empty
59  merging [h] = h
60  merging hs  = merging (sweep hs)
61
62  sweep []         = []
63  sweep [h]        = [h]
64  sweep (h1:h2:hs) = (h1 `merge` h2) : sweep hs
65
66toList :: Heap a -> [a]
67toList h = toList' [h]
68 where
69  toList' []                  = []
70  toList' (Empty        : hs) = toList' hs
71  toList' (Node x h1 h2 : hs) = x : toList' (h1:h2:hs)
72
73toSortedList :: Ord a => Heap a -> [a]
74toSortedList Empty          = []
75toSortedList (Node x h1 h2) = x : toList (h1 `merge` h2)
76
77--------------------------------------------------------------------------
78-- specification
79
80invariant :: Ord a => Heap a -> Bool
81invariant Empty          = True
82invariant (Node x h1 h2) = x <=? h1 && x <=? h2 && invariant h1 && invariant h2
83
84(<=?) :: Ord a => a -> Heap a -> Bool
85x <=? Empty      = True
86x <=? Node y _ _ = x <= y
87
88(==?) :: Ord a => Heap a -> [a] -> Bool
89h ==? xs = invariant h && sort (toList h) == sort xs
90
91--------------------------------------------------------------------------
92-- properties
93
94prop_Empty =
95  empty ==? ([] :: [Int])
96
97prop_IsEmpty (h :: Heap Int) =
98  isEmpty h == null (toList h)
99
100prop_Unit (x :: Int) =
101  unit x ==? [x]
102
103prop_Size (h :: Heap Int) =
104  size h == length (toList h)
105
106prop_Insert x (h :: Heap Int) =
107  insert x h ==? (x : toList h)
108
109prop_RemoveMin (h :: Heap Int) =
110  cover 80 (size h > 1) "non-trivial" $
111  case removeMin h of
112    Nothing     -> h ==? []
113    Just (x,h') -> x == minimum (toList h) && h' ==? (toList h \\ [x])
114
115prop_Merge h1 (h2 :: Heap Int) =
116  (h1 `merge` h2) ==? (toList h1 ++ toList h2)
117
118prop_FromList (xs :: [Int]) =
119  fromList xs ==? xs
120
121prop_ToSortedList (h :: Heap Int) =
122  h ==? xs && xs == sort xs
123 where
124  xs = toSortedList h
125
126--------------------------------------------------------------------------
127-- generators
128
129instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where
130  arbitrary = sized (arbHeap Nothing)
131   where
132    arbHeap mx n =
133      frequency $
134        [ (1, return Empty) ] ++
135        [ (7, do my <- arbitrary `suchThatMaybe` ((>= mx) . Just)
136                 case my of
137                   Nothing -> return Empty
138                   Just y  -> liftM2 (Node y) arbHeap2 arbHeap2
139                    where arbHeap2 = arbHeap (Just y) (n `div` 2))
140        | n > 0
141        ]
142
143--------------------------------------------------------------------------
144-- main
145
146return []
147main = $quickCheckAll
148
149--------------------------------------------------------------------------
150-- the end.
151{-
152  shrink Empty          = []
153  shrink (Node x h1 h2) =
154       [ h1, h2 ]
155    ++ [ Node x  h1' h2  | h1' <- shrink h1, x  <=? h1' ]
156    ++ [ Node x  h1  h2' | h2' <- shrink h2, x  <=? h2' ]
157    ++ [ Node x' h1  h2  | x'  <- shrink x,  x' <=? h1, x' <=? h2 ]
158-}
159
160-- toSortedList (Node x h1 h2) = x : toSortedList (h1 `merge` h2)
161
162{-
163prop_HeapIsNotSorted (h :: Heap Int) =
164  expectFailure $
165    toList h == toSortedList h
166-}
167
168