module Data.Ranged.RangedSet (
   -- ** Ranged Set Type
   RSet,
   rSetRanges,
   -- ** Ranged Set construction functions and their preconditions
   makeRangedSet,
   unsafeRangedSet,
   validRangeList,
   normaliseRangeList,
   rSingleton,
   rSetUnfold,
   -- ** Predicates
   rSetIsEmpty,
   rSetIsFull,
   (-?-),  rSetHas,
   (-<=-), rSetIsSubset,
   (-<-),  rSetIsSubsetStrict,
   -- ** Set Operations
   (-\/-), rSetUnion,
   (-/\-), rSetIntersection,
   (-!-),  rSetDifference,
   rSetNegation,
   -- ** Useful Sets
   rSetEmpty,
   rSetFull,
   -- ** QuickCheck Properties
   -- *** Construction
   prop_validNormalised,
   prop_has,
   prop_unfold,
   -- *** Basic Operations
   prop_union,
   prop_intersection,
   prop_difference,
   prop_negation,
   prop_not_empty,
   -- *** Some Identities and Inequalities
   -- $ConstructionProperties
   -- $BasicOperationProperties
   -- $SomeIdentitiesAndInequalities
   prop_empty,
   prop_full,
   prop_empty_intersection,
   prop_full_union,
   prop_union_superset,
   prop_intersection_subset,
   prop_diff_intersect,
   prop_subset,
   prop_strict_subset,
   prop_union_strict_superset,
   prop_intersection_commutes,
   prop_union_commutes,
   prop_intersection_associates,
   prop_union_associates,
   prop_de_morgan_intersection,
   prop_de_morgan_union,
) where

import Data.Ranged.Boundaries
import Data.Ranged.Ranges
import Data.Monoid
import Data.Semigroup as Sem

import Data.List
import Test.QuickCheck

infixl 7 -/\-
infixl 6 -\/-, -!-
infixl 5 -<=-, -<-, -?-

-- | An RSet (for Ranged Set) is a list of ranges.  The ranges must be sorted
-- and not overlap.
newtype RSet v = RSet {RSet v -> [Range v]
rSetRanges :: [Range v]}
   deriving (RSet v -> RSet v -> Bool
(RSet v -> RSet v -> Bool)
-> (RSet v -> RSet v -> Bool) -> Eq (RSet v)
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RSet v -> RSet v -> Bool
$c/= :: forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
== :: RSet v -> RSet v -> Bool
$c== :: forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
Eq, Int -> RSet v -> ShowS
[RSet v] -> ShowS
RSet v -> String
(Int -> RSet v -> ShowS)
-> (RSet v -> String) -> ([RSet v] -> ShowS) -> Show (RSet v)
forall v. (Show v, DiscreteOrdered v) => Int -> RSet v -> ShowS
forall v. (Show v, DiscreteOrdered v) => [RSet v] -> ShowS
forall v. (Show v, DiscreteOrdered v) => RSet v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RSet v] -> ShowS
$cshowList :: forall v. (Show v, DiscreteOrdered v) => [RSet v] -> ShowS
show :: RSet v -> String
$cshow :: forall v. (Show v, DiscreteOrdered v) => RSet v -> String
showsPrec :: Int -> RSet v -> ShowS
$cshowsPrec :: forall v. (Show v, DiscreteOrdered v) => Int -> RSet v -> ShowS
Show, Eq (RSet v)
Eq (RSet v)
-> (RSet v -> RSet v -> Ordering)
-> (RSet v -> RSet v -> Bool)
-> (RSet v -> RSet v -> Bool)
-> (RSet v -> RSet v -> Bool)
-> (RSet v -> RSet v -> Bool)
-> (RSet v -> RSet v -> RSet v)
-> (RSet v -> RSet v -> RSet v)
-> Ord (RSet v)
RSet v -> RSet v -> Bool
RSet v -> RSet v -> Ordering
RSet v -> RSet v -> RSet v
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v. DiscreteOrdered v => Eq (RSet v)
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Ordering
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
min :: RSet v -> RSet v -> RSet v
$cmin :: forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
max :: RSet v -> RSet v -> RSet v
$cmax :: forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
>= :: RSet v -> RSet v -> Bool
$c>= :: forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
> :: RSet v -> RSet v -> Bool
$c> :: forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
<= :: RSet v -> RSet v -> Bool
$c<= :: forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
< :: RSet v -> RSet v -> Bool
$c< :: forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
compare :: RSet v -> RSet v -> Ordering
$ccompare :: forall v. DiscreteOrdered v => RSet v -> RSet v -> Ordering
$cp1Ord :: forall v. DiscreteOrdered v => Eq (RSet v)
Ord)

instance DiscreteOrdered a => Sem.Semigroup (RSet a) where
    <> :: RSet a -> RSet a -> RSet a
(<>) = RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
rSetUnion

instance DiscreteOrdered a => Monoid (RSet a) where
    mempty :: RSet a
mempty = RSet a
forall a. DiscreteOrdered a => RSet a
rSetEmpty
    mappend :: RSet a -> RSet a -> RSet a
