Set.dcl 15.1 KB
Newer Older
1 2
definition module Data.Set

3
/**
Camil Staps's avatar
Camil Staps committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
 * An efficient implementation of sets.
 *
 * The implementation of `Set` is based on size balanced binary trees (or trees
 * of bounded balance) as described by:
 *
 * - Stephen Adams, "Efficient sets: a balancing act",
 *	 Journal of Functional Programming 3(4):553-562, October 1993,
 *	 <http://www.swiss.ai.mit.edu/~adams/BB/>.
 *
 * - J. Nievergelt and E.M. Reingold, "Binary search trees of bounded balance",
 *	 SIAM journal of computing 2(1), March 1973.
 *
 * Note that the implementation is left-biased -- the elements of a first
 * argument are always preferred to the second, for example in {{`union`}} or
 * {{`insert`}}. Of course, left-biasing can only be observed when equality is
 * an equivalence relation instead of structural equality.
 *
 * This module is ported from Haskell's Data.Set (copyright Daan Leijen 2002)
 * by Lszl Domoszlai, 2013.
 *
24
 * @property-bootstrap
25 26 27 28 29 30
 *     import StdBool, StdChar, StdInt, StdOrdList, StdTuple
 *     from StdList import ++, all, isMember, removeDup,
 *         instance == [a], instance length []
 *     import qualified StdList
 *     from Data.Func import on, `on`
 *     import Data.GenLexOrd
31
 *
32 33 34 35 36 37
 *     derive genShow Maybe
 *     genShow{|Set|} show sep p xs rest = ["Set{":showList (toList xs) ["}":rest]]
 *     where
 *         showList [x]    rest = show sep False x rest
 *         showList [x:xs] rest = show sep False x [",":showList xs rest]
 *         showList []     rest = rest
38
 *
39
 *     :: Predicate a = ConstTrue | IsMember [a]
40
 *
41 42 43
 *     pred :: (Predicate a) a -> Bool | Eq a
 *     pred ConstTrue     _ = True
 *     pred (IsMember cs) c = isMember c cs
44
 *
45 46
 *     derive class Gast Predicate
 *     derive gPrint Maybe, Set
47
 *
48 49 50
 *     // Check that all elements from a list are in a set.
 *     contains :: (Set a) [a] -> Bool | < a
 *     contains d xs = all (\x -> member x d) xs
51
 *
52 53 54
 *     // Check that no elements from a list are in a set.
 *     does_not_contain :: (Set a) [a] -> Bool | < a
 *     does_not_contain d ys = all (\y -> notMember y d) ys
55
 *
56 57 58
 *     // Check that all elements from a set are in a list.
 *     all_in :: (Set a) [a] -> Bool | Eq a
 *     all_in s xs = all (\e -> isMember e xs) (toList s)
59 60
 *
 * @property-test-with a = Char
61 62
 *
 * @property-test-generator [a] -> Set a | < a
63
 *     gen xs = fromList xs
64 65
 */

66 67
from StdOverloaded	import class ==, class < (..)
from StdClass import class Ord (..), <=, >
68 69
from StdList import foldl, map
from Data.Maybe	import :: Maybe
70
from StdBool import not, &&
Camil Staps's avatar
Camil Staps committed
71 72
from Data.GenEq import generic gEq
from Data.GenLexOrd import generic gLexOrd, :: LexOrd
Mart Lubbers's avatar
Mart Lubbers committed
73 74
import qualified Data.Foldable
from Data.Foldable import class Foldable
75

