{- 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 a b = a /= b

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

-- | A set used for testing M1 defined so that the M1 condition is true.
data M1set a
  = M1set
      { m11 :: Interval a
      , m12 :: Interval a
      , m13 :: Interval a
      , m14 :: Interval a
      }
  deriving (Show)

instance Arbitrary (M1set Int) where
  arbitrary = do
    x <- arbitrary
    a <- arbitrary
    b <- arbitrary
    m1set x a b <$> arbitrary

instance Arbitrary (M1set DT.Day) where
  arbitrary = do
    x <- arbitrary
    a <- arbitrary
    b <- arbitrary
    m1set x a b <$> arbitrary

instance Arbitrary (M1set DT.UTCTime) where
  arbitrary = do
    x <- arbitrary
    a <- genNominalDiffTime
    b <- genNominalDiffTime
    m1set x a b <$> genNominalDiffTime


-- | A set used for testing M2 defined so that the M2 condition is true.
data M2set a
  = M2set
      { m21 :: Interval a
      , m22 :: Interval a
      , m23 :: Interval a
      , m24 :: Interval a
      }
  deriving (Show)

instance Arbitrary (M2set Int) where
  arbitrary = do
    x <- arbitrary
    a <- arbitrary
    b <- arbitrary
    m2set x a b <$> arbitrary

instance Arbitrary (M2set DT.Day) where
  arbitrary = do
    x <- arbitrary
    a <- arbitrary
    b <- arbitrary
    m2set x a b <$> arbitrary

instance Arbitrary (M2set DT.UTCTime) where
  arbitrary = do
    x <- arbitrary
    a <- arbitrary
    b <- genNominalDiffTime
    m2set x a b <$> genNominalDiffTime

-- | A set used for testing M5.
data M5set a
  = M5set
      { m51 :: Interval a
      , m52 :: Interval a
      }
  deriving (Show)

instance Arbitrary (M5set Int) where
  arbitrary = do
    x <- arbitrary
    a <- arbitrary
    m5set x a <$> arbitrary

instance Arbitrary (M5set DT.Day) where
  arbitrary = do
    x <- arbitrary
    a <- arbitrary
    m5set x a <$> arbitrary

instance Arbitrary (M5set DT.UTCTime) where
  arbitrary = do
    x <- arbitrary
    a <- genNominalDiffTime
    m5set x a <$> 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 x a b c = M1set p1 p2 p3 p4
  where p1 = x                          -- interval i in prop_IAaxiomM1
        p2 = beginerval a (end x)       -- interval j in prop_IAaxiomM1
        p3 = beginerval b (end x)       -- interval k in prop_IAaxiomM1
        p4 = enderval (makePos c) (begin 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 x =
  (i `meets` j && i `meets` k && l `meets` j) ==> (l `meets` k)
  where i = m11 x
        j = m12 x
        k = m13 x
        l = m14 x

-- | Smart constructor of 'M2set'.
m2set :: (SizedIv (Interval a)) => Interval a -> Interval a -> Moment (Interval a) -> Moment (Interval a) -> M2set a
m2set x y a b = M2set p1 p2 p3 p4
  where p1 = x                          -- interval i in prop_IAaxiomM2
        p2 = beginerval a (end x)       -- interval j in prop_IAaxiomM2
        p3 = y                          -- interval k in prop_IAaxiomM2
        p4 = beginerval b (end 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 x =
  (i `meets` j && k `meets` l) ==>
    (i `meets` l)  `xor`
    isRight m `xor`
    isRight n
    where i = m21 x
          j = m22 x
          k = m23 x
          l = m24 x
          m = parseInterval (end i) (begin l)
          n = parseInterval (end k) (begin 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 x = not (x `meets` x) === 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 x =
  (i `meets` j) ==> not (j `meets` i)
  where i = m21 x
        j = m22 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 b i =
  (j `meets` i && i `meets` k) === True
  where j = enderval   b (begin i)
        k = beginerval b (end 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 b x =
  ((m `meets` i && i `meets` j && j `meets` n) &&
    (m `meets` k && k `meets` n)) === True
  where i = m21 x
        j = m22 x
        m = enderval   b (begin i)
        n = beginerval b (end j)
        k = safeInterval (end m, begin 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 x a b = M5set p1 p2
  where p1 = x                     -- interval i in prop_IAaxiomM5
        p2 = beginerval a ps       -- interval l in prop_IAaxiomM5
        ps = end (expandr (makePos b) 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 x =
  ((i `meets` j && j `meets` l) &&
   (i `meets` k && k `meets` l)) === (j == k)
  where i = m51 x
        j = safeInterval (end i, begin l)
        k = j
        l = m52 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 b x =
  ((m `meets` i && i `meets` j && j `meets` n) &&
    (m `meets` ij && ij `meets` n)) === True
  where i = m21 x
        j = m22 x
        m = enderval   b (begin i)
        n = beginerval b (end j)
        ij = fromJust $ i .+. j