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


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 :: 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 {
     M1set a -> Interval a
m11 :: Interval a
   , M1set a -> Interval a
m12 :: Interval a
   , M1set a -> Interval a
m13 :: Interval 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 {
    M2set a -> Interval a
m21 :: Interval a
  , M2set a -> Interval a
m22 :: Interval a
  , M2set a -> Interval a
m23 :: Interval 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 {
     M5set a -> Interval a
m51 :: Interval 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 a => 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 a => 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 a => 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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
l ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 a => 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 a => 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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
k ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 a => i a -> a
end Interval a
i) (Interval a -> a
forall (i :: * -> *) a. Intervallic i a => 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 a => i a -> a
end Interval a
k) (Interval a -> a
forall (i :: * -> *) a. Intervallic i a => 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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 a => 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 a => 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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n) Bool -> Bool -> Bool
&&
        (Interval a
m ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
k ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 a => 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 a => 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 a => 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 a => i a -> a
begin Interval a
n) (Interval a -> a
forall (i :: * -> *) a. Intervallic i a => 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 a => i a -> a
end (b -> Interval a -> Interval a
forall a b (i :: * -> *).
(IntervalSizeable a b, Intervallic i a) =>
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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
l) Bool -> Bool -> Bool
&&
       (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
k Bool -> Bool -> Bool
&& Interval a
k ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 a => 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 a => 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 a => i a -> a
begin Interval a
l) (Interval a -> a
forall (i :: * -> *) a. Intervallic i a => 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 (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
i Bool -> Bool -> Bool
&& Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j Bool -> Bool -> Bool
&& Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
n) Bool -> Bool -> Bool
&&
        (Interval a
m ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
ij Bool -> Bool -> Bool
&& Interval a
ij ComparativePredicateOf2 (Interval a) (Interval a)
forall (i0 :: * -> *) a (i1 :: * -> *).
(Intervallic i0 a, Intervallic i1 a) =>
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 a => 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 a => 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