76 77 78
/**
 * A `Set a` is an unordered, uncounted collection of values of type `a`.
 *
79 80 81
 * Like with keys in `Map`, avoid tuple elements since this can be slow.
 * Instead, define a (local) record with strict fields where appropriate.
 *
82
 * @invariant integrity: A.s :: Set a | Eq, genShow{|*|}, gPrint{|*|} a:
83 84 85 86
 *     // Check that the data structure is still correct.
 *     name "no_duplicates" (no_duplicates s) /\
 *     name "log_size"      (log_size s) /\
 *     name "sizes_correct" (sizes_correct s)
87 88
 *
 * @invariant no_duplicates: A.s :: Set a | Eq, genShow{|*|}, gPrint{|*|} a:
89
 *     xs =.= removeDup xs where xs = toList s
90 91
 *
 * @invariant log_size: A.s :: Set a:
92 93 94
 *     check (<) nelem (2 ^ depth s)
 *     where
 *         nelem = size s
95
 *
96 97 98
 *         depth :: (Set a) -> Int
 *         depth Tip = 0
 *         depth (Bin _ _ l r) = 1 + (max `on` depth) l r
99 100
 *
 * @invariant sizes_correct: A.s :: Set a:
101 102 103 104 105 106
 *     case s of
 *         Tip              -> prop True
 *         b=:(Bin _ _ l r) ->
 *             size b =.= 1 + size l + size r /\
 *             sizes_correct l /\
 *             sizes_correct r
107
 */
108
:: Set a = Tip
109
         | Bin !Int !a !(Set a) !(Set a)
110

111 112
instance == (Set a) | == a
instance < (Set a) | < a
113 114
derive gEq Set
derive gLexOrd Set
115
instance Foldable Set
116

Camil Staps's avatar
Camil Staps committed
117 118 119
/**
 * True iff this is the empty set.
 * @type (Set a) -> Bool
120
 * @property equivalence with size 0: A.s :: Set a:
121
 *     size s == 0 <==> null s
122
 * @property equivalence with newSet: A.s :: Set a:
123
 *     s == newSet <==> null s
Camil Staps's avatar
Camil Staps committed
124
 */
125 126 127 128
null s :== case s of
             Tip -> True
             (Bin sz _ _ _) -> False

Camil Staps's avatar
Camil Staps committed
129 130 131
/**
 * The number of elements in the set.
 * @type (Set a) -> Int
132
 * @property correctness: A.s :: Set a:
133
 *     size s =.= length (toList s)
Camil Staps's avatar
Camil Staps committed
134
 */
135 136 137
size s :== case s of
             Tip -> 0
             (Bin sz _ _ _) -> sz
138

Camil Staps's avatar
Camil Staps committed
139
/**
Camil Staps's avatar
Camil Staps committed
140 141
 * Is the element in the set?
 * @complexity O(log n)
142
 * @property correctness: A.x :: a; s :: Set a:
143
 *     member x s <==> isMember x (toList s)
Camil Staps's avatar
Camil Staps committed
144
 */
145
member    :: !a !(Set a) -> Bool | < a
146
	special a=Int; a=String
147

Camil Staps's avatar
Camil Staps committed
148 149
/**
 * Checks if an element is not in the set.
Camil Staps's avatar
Camil Staps committed
150
 * @complexity O(log n)
Camil Staps's avatar
Camil Staps committed
151 152
 * @type a (Set a) -> Bool | <, == a
 */
153 154
notMember x t :== not (member x t)

Camil Staps's avatar
Camil Staps committed
155 156 157
/**
 * Is t1 a subset of t2?
 * @type (Set a) (Set a) -> Bool | <, == a
Camil Staps's avatar
Camil Staps committed
158
 * @complexity O(n+m)
159
 * @property correctness: A.xs :: Set a; ys :: Set a:
160
 *     isSubsetOf xs ys <==> all (\x -> isMember x (toList ys)) (toList xs)
Camil Staps's avatar
Camil Staps committed
161
 */
162 163
isSubsetOf t1 t2 :== (size t1 <= size t2) && (isSubsetOfX t1 t2)

164
isSubsetOfX :: !(Set a) !(Set a) -> Bool | < a
165
	special a=Int; a=String
166

Camil Staps's avatar
Camil Staps committed
167 168 169
/**
 * Is t1 a proper subset of t2?
 * @type (Set a) (Set a) -> Bool | <, == a
Camil Staps's avatar
Camil Staps committed
170
 * @complexity O(n+m)
171
 * @property correctness: A.xs :: Set a; ys :: Set a:
172 173 174 175
 *     isProperSubsetOf xs ys
 *         <==> all (\x -> isMember x ys`) xs` && not (all (\y -> isMember y xs`) ys`)
 *     where
 *         (xs`,ys`) = (toList xs, toList ys)
Camil Staps's avatar
Camil Staps committed
176
 */
