{- HLINT ignore -}
{-|
Module      : Interval Algebra Axioms
Description : Properties of Intervals
Copyright   : (c) NoviSci, Inc 2020
License     : BSD3
Maintainer  : bsaul@novisci.com

This module exports a single typeclass @IntervalAxioms@ which contains
property-based tests for the axioms in section 1 of [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x).
The notation below is that of the original paper.

This module is useful if creating a new instance of interval types that you want to test.

-}

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}


module IntervalAlgebra.Axioms
  ( IntervalAxioms(..)
  , M1set(..)
  , M2set(..)
  , M5set(..)
  ) where

import           Data.Either               (isRight)
import           Data.Maybe                (fromJust, isJust, isNothing)
import           Data.Set                  (Set, disjointUnion, fromList,
                                            member)
import           Data.Time                 as DT (Day (..), DiffTime,
                                                  NominalDiffTime, UTCTime (..))
import           IntervalAlgebra.Arbitrary
import           IntervalAlgebra.Core
import           Test.QuickCheck           (Arbitrary (arbitrary), Property,
                                            (===), (==>))


xor :: Bool -> Bool -> Bool
xor :: Bool -> Bool -> Bool
xor Bool
a Bool
b = Bool
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
b

-- | Internal function for converting a number to a strictly positive value.
makePos :: (Ord b, Num b) => b -> b
makePos :: forall b. (Ord b, Num b) => b -> b
makePos b
x | b
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
0    = b
x b -> b -> b
forall a. Num a => a -> a -> a
+ b
1
          | b
x b -> b -> Bool
forall a. Ord a => a -> a -> Bool
< b
0     = b -> b
forall a. Num a => a -> a
negate b
x
          | Bool
otherwise = b
x

-- | A set used for testing M1 defined so that the M1 condition is true.
data M1set a = M1set
  { forall a. M1set a -> Interval a
m11 :: Interval a
  , forall a. M1set a -> Interval a
m12 :: Interval a
  , forall a. M1set a -> Interval a
m13 :: Interval a
  , forall a. M1set a -> Interval a
m14 :: Interval a
  }
  deriving Int -> M1set a -> ShowS
[M1set a] -> ShowS
M1set a -> String
(Int -> M1set a -> ShowS)
-> (M1set a -> String) -> ([M1set a] -> ShowS) -> Show (M1set a)
forall a. (Show a, Ord a) => Int -> M1set a -> ShowS
forall a. (Show a, Ord a) => [M1set a] -> ShowS
forall a. (Show a, Ord a) => M1set a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M1set a] -> ShowS
$cshowList :: forall a. (Show a, Ord a) => [M1set a] -> ShowS
show :: M1set a -> String
$cshow :: forall a. (Show a, Ord a) => M1set a -> String
showsPrec :: Int -> M1set a -> ShowS
$cshowsPrec :: forall a. (Show a, Ord a) => Int -> M1set a -> ShowS
Show

instance Arbitrary (M1set Int) where
  arbitrary :: Gen (M1set Int)
arbitrary = do
    Interval Int
x <- Gen (Interval Int)
forall a. Arbitrary a => Gen a
arbitrary
    Int
a <- Gen Int
forall a. Arbitrary a => Gen a
arbitrary
    Int
b <- Gen Int
forall a. Arbitrary a => Gen a
arbitrary
    Interval Int -> Int -> Int -> Int -> M1set Int
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> b -> M1set a
m1set Interval Int
x Int
a Int
b (Int -> M1set Int) -> Gen Int -> Gen (M1set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M1set DT.Day) where
  arbitrary :: Gen (M1set Day)
arbitrary = do
    Interval Day
x <- Gen (Interval Day)
forall a. Arbitrary a => Gen a
arbitrary
    Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
    Integer
b <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
    Interval Day -> Integer -> Integer -> Integer -> M1set Day
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> b -> M1set a
m1set Interval Day
x Integer
a Integer
b (Integer -> M1set Day) -> Gen Integer -> Gen (M1set Day)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M1set DT.UTCTime) where
  arbitrary :: Gen (M1set UTCTime)
arbitrary = do
    Interval UTCTime
x <- Gen (Interval UTCTime)
forall a. Arbitrary a => Gen a
arbitrary
    NominalDiffTime
a <- Gen NominalDiffTime
forall a. Arbitrary a => Gen a
arbitrary
    NominalDiffTime