mappend = RSet a -> RSet a -> RSet a
forall a. Semigroup a => a -> a -> a
(Sem.<>)

-- | 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.
validRangeList :: DiscreteOrdered v => [Range v] -> Bool

validRangeList :: [Range v] -> Bool
validRangeList [] = Bool
True
validRangeList [Range Boundary v
lower Boundary v
upper] = Boundary v
lower Boundary v -> Boundary v -> Bool
forall a. Ord a => a -> a -> Bool
<= Boundary v
upper
validRangeList [Range v]
rs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Range v -> Range v -> Bool) -> [Range v] -> [Range v] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Range v -> Range v -> Bool
forall v. DiscreteOrdered v => Range v -> Range v -> Bool
okAdjacent [Range v]
rs ([Range v] -> [Range v]
forall a. [a] -> [a]
tail [Range v]
rs)
   where
      okAdjacent :: Range v -> Range v -> Bool
okAdjacent (Range Boundary v
lower1 Boundary v
upper1) (Range Boundary v
lower2 Boundary v
upper2) =
         Boundary v
lower1 Boundary v -> Boundary v -> Bool
forall a. Ord a => a -> a -> Bool
<= Boundary v
upper1 Bool -> Bool -> Bool
&& Boundary v
upper1 Boundary v -> Boundary v -> Bool
forall a. Ord a => a -> a -> Bool
<= Boundary v
lower2 Bool -> Bool -> Bool
&& Boundary v
lower2 Boundary v -> Boundary v -> Bool
forall a. Ord a => a -> a -> Bool
<= Boundary v
upper2


-- | Rearrange and merge the ranges in the list so that they are in order and
-- non-overlapping.
normaliseRangeList :: DiscreteOrdered v => [Range v] -> [Range v]
normaliseRangeList :: [Range v] -> [Range v]
normaliseRangeList = [Range v] -> [Range v]
forall v. DiscreteOrdered v => [Range v] -> [Range v]
normalise ([Range v] -> [Range v])
-> ([Range v] -> [Range v]) -> [Range v] -> [Range v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Range v] -> [Range v]
forall a. Ord a => [a] -> [a]
sort ([Range v] -> [Range v])
-> ([Range v] -> [Range v]) -> [Range v] -> [Range v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range v -> Bool) -> [Range v] -> [Range v]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Range v -> Bool) -> Range v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range v -> Bool
forall v. DiscreteOrdered v => Range v -> Bool
rangeIsEmpty)


-- Private routine: normalise a range list that is known to be already sorted.
-- This precondition is not checked.
normalise :: DiscreteOrdered v => [Range v] -> [Range v]
normalise :: [Range v] -> [Range v]
normalise (Range v
r1:Range v
r2:[Range v]
rs) =
         if Range v -> Range v -> Bool
forall v. DiscreteOrdered v => Range v -> Range v -> Bool
overlap Range v
r1 Range v
r2
               then [Range v] -> [Range v]
forall v. DiscreteOrdered v => [Range v] -> [Range v]
normalise ([Range v] -> [Range v]) -> [Range v] -> [Range v]
forall a b. (a -> b) -> a -> b
$
                       Boundary v -> Boundary v -> Range v
forall v. Boundary v -> Boundary v -> Range v
Range (Range v -> Boundary v
forall v. Range v -> Boundary v
rangeLower Range v
r1)
                             (Boundary v -> Boundary v -> Boundary v
forall a. Ord a => a -> a -> a
max (Range v -> Boundary v
forall v. Range v -> Boundary v
rangeUpper Range v
r1) (Range v -> Boundary v
forall v. Range v -> Boundary v
rangeUpper Range v
r2))
                       Range v -> [Range v] -> [Range v]
forall a. a -> [a] -> [a]
: [Range v]
rs
               else Range v
r1 Range v -> [Range v] -> [Range v]
forall a. a -> [a] -> [a]
: ([Range v] -> [Range v]
forall v. DiscreteOrdered v => [Range v] -> [Range v]
normalise ([Range v] -> [Range v]) -> [Range v] -> [Range v]
forall a b. (a -> b) -> a -> b
$ Range v
r2 Range v -> [Range v] -> [Range v]
forall a. a -> [a] -> [a]
: [Range v]
rs)
   where
      overlap :: Range v -> Range v -> Bool
overlap (Range Boundary v
_ Boundary v
upper1) (Range Boundary v
lower2 Boundary v
_) = Boundary v
upper1 Boundary v -> Boundary v -> Bool
forall a. Ord a => a -> a -> Bool
>= Boundary v
lower2

normalise [Range v]
rs = [Range v]
rs


-- | Create a new Ranged Set from a list of ranges.  The list may contain
-- ranges that overlap or are not in ascending order.
makeRangedSet :: DiscreteOrdered v => [Range v] -> RSet v
makeRangedSet :: [Range v] -> RSet v
makeRangedSet = [Range v] -> RSet v
forall v. [Range v] -> RSet v
RSet ([Range v] -> RSet v)
-> ([Range v] -> [Range v]) -> [Range v] -> RSet v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Range v] -> [Range v]
forall v. DiscreteOrdered v => [Range v] -> [Range v]
normaliseRangeList