177
isProperSubsetOf s1 s2 :== (size s1 < size s2) && (isSubsetOf s1 s2)
178

Camil Staps's avatar
Camil Staps committed
179 180
/**
 * The empty set.
Camil Staps's avatar
Camil Staps committed
181
 * @complexity O(1)
182
 * @property is null:
183
 *     null newSet
Camil Staps's avatar
Camil Staps committed
184
 */
László Domoszlai's avatar
newSet  
László Domoszlai committed
185
newSet :: Set a
Camil Staps's avatar
Camil Staps committed
186 187 188

/**
 * Create a singleton set.
Camil Staps's avatar
Camil Staps committed
189
 * @complexity O(1)
Camil Staps's avatar
Camil Staps committed
190
 */
191
singleton :: !u:a -> w:(Set u:a), [w <= u]
192

Camil Staps's avatar
Camil Staps committed
193
/**
Camil Staps's avatar
Camil Staps committed
194 195
 * Insert an element in a set. If the set already contains an element equal to
 * the given value, it is replaced with the new value.
196
 *
Camil Staps's avatar
Camil Staps committed
197
 * @complexity O(log n)
198
 * @property correctness: A.x :: a; xs :: Set a:
199 200 201 202
 *     let xs` = insert x xs in
 *         check member x xs` /\             // Membership
 *         check contains xs` (toList xs) /\ // Rest untouched
 *         integrity xs`                     // Data structure integrity
Camil Staps's avatar
Camil Staps committed
203
 */
204
insert :: !a !.(Set a) -> Set a | < a
205
	special a=Int; a=String
Camil Staps's avatar
Camil Staps committed
206 207 208

/**
 * Delete an element from a set.
Camil Staps's avatar
Camil Staps committed
209 210
 *
 * @complexity O(log n)
211
 * @property correctness: A.x :: a; xs :: Set a:
212 213 214 215
 *     let xs` = delete x xs in
 *         check notMember x xs` /\                                // Membership
 *         check contains xs` [x` \\ x` <- toList xs | x` <> x] /\ // Rest untouched
 *         integrity xs`                                           // Data structure integrity
Camil Staps's avatar
Camil Staps committed
216
 */
217
delete :: !a !.(Set a) -> Set a | < a
218
	special a=Int; a=String
219

Camil Staps's avatar
Camil Staps committed
220 221
/**
 * The minimal element of a set.
Camil Staps's avatar
Camil Staps committed
222
 * @complexity O(log n)
223
 * @property correctness: A.xs :: Set a:
224
 *     minList (toList xs) == findMin xs
225
 * @precondition not (null xs)
Camil Staps's avatar
Camil Staps committed
226
 */
227
findMin :: !(Set a) -> a
Camil Staps's avatar
Camil Staps committed
228 229 230

/**
 * The maximal element of a set.
Camil Staps's avatar
Camil Staps committed
231
 * @complexity O(log n)
232
 * @property correctness: A.xs :: Set a:
233
 *     maxList (toList xs) == findMax xs
234
 * @precondition not (null xs)
Camil Staps's avatar
Camil Staps committed
235
 */
236
findMax :: !(Set a) -> a
Camil Staps's avatar
Camil Staps committed
237 238 239

/**
 * Delete the minimal element.
Camil Staps's avatar
Camil Staps committed
240
 * @complexity O(log n)
241
 * @property correctness: A.xs :: Set a:
242 243 244 245 246 247
 *     case xs of
 *         Tip -> prop (null (deleteMin newSet))
 *         xs  -> let xs` = deleteMin xs in
 *             check notMember (minList (toList xs)) xs` /\
 *             size xs` =.= size xs - 1 /\
 *             integrity xs`
Camil Staps's avatar
Camil Staps committed
248
 */
249
deleteMin :: !.(Set a) -> Set a
Camil Staps's avatar
Camil Staps committed
250 251 252