b <- Gen NominalDiffTime
forall a. Arbitrary a => Gen a
arbitrary
    Interval UTCTime
-> NominalDiffTime
-> NominalDiffTime
-> NominalDiffTime
-> M1set UTCTime
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> b -> M1set a
m1set Interval UTCTime
x NominalDiffTime
a NominalDiffTime
b (NominalDiffTime -> M1set UTCTime)
-> Gen NominalDiffTime -> Gen (M1set UTCTime)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen NominalDiffTime
forall a. Arbitrary a => Gen a
arbitrary


-- | A set used for testing M2 defined so that the M2 condition is true.
data M2set a = M2set
  { forall a. M2set a -> Interval a
m21 :: Interval a
  , forall a. M2set a -> Interval a
m22 :: Interval a
  , forall a. M2set a -> Interval a
m23 :: Interval a
  , forall a. M2set a -> Interval a
m24 :: Interval a
  }
  deriving Int -> M2set a -> ShowS
[M2set a] -> ShowS
M2set a -> String
(Int -> M2set a -> ShowS)
-> (M2set a -> String) -> ([M2set a] -> ShowS) -> Show (M2set a)
forall a. (Show a, Ord a) => Int -> M2set a -> ShowS
forall a. (Show a, Ord a) => [M2set a] -> ShowS
forall a. (Show a, Ord a) => M2set a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M2set a] -> ShowS
$cshowList :: forall a. (Show a, Ord a) => [M2set a] -> ShowS
show :: M2set a -> String
$cshow :: forall a. (Show a, Ord a) => M2set a -> String
showsPrec :: Int -> M2set a -> ShowS
$cshowsPrec :: forall a. (Show a, Ord a) => Int -> M2set a -> ShowS
Show

instance Arbitrary (M2set Int) where
  arbitrary :: Gen (M2set Int)
arbitrary = do
    Interval Int
x <- Gen (Interval Int)
forall a. Arbitrary a => Gen a
arbitrary
    Interval Int
a <- Gen (Interval Int)
forall a. Arbitrary a => Gen a
arbitrary
    Int
b <- Gen Int
forall a. Arbitrary a => Gen a
arbitrary
    Interval Int -> Interval Int -> Int -> Int -> M2set Int
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> Interval a -> b -> b -> M2set a
m2set Interval Int
x Interval Int
a Int
b (Int -> M2set Int) -> Gen Int -> Gen (M2set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M2set DT.Day) where
  arbitrary :: Gen (M2set Day)
arbitrary = do
    Interval Day
x <- Gen (Interval Day)
forall a. Arbitrary a => Gen a
arbitrary
    Interval Day
a <- Gen (Interval Day)
forall a. Arbitrary a => Gen a
arbitrary
    Integer
b <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
    Interval Day -> Interval Day -> Integer -> Integer -> M2set Day
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> Interval a -> b -> b -> M2set a
m2set Interval Day
x Interval Day
a Integer
b (Integer -> M2set Day) -> Gen Integer -> Gen (M2set Day)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M2set DT.UTCTime) where
  arbitrary :: Gen (M2set UTCTime)
arbitrary = do
    Interval UTCTime
x <- Gen (Interval UTCTime)
forall a. Arbitrary a => Gen a
arbitrary
    Interval UTCTime
a <- Gen (Interval UTCTime)
forall a. Arbitrary a => Gen a
arbitrary
    NominalDiffTime
b <- Gen NominalDiffTime
forall a. Arbitrary a => Gen a
arbitrary
    Interval UTCTime
-> Interval UTCTime
-> NominalDiffTime
-> NominalDiffTime
-> M2set UTCTime
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> Interval a -> b -> b -> M2set a
m2set Interval UTCTime
x Interval UTCTime
a NominalDiffTime
b (NominalDiffTime -> M2set UTCTime)
-> Gen NominalDiffTime -> Gen (M2set UTCTime)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen NominalDiffTime
forall a. Arbitrary a => Gen a
arbitrary

-- | A set used for testing M5.
data M5set a = M5set
  { forall a. M5set a -> Interval a
m51 :: Interval a
  , forall a. M5set a -> Interval a
m52 :: Interval a
  }
  deriving Int -> M5set a -> ShowS
