|
|
|
|
|
|
| Synopsis |
|
|
|
|
| Ranged Set Type
|
|
|
| An RSet (for Ranged Set) is a list of ranges. The ranges must be sorted
and not overlap.
|  Instances | |
|
|
|
|
| Ranged Set construction functions and their preconditions
|
|
|
| Create a new Ranged Set from a list of ranges. The list may contain
ranges that overlap or are not in ascending order.
|
|
|
| Create a new Ranged Set from a list of ranges. validRangeList ranges
must return True. This precondition is not checked.
|
|
|
| Determine if the ranges in the list are both in order and non-overlapping.
If so then they are suitable input for the unsafeRangedSet function.
|
|
|
| Rearrange and merge the ranges in the list so that they are in order and
non-overlapping.
|
|
|
| Create a Ranged Set from a single element.
|
|
|
| :: DiscreteOrdered a | | | => Boundary a | A first lower boundary.
| | -> Boundary a -> Boundary a | A function from a lower boundary to an upper boundary, which must
return a result greater than the argument (not checked).
| | -> Boundary a -> Maybe (Boundary a) | A function from a lower boundary to Maybe the successor lower
boundary, which must return a result greater than the argument
(not checked). If ranges overlap then they will be merged.
| | -> RSet a | | | Construct a range set.
|
|
|
| Predicates
|
|
|
| True if the set has no members.
|
|
|
| True if the negation of the set has no members.
|
|
|
| True if the value is within the ranged set. Infix precedence is left 5.
|
|
|
True if the first argument is a subset of the second argument, or is
equal.
Infix precedence is left 5.
|
|
|
True if the first argument is a strict subset of the second argument.
Infix precedence is left 5.
|
|
| Set Operations
|
|
|
| Set union for ranged sets. Infix precedence is left 6.
|
|
|
| Set intersection for ranged sets. Infix precedence is left 7.
|
|
|
| Set difference. Infix precedence is left 6.
|
|
|
| Set negation.
|
|
| Useful Sets
|
|
|
| The empty set.
|
|
|
| The set that contains everything.
|
|
| QuickCheck Properties
|
|
| Construction
|
|
|
A normalised range list is valid for unsafeRangedSet
prop_validNormalised ls = validRangeList $ normaliseRangeList ls
|
|
|
Iff a value is in a range list then it is in a ranged set
constructed from that list.
prop_has ls v = (ls `rangeListHas` v) == makeRangedSet ls -?- v
|
|
|
Verifies the correct membership of a set containing all integers
starting with the digit "1" up to 19999.
prop_unfold = (v <= 99999 && head (show v) == '1') == (initial1 -?- v)
where
initial1 = rSetUnfold (BoundaryBelow 1) addNines times10
addNines (BoundaryBelow n) = BoundaryAbove $ n * 2 - 1
times10 (BoundaryBelow n) =
if n <= 1000 then Just $ BoundaryBelow $ n * 10 else Nothing
|
|
| Basic Operations
|
|
|
Iff a value is in either of two ranged sets then it is in the union of
those two sets.
prop_union rs1 rs2 v =
(rs1 -?- v || rs2 -?- v) == ((rs1 -\/- rs2) -?- v)
|
|
|
Iff a value is in both of two ranged sets then it is n the intersection
of those two sets.
prop_intersection rs1 rs2 v =
(rs1 -?- v && rs2 -?- v) == ((rs1 -/\- rs2) -?- v)
|
|
|
Iff a value is in ranged set 1 and not in ranged set 2 then it is in the
difference of the two.
prop_difference rs1 rs2 v =
(rs1 -?- v && not (rs2 -?- v)) == ((rs1 -!- rs2) -?- v)
|
|
|
Iff a value is not in a ranged set then it is in its negation.
prop_negation rs v = rs -?- v == not (rSetNegation rs -?- v)
|
|
|
A set that contains a value is not empty
prop_not_empty rs v = (rs -?- v) ==> not (rSetIsEmpty rs)
|
|
| Some Identities and Inequalities
|
|
|
The empty set has no members.
prop_empty v = not (rSetEmpty -?- v)
|
|
|
The full set has every member.
prop_full v = rSetFull -?- v
|
|
|
The intersection of a set with its negation is empty.
prop_empty_intersection rs =
rSetIsEmpty (rs -/\- rSetNegation rs)
|
|
|
The union of a set with its negation is full.
prop_full_union rs v =
rSetIsFull (rs -\/- rSetNegation rs)
|
|
|
The union of two sets is the non-strict superset of both.
prop_union_superset rs1 rs2 =
rs1 -<=- u && rs2 -<=- u
where
u = rs1 -\/- rs2
|
|
|
The intersection of two sets is the non-strict subset of both.
prop_intersection_subset rs1 rs2 =
i -<=- rs1 && i -<=- rs2
where
i = rs1 -/\- rs2
|
|
|
The difference of two sets intersected with the subtractand is empty.
prop_diff_intersect rs1 rs2 =
rSetIsEmpty ((rs1 -!- rs2) -/\- rs2)
|
|
|
A set is the non-strict subset of itself.
prop_subset rs = rs -<=- rs
|
|
|
A set is not the strict subset of itself.
prop_strict_subset rs = not (rs -<- rs)
|
|
|
If rs1 - rs2 is not empty then the union of rs1 and rs2 will be a strict
superset of rs2.
prop_union_strict_superset rs1 rs2 =
(not $ rSetIsEmpty (rs1 -!- rs2))
==> (rs2 -<- (rs1 -\/- rs2))
|
|
|
Intersection commutes.
prop_intersection_commutes rs1 rs2 = (rs1 -/\- rs2) == (rs2 -/\- rs1)
|
|
|
Union commutes.
prop_union_commutes rs1 rs2 = (rs1 -\/- rs2) == (rs2 -\/- rs1)
|
|
|
Intersection associates.
prop_intersection_associates rs1 rs2 rs3 =
((rs1 -/\- rs2) -/\- rs3) == (rs1 -/\- (rs2 -/\- rs3))
|
|
|
Union associates.
prop_union_associates rs1 rs2 rs3 =
((rs1 -\/- rs2) -\/- rs3) == (rs1 -\/- (rs2 -\/- rs3))
|
|
|
De Morgan's Law for Intersection.
prop_de_morgan_intersection rs1 rs2 =
rSetNegation (rs1 -/\- rs2) == (rSetNegation rs1 -\/- rSetNegation rs2)
|
|
|
De Morgan's Law for Union.
prop_de_morgan_union rs1 rs2 =
rSetNegation (rs1 -\/- rs2) == (rSetNegation rs1 -/\- rSetNegation rs2)
|
|
| Produced by Haddock version 2.3.0 |