/**
 * Delete the maximal element.
Camil Staps's avatar
Camil Staps committed
253
 * @complexity O(log n)
254
 * @property correctness: A.xs :: Set a:
255 256 257 258 259 260
 *     case xs of
 *         Tip -> prop (null (deleteMax newSet))
 *         xs  -> let xs` = deleteMax xs in
 *             check notMember (maxList (toList xs)) xs` /\
 *             size xs` =.= size xs - 1 /\
 *             integrity xs`
Camil Staps's avatar
Camil Staps committed
261
 */
262
deleteMax :: !.(Set a) -> Set a
Camil Staps's avatar
Camil Staps committed
263 264 265

/**
 * deleteFindMin set = (findMin set, deleteMin set)
Camil Staps's avatar
Camil Staps committed
266
 * @complexity O(log n)
267
 * @property correctness: A.xs :: Set a:
268 269 270
 *     let (m,xs`) = deleteFindMin xs in
 *         m =.= min /\ notMember min xs`
 *     where min = minList (toList xs)
271
 * @precondition not (null xs)
Camil Staps's avatar
Camil Staps committed
272
 */
273
deleteFindMin :: !.(Set a) -> (!a, !Set a)
Camil Staps's avatar
Camil Staps committed
274 275 276

/**
 * deleteFindMax set = (findMax set, deleteMax set)
Camil Staps's avatar
Camil Staps committed
277
 * @complexity O(log n)
278
 * @property correctness: A.xs :: Set a:
279 280 281
 *     let (m,xs`) = deleteFindMax xs in
 *         m =.= max /\ notMember max xs`
 *     where max = maxList (toList xs)
282
 * @precondition not (null xs)
Camil Staps's avatar
Camil Staps committed
283
 */
284
deleteFindMax :: !.(Set a) -> (!a, !Set a)
Camil Staps's avatar
Camil Staps committed
285 286 287 288

/**
 * Retrieves the minimal key of the set, and the set stripped of that element,
 * or 'Nothing' if passed an empty set.
Camil Staps's avatar
Camil Staps committed
289
 * @complexity O(log n)
290
 * @property correctness: A.xs :: Set a:
291 292 293
 *     if (null xs)
 *         (Nothing =.= minView xs)
 *         (Just (deleteFindMin xs) =.= minView xs)
Camil Staps's avatar
Camil Staps committed
294
 */
295
minView :: !.(Set a) -> .(Maybe (!a, !Set a))
Camil Staps's avatar
Camil Staps committed
296 297 298 299

/**
 * Retrieves the maximal key of the set, and the set stripped of that element,
 * or 'Nothing' if passed an empty set.
Camil Staps's avatar
Camil Staps committed
300
 * @complexity O(log n)
301
 * @property correctness: A.xs :: Set a:
302 303 304
 *     if (null xs)
 *         (Nothing =.= maxView xs)
 *         (Just (deleteFindMax xs) =.= maxView xs)
Camil Staps's avatar
Camil Staps committed
305
 */
306
maxView :: !.(Set a) -> .(Maybe (!a, !Set a))
307

Camil Staps's avatar
Camil Staps committed
308
/**
Camil Staps's avatar
Camil Staps committed
309 310
 * The union of two sets, preferring the first set when equal elements are
 * encountered.
Camil Staps's avatar
Camil Staps committed
311
 * @complexity O(n+m)
312
 * @property correctness: A.xs :: Set a; ys :: Set a:
313 314 315 316 317 318
 *     check contains u elems    // No missing elements
 *         /\ check all_in u elems // No junk
 *         /\ integrity u          // Data structure integrity
 *     where
 *         u = union xs ys
 *         elems = toList xs ++ toList ys
Camil Staps's avatar
Camil Staps committed
319
 */
Camil Staps's avatar
Camil Staps committed
320
union :: !u:(Set a) !u:(Set a) -> Set a | < a
321
	special a=Int; a=String
Camil Staps's avatar
Camil Staps committed
322 323 324

/**
 * The union of a list of sets.
Camil Staps's avatar
Camil Staps committed
325
 * @type !u:[v:(Set a)] -> Set a | < a, [u <= v]
Camil Staps's avatar
Camil Staps committed
326
 */
