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