[M5set a] -> ShowS
M5set a -> String
(Int -> M5set a -> ShowS)
-> (M5set a -> String) -> ([M5set a] -> ShowS) -> Show (M5set a)
forall a. (Show a, Ord a) => Int -> M5set a -> ShowS
forall a. (Show a, Ord a) => [M5set a] -> ShowS
forall a. (Show a, Ord a) => M5set a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M5set a] -> ShowS
$cshowList :: forall a. (Show a, Ord a) => [M5set a] -> ShowS
show :: M5set a -> String
$cshow :: forall a. (Show a, Ord a) => M5set a -> String
showsPrec :: Int -> M5set a -> ShowS
$cshowsPrec :: forall a. (Show a, Ord a) => Int -> M5set a -> ShowS
Show

instance Arbitrary (M5set Int) where
  arbitrary :: Gen (M5set Int)
arbitrary = do
    Interval Int
x <- Gen (Interval Int)
forall a. Arbitrary a => Gen a
arbitrary
    Int
a <- Gen Int
forall a. Arbitrary a => Gen a
arbitrary
    Interval Int -> Int -> Int -> M5set Int
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> M5set a
m5set Interval Int
x Int
a (Int -> M5set Int) -> Gen Int -> Gen (M5set Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M5set DT.Day) where
  arbitrary :: Gen (M5set Day)
arbitrary = do
    Interval Day
x <- Gen (Interval Day)
forall a. Arbitrary a => Gen a
arbitrary
    Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
    Interval Day -> Integer -> Integer -> M5set Day
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> M5set a
m5set Interval Day
x Integer
a (Integer -> M5set Day) -> Gen Integer -> Gen (M5set Day)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
forall a. Arbitrary a => Gen a
arbitrary

instance Arbitrary (M5set DT.UTCTime) where
  arbitrary :: Gen (M5set UTCTime)
arbitrary = do
    Interval UTCTime
x <- Gen (Interval UTCTime)
forall a. Arbitrary a => Gen a
arbitrary
    NominalDiffTime
a <- Gen NominalDiffTime
forall a. Arbitrary a => Gen a
arbitrary
    Interval UTCTime
-> NominalDiffTime -> NominalDiffTime -> M5set UTCTime
forall a b.
(IntervalAxioms a b, IntervalSizeable a b) =>
Interval a -> b -> b -> M5set a
m5set Interval UTCTime
x NominalDiffTime
a (NominalDiffTime -> M5set UTCTime)
-> Gen NominalDiffTime -> Gen (M5set UTCTime)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen NominalDiffTime
forall a. Arbitrary a => Gen a
arbitrary

-- | = "An Axiomatization of Interval Time".
class ( IntervalSizeable a b ) => IntervalAxioms a b where

    -- | Smart constructor of 'M1set'.
    m1set :: (IntervalSizeable a b) => Interval a -> b -> b -> b -> M1set a
    m1set Interval a
x b
a b
b b
c = Interval a -> Interval a -> Interval a -> Interval a -> M1set a
forall a.
Interval a -> Interval a -> Interval a -> Interval a -> M1set a
M1set Interval a
p1 Interval a
p2 Interval a
p3 Interval a
p4
      where p1 :: Interval a
p1 = Interval a
x                          -- interval i in prop_IAaxiomM1
            p2 :: Interval a
p2 = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
a (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
x)       -- interval j in prop_IAaxiomM1
            p3 :: Interval a
p3 = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
x)       -- interval k in prop_IAaxiomM1
            p4 :: Interval a
p4 = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
enderval (b -> b
forall b. (Ord b, Num b) => b -> b
makePos b
c) (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
p2)

    {- |

    == Axiom M1

    The first axiom of Allen and Hayes (1987) states that if "two periods both
    meet a third, thn any period met by one must also be met by the other."
    That is:

    \[
      \forall \text{ i,j,k,l } s.t. (i:j \text{ & } i:k \text{ & } l:j) \implies l:k
    \]
    -}
    prop_IAaxiomM1 :: (Ord a) => M1set a -> Property
    prop_IAaxiomM1 M1set a