-- | Create a new Ranged Set from a list of ranges. @validRangeList ranges@
-- must return @True@.  This precondition is not checked.
unsafeRangedSet :: DiscreteOrdered v => [Range v] -> RSet v
unsafeRangedSet :: [Range v] -> RSet v
unsafeRangedSet = [Range v] -> RSet v
forall v. [Range v] -> RSet v
RSet

-- | Create a Ranged Set from a single element.
rSingleton :: DiscreteOrdered v => v -> RSet v
rSingleton :: v -> RSet v
rSingleton v
v = [Range v] -> RSet v
forall v. DiscreteOrdered v => [Range v] -> RSet v
unsafeRangedSet [v -> Range v
forall v. DiscreteOrdered v => v -> Range v
singletonRange v
v]

-- | True if the set has no members.
rSetIsEmpty :: DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty :: RSet v -> Bool
rSetIsEmpty = [Range v] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Range v] -> Bool) -> (RSet v -> [Range v]) -> RSet v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSet v -> [Range v]
forall v. RSet v -> [Range v]
rSetRanges


-- | True if the negation of the set has no members.
rSetIsFull :: DiscreteOrdered v => RSet v -> Bool
rSetIsFull :: RSet v -> Bool
rSetIsFull = RSet v -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty (RSet v -> Bool) -> (RSet v -> RSet v) -> RSet v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSet v -> RSet v
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation


-- | True if the value is within the ranged set.  Infix precedence is left 5.
rSetHas, (-?-) :: DiscreteOrdered v => RSet v -> v -> Bool
rSetHas :: RSet v -> v -> Bool
rSetHas (RSet [Range v]
ls) v
value = [Range v] -> Bool
rSetHas1 [Range v]
ls
   where
      rSetHas1 :: [Range v] -> Bool
rSetHas1 [] = Bool
False
      rSetHas1 (Range v
r:[Range v]
rs)
         | v
value v -> Boundary v -> Bool
forall v. Ord v => v -> Boundary v -> Bool
/>/ Range v -> Boundary v
forall v. Range v -> Boundary v
rangeLower Range v
r = Range v -> v -> Bool
forall v. Ord v => Range v -> v -> Bool
rangeHas Range v
r v
value Bool -> Bool -> Bool
|| [Range v] -> Bool
rSetHas1 [Range v]
rs
         | Bool
otherwise              = Bool
False

-?- :: RSet v -> v -> Bool
(-?-) = RSet v -> v -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
rSetHas

-- | True if the first argument is a subset of the second argument, or is
-- equal.
--
-- Infix precedence is left 5.
rSetIsSubset, (-<=-) :: DiscreteOrdered v => RSet v -> RSet v -> Bool
rSetIsSubset :: RSet v -> RSet v -> Bool
rSetIsSubset RSet v
rs1 RSet v
rs2 = RSet v -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty (RSet v
rs1 RSet v -> RSet v -> RSet v
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-!- RSet v
rs2)
-<=- :: RSet v -> RSet v -> Bool
(-<=-) = RSet v -> RSet v -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
rSetIsSubset


-- | True if the first argument is a strict subset of the second argument.
--
-- Infix precedence is left 5.
rSetIsSubsetStrict, (-<-) :: DiscreteOrdered v => RSet v -> RSet v -> Bool
rSetIsSubsetStrict :: RSet v -> RSet v -> Bool
rSetIsSubsetStrict RSet v
rs1 RSet v
rs2 =
   RSet v -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty (RSet v
rs1 RSet v -> RSet v -> RSet v
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-!- RSet v
rs2)
   Bool -> Bool -> Bool
&& Bool -> Bool
not (RSet v -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty (RSet v
rs2 RSet v -> RSet v -> RSet v
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-!- RSet v
rs1))

-<- :: RSet v -> RSet v -> Bool
(-<-) = RSet v -> RSet v -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
rSetIsSubsetStrict

-- | Set union for ranged sets.  Infix precedence is left 6.
rSetUnion, (-\/-) :: DiscreteOrdered v => RSet v -> RSet v -> RSet v
-- Implementation note: rSetUnion merges the two lists into a single
-- sorted list and then calls normalise to combine overlapping ranges.
rSetUnion :: RSet v -> RSet v -> RSet v
rSetUnion (RSet [Range v]
ls1) (RSet [Range v]
ls2) = [Range v] -> RSet v
forall v. [Range v] -> RSet v
RSet ([Range v] -> RSet v) -> [Range v] -> RSet v
forall a b. (a -> b) -> a -> b
$ [Range v] -> [Range v]
forall v. DiscreteOrdered v => [Range v] -> [Range v]
normalise ([Range v] -> [Range v]) -> [Range v] -> [Range v]
forall a b. (a -> b) -> a -> b
$ [Range v] -> [Range v] -> [Range v]
forall a. Ord a => [a] -> [a] -> [a]
merge [Range v]
ls1 [Range v]
ls2
   where
      merge :: [a] -> [a] -> [a]
