{-|
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.

-}
{- HLINT ignore -}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module IntervalAlgebra.RelationProperties
  ( IntervalRelationProperties(..)
  ) where

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

allIArelations :: (Ord a) => [ComparativePredicateOf1 (Interval a)]
allIArelations :: forall a. Ord a => [ComparativePredicateOf1 (Interval a)]
allIArelations =
  [ forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
equals
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
meets
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
metBy
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
before
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
after
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
starts
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
startedBy
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
finishes
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
finishedBy
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
overlaps
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
overlappedBy
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
during
  , forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
contains
  ]

-- | A collection of properties for the interval algebra. Some of these come from
--   figure 2 in  [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x).
class ( IntervalSizeable a b ) => IntervalRelationProperties a b where

    -- | For any two pair of intervals exactly one 'IntervalRelation' should hold
    prop_exclusiveRelations::  Interval a -> Interval a -> Property
    prop_exclusiveRelations Interval a
x Interval a
y =
      (  Int
1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Interval a -> Interval a -> Bool
r -> Interval a -> Interval a -> Bool
r Interval a
x Interval a
y) forall a. Ord a => [ComparativePredicateOf1 (Interval a)]
allIArelations)) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True

    -- | Given a set of interval relations and predicate function, test that the
    -- predicate between two interval is equivalent to the relation of two intervals
    -- being in the set of relations.
    prop_predicate_unions :: Ord a =>
          Set IntervalRelation
        -> ComparativePredicateOf2 (Interval a) (Interval a)
        -> Interval a
        -> Interval a
        -> Property
    prop_predicate_unions Set IntervalRelation
s Interval a -> Interval a -> Bool
pred Interval a
i0 Interval a
i1 =
      Interval a -> Interval a -> Bool
pred Interval a
i0 Interval a
i1 forall a. (Eq a, Show a) => a -> a -> Property
=== (forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
i0 a -> i1 a -> IntervalRelation
relate Interval a
i0 Interval a
i1 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set IntervalRelation
s)

    prop_IAbefore :: Interval a -> Interval a -> Property
    prop_IAbefore Interval a
i Interval a
j =
      forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
before Interval a
i Interval a
j forall prop. Testable prop => Bool -> prop -> Property
==> (Interval a
i 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 forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j)
        where k :: Interval a
k = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j) (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)) (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)

    prop_IAstarts:: Interval a -> Interval a -> Property
    prop_IAstarts Interval a
i Interval a
j
      | forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
starts Interval a
i Interval a
j = (Interval a
j forall a. Eq a => a -> a -> Bool
== forall a. HasCallStack => Maybe a -> a
fromJust (Interval a
i forall (i :: * -> *) a.
IntervalCombinable i a =>
i a -> i a -> Maybe (i a)
.+. Interval a
k)) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      | Bool
otherwise     = forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
starts Interval a
i Interval a
j forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
False
        where k :: Interval a
k = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
j) (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)) (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)

    prop_IAfinishes:: Interval a -> Interval a -> Property
    prop_IAfinishes Interval a
i Interval a
j
      | forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
finishes Interval a
i Interval a
j = (Interval a
j forall a. Eq a => a -> a -> Bool
== forall a. HasCallStack => Maybe a -> a
fromJust ( Interval a
k forall (i :: * -> *) a.
IntervalCombinable i a =>
i a -> i a -> Maybe (i a)
.+. Interval a
i)) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      | Bool
otherwise       = forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
finishes Interval a
i Interval a
j forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
False
        where k :: Interval a
k = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j)) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j)

    prop_IAoverlaps:: Interval a -> Interval a -> Property
    prop_IAoverlaps Interval a
i Interval a
j
      | forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