327 328
unions ts :== foldl union newSet ts

Camil Staps's avatar
Camil Staps committed
329 330
/**
 * Difference of two sets.
Camil Staps's avatar
Camil Staps committed
331
 * @complexity O(n+m)
332
 * @property correctness: A.xs :: Set a; ys :: Set a:
333 334 335 336 337 338
 *     check does_not_contain d ys`                                 // No remaining elements
 *         /\ check contains d [x \\ x <- xs` | not (isMember x ys`)] // All good elements
 *         /\ integrity d                                             // Data structure integrity
 *     where
 *         d = difference xs ys
 *         (xs`,ys`) = (toList xs, toList ys)
Camil Staps's avatar
Camil Staps committed
339
 */
Camil Staps's avatar
Camil Staps committed
340
difference :: !(Set a) !(Set a) -> Set a | < a
341
	special a=Int; a=String
Camil Staps's avatar
Camil Staps committed
342 343 344

/**
 * The intersection of two sets.
Camil Staps's avatar
Camil Staps committed
345 346
 * Elements of the result come from the first set.
 * @complexity O(n+m)
347
 * @property correctness: A.xs :: Set a; ys :: Set a:
348 349 350 351 352 353 354
 *     check does_not_contain i [x \\ x <- xs` | not (isMember x ys`)]      // No junk
 *         /\ check does_not_contain i [y \\ y <- ys` | not (isMember y xs`)] // No junk
 *         /\ check contains i [x \\ x <- xs` | isMember x ys`]               // All good elements
 *         /\ integrity i                                                   // Data structure integrity
 *     where
 *         i = intersection xs ys
 *         (xs`,ys`) = (toList xs, toList ys)
Camil Staps's avatar
Camil Staps committed
355
 */
Camil Staps's avatar
Camil Staps committed
356
intersection :: !(Set a) !(Set a) -> Set a | < a
357
	special a=Int; a=String
Camil Staps's avatar
Camil Staps committed
358 359 360 361 362

/**
 * The intersection of a list of sets.
 * Elements of the result come from the first set
 */
Camil Staps's avatar
Camil Staps committed
363
intersections :: ![Set a] -> Set a | < a
364
	special a=Int; a=String
365

Camil Staps's avatar
Camil Staps committed
366 367
/**
 * Filter all elements that satisfy the predicate.
Camil Staps's avatar
Camil Staps committed
368
 * @complexity O(n)
369
 * @property correctness: A.p :: Predicate a; xs :: Set a:
370 371
 *     sort (toList (filter (pred p) xs))
 *         =.= sort (removeDup ('StdList'.filter (pred p) (toList xs)))
Camil Staps's avatar
Camil Staps committed
372
 */
373
filter :: !(a -> Bool) !(Set a) -> Set a
Camil Staps's avatar
Camil Staps committed
374 375 376 377

/**
 * Partition the set into two sets, one with all elements that satisfy the
 * predicate and one with all elements that don't satisfy the predicate.
Camil Staps's avatar
Camil Staps committed
378
 * See also {{`split`}}.
379
 *
Camil Staps's avatar
Camil Staps committed
380
 * @complexity O(n)
381
 * @property correctness: A.p :: Predicate a; xs :: Set a:
382 383 384 385 386 387 388 389 390 391 392
 *     all p` true`                                // Right split
 *         /\ all (\x -> not (p` x)) false`
 *         /\ all (\x -> isMember x (toList xs)) xs` // No junk
 *         /\ all (\x -> isMember x xs`) (toList xs) // All members used
 *         /\ integrity true                         // Data structure integrity
 *         /\ integrity false
 *     where
 *         p` = pred p
 *         (true,false) = partition p` xs
 *         (true`,false`) = (toList true, toList false)
 *         xs` = true` ++ false`
Camil Staps's avatar
Camil Staps committed
393
 */
394
partition :: !(a -> Bool) !(Set a) -> (!Set a, !Set a)
Camil Staps's avatar
Camil Staps committed
395 396 397 398 399 400