merge [a]
ms1 [] = [a]
ms1
      merge [] [a]
ms2 = [a]
ms2
      merge ms1 :: [a]
ms1@(a
h1:[a]
t1) ms2 :: [a]
ms2@(a
h2:[a]
t2) =
         if a
h1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<  a
h2
            then a
h1 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
merge [a]
t1 [a]
ms2
            else a
h2 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
merge [a]
ms1 [a]
t2

-\/- :: RSet v -> RSet v -> RSet v
(-\/-) = RSet v -> RSet v -> RSet v
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
rSetUnion

-- | Set intersection for ranged sets.  Infix precedence is left 7.
rSetIntersection, (-/\-) :: DiscreteOrdered v => RSet v -> RSet v -> RSet v
rSetIntersection :: RSet v -> RSet v -> RSet v
rSetIntersection (RSet [Range v]
ls1) (RSet [Range v]
ls2) =
   [Range v] -> RSet v
forall v. [Range v] -> RSet v
RSet ([Range v] -> RSet v) -> [Range v] -> RSet v
forall a b. (a -> b) -> a -> b
$ (Range v -> Bool) -> [Range v] -> [Range v]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Range v -> Bool) -> Range v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range v -> Bool
forall v. DiscreteOrdered v => Range v -> Bool
rangeIsEmpty) ([Range v] -> [Range v]) -> [Range v] -> [Range v]
forall a b. (a -> b) -> a -> b
$ [Range v] -> [Range v] -> [Range v]
forall v. DiscreteOrdered v => [Range v] -> [Range v] -> [Range v]
merge [Range v]
ls1 [Range v]
ls2
   where
      merge :: [Range v] -> [Range v] -> [Range v]
merge ms1 :: [Range v]
ms1@(Range v
h1:[Range v]
t1) ms2 :: [Range v]
ms2@(Range v
h2:[Range v]
t2) =
         Range v -> Range v -> Range v
forall v. DiscreteOrdered v => Range v -> Range v -> Range v
rangeIntersection Range v
h1 Range v
h2
         Range v -> [Range v] -> [Range v]
forall a. a -> [a] -> [a]
: if Range v -> Boundary v
forall v. Range v -> Boundary v
rangeUpper Range v
h1 Boundary v -> Boundary v -> Bool
forall a. Ord a => a -> a -> Bool
< Range v -> Boundary v
forall v. Range v -> Boundary v
rangeUpper Range v
h2
               then [Range v] -> [Range v] -> [Range v]
merge [Range v]
t1 [Range v]
ms2
               else [Range v] -> [Range v] -> [Range v]
merge [Range v]
ms1 [Range v]
t2
      merge [Range v]
_ [Range v]
_ = []

-/\- :: RSet v -> RSet v -> RSet v
(-/\-) = RSet v -> RSet v -> RSet v
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
rSetIntersection


-- | Set difference.  Infix precedence is left 6.
rSetDifference, (-!-) :: DiscreteOrdered v => RSet v -> RSet v -> RSet v
rSetDifference :: RSet v -> RSet v -> RSet v
rSetDifference RSet v
rs1 RSet v
rs2 = RSet v
rs1 RSet v -> RSet v -> RSet v
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- (RSet v -> RSet v
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation RSet v
rs2)
-!- :: RSet v -> RSet v -> RSet v
(-!-) = RSet v -> RSet v -> RSet v
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
rSetDifference


-- | Set negation.
rSetNegation :: DiscreteOrdered a => RSet a -> RSet a
rSetNegation :: RSet a -> RSet a
rSetNegation RSet a
set = [Range a] -> RSet a
forall v. [Range v] -> RSet v
RSet ([Range a] -> RSet a) -> [Range a] -> RSet a
forall a b. (a -> b) -> a -> b
$ [Boundary a] -> [Range a]
forall v. [Boundary v] -> [Range v]
ranges1 ([Boundary a] -> [Range a]) -> [Boundary a] -> [Range a]
forall a b. (a -> b) -> a -> b
$ [Boundary a]
setBounds1
   where
      ranges1 :: [Boundary v] -> [Range v]
ranges1 (Boundary v
b1:Boundary v
b2:[Boundary v]
bs) = Boundary v -> Boundary v -> Range v
forall v. Boundary v -> Boundary v -> Range v
Range Boundary v
b1 Boundary v
b2 Range v -> [Range v] -> [Range v]
forall a. a -> [a] -> [a]
: [Boundary v] -> [Range v]
ranges1 [Boundary v]
bs
      ranges1 [Boundary v
BoundaryAboveAll] = []
      ranges1 [Boundary v
b] = [Boundary v -> Boundary v -> Range v
forall v. Boundary v -> Boundary v -> Range v
Range Boundary v
b Boundary v
forall a. Boundary a
BoundaryAboveAll]
      ranges1 [Boundary v]
_ = []
      setBounds1 :: [Boundary a]