x =
      (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
l ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (Interval a
l ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k)
      where i :: Interval a
i = M1set a -> Interval a
forall a. M1set a -> Interval a
m11 M1set a
x
            j :: Interval a
j = M1set a -> Interval a
forall a. M1set a -> Interval a
m12 M1set a
x
            k :: Interval a
k = M1set a -> Interval a
forall a. M1set a -> Interval a
m13 M1set a
x
            l :: Interval a
l = M1set a -> Interval a
forall a. M1set a -> Interval a
m14 M1set a
x

    -- | Smart constructor of 'M2set'.
    m2set :: (IntervalSizeable a b)=> Interval a -> Interval a -> b -> b -> M2set a
    m2set Interval a
x Interval a
y b
a b
b = Interval a -> Interval a -> Interval a -> Interval a -> M2set a
forall a.
Interval a -> Interval a -> Interval a -> Interval a -> M2set a
M2set Interval a
p1 Interval a
p2 Interval a
p3 Interval a
p4
      where p1 :: Interval a
p1 = Interval a
x                          -- interval i in prop_IAaxiomM2
            p2 :: Interval a
p2 = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
a (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
x)       -- interval j in prop_IAaxiomM2
            p3 :: Interval a
p3 = Interval a
y                          -- interval k in prop_IAaxiomM2
            p4 :: Interval a
p4 = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
y)       -- interval l in prop_IAaxiomM2

    {- |

    == Axiom M2

    If period i meets period j and period k meets l,
    then exactly one of the following holds:

      1) i meets l;
      2) there is an m such that i meets m and m meets l;
      3) there is an n such that k meets n and n meets j.

    That is,

    \[
      \forall i,j,k,l s.t. (i:j \text { & } k:l) \implies
        i:l \oplus
        (\exists m s.t. i:m:l) \oplus
        (\exists m s.t. k:m:j)
    \]

    -}

    prop_IAaxiomM2 :: (IntervalSizeable a b, Show a) =>
        M2set a -> Property
    prop_IAaxiomM2 M2set a
x =
      (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
k ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
        (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l)  Bool -> Bool -> Bool
`xor`
        Either ParseErrorInterval (Interval a) -> Bool
forall a b. Either a b -> Bool
isRight Either ParseErrorInterval (Interval a)
m Bool -> Bool -> Bool
`xor`
        Either ParseErrorInterval (Interval a) -> Bool
forall a b. Either a b -> Bool
isRight Either ParseErrorInterval (Interval a)
n
        where i :: Interval a
i = M2set a -> Interval a
forall a. M2set a -> Interval a
m21 M2set a
x
              j :: Interval a
j = M2set a -> Interval a
forall a. M2set a -> Interval a
m22 M2set a
x
              k :: Interval a
k = M2set a -> Interval a
forall a. M2set a -> Interval a
m23 M2set a
x
              l :: Interval a
l = M2set a -> Interval a
forall a. M2set a -> Interval a
m24 M2set a
x
              m :: Either ParseErrorInterval (Interval a)
m = a -> a -> Either ParseErrorInterval (Interval a)
forall a.
(Show a, Ord a) =>
a -> a -> Either ParseErrorInterval (Interval a)
parseInterval (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i) (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
l)
              n :: Either ParseErrorInterval (Interval a)
n = a -> a -> Either ParseErrorInterval (Interval a)
forall a.
(Show a, Ord a) =>
a -> a -> Either ParseErrorInterval (Interval a)
parseInterval (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
k) (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j)

    {- |

    == Axiom ML1

    An interval cannot meet itself.

    \[
      \forall i \lnot i:i
    \]
    -}

    prop_IAaxiomML1 :: (Ord a) => Interval a -> Property
    prop_IAaxiomML1 Interval a
x = Bool -> Bool
not (Interval a
x ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
x) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

    {- |

    == Axiom ML2

    If i meets j then j does not meet i.

    \[
    \forall i,j i:j \implies \lnot j:i
    \]
    -}

    prop_IAaxiomML2 :: (Ord a)=> M2set a -> Property
    prop_IAaxiomML2 M2set a
x =
      (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> Bool -> Bool
not (Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i)
      where i :: Interval a
i = M2set a -> Interval a
forall a. M2set a -> Interval a
m21 M2set a
x
            j :: Interval a
j = M2set a -> Interval a
forall a. M2set a -> Interval a
m22 M2set a
x

    {- |

    == Axiom M3

    Time does not start or stop:

    \[
    \forall i \exists j,k s.t. j:i:k
    \]
    -}

    prop_IAaxiomM3 :: (IntervalSizeable a b)=>
          b -> Interval a -> Property
    prop_IAaxiomM3 b
b Interval a
i =
      (Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      where j :: Interval a
j = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
enderval   b
b (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i)
            k :: Interval a
k = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)

    {- |
      ML3 says that For all i, there does not exist m such that i meets m and
      m meet i. Not testing that this axiom holds, as I'm not sure how I would
      test the lack of existence easily.
    -}

    {- |

    == Axiom M4

    If two meets are separated by intervals, then this sequence is a longer interval.

    \[
    \forall i,j i:j \implies (\exists k,m,n s.t m:i:j:n \text { & } m:k:n)
    \]
    -}

    prop_IAaxiomM4 :: (IntervalSizeable a b)=>
        b -> M2set a -> Property
    prop_IAaxiomM4 b
b M2set a
x =
      ((Interval a
m ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n) Bool -> Bool -> Bool
&&
        (Interval a
m ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
k ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n)) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      where i :: Interval a
i = M2set a -> Interval a
forall a. M2set a -> Interval a
m21 M2set a
x
            j :: Interval a
j = M2set a -> Interval a
forall a. M2set a -> Interval a
m22 M2set a
x
            m :: Interval a
m = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
enderval   b
b (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i)
            n :: Interval a
n = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
j)
            k :: Interval a
k = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
g (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
m)
            g :: b
g = a -> a -> b
forall a b. IntervalSizeable a b => a -> a -> b
diff (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
n) (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
m)


    -- | Smart constructor of 'M5set'.
    m5set :: (IntervalSizeable a b)=> Interval a -> b -> b -> M5set a
    m5set Interval a
x b
a b
b = Interval a -> Interval a -> M5set a
forall a. Interval a -> Interval a -> M5set a
M5set Interval a
p1 Interval a
p2
      where p1 :: Interval a
p1 = Interval a
x                     -- interval i in prop_IAaxiomM5
            p2 :: Interval a
p2 = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
a a
ps       -- interval l in prop_IAaxiomM5
            ps :: a
ps = Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end (b -> Interval a -> Interval a
forall a b (i :: * -> *).
(IntervalSizeable a b, Intervallic i) =>
b -> i a -> i a
expandr (b -> b
forall b. (Ord b, Num b) => b -> b
makePos b
b) Interval a
x) -- creating l by shifting and expanding i

    {- |

    == Axiom M5

    There is only one time period between any two meeting places.

    \[
    \forall i,j,k,l (i:j:l \text{ & } i:k:l) \equiv j = k
    \]
    -}
    prop_IAaxiomM5 :: (IntervalSizeable a b) =>
        M5set a -> Property
    prop_IAaxiomM5 M5set a
x =
      ((Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l) Bool -> Bool -> Bool
&&
       (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
k ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l)) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall a. Eq a => a -> a -> Bool
== Interval a
k)
      where i :: Interval a
