@@ -23,37 +23,6 @@ module Data.Ranged.RangedSet (
23
23
-- ** Useful Sets
24
24
rSetEmpty ,
25
25
rSetFull ,
26
- -- ** QuickCheck Properties
27
- -- *** Construction
28
- prop_validNormalised ,
29
- prop_has ,
30
- prop_unfold ,
31
- -- *** Basic Operations
32
- prop_union ,
33
- prop_intersection ,
34
- prop_difference ,
35
- prop_negation ,
36
- prop_not_empty ,
37
- -- *** Some Identities and Inequalities
38
- -- $ConstructionProperties
39
- -- $BasicOperationProperties
40
- -- $SomeIdentitiesAndInequalities
41
- prop_empty ,
42
- prop_full ,
43
- prop_empty_intersection ,
44
- prop_full_union ,
45
- prop_union_superset ,
46
- prop_intersection_subset ,
47
- prop_diff_intersect ,
48
- prop_subset ,
49
- prop_strict_subset ,
50
- prop_union_strict_superset ,
51
- prop_intersection_commutes ,
52
- prop_union_commutes ,
53
- prop_intersection_associates ,
54
- prop_union_associates ,
55
- prop_de_morgan_intersection ,
56
- prop_de_morgan_union ,
57
26
) where
58
27
59
28
import Data.Ranged.Boundaries
@@ -65,7 +34,6 @@ import Data.Monoid
65
34
#endif
66
35
67
36
import Data.List
68
- import Test.QuickCheck
69
37
70
38
infixl 7 -/\-
71
39
infixl 6 -\/- , -!-
@@ -256,244 +224,3 @@ rSetUnfold bound upperFunc succFunc = RSet $ normalise $ ranges1 bound
256
224
: case succFunc b of
257
225
Just b2 -> ranges1 b2
258
226
Nothing -> []
259
-
260
-
261
- -- QuickCheck Generators
262
-
263
- instance (Arbitrary v , DiscreteOrdered v ) =>
264
- Arbitrary (RSet v )
265
- where
266
- arbitrary = frequency [
267
- (1 , return rSetEmpty),
268
- (1 , return rSetFull),
269
- (18 , do
270
- ls <- arbitrary
271
- return $ makeRangedSet $ rangeList $ sort ls
272
- )]
273
- where
274
- -- Arbitrary lists of ranges don't give many interesting sets after
275
- -- normalisation. So instead generate a sorted list of boundaries
276
- -- and pair them off. Odd boundaries are dropped.
277
- rangeList (b1: b2: bs) = Range b1 b2 : rangeList bs
278
- rangeList _ = []
279
-
280
- instance (CoArbitrary v , DiscreteOrdered v ) =>
281
- CoArbitrary (RSet v )
282
- where
283
- coarbitrary (RSet ls) = variant (0 :: Int ) . coarbitrary ls
284
-
285
- -- ==================================================================
286
- -- QuickCheck Properties
287
- -- ==================================================================
288
-
289
- ---------------------------------------------------------------------
290
- -- Construction properties
291
- ---------------------------------------------------------------------
292
-
293
- -- | A normalised range list is valid for unsafeRangedSet
294
- --
295
- -- > prop_validNormalised ls = validRangeList $ normaliseRangeList ls
296
- prop_validNormalised :: (DiscreteOrdered a ) => [Range a ] -> Bool
297
- prop_validNormalised ls = validRangeList $ normaliseRangeList ls
298
-
299
-
300
- -- | Iff a value is in a range list then it is in a ranged set
301
- -- constructed from that list.
302
- --
303
- -- > prop_has ls v = (ls `rangeListHas` v) == makeRangedSet ls -?- v
304
- prop_has :: (DiscreteOrdered a ) => [Range a ] -> a -> Bool
305
- prop_has ls v = (ls `rangeListHas` v) == makeRangedSet ls -?- v
306
-
307
-
308
- -- | Verifies the correct membership of a set containing all integers
309
- -- starting with the digit \"1\" up to 19999.
310
- --
311
- -- > prop_unfold = (v <= 99999 && head (show v) == '1') == (initial1 -?- v)
312
- -- > where
313
- -- > initial1 = rSetUnfold (BoundaryBelow 1) addNines times10
314
- -- > addNines (BoundaryBelow n) = BoundaryAbove $ n * 2 - 1
315
- -- > times10 (BoundaryBelow n) =
316
- -- > if n <= 1000 then Just $ BoundaryBelow $ n * 10 else Nothing
317
-
318
- prop_unfold :: Integer -> Bool
319
- prop_unfold v = (v <= 99999 && head (show v) == ' 1' ) == (initial1 -?- v)
320
- where
321
- initial1 = rSetUnfold (BoundaryBelow 1 ) addNines times10
322
- addNines (BoundaryBelow n) = BoundaryAbove $ n * 2 - 1
323
- addNines _ = error " Can't happen"
324
- times10 (BoundaryBelow n) =
325
- if n <= 10000 then Just $ BoundaryBelow $ n * 10 else Nothing
326
- times10 _ = error " Can't happen"
327
-
328
- ---------------------------------------------------------------------
329
- -- Basic operation properties
330
- ---------------------------------------------------------------------
331
-
332
- -- | Iff a value is in either of two ranged sets then it is in the union of
333
- -- those two sets.
334
- --
335
- -- > prop_union rs1 rs2 v =
336
- -- > (rs1 -?- v || rs2 -?- v) == ((rs1 -\/- rs2) -?- v)
337
- prop_union :: (DiscreteOrdered a ) => RSet a -> RSet a -> a -> Bool
338
- prop_union rs1 rs2 v = (rs1 -?- v || rs2 -?- v) == ((rs1 -\/- rs2) -?- v)
339
-
340
- -- | Iff a value is in both of two ranged sets then it is n the intersection
341
- -- of those two sets.
342
- --
343
- -- > prop_intersection rs1 rs2 v =
344
- -- > (rs1 -?- v && rs2 -?- v) == ((rs1 -/\- rs2) -?- v)
345
- prop_intersection :: (DiscreteOrdered a ) => RSet a -> RSet a -> a -> Bool
346
- prop_intersection rs1 rs2 v =
347
- (rs1 -?- v && rs2 -?- v) == ((rs1 -/\- rs2) -?- v)
348
-
349
- -- | Iff a value is in ranged set 1 and not in ranged set 2 then it is in the
350
- -- difference of the two.
351
- --
352
- -- > prop_difference rs1 rs2 v =
353
- -- > (rs1 -?- v && not (rs2 -?- v)) == ((rs1 -!- rs2) -?- v)
354
- prop_difference :: (DiscreteOrdered a ) => RSet a -> RSet a -> a -> Bool
355
- prop_difference rs1 rs2 v =
356
- (rs1 -?- v && not (rs2 -?- v)) == ((rs1 -!- rs2) -?- v)
357
-
358
- -- | Iff a value is not in a ranged set then it is in its negation.
359
- --
360
- -- > prop_negation rs v = rs -?- v == not (rSetNegation rs -?- v)
361
- prop_negation :: (DiscreteOrdered a ) => RSet a -> a -> Bool
362
- prop_negation rs v = rs -?- v == not (rSetNegation rs -?- v)
363
-
364
- -- | A set that contains a value is not empty
365
- --
366
- -- > prop_not_empty rs v = (rs -?- v) ==> not (rSetIsEmpty rs)
367
- prop_not_empty :: (DiscreteOrdered a ) => RSet a -> a -> Property
368
- prop_not_empty rs v = (rs -?- v) ==> not (rSetIsEmpty rs)
369
-
370
- ---------------------------------------------------------------------
371
- -- Some identities and inequalities of sets
372
- ---------------------------------------------------------------------
373
-
374
- -- | The empty set has no members.
375
- --
376
- -- > prop_empty v = not (rSetEmpty -?- v)
377
- prop_empty :: (DiscreteOrdered a ) => a -> Bool
378
- prop_empty v = not (rSetEmpty -?- v)
379
-
380
- -- | The full set has every member.
381
- --
382
- -- > prop_full v = rSetFull -?- v
383
- prop_full :: (DiscreteOrdered a ) => a -> Bool
384
- prop_full v = rSetFull -?- v
385
-
386
- -- | The intersection of a set with its negation is empty.
387
- --
388
- -- > prop_empty_intersection rs =
389
- -- > rSetIsEmpty (rs -/\- rSetNegation rs)
390
- prop_empty_intersection :: (DiscreteOrdered a ) => RSet a -> Bool
391
- prop_empty_intersection rs =
392
- rSetIsEmpty (rs -/\- rSetNegation rs)
393
-
394
- -- | The union of a set with its negation is full.
395
- --
396
- -- > prop_full_union rs v =
397
- -- > rSetIsFull (rs -\/- rSetNegation rs)
398
- prop_full_union :: (DiscreteOrdered a ) => RSet a -> Bool
399
- prop_full_union rs =
400
- rSetIsFull (rs -\/- rSetNegation rs)
401
-
402
- -- | The union of two sets is the non-strict superset of both.
403
- --
404
- -- > prop_union_superset rs1 rs2 =
405
- -- > rs1 -<=- u && rs2 -<=- u
406
- -- > where
407
- -- > u = rs1 -\/- rs2
408
- prop_union_superset :: (DiscreteOrdered a ) => RSet a -> RSet a -> Bool
409
- prop_union_superset rs1 rs2 =
410
- rs1 -<=- u && rs2 -<=- u
411
- where
412
- u = rs1 -\/- rs2
413
-
414
- -- | The intersection of two sets is the non-strict subset of both.
415
- --
416
- -- > prop_intersection_subset rs1 rs2 =
417
- -- > i -<=- rs1 && i -<=- rs2
418
- -- > where
419
- -- > i = rs1 -/\- rs2
420
- prop_intersection_subset :: (DiscreteOrdered a ) => RSet a -> RSet a -> Bool
421
- prop_intersection_subset rs1 rs2 = i -<=- rs1 && i -<=- rs2
422
- where
423
- i = rs1 -/\- rs2
424
-
425
- -- | The difference of two sets intersected with the subtractand is empty.
426
- --
427
- -- > prop_diff_intersect rs1 rs2 =
428
- -- > rSetIsEmpty ((rs1 -!- rs2) -/\- rs2)
429
- prop_diff_intersect :: (DiscreteOrdered a ) => RSet a -> RSet a -> Bool
430
- prop_diff_intersect rs1 rs2 = rSetIsEmpty ((rs1 -!- rs2) -/\- rs2)
431
-
432
- -- | A set is the non-strict subset of itself.
433
- --
434
- -- > prop_subset rs = rs -<=- rs
435
- prop_subset :: (DiscreteOrdered a ) => RSet a -> Bool
436
- prop_subset rs = rs -<=- rs
437
-
438
- -- | A set is not the strict subset of itself.
439
- --
440
- -- > prop_strict_subset rs = not (rs -<- rs)
441
- prop_strict_subset :: (DiscreteOrdered a ) => RSet a -> Bool
442
- prop_strict_subset rs = not (rs -<- rs)
443
-
444
- -- | If rs1 - rs2 is not empty then the union of rs1 and rs2 will be a strict
445
- -- superset of rs2.
446
- --
447
- -- > prop_union_strict_superset rs1 rs2 =
448
- -- > (not $ rSetIsEmpty (rs1 -!- rs2))
449
- -- > ==> (rs2 -<- (rs1 -\/- rs2))
450
- prop_union_strict_superset :: (DiscreteOrdered a ) => RSet a -> RSet a -> Property
451
- prop_union_strict_superset rs1 rs2 =
452
- (not $ rSetIsEmpty (rs1 -!- rs2)) ==> (rs2 -<- (rs1 -\/- rs2))
453
-
454
- -- | Intersection commutes.
455
- --
456
- -- > prop_intersection_commutes rs1 rs2 = (rs1 -/\- rs2) == (rs2 -/\- rs1)
457
- prop_intersection_commutes :: (DiscreteOrdered a ) => RSet a -> RSet a -> Bool
458
- prop_intersection_commutes rs1 rs2 = (rs1 -/\- rs2) == (rs2 -/\- rs1)
459
-
460
- -- | Union commutes.
461
- --
462
- -- > prop_union_commutes rs1 rs2 = (rs1 -\/- rs2) == (rs2 -\/- rs1)
463
- prop_union_commutes :: (DiscreteOrdered a ) => RSet a -> RSet a -> Bool
464
- prop_union_commutes rs1 rs2 = (rs1 -\/- rs2) == (rs2 -\/- rs1)
465
-
466
- -- | Intersection associates.
467
- --
468
- -- > prop_intersection_associates rs1 rs2 rs3 =
469
- -- > ((rs1 -/\- rs2) -/\- rs3) == (rs1 -/\- (rs2 -/\- rs3))
470
- prop_intersection_associates :: (DiscreteOrdered a ) =>
471
- RSet a -> RSet a -> RSet a -> Bool
472
- prop_intersection_associates rs1 rs2 rs3 =
473
- ((rs1 -/\- rs2) -/\- rs3) == (rs1 -/\- (rs2 -/\- rs3))
474
-
475
- -- | Union associates.
476
- --
477
- -- > prop_union_associates rs1 rs2 rs3 =
478
- -- > ((rs1 -\/- rs2) -\/- rs3) == (rs1 -\/- (rs2 -\/- rs3))
479
- prop_union_associates :: (DiscreteOrdered a ) =>
480
- RSet a -> RSet a -> RSet a -> Bool
481
- prop_union_associates rs1 rs2 rs3 =
482
- ((rs1 -\/- rs2) -\/- rs3) == (rs1 -\/- (rs2 -\/- rs3))
483
-
484
- -- | De Morgan's Law for Intersection.
485
- --
486
- -- > prop_de_morgan_intersection rs1 rs2 =
487
- -- > rSetNegation (rs1 -/\- rs2) == (rSetNegation rs1 -\/- rSetNegation rs2)
488
- prop_de_morgan_intersection :: (DiscreteOrdered a ) => RSet a -> RSet a -> Bool
489
- prop_de_morgan_intersection rs1 rs2 =
490
- rSetNegation (rs1 -/\- rs2) == (rSetNegation rs1 -\/- rSetNegation rs2)
491
-
492
- -- | De Morgan's Law for Union.
493
- --
494
- -- > prop_de_morgan_union rs1 rs2 =
495
- -- > rSetNegation (rs1 -\/- rs2) == (rSetNegation rs1 -/\- rSetNegation rs2)
496
-
497
- prop_de_morgan_union :: (DiscreteOrdered a ) => RSet a -> RSet a -> Bool
498
- prop_de_morgan_union rs1 rs2 =
499
- rSetNegation (rs1 -\/- rs2) == (rSetNegation rs1 -/\- rSetNegation rs2)
0 commit comments