overlaps Interval a
i Interval a
j = ((Interval a
i forall a. Eq a => a -> a -> Bool
== forall a. HasCallStack => Maybe a -> a
fromJust ( Interval a
k forall (i :: * -> *) a.
IntervalCombinable i a =>
i a -> i a -> Maybe (i a)
.+. Interval a
l )) Bool -> Bool -> Bool
&&
                          (Interval a
j forall a. Eq a => a -> a -> Bool
== forall a. HasCallStack => Maybe a -> a
fromJust ( Interval a
l forall (i :: * -> *) a.
IntervalCombinable i a =>
i a -> i a -> Maybe (i a)
.+. Interval a
m ))) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      | Bool
otherwise       = forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
overlaps Interval a
i Interval a
j forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
False
        where k :: Interval a
k = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i)) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i)
              l :: Interval a
l = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)   (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j)) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j)
              m :: Interval a
m = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
j)   (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i))   (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)

    prop_IAduring:: Interval a -> Interval a-> Property
    prop_IAduring Interval a
i Interval a
j
      | forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
during Interval a
i Interval a
j = (Interval a
j forall a. Eq a => a -> a -> Bool
== forall a. HasCallStack => Maybe a -> a
fromJust ( forall a. HasCallStack => Maybe a -> a
fromJust (Interval a
k forall (i :: * -> *) a.
IntervalCombinable i a =>
i a -> i a -> Maybe (i a)
.+. Interval a
i) forall (i :: * -> *) a.
IntervalCombinable i a =>
i a -> i a -> Maybe (i a)
.+. Interval a
l)) forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True
      | Bool
otherwise     = forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
during Interval a
i Interval a
j forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
False
        where k :: Interval a
k = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
i) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j)) (forall (i :: * -> *) a. Intervallic i => i a -> a
begin Interval a
j)
              l :: Interval a
l = forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (forall a b. IntervalSizeable a b => a -> a -> b
diff (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
j)   (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i))   (forall (i :: * -> *) a. Intervallic i => i a -> a
end Interval a
i)

    prop_disjoint_predicate :: (Ord a) =>
          Interval a
        -> Interval a
        -> Property
    prop_disjoint_predicate = forall a b.
(IntervalRelationProperties a b, Ord a) =>
Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
prop_predicate_unions Set IntervalRelation
disjointRelations forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
disjoint

    prop_notdisjoint_predicate :: (Ord a) =>
          Interval a
        -> Interval a
        -> Property
    prop_notdisjoint_predicate =
      forall a b.
(IntervalRelationProperties a b, Ord a) =>
Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
prop_predicate_unions (Set IntervalRelation -> Set IntervalRelation
complement Set IntervalRelation
disjointRelations) forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
notDisjoint

    prop_concur_predicate :: (Ord a) =>
          Interval a
        -> Interval a
        -> Property
    prop_concur_predicate =
      forall a b.
(IntervalRelationProperties a b, Ord a) =>
Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
prop_predicate_unions (Set IntervalRelation -> Set IntervalRelation
complement Set IntervalRelation
disjointRelations) forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
concur

    prop_within_predicate :: (Ord a) =>
          Interval a
        -> Interval a
        -> Property
    prop_within_predicate = forall a b.
(IntervalRelationProperties a b, Ord a) =>
Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
prop_predicate_unions Set IntervalRelation
withinRelations forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
within

    prop_enclosedBy_predicate :: (Ord a) =>
          Interval a
        -> Interval a
        -> Property
    prop_enclosedBy_predicate = forall a b.
(IntervalRelationProperties a b, Ord a) =>
Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
prop_predicate_unions Set IntervalRelation
withinRelations forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
enclosedBy

    prop_encloses_predicate :: (Ord a) =>
          Interval a
        -> Interval a
        -> Property
    prop_encloses_predicate = forall a b.
(IntervalRelationProperties a b, Ord a) =>
Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
prop_predicate_unions (Set IntervalRelation -> Set IntervalRelation
converse Set IntervalRelation
withinRelations) forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
encloses

instance IntervalRelationProperties Int Int
instance IntervalRelationProperties Day Integer
instance IntervalRelationProperties UTCTime NominalDiffTime