i = M5set a -> Interval a
forall a. M5set a -> Interval a
m51 M5set a
x
            j :: Interval a
j = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
g (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)
            k :: Interval a
k = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
g (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)
            g :: b
g = a -> a -> b
forall a b. IntervalSizeable a b => a -> a -> b
diff (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
l) (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)
            l :: Interval a
l = M5set a -> Interval a
forall a. M5set a -> Interval a
m52 M5set a
x

    {- |

    == Axiom M4.1

    Ordered unions:

    \[
    \forall i,j i:j \implies (\exists m,n s.t. m:i:j:n \text{ & } m:(i+j):n)
    \]
    -}
    prop_IAaxiomM4_1 :: (IntervalSizeable a b)=>
                    b -> M2set a -> Property
    prop_IAaxiomM4_1 b
b M2set a
x =
      ((Interval a
m ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n) Bool -> Bool -> Bool
&&
        (Interval a
m ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
ij Bool -> Bool -> Bool
&& Interval a
ij ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n)) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      where i :: Interval a
i = M2set a -> Interval a
forall a. M2set a -> Interval a
m21 M2set a
x
            j :: Interval a
j = M2set a -> Interval a
forall a. M2set a -> Interval a
m22 M2set a
x
            m :: Interval a
m = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
enderval   b
b (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i)
            n :: Interval a
n = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval b
b (Interval a -> a
forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
j)
            ij :: Interval a
ij = Maybe (Interval a) -> Interval a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Interval a) -> Interval a)
-> Maybe (Interval a) -> Interval a
forall a b. (a -> b) -> a -> b
$ Interval a
i Interval a -> Interval a -> Maybe (Interval a)
forall (i :: * -> *) a.
IntervalCombinable i a =>
i a -> i a -> Maybe (i a)
.+. Interval a
j

instance IntervalAxioms Int Int
instance IntervalAxioms Day Integer
instance IntervalAxioms UTCTime NominalDiffTime