setBounds1 = case [Boundary a]
setBounds of
         (Boundary a
BoundaryBelowAll : [Boundary a]
bs)  -> [Boundary a]
bs
         [Boundary a]
_                        -> Boundary a
forall a. Boundary a
BoundaryBelowAll Boundary a -> [Boundary a] -> [Boundary a]
forall a. a -> [a] -> [a]
: [Boundary a]
setBounds
      setBounds :: [Boundary a]
setBounds = [Range a] -> [Boundary a]
forall v. [Range v] -> [Boundary v]
bounds ([Range a] -> [Boundary a]) -> [Range a] -> [Boundary a]
forall a b. (a -> b) -> a -> b
$ RSet a -> [Range a]
forall v. RSet v -> [Range v]
rSetRanges RSet a
set
      bounds :: [Range v] -> [Boundary v]
bounds (Range v
r:[Range v]
rs) = Range v -> Boundary v
forall v. Range v -> Boundary v
rangeLower Range v
r Boundary v -> [Boundary v] -> [Boundary v]
forall a. a -> [a] -> [a]
: Range v -> Boundary v
forall v. Range v -> Boundary v
rangeUpper Range v
r Boundary v -> [Boundary v] -> [Boundary v]
forall a. a -> [a] -> [a]
: [Range v] -> [Boundary v]
bounds [Range v]
rs
      bounds [Range v]
_ = []

-- | The empty set.
rSetEmpty :: DiscreteOrdered a => RSet a
rSetEmpty :: RSet a
rSetEmpty = [Range a] -> RSet a
forall v. [Range v] -> RSet v
RSet []

-- | The set that contains everything.
rSetFull :: DiscreteOrdered a => RSet a
rSetFull :: RSet a
rSetFull = [Range a] -> RSet a
forall v. [Range v] -> RSet v
RSet [Boundary a -> Boundary a -> Range a
forall v. Boundary v -> Boundary v -> Range v
Range Boundary a
forall a. Boundary a
BoundaryBelowAll Boundary a
forall a. Boundary a
BoundaryAboveAll]

-- | Construct a range set.
rSetUnfold :: 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
rSetUnfold :: Boundary a
-> (Boundary a -> Boundary a)
-> (Boundary a -> Maybe (Boundary a))
-> RSet a
rSetUnfold Boundary a
bound Boundary a -> Boundary a
upperFunc Boundary a -> Maybe (Boundary a)
succFunc = [Range a] -> RSet a
forall v. [Range v] -> RSet v
RSet ([Range a] -> RSet a) -> [Range a] -> RSet a
forall a b. (a -> b) -> a -> b
$ [Range a] -> [Range a]
forall v. DiscreteOrdered v => [Range v] -> [Range v]
normalise ([Range a] -> [Range a]) -> [Range a] -> [Range a]
forall a b. (a -> b) -> a -> b
$ Boundary a -> [Range a]
ranges1 Boundary a
bound
   where
      ranges1 :: Boundary a -> [Range a]
ranges1 Boundary a
b =
         Boundary a -> Boundary a -> Range a
forall v. Boundary v -> Boundary v -> Range v
Range Boundary a
b (Boundary a -> Boundary a
upperFunc Boundary a
b)
         Range a -> [Range a] -> [Range a]
forall a. a -> [a] -> [a]
: case Boundary a -> Maybe (Boundary a)
succFunc Boundary a
b of
            Just Boundary a
b2 -> Boundary a -> [Range a]
ranges1 Boundary a
b2
            Maybe (Boundary a)
Nothing -> []


-- QuickCheck Generators

instance (Arbitrary v, DiscreteOrdered v, Show v) =>
      Arbitrary (RSet v)
   where
   arbitrary :: Gen (RSet v)
arbitrary = [(Int, Gen (RSet v))] -> Gen (RSet v)
forall a. [(Int, Gen a)] -> Gen a
frequency [
      (Int
1, RSet v -> Gen (RSet v)
forall (m :: * -> *) a. Monad m => a -> m a
return RSet v
forall a. DiscreteOrdered a => RSet a
rSetEmpty),
      (Int
1, RSet v -> Gen (RSet v)
forall (m :: * -> *) a. Monad m => a -> m a
return RSet v
forall a. DiscreteOrdered a => RSet a
rSetFull),
      (Int
18, do
         [Boundary v]
ls <- Gen [Boundary v]
forall a. Arbitrary a => Gen a
arbitrary
         RSet v -> Gen (RSet v)
forall (m :: * -> *) a. Monad m => a -> m a
return (RSet v -> Gen (RSet v)) -> RSet v -> Gen (RSet v)
forall a b. (a -> b) -> a -> b
$ [Range v] -> RSet v
forall v. DiscreteOrdered v => [Range v] -> RSet v
makeRangedSet ([Range v] -> RSet v) -> [Range v] -> RSet v
forall a b. (a -> b) -> a -> b
$ [Boundary v] -> [Range v]
forall v. [Boundary v] -> [Range v]
rangeList ([Boundary v] -> [Range v]) -> [Boundary v] -> [Range v]
forall a b. (a -> b) -> a -> b
$ [Boundary v] -> [Boundary v]
forall a. Ord a => [a] -> [a]
sort [Boundary v]
ls
      )]
      where
         -- Arbitrary lists of ranges don't give many interesting sets after
         -- normalisation.  So instead generate a sorted list of boundaries
         -- and pair them off.  Odd boundaries are dropped.
         rangeList :: [Boundary v] -> [Range v]