/**
 * Split a set in elements less and elements greater than a certain pivot.
 *
 * @param The pivot.
 * @param The set.
401
 * @result A tuple of two sets containing small and large values.
Camil Staps's avatar
Camil Staps committed
402
 * @complexity O(log n)
403
 *
404
 * @property correctness: A.p :: a; xs :: Set a:
405 406 407 408 409 410 411 412 413 414 415
 *     all ((>) p) lt`                        // Right split
 *         /\ all ((<) p) gt`
 *         /\ all (\x -> isMember x xsminp) xs` // No junk
 *         /\ all (\x -> isMember x xs`) xsminp // All members used
 *         /\ integrity lt                      // Data structure integrity
 *         /\ integrity gt
 *     where
 *         xsminp = 'StdList'.filter ((<>) p) (toList xs)
 *         (lt,gt) = split p xs
 *         (lt`,gt`) = (toList lt, toList gt)
 *         xs` = lt` ++ gt`
Camil Staps's avatar
Camil Staps committed
416
 */
417
split :: !a !(Set a) -> (!Set a, !Set a) | < a
418
	special a=Int; a=String
Camil Staps's avatar
Camil Staps committed
419 420 421 422

/**
 * Performs a 'split' but also returns whether the pivot element was found in
 * the original set.
Camil Staps's avatar
Camil Staps committed
423 424
 *
 * @complexity O(log n)
425
 * @property correctness: A.p :: a; xs :: Set a:
426 427 428 429 430 431 432 433 434 435 436 437
 *     all ((>) p) lt`                        // Right split
 *         /\ all ((<) p) gt`
 *         /\ all (\x -> isMember x xsminp) xs` // No junk
 *         /\ all (\x -> isMember x xs`) xsminp // All members used
 *         /\ bool =.= isMember p (toList xs)   // Boolean is correct
 *         /\ integrity lt                      // Data structure integrity
 *         /\ integrity gt
 *     where
 *         xsminp = 'StdList'.filter ((<>) p) (toList xs)
 *         (lt,bool,gt) = splitMember p xs
 *         (lt`,gt`) = (toList lt, toList gt)
 *         xs` = lt` ++ gt`
Camil Staps's avatar
Camil Staps committed
438
 */
439
splitMember :: !a !(Set a) -> (!Set a, !Bool, !Set a) | < a
440
	special a=Int; a=String
441

Camil Staps's avatar
Camil Staps committed
442 443 444
/**
 * Convert the set to an ascending list of elements.
 * @type (Set a) -> [a]
Camil Staps's avatar
Camil Staps committed
445
 * @complexity O(n)
446
 * @property composition with fromList is identity: A.xs :: Set a:
447
 *     xs =.= fromList (toList xs)
Camil Staps's avatar
Camil Staps committed
448
 */
449 450
toList s :== toAscList s

Camil Staps's avatar
Camil Staps committed
451 452
/**
 * Same as toList.
Camil Staps's avatar
Camil Staps committed
453
 * @complexity O(n)
Camil Staps's avatar
Camil Staps committed
454 455
 * @type (Set a) -> [a]
 */
Mart Lubbers's avatar
Mart Lubbers committed
456
toAscList t :== 'Data.Foldable'.foldr` (\a as -> [a:as]) [] t
457

Camil Staps's avatar
Camil Staps committed
458 459
/**
 * Create a set from a list of elements.
Camil Staps's avatar
Camil Staps committed
460
 * @complexity O(n*log n)
Camil Staps's avatar
Camil Staps committed
461
 */
462
fromList :: ![a] -> Set a | < a
463
	special a=Int; a=String
464

Camil Staps's avatar
Camil Staps committed
465 466 467 468
/**
 * Map a function to all elements in a set.
 * @type (a -> b) (Set a) -> Set b | <, == a & <, == b
 */
469
mapSet f s :== fromList (map f (toList s))
470

Camil Staps's avatar
Camil Staps committed
471 472 473
/**
 * Map a set without converting it to and from a list.
 */
474
mapSetMonotonic :: !(a -> b) !(Set a) -> Set b