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

This module exports utilities for 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 ExplicitForAll        #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}


module IntervalAlgebra.Axioms 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           IntervalAlgebra.IntervalUtilities ((.+.))
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 :: 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.
(SizedIv (Interval a), b ~ Moment (Interval a), Ord b, Num 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.
(SizedIv (Interval a), b ~ Moment (Interval a), Ord b, Num 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
genNominalDiffTime
    NominalDiffTime
b <- Gen NominalDiffTime
genNominalDiffTime
    Interval UTCTime
-> NominalDiffTime
-> NominalDiffTime
-> NominalDiffTime
-> M1set UTCTime
forall a b.
(SizedIv (Interval a), b ~ Moment (Interval a), Ord b, Num 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
genNominalDiffTime


-- | 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
-> Moment (Interval Int)
-> Moment (Interval Int)
-> M2set Int
forall a.
SizedIv (Interval a) =>
Interval a
-> Interval a
-> Moment (Interval a)
-> Moment (Interval a)
-> M2set a
m2set Interval Int
x Interval Int
a Int
Moment (Interval 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
-> Moment (Interval Day)
-> Moment (Interval Day)
-> M2set Day
forall a.
SizedIv (Interval a) =>
Interval a
-> Interval a
-> Moment (Interval a)
-> Moment (Interval a)
-> M2set a
m2set Interval Day
x Interval Day
a Integer
Moment (Interval Day)
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
genNominalDiffTime
    Interval UTCTime
-> Interval UTCTime
-> Moment (Interval UTCTime)
-> Moment (Interval UTCTime)
-> M2set UTCTime
forall a.
SizedIv (Interval a) =>
Interval a
-> Interval a
-> Moment (Interval a)
-> Moment (Interval a)
-> M2set a
m2set Interval UTCTime
x Interval UTCTime
a NominalDiffTime
Moment (Interval UTCTime)
b (NominalDiffTime -> M2set UTCTime)
-> Gen NominalDiffTime -> Gen (M2set UTCTime)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen NominalDiffTime
genNominalDiffTime

-- | 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
-> Moment (Interval Int) -> Moment (Interval Int) -> M5set Int
forall a.
(SizedIv (Interval a), Eq a, Ord (Moment (Interval a)),
 Num (Moment (Interval a))) =>
Interval a -> Moment (Interval a) -> Moment (Interval a) -> M5set a
m5set Interval Int
x Int
Moment (Interval 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
-> Moment (Interval Day) -> Moment (Interval Day) -> M5set Day
forall a.
(SizedIv (Interval a), Eq a, Ord (Moment (Interval a)),
 Num (Moment (Interval a))) =>
Interval a -> Moment (Interval a) -> Moment (Interval a) -> M5set a
m5set Interval Day
x Integer
Moment (Interval Day)
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
genNominalDiffTime
    Interval UTCTime
-> Moment (Interval UTCTime)
-> Moment (Interval UTCTime)
-> M5set UTCTime
forall a.
(SizedIv (Interval a), Eq a, Ord (Moment (Interval a)),
 Num (Moment (Interval a))) =>
Interval a -> Moment (Interval a) -> Moment (Interval a) -> M5set a
m5set Interval UTCTime
x NominalDiffTime
Moment (Interval UTCTime)
a (NominalDiffTime -> M5set UTCTime)
-> Gen NominalDiffTime -> Gen (M5set UTCTime)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen NominalDiffTime
genNominalDiffTime

-- Axiom functions

-- | Smart constructor of 'M1set'.
m1set :: (SizedIv (Interval a), b ~ Moment (Interval a), Ord b, Num b) => Interval a -> b -> b -> b -> M1set a
m1set :: 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 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
beginerval b
Moment (Interval a)
a (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
end Interval a
x)       -- interval j in prop_IAaxiomM1
        p3 :: Interval a
p3 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
beginerval b
Moment (Interval a)
b (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
end Interval a
x)       -- interval k in prop_IAaxiomM1
        p4 :: Interval a
p4 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
enderval (b -> b
forall b. (Ord b, Num b) => b -> b
makePos b
c) (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval 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 :: (Iv (Interval a), SizedIv (Interval a)) => M1set a -> Property
prop_IAaxiomM1 :: M1set a -> Property
prop_IAaxiomM1 M1set a
x =
  (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: (SizedIv (Interval a)) => Interval a -> Interval a -> Moment (Interval a) -> Moment (Interval a) -> M2set a
m2set :: Interval a
-> Interval a
-> Moment (Interval a)
-> Moment (Interval a)
-> M2set a
m2set Interval a
x Interval a
y Moment (Interval a)
a Moment (Interval a)
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 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
beginerval Moment (Interval a)
a (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval 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 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
beginerval Moment (Interval a)
b (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval 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 :: (SizedIv (Interval a), Show a, Ord a) =>
    M2set a -> Property
prop_IAaxiomM2 :: M2set a -> Property
prop_IAaxiomM2 M2set a
x =
  (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
end Interval a
i) (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval 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.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
end Interval a
k) (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
begin Interval a
j)

{- |

== Axiom ML1

An interval cannot meet itself.

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

prop_IAaxiomML1 :: (Iv (Interval a), SizedIv (Interval a)) => Interval a -> Property
prop_IAaxiomML1 :: Interval a -> Property
prop_IAaxiomML1 Interval a
x = Bool -> Bool
not (Interval a
x ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Iv (Interval 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 :: (Iv (Interval a), SizedIv (Interval a))=> M2set a -> Property
prop_IAaxiomML2 :: M2set a -> Property
prop_IAaxiomML2 M2set a
x =
  (Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: (Iv (Interval a), SizedIv (Interval a))=>
      Moment (Interval a) -> Interval a -> Property
prop_IAaxiomM3 :: Moment (Interval a) -> Interval a -> Property
prop_IAaxiomM3 Moment (Interval a)
b Interval a
i =
  (Interval a
j ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
enderval   Moment (Interval a)
b (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
begin Interval a
i)
        k :: Interval a
k = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
beginerval Moment (Interval a)
b (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval 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 :: forall a. (Iv (Interval a), SizedIv (Interval a), Ord (Moment (Interval a)))=>
    Moment (Interval a) -> M2set a -> Property
prop_IAaxiomM4 :: Moment (Interval a) -> M2set a -> Property
prop_IAaxiomM4 Moment (Interval a)
b M2set a
x =
  ((Interval a
m ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
enderval   Moment (Interval a)
b (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
begin Interval a
i)
        n :: Interval a
n = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
beginerval Moment (Interval a)
b (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
end Interval a
j)
        k :: Interval a
k = (a, a) -> Interval a
forall a.
(SizedIv (Interval a), Ord (Moment (Interval a))) =>
(a, a) -> Interval a
safeInterval (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
end Interval a
m, Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
begin Interval a
n)


-- | Smart constructor of 'M5set'.
m5set :: (SizedIv (Interval a), Eq a, Ord (Moment (Interval a)), Num (Moment (Interval a)))=> Interval a -> Moment (Interval a) -> Moment (Interval a) -> M5set a
m5set :: Interval a -> Moment (Interval a) -> Moment (Interval a) -> M5set a
m5set Interval a
x Moment (Interval a)
a Moment (Interval a)
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 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
beginerval Moment (Interval a)
a a
ps       -- interval l in prop_IAaxiomM5
        ps :: a
ps = Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
end (Moment (Interval a) -> Interval a -> Interval a
forall a (i :: * -> *).
(SizedIv (Interval a), Intervallic i) =>
Moment (Interval a) -> i a -> i a
expandr (Moment (Interval a) -> Moment (Interval a)
forall b. (Ord b, Num b) => b -> b
makePos Moment (Interval a)
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 :: forall a. (SizedIv (Interval a), Ord a, Ord (Moment (Interval a))) =>
    M5set a -> Property
prop_IAaxiomM5 :: M5set a -> Property
prop_IAaxiomM5 M5set a
x =
  ((Interval a
i ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 = (a, a) -> Interval a
forall a.
(SizedIv (Interval a), Ord (Moment (Interval a))) =>
(a, a) -> Interval a
safeInterval (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
end Interval a
i, Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
begin Interval a
l)
        k :: Interval a
k = Interval a
j
        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 :: (SizedIv (Interval a), Ord a, Ord (Moment (Interval a))) =>
                Moment (Interval a) -> M2set a -> Property
prop_IAaxiomM4_1 :: Moment (Interval a) -> M2set a -> Property
prop_IAaxiomM4_1 Moment (Interval a)
b M2set a
x =
  ((Interval a
m ComparativePredicateOf2 (Interval a) (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 :: * -> *).
(Iv (Interval 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 = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
enderval   Moment (Interval a)
b (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval a), Intervallic i) =>
i a -> a
begin Interval a
i)
        n :: Interval a
n = Moment (Interval a) -> a -> Interval a
forall a.
SizedIv (Interval a) =>
Moment (Interval a) -> a -> Interval a
beginerval Moment (Interval a)
b (Interval a -> a
forall (i :: * -> *) a.
(SizedIv (Interval 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 a (i :: * -> *).
(Iv (Interval a), Ord (Moment (Interval a)), SizedIv (Interval a),
 Intervallic i) =>
i a -> i a -> Maybe (Interval a)
.+. Interval a
j