rangeList (Boundary v
b1:Boundary v
b2:[Boundary v]
bs) = Boundary v -> Boundary v -> Range v
forall v. Boundary v -> Boundary v -> Range v
Range Boundary v
b1 Boundary v
b2 Range v -> [Range v] -> [Range v]
forall a. a -> [a] -> [a]
: [Boundary v] -> [Range v]
rangeList [Boundary v]
bs
         rangeList [Boundary v]
_ = []

instance (CoArbitrary v, DiscreteOrdered v, Show v) =>
      CoArbitrary (RSet v)
   where
   coarbitrary :: RSet v -> Gen b -> Gen b
coarbitrary (RSet [Range v]
ls) = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
variant (Int
0 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Range v] -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary [Range v]
ls

-- ==================================================================
-- QuickCheck Properties
-- ==================================================================

---------------------------------------------------------------------
-- Construction properties
---------------------------------------------------------------------

-- | A normalised range list is valid for unsafeRangedSet
--
-- > prop_validNormalised ls = validRangeList $ normaliseRangeList ls
prop_validNormalised :: (DiscreteOrdered a) => [Range a] -> Bool
prop_validNormalised :: [Range a] -> Bool
prop_validNormalised [Range a]
ls = [Range a] -> Bool
forall v. DiscreteOrdered v => [Range v] -> Bool
validRangeList ([Range a] -> Bool) -> [Range a] -> Bool
forall a b. (a -> b) -> a -> b
$ [Range a] -> [Range a]
forall v. DiscreteOrdered v => [Range v] -> [Range v]
normaliseRangeList [Range a]
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
prop_has :: (DiscreteOrdered a) => [Range a] -> a -> Bool
prop_has :: [Range a] -> a -> Bool
prop_has [Range a]
ls a
v = ([Range a]
ls [Range a] -> a -> Bool
forall v. Ord v => [Range v] -> v -> Bool
`rangeListHas` a
v) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== [Range a] -> RSet a
forall v. DiscreteOrdered v => [Range v] -> RSet v
makeRangedSet [Range a]
ls RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
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

prop_unfold :: Integer -> Bool
prop_unfold :: Integer -> Bool
prop_unfold Integer
v = (Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
99999 Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
head (Integer -> String
forall a. Show a => a -> String
show Integer
v) Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'1') Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (RSet Integer
initial1 RSet Integer -> Integer -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- Integer
v)
   where
      initial1 :: RSet Integer
initial1 = Boundary Integer
-> (Boundary Integer -> Boundary Integer)
-> (Boundary Integer -> Maybe (Boundary Integer))
-> RSet Integer
forall a.
DiscreteOrdered a =>
Boundary a
-> (Boundary a -> Boundary a)
-> (Boundary a -> Maybe (Boundary a))
-> RSet a
rSetUnfold (Integer -> Boundary Integer
forall a. a -> Boundary a
BoundaryBelow Integer
1) Boundary Integer -> Boundary Integer
forall a. Num a => Boundary a -> Boundary a
addNines Boundary Integer -> Maybe (Boundary Integer)
forall a. (Ord a, Num a) => Boundary a -> Maybe (Boundary a)
times10
      addNines :: Boundary a -> Boundary a
addNines (BoundaryBelow a
n) = a -> Boundary a
forall a. a -> Boundary a
BoundaryAbove (a -> Boundary a) -> a -> Boundary a
forall a b. (a -> b) -> a -> b
$ a
n a -> a -> a
forall a. Num a => a -> a -> a
* a
2 a -> a -> a
forall a. Num a => a -> a -> a
- a
1
      addNines Boundary a
_ = String -> Boundary a
forall a. HasCallStack => String -> a
error String
"Can't happen"
      times10 :: Boundary a -> Maybe (Boundary a)
times10 (BoundaryBelow a
n) =
         if a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
10000 then Boundary a -> Maybe (Boundary a)
forall a. a -> Maybe a
Just (Boundary a -> Maybe (Boundary a))
-> Boundary a -> Maybe (Boundary a)
forall a b. (a -> b) -> a -> b
$ a -> Boundary a
forall a. a -> Boundary a
BoundaryBelow (a -> Boundary a) -> a -> Boundary a
forall a b. (a -> b) -> a -> b
$ a
n a -> a -> a
forall a. Num a => a -> a -> a
* a
10 else Maybe (Boundary a)
forall a. Maybe a
Nothing
      times10 Boundary a
_ = String -> Maybe (Boundary a)
forall a. HasCallStack => String -> a
error String
"Can't happen"

---------------------------------------------------------------------
-- Basic operation properties
---------------------------------------------------------------------

