interval-algebra-2.1.2: src/IntervalAlgebra/Axioms.hs
{- HLINT ignore -}
{-|
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 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 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 <- arbitrary
b <- arbitrary
m1set x a b <$> arbitrary
-- | 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 <- arbitrary
m2set x a b <$> arbitrary
-- | 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 <- arbitrary
m5set x 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 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 :: (Ord 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 :: (IntervalSizeable a b)=> Interval a -> Interval a -> b -> b -> 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 :: (IntervalSizeable a b, Show 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 :: (Ord 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 :: (Ord 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 :: (IntervalSizeable a b)=>
b -> 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 :: (IntervalSizeable a b)=>
b -> 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 = beginerval g (end m)
g = diff (begin n) (end m)
-- | Smart constructor of 'M5set'.
m5set :: (IntervalSizeable a b)=> Interval a -> b -> b -> 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 :: (IntervalSizeable a b) =>
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 = beginerval g (end i)
k = beginerval g (end i)
g = diff (begin l) (end i)
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 :: (IntervalSizeable a b)=>
b -> 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
instance IntervalAxioms Int Int
instance IntervalAxioms Day Integer
instance IntervalAxioms UTCTime NominalDiffTime