{-|
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 =
  [ ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
equals
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
meets
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
metBy
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
before
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
after
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
starts
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
startedBy
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
finishes
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
finishedBy
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
overlaps
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
overlappedBy
  , ComparativePredicateOf1 (Interval a)
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
during
  , ComparativePredicateOf1 (Interval a)
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
forall a. a -> a
id ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ ((Interval a -> Interval a -> Bool) -> Bool)
-> [Interval a -> Interval a -> Bool] -> [Bool]
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) [Interval a -> Interval a -> Bool]
forall a. Ord a => [ComparativePredicateOf1 (Interval a)]
allIArelations)) Bool -> Bool -> Property
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 Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (Interval a -> Interval a -> IntervalRelation
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
i0 a -> i1 a -> IntervalRelation
relate Interval a
i0 Interval a
i1 IntervalRelation -> Set IntervalRelation -> Bool
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 =
      Interval a -> Interval a -> Bool
forall a (i0 :: * -> *) (i1 :: * -> *).
(Ord a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
before Interval a
i Interval a
j Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (Interval a
i Interval a -> Interval a -> Bool
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 Interval a -> Interval a -> Bool
forall a (i0 :: * -> *) (i1 :: * -> *).
(Eq a, Intervallic i0, Intervallic i1) =>
ComparativePredicateOf2 (i0 a) (i1 a)
`meets` Interval a
j)
        where k :: Interval a
k = b -> a -> Interval a
forall a b. IntervalSizeable a b => b -> a -> Interval a
beginerval (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
j) (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
end Interval a
i)

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

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

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

    prop_disjoint_predicate :: (Ord a) =>
          Interval a
        -> Interval a
        -> Property
    prop_disjoint_predicate = Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
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 Interval a -> Interval a -> Bool
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 =
      Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
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) Interval a -> Interval a -> Bool
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 =
      Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
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) Interval a -> Interval a -> Bool
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 = Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
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 Interval a -> Interval a -> Bool
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 = Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
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 Interval a -> Interval a -> Bool
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 = Set IntervalRelation
-> (Interval a -> Interval a -> Bool)
-> Interval a
-> Interval a
-> Property
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) Interval a -> Interval a -> Bool
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