-- | 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)
prop_union :: (DiscreteOrdered a ) => RSet a -> RSet a -> a -> Bool
prop_union :: RSet a -> RSet a -> a -> Bool
prop_union RSet a
rs1 RSet a
rs2 a
v = (RSet a
rs1 RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v Bool -> Bool -> Bool
|| RSet a
rs2 RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== ((RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
rs2) RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
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)
prop_intersection :: (DiscreteOrdered a) => RSet a -> RSet a -> a -> Bool
prop_intersection :: RSet a -> RSet a -> a -> Bool
prop_intersection RSet a
rs1 RSet a
rs2 a
v =
   (RSet a
rs1 RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v Bool -> Bool -> Bool
&& RSet a
rs2 RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== ((RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs2) RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
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)
prop_difference :: (DiscreteOrdered a) => RSet a -> RSet a -> a -> Bool
prop_difference :: RSet a -> RSet a -> a -> Bool
prop_difference RSet a
rs1 RSet a
rs2 a
v =
   (RSet a
rs1 RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v Bool -> Bool -> Bool
&& Bool -> Bool
not (RSet a
rs2 RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v)) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== ((RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-!- RSet a
rs2) RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
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)
prop_negation :: (DiscreteOrdered a) => RSet a -> a -> Bool
prop_negation :: RSet a -> a -> Bool
prop_negation RSet a
rs a
v = RSet a
rs RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Bool
not (RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation RSet a
rs RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v)

-- | A set that contains a value is not empty
--
-- > prop_not_empty rs v = (rs -?- v) ==> not (rSetIsEmpty rs)
prop_not_empty :: (DiscreteOrdered a) => RSet a -> a -> Property
prop_not_empty :: RSet a -> a -> Property
prop_not_empty RSet a
rs a
v = (RSet a
rs RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> Bool -> Bool
not (RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty RSet a
rs)

---------------------------------------------------------------------
-- Some identities and inequalities of sets
---------------------------------------------------------------------

-- | The empty set has no members.
--
-- > prop_empty v = not (rSetEmpty -?- v)
prop_empty :: (DiscreteOrdered a) => a -> Bool
prop_empty :: a -> Bool
prop_empty a
v = Bool -> Bool
not (RSet a
forall a. DiscreteOrdered a => RSet a
rSetEmpty RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v)

-- | The full set has every member.
--
-- > prop_full v = rSetFull -?- v
prop_full :: (DiscreteOrdered a) => a -> Bool
prop_full :: a -> Bool
prop_full a
v = RSet a
forall a. DiscreteOrdered a => RSet a
rSetFull RSet a -> a -> Bool
forall v. DiscreteOrdered v => RSet v -> v -> Bool
-?- a
v

-- | The intersection of a set with its negation is empty.
--
-- > prop_empty_intersection rs =
-- >    rSetIsEmpty (rs -/\- rSetNegation rs)
prop_empty_intersection :: (DiscreteOrdered a) => RSet a -> Bool
prop_empty_intersection :: RSet a -> Bool
prop_empty_intersection RSet a
rs =
   RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty (RSet a
rs RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation RSet a
rs)

-- | The union of a set with its negation is full.
--
-- > prop_full_union rs v =
-- >    rSetIsFull (rs -\/- rSetNegation rs)
prop_full_union :: (DiscreteOrdered a) => RSet a -> Bool
prop_full_union :: RSet a -> Bool
prop_full_union RSet a
rs =
   RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsFull (RSet a
rs RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation RSet a
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
prop_union_superset :: (DiscreteOrdered a) => RSet a -> RSet a -> Bool
prop_union_superset :: RSet a -> RSet a -> Bool
prop_union_superset RSet a
rs1 RSet a
rs2 =
   RSet a
rs1 RSet a -> RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
-<=- RSet a
u Bool -> Bool -> Bool
&& RSet a
rs2 RSet a -> RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
-<=- RSet a
u
   where
      u :: RSet a
u = RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
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
prop_intersection_subset :: (DiscreteOrdered a) => RSet a -> RSet a -> Bool
prop_intersection_subset :: RSet a -> RSet a -> Bool
prop_intersection_subset RSet a
rs1 RSet a
rs2 = RSet a
i RSet a -> RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
-<=- RSet a
rs1 Bool -> Bool -> Bool
&& RSet a
i RSet a -> RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
-<=- RSet a
rs2
   where
      i :: RSet a
i = RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs2

-- | The difference of two sets intersected with the subtractand is empty.
--
-- > prop_diff_intersect rs1 rs2 =
-- >    rSetIsEmpty ((rs1 -!- rs2) -/\- rs2)
prop_diff_intersect :: (DiscreteOrdered a) => RSet a -> RSet a -> Bool
prop_diff_intersect :: RSet a -> RSet a -> Bool
prop_diff_intersect RSet a
rs1 RSet a
rs2 = RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty ((RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-!- RSet a
rs2) RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs2)

-- | A set is the non-strict subset of itself.
--
-- > prop_subset rs = rs -<=- rs
prop_subset :: (DiscreteOrdered a) => RSet a -> Bool
prop_subset :: RSet a -> Bool
prop_subset RSet a
rs = RSet a
rs RSet a -> RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
-<=- RSet a
rs

-- | A set is not the strict subset of itself.
--
-- > prop_strict_subset rs = not (rs -<- rs)
prop_strict_subset :: (DiscreteOrdered a) => RSet a -> Bool
prop_strict_subset :: RSet a -> Bool
prop_strict_subset RSet a
rs = Bool -> Bool
not (RSet a
rs RSet a -> RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
-<- RSet a
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))
prop_union_strict_superset :: (DiscreteOrdered a) => RSet a -> RSet a -> Property
prop_union_strict_superset :: RSet a -> RSet a -> Property
prop_union_strict_superset RSet a
rs1 RSet a
rs2 =
   (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> Bool
rSetIsEmpty (RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-!- RSet a
rs2)) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (RSet a
rs2 RSet a -> RSet a -> Bool
forall v. DiscreteOrdered v => RSet v -> RSet v -> Bool
-<- (RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
rs2))

-- | Intersection commutes.
--
-- > prop_intersection_commutes rs1 rs2 = (rs1 -/\- rs2) == (rs2 -/\- rs1)
prop_intersection_commutes :: (DiscreteOrdered a) => RSet a -> RSet a -> Bool
prop_intersection_commutes :: RSet a -> RSet a -> Bool
prop_intersection_commutes RSet a
rs1 RSet a
rs2 = (RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs2) RSet a -> RSet a -> Bool
forall a. Eq a => a -> a -> Bool
== (RSet a
rs2 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs1)

-- | Union commutes.
--
-- > prop_union_commutes rs1 rs2 = (rs1 -\/- rs2) == (rs2 -\/- rs1)
prop_union_commutes :: (DiscreteOrdered a) => RSet a -> RSet a -> Bool
prop_union_commutes :: RSet a -> RSet a -> Bool
prop_union_commutes RSet a
rs1 RSet a
rs2 = (RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
rs2) RSet a -> RSet a -> Bool
forall a. Eq a => a -> a -> Bool
== (RSet a
rs2 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
rs1)

-- | Intersection associates.
--
-- > prop_intersection_associates rs1 rs2 rs3 =
-- >    ((rs1 -/\- rs2) -/\- rs3) == (rs1 -/\- (rs2 -/\- rs3))
prop_intersection_associates :: (DiscreteOrdered a) =>
   RSet a -> RSet a  -> RSet a -> Bool
prop_intersection_associates :: RSet a -> RSet a -> RSet a -> Bool
prop_intersection_associates RSet a
rs1 RSet a
rs2 RSet a
rs3 =
   ((RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs2) RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs3) RSet a -> RSet a -> Bool
forall a. Eq a => a -> a -> Bool
== (RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- (RSet a
rs2 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs3))

-- | Union associates.
--
-- > prop_union_associates rs1 rs2 rs3 =
-- >    ((rs1 -\/- rs2) -\/- rs3) == (rs1 -\/- (rs2 -\/- rs3))
prop_union_associates :: (DiscreteOrdered a) =>
   RSet a -> RSet a  -> RSet a -> Bool
prop_union_associates :: RSet a -> RSet a -> RSet a -> Bool
prop_union_associates RSet a
rs1 RSet a
rs2 RSet a
rs3 =
   ((RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
rs2) RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
rs3) RSet a -> RSet a -> Bool
forall a. Eq a => a -> a -> Bool
== (RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- (RSet a
rs2 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
rs3))

-- | De Morgan's Law for Intersection.
--
-- > prop_de_morgan_intersection rs1 rs2 =
-- >    rSetNegation (rs1 -/\- rs2) == (rSetNegation rs1 -\/- rSetNegation rs2)
prop_de_morgan_intersection :: (DiscreteOrdered a) => RSet a -> RSet a -> Bool
prop_de_morgan_intersection :: RSet a -> RSet a -> Bool
prop_de_morgan_intersection RSet a
rs1 RSet a
rs2 =
   RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation (RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a
rs2) RSet a -> RSet a -> Bool
forall a. Eq a => a -> a -> Bool
== (RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation RSet a
rs2)

-- | De Morgan's Law for Union.
--
-- > prop_de_morgan_union rs1 rs2 =
-- >    rSetNegation (rs1 -\/- rs2) == (rSetNegation rs1 -/\- rSetNegation rs2)

prop_de_morgan_union :: (DiscreteOrdered a) => RSet a -> RSet a -> Bool
prop_de_morgan_union :: RSet a -> RSet a -> Bool
prop_de_morgan_union RSet a
rs1 RSet a
rs2 =
   RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation (RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-\/- RSet a
rs2) RSet a -> RSet a -> Bool
forall a. Eq a => a -> a -> Bool
== (RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation RSet a
rs1 RSet a -> RSet a -> RSet a
forall v. DiscreteOrdered v => RSet v -> RSet v -> RSet v
-/\- RSet a -> RSet a
forall a. DiscreteOrdered a => RSet a -> RSet a
rSetNegation RSet a
rs2)