diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,13 @@ # Changelog for interval-algebra +## 1.0.0 + +* Moves the main `IntervalAlgebra` module to `IntervalAlgebra.Core` and `IntervalAlgebra` now reexports `IntervalAlgebra.Core`, `IntervalAlgebra.IntervalUtilites`, and `IntervalAlgebra.PairedInterval`. +* Creates a new `IntervalAlgebra.Axioms` module containing the `IntervalAxioms` typeclass of property tests of the interval algebra axioms. These were in the testing suite. Including this as a module in case users need add new `Interval` types and want to test the axioms. +* Creates a new `IntervalAlgebra.RelationProperties` module containing a typeclass of property tests of the interval algebra. These were in the testing suite. Including this as a module in case users need add new `Interval` types and want to test the axioms. +* Adds `UTCTime`/`NominalDiffTime` instance for `IntervalSizeable`. +* Adds additional tests to the testing suite. + ## 0.10.2 * Adds the `momentize` function for changing the duration of some interval value to a moment. diff --git a/interval-algebra.cabal b/interval-algebra.cabal --- a/interval-algebra.cabal +++ b/interval-algebra.cabal @@ -1,6 +1,6 @@ cabal-version: 2.2 name: interval-algebra -version: 0.10.2 +version: 1.0.0 synopsis: An implementation of Allen's interval algebra for temporal logic description: Please see the README on GitHub at category: Algebra,Time @@ -23,9 +23,12 @@ library exposed-modules: IntervalAlgebra + IntervalAlgebra.Core IntervalAlgebra.IntervalUtilities - IntervalAlgebra.Arbitrary IntervalAlgebra.PairedInterval + IntervalAlgebra.Axioms + IntervalAlgebra.RelationProperties + IntervalAlgebra.Arbitrary other-modules: Paths_interval_algebra autogen-modules: @@ -42,10 +45,40 @@ , QuickCheck == 2.14.2 default-language: Haskell2010 +test-suite axioms + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + AxiomsSpec + hs-source-dirs: + test-axioms + ghc-options: -threaded -rtsopts -with-rtsopts=-N + build-depends: + QuickCheck == 2.14.2 + , base >=4.7 && <5 + , hspec == 2.8.2 + , interval-algebra + , time >=1.8 && <2 + default-language: Haskell2010 + +test-suite relations + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + RelationPropertiesSpec + hs-source-dirs: + test-relation-properties + ghc-options: -threaded -rtsopts -with-rtsopts=-N + build-depends: + QuickCheck == 2.14.2 + , base >=4.7 && <5 + , hspec == 2.8.2 + , interval-algebra + , time >=1.8 && <2 + default-language: Haskell2010 + test-suite interval-algebra-test type: exitcode-stdio-1.0 - -- this type means successful test run returns the zero exit code, - -- and a failed test run returns a non-zero exit code main-is: Spec.hs other-modules: IntervalAlgebraSpec diff --git a/src/IntervalAlgebra.hs b/src/IntervalAlgebra.hs --- a/src/IntervalAlgebra.hs +++ b/src/IntervalAlgebra.hs @@ -10,763 +10,19 @@ and axiomatized in [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x). A good primer on Allen's algebra can be [found here](https://thomasalspaugh.org/pub/fnd/allen.html). -= Design - -The module is built around three typeclasses designed to separate concerns of -constructing, relating, and combining types that contain @'Interval'@s: - -1. @'Intervallic'@ provides an interface to the data structures which contain an - @'Interval'@. -2. @'IntervalCombinable'@ provides an interface to methods of combining two - @'Interval's@. -3. @'IntervalSizeable'@ provides methods for measuring and modifying the size of - an interval. +This main module reexports @IntervalAlgebra.Core@, @IntervalAlgebra.IntervalUtilities@, +and @IntervalAlgebra.PairedInterval@, which is probably more than enough to get +going for most cases. -} {-# LANGUAGE Safe #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE AllowAmbiguousTypes #-} - -module IntervalAlgebra( - - -- * Intervals - Interval - , Intervallic(..) - , begin - , end - - -- ** Create new intervals - , parseInterval - , beginerval - , enderval - - -- ** Modify intervals - , expand - , expandl - , expandr - - -- * Interval Algebra - - -- ** Interval Relations and Predicates - , IntervalRelation(..) - - {- | - === Meets, Metby - - > x `meets` y - > y `metBy` x - - @ - x: |-----| - y: |-----| - @ - -} - , meets , metBy - - {- | - === Before, After - - > x `before` y - > y `after` x - - @ - x: |-----| - y: |-----| - @ - -} - , before , after - - {- | - === Overlaps, OverlappedBy - - > x `overlaps` y - > y `overlappedBy` x - - @ - x: |-----| - y: |-----| - @ - -} - , overlaps , overlappedBy - - {- | - === Finishes, FinishedBy - - > x `finishes` y - > y `finishedBy` x - - @ - x: |---| - y: |-----| - @ - -} - , finishedBy , finishes - - {- | - === During, Contains - - > x `during` y - > y `contains` x - - @ - x: |-| - y: |-----| - @ - -} - , contains , during - - {- | - === Starts, StartedBy - - > x `starts` y - > y `startedBy` x - - @ - x: |---| - y: |-----| - @ - -} - , starts , startedBy - - {- | - === Equal - - > x `equal` y - > y `equal` x - - @ - x: |-----| - y: |-----| - @ - -} - , equals - - -- ** Additional predicates and utilities - , precedes, precededBy - , disjoint , notDisjoint, concur - , within, enclose, enclosedBy - , (<|>) - , predicate, unionPredicates - , disjointRelations, withinRelations - , ComparativePredicateOf1 - , ComparativePredicateOf2 - , beginervalFromEnd - , endervalFromBegin - , diffFromBegin - , diffFromEnd - , momentize - - -- ** Algebraic operations - , intervalRelations - , relate - , compose - , complement - , union - , intersection - , converse - - -- * Combine two intervals - , IntervalCombinable(..) - , extenterval - - -- * Measure an interval - , IntervalSizeable(..) - +module IntervalAlgebra( + module IntervalAlgebra.Core + , module IntervalAlgebra.IntervalUtilities + , module IntervalAlgebra.PairedInterval ) where -import Prelude ( Eq, Show, Enum(..), Bounded(..) - , Maybe(..), Either(..), String, Bool(..) - , Integer, Int, Num - , map, otherwise, show - , any, negate, not - , replicate - , (++), (==), (&&), (+), (-), (!!)) -import Data.Function ( ($), id, (.), flip ) -import Data.Functor ( Functor(fmap) ) -import Data.Ord ( Ord(..), Ordering(..), min, max ) -import Data.Semigroup ( Semigroup((<>)) ) -import qualified Data.Set ( Set - , fromList - , difference - , intersection - , union - , map - , toList ) -import Data.Tuple ( fst, snd ) -import Data.Time as DT ( Day - , addDays - , diffDays ) -import Control.Applicative ( Applicative(pure) ) - -{- | An @'Interval' a@ is a pair \( (x, y) \text{ such that } x < y\). To create -intervals use the @'parseInterval'@, @'beginerval'@, or @'enderval'@ functions. --} -newtype Interval a = Interval (a, a) deriving (Eq) - --- | Safely parse a pair of @a@s to create an @'Interval' a@. --- --- >>> parseInterval 0 1 --- Right (0, 1) --- --- >>> parseInterval 1 0 --- Left "0<1" --- -parseInterval :: (Show a, Ord a) => a -> a -> Either String (Interval a) -parseInterval x y - -- TODO: create more general framework for error handling - | y < x = Left $ show y ++ "<" ++ show x - | otherwise = Right $ Interval (x, y) - -intervalBegin :: (Ord a) => Interval a -> a -intervalBegin (Interval x) = fst x - -intervalEnd :: (Ord a) => Interval a -> a -intervalEnd (Interval x) = snd x - -instance Functor Interval where - fmap f (Interval (x, y)) = Interval (f x, f y) - -instance (Show a, Ord a) => Show (Interval a) where - show x = "(" ++ show (begin x) ++ ", " ++ show (end x) ++ ")" - -{- | -The @'Intervallic'@ typeclass defines how to get and set the 'Interval' content -of a data structure. It also includes functions for getting the endpoints of the -'Interval' via @'begin'@ and @'end'@. - ->>> getInterval (Interval (0, 10)) -(0, 10) - ->>> begin (Interval (0, 10)) -0 - ->>> end (Interval (0, 10)) -10 --} -class (Ord a) => Intervallic i a where - - -- | Get the interval from an @i a@. - getInterval :: i a -> Interval a - - -- | Set the interval in an @i a@. - setInterval :: i a -> Interval a -> i a - --- | Access the endpoints of an @i a@ . -begin, end :: Intervallic i a => i a -> a -begin = intervalBegin . getInterval -end = intervalEnd . getInterval - -{- | -The 'IntervalRelation' type and the associated predicate functions enumerate -the thirteen possible ways that two @'Interval'@ objects may 'relate' according -to Allen's interval algebra. Constructors are shown with their corresponding -predicate function. --} -data IntervalRelation = - Before -- ^ `before` - | Meets -- ^ `meets` - | Overlaps -- ^ `overlaps` - | FinishedBy -- ^ `finishedBy` - | Contains -- ^ `contains` - | Starts -- ^ `starts` - | Equals -- ^ `equals` - | StartedBy -- ^ `startedBy` - | During -- ^ `during` - | Finishes -- ^ `finishes` - | OverlappedBy -- ^ `overlappedBy` - | MetBy -- ^ `metBy` - | After -- ^ `after` - deriving (Eq, Show, Enum) - -instance Bounded IntervalRelation where - minBound = Before - maxBound = After - -instance Ord IntervalRelation where - compare x y = compare (fromEnum x) (fromEnum y) - --- | Does x `meets` y? Is x metBy y? -meets, metBy :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -meets x y = end x == begin y -metBy = flip meets - --- | Is x before y? Is x after y? -before, after, precedes, precededBy :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -before x y = end x < begin y -after = flip before -precedes = before -precededBy = after --- | Does x overlap y? Is x overlapped by y? -overlaps, overlappedBy :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -overlaps x y = begin x < begin y && end x < end y && end x > begin y -overlappedBy = flip overlaps - --- | Does x start y? Is x started by y? -starts, startedBy :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -starts x y = begin x == begin y && end x < end y -startedBy = flip starts - --- | Does x finish y? Is x finished by y? -finishes, finishedBy :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -finishes x y = begin x > begin y && end x == end y -finishedBy = flip finishes - --- | Is x during y? Does x contain y? -during, contains :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -during x y = begin x > begin y && end x < end y -contains = flip during - --- | Does x equal y? -equals :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -equals x y = begin x == begin y && end x == end y - --- | Operator for composing the union of two predicates -(<|>) :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) - -> ComparativePredicateOf2 (i0 a) (i1 a) - -> ComparativePredicateOf2 (i0 a) (i1 a) -(<|>) f g = unionPredicates [f, g] - --- | The set of @IntervalRelation@ meaning two intervals are disjoint. -disjointRelations :: Data.Set.Set IntervalRelation -disjointRelations = toSet [Before, After, Meets, MetBy] - --- | The set of @IntervalRelation@ meaning one interval is within the other. -withinRelations :: Data.Set.Set IntervalRelation -withinRelations = toSet [Starts, During, Finishes, Equals] - --- | Are x and y disjoint ('before', 'after', 'meets', or 'metBy')? -disjoint :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -disjoint = predicate disjointRelations - --- | Are x and y not disjoint (concur); i.e. do they share any support? This is --- the 'complement' of 'disjoint'. -notDisjoint, concur :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -notDisjoint = predicate (complement disjointRelations) -concur = notDisjoint - --- | Is x entirely *within* (enclosed by) the endpoints of y? That is, 'during', --- 'starts', 'finishes', or 'equals'? -within, enclosedBy:: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -within = predicate withinRelations -enclosedBy = within - --- | Does x enclose y? That is, is y 'within' x? -enclose :: (Intervallic i0 a, Intervallic i1 a)=> - ComparativePredicateOf2 (i0 a) (i1 a) -enclose = flip enclosedBy - --- | The 'Data.Set.Set' of all 'IntervalRelation's. -intervalRelations :: Data.Set.Set IntervalRelation -intervalRelations = Data.Set.fromList (Prelude.map toEnum [0..12] ::[IntervalRelation]) - --- | Find the converse of a single 'IntervalRelation' -converseRelation :: IntervalRelation -> IntervalRelation -converseRelation x = toEnum (12 - fromEnum x) - --- | Shortcut to creating a 'Set IntervalRelation' from a list. -toSet :: [IntervalRelation ] -> Data.Set.Set IntervalRelation -toSet = Data.Set.fromList - --- | Compose a list of interval relations with _or_ to create a new --- @'ComparativePredicateOf1' i a@. For example, --- @unionPredicates [before, meets]@ creates a predicate function determining --- if one interval is either before or meets another interval. -unionPredicates :: [ComparativePredicateOf2 a b] -> ComparativePredicateOf2 a b -unionPredicates fs x y = any (\ f -> f x y) fs - --- | Maps an 'IntervalRelation' to its corresponding predicate function. -toPredicate :: (Intervallic i0 a, Intervallic i1 a) => - IntervalRelation - -> ComparativePredicateOf2 (i0 a) (i1 a) -toPredicate r = - case r of - Before -> before - Meets -> meets - Overlaps -> overlaps - FinishedBy -> finishedBy - Contains -> contains - Starts -> starts - Equals -> equals - StartedBy -> startedBy - During -> during - Finishes -> finishes - OverlappedBy -> overlappedBy - MetBy -> metBy - After -> after - --- | Given a set of 'IntervalRelation's return a list of 'predicate' functions --- corresponding to each relation. -predicates :: (Intervallic i0 a, Intervallic i1 a)=> - Data.Set.Set IntervalRelation - -> [ComparativePredicateOf2 (i0 a) (i1 a)] -predicates x = Prelude.map toPredicate (Data.Set.toList x) - --- | Forms a predicate function from the union of a set of 'IntervalRelation's. -predicate :: (Intervallic i0 a, Intervallic i1 a)=> - Data.Set.Set IntervalRelation - -> ComparativePredicateOf2 (i0 a) (i1 a) -predicate = unionPredicates.predicates - --- | The lookup table for the compositions of interval relations. -composeRelationLookup :: [[[IntervalRelation]]] -composeRelationLookup = - [ [p , p , p , p , p , p , p , p , pmosd, pmosd, pmosd, pmosd, full ] - , [p , p , p , p , p , m , m , m , osd , osd , osd , fef , dsomp] - , [p , p , pmo , pmo , pmofd, o , o , ofd , osd , osd , cncr , dso , dsomp] - , [p , m , o , f' , d' , o , f', d' , osd , fef , dso , dso , dsomp] - , [pmofd, ofd , ofd , d' , d' , ofd , d', d' , cncr , dso , dso , dso , dsomp] - , [p , p , pmo , pmo , pmofd, s , s , ses , d , d , dfo , m' , p' ] - , [p , m , o , f' , d' , s , e , s' , d , f , o' , m' , p' ] - , [pmofd, ofd , ofd , d' , d' , ses , s', s' , dfo , o' , o' , m' , p' ] - , [p , p , pmosd, pmosd, full , d , d , dfomp, d , d , dfomp, p' , p' ] - , [p , m , osd , fef , dsomp, d , f , omp , d , f , omp , p' , p' ] - , [pmofd, ofd , cncr , dso , dsomp, dfo , o', omp , dfo , o' , omp , p' , p' ] - , [pmofd, ses , dfo , m' , p' , dfo , m', p' , dfo , m' , p' , p' , p' ] - , [full , dfomp, dfomp, p' , p' , dfomp, p', p' , dfomp, p' , p' , p' , p' ] - ] - where p = [Before] - m = [Meets] - o = [Overlaps] - f' = [FinishedBy] - d' = [Contains] - s = [Starts] - e = [Equals] - s' = [StartedBy] - d = [During] - f = [Finishes] - o' = [OverlappedBy] - m' = [MetBy] - p' = [After] - ses = s ++ e ++ s' - fef = f' ++ e ++ f - pmo = p ++ m ++ o - pmofd = pmo ++ f' ++ d' - osd = o ++ s ++ d - ofd = o ++ f' ++ d' - omp = o' ++ m' ++ p' - dfo = d ++ f ++ o' - dfomp = dfo ++ m' ++ p' - dso = d' ++ s' ++ o' - dsomp = dso ++ m' ++ p' - pmosd = p ++ m ++ osd - cncr = o ++ f' ++ d' ++ s ++ e ++ s' ++ d ++ f ++ o' - full = p ++ m ++ cncr ++ m' ++ p' - --- | Compare two @i a@ to determine their 'IntervalRelation'. --- --- >>> relate (Interval (0::Int, 1)) (Interval (1, 2)) --- Meets --- --- >>> relate (Interval (1::Int, 2)) (Interval (0, 1)) --- MetBy --- -relate :: (Intervallic i0 a, Intervallic i1 a) => i0 a -> i1 a -> IntervalRelation -relate x y - | x `before` y = Before - | x `after` y = After - | x `meets` y = Meets - | x `metBy` y = MetBy - | x `overlaps` y = Overlaps - | x `overlappedBy` y = OverlappedBy - | x `starts` y = Starts - | x `startedBy` y = StartedBy - | x `finishes` y = Finishes - | x `finishedBy` y = FinishedBy - | x `during` y = During - | x `contains` y = Contains - | otherwise = Equals - --- | Compose two interval relations according to the rules of the algebra. --- The rules are enumerated according to . -compose :: IntervalRelation - -> IntervalRelation - -> Data.Set.Set IntervalRelation -compose x y = toSet (composeRelationLookup !! fromEnum x !! fromEnum y) - --- | Finds the complement of a @'Data.Set.Set' 'IntervalRelation'@. -complement :: Data.Set.Set IntervalRelation -> Data.Set.Set IntervalRelation -complement = Data.Set.difference intervalRelations - --- | Find the intersection of two 'Data.Set.Set's of 'IntervalRelation's. -intersection :: Data.Set.Set IntervalRelation - -> Data.Set.Set IntervalRelation - -> Data.Set.Set IntervalRelation -intersection = Data.Set.intersection - --- | Find the union of two 'Data.Set.Set's of 'IntervalRelation's. -union :: Data.Set.Set IntervalRelation - -> Data.Set.Set IntervalRelation - -> Data.Set.Set IntervalRelation -union = Data.Set.union - --- | Find the converse of a @'Data.Set.Set' 'IntervalRelation'@. -converse :: Data.Set.Set IntervalRelation - -> Data.Set.Set IntervalRelation -converse = Data.Set.map converseRelation - -{- | -The 'IntervalSizeable' typeclass provides functions to determine the size of an -'Intervallic' type and to resize an 'Interval a'. --} -class (Ord a, Num b, Ord b) => IntervalSizeable a b| a -> b where - - -- | The smallest duration for an 'Interval a'. - moment :: b - moment = 1 - - -- | Gives back a 'moment' based on the input's type. - moment' :: Intervallic i a => i a -> b - moment' x = moment @a - - -- | Determine the duration of an @'i a'@. - duration :: Intervallic i a => i a -> b - duration x = diff (end x) (begin x) - - -- | Shifts an @a@. Most often, the @b@ will be the same type as @a@. - -- But for example, if @a@ is 'Day' then @b@ could be 'Int'. - add :: b -> a -> a - - -- | Takes the difference between two @a@ to return a @b@. - diff :: a -> a -> b - --- | Resize an @i a@ to by expanding to "left" by @l@ and to the --- "right" by @r@. In the case that @l@ or @r@ are less than a 'moment' --- the respective endpoints are unchanged. --- --- >>> expand 0 0 (Interval (0::Int, 2::Int)) --- (0, 2) --- --- >>> expand 1 1 (Interval (0::Int, 2::Int)) --- (-1, 3) --- -expand :: (IntervalSizeable a b, Intervallic i a) => - b -- ^ duration to subtract from the 'begin' - -> b -- ^ duration to add to the 'end' - -> i a - -> i a -expand l r p = setInterval p i - where s = if l < moment' p then 0 else negate l - e = if r < moment' p then 0 else r - i = Interval (add s $ begin p, add e $ end p) - --- | Expands an @i a@ to "left". --- --- >>> expandl 2 (Interval (0::Int, 2::Int)) --- (-2, 2) --- -expandl :: (IntervalSizeable a b, Intervallic i a) => b -> i a -> i a -expandl i = expand i 0 - --- | Expands an @i a@ to "right". --- --- >>> expandr 2 (Interval (0::Int, 2::Int)) --- (0, 4) --- -expandr :: (IntervalSizeable a b, Intervallic i a) => b -> i a -> i a -expandr = expand 0 - --- | Safely creates an 'Interval a' using @x@ as the 'begin' and adding --- @max 'moment' dur@ to @x@ as the 'end'. --- --- >>> beginerval (0::Int) (0::Int) --- (0, 1) --- --- >>> beginerval (1::Int) (0::Int) --- (0, 1) --- --- >>> beginerval (2::Int) (0::Int) --- (0, 2) --- -beginerval :: (IntervalSizeable a b) => - b -- ^ @dur@ation to add to the 'begin' - -> a -- ^ the 'begin' point of the 'Interval' - -> Interval a -beginerval dur x = Interval (x, y) - where i = Interval (x, x) - d = max (moment' i) dur - y = add d x -{-# INLINABLE beginerval #-} - --- | Safely creates an 'Interval a' using @x@ as the 'end' and adding --- @negate max 'moment' dur@ to @x@ as the 'begin'. --- --- >>> enderval (0::Int) (0::Int) --- (-1, 0) --- --- >>> enderval (1::Int) (0::Int) --- (-1, 0) --- --- >>> enderval (2::Int) (0::Int) --- (-2, 0) --- -enderval :: (IntervalSizeable a b) => - b -- ^ @dur@ation to subtract from the 'end' - -> a -- ^ the 'end' point of the 'Interval' - -> Interval a -enderval dur x = Interval (add (negate $ max (moment' i) dur) x, x) - where i = Interval (x, x) -{-# INLINABLE enderval #-} - --- | Creates a new Interval from the 'end' of an @i a@. -beginervalFromEnd :: (IntervalSizeable a b, Intervallic i a) => - b -- ^ @dur@ation to add to the 'end' - -> i a -- ^ the @i a@ from which to get the 'end' - -> Interval a -beginervalFromEnd d i = beginerval d (end i) - --- | Creates a new Interval from the 'begin' of an @i a@. -endervalFromBegin :: (IntervalSizeable a b, Intervallic i a) => - b -- ^ @dur@ation to subtract from the 'begin' - -> i a -- ^ the @i a@ from which to get the 'begin' - -> Interval a -endervalFromBegin d i = enderval d (begin i) - --- | Creates a new @Interval@ spanning the extent x and y. --- --- >>> extenterval (Interval (0, 1)) (Interval (9, 10)) --- (0, 10) --- -extenterval :: Intervallic i a => i a -> i a -> Interval a -extenterval x y = Interval (s, e) - where s = min (begin x) (begin y) - e = max (end x) (end y) - --- | Modifies the endpoints of second argument's interval by taking the difference --- from the first's input's 'begin'. --- >>> diffFromBegin (Interval ((5::Int), 6)) (Interval (10, 15)) --- (5, 10) --- --- >>> diffFromBegin (Interval ((1::Int), 2)) (Interval (3, 15)) --- (2, 14) --- -diffFromBegin :: ( IntervalSizeable a b - , Functor i1 - , Intervallic i0 a ) => - i0 a -> i1 a -> i1 b -diffFromBegin i = fmap (`diff` begin i) - --- | Modifies the endpoints of second argument's interval by taking the difference --- from the first's input's 'end'. --- >>> diffFromEnd (Interval ((5::Int), 6)) (Interval (10, 15)) --- (4, 9) --- --- >>> diffFromEnd (Interval ((1::Int), 2)) (Interval (3, 15)) --- (1, 13) --- -diffFromEnd :: ( IntervalSizeable a b - , Functor i1 - , Intervallic i0 a ) => - i0 a -> i1 a -> i1 b -diffFromEnd i = fmap (`diff` end i) - --- | Changes the duration of an 'Intervallic' value to a moment starting at the --- 'begin' of the interval. --- --- >>> momentize (Interval (6, 10)) --- (6, 7) --- -momentize :: ( IntervalSizeable a b, Intervallic i a ) => - i a -> i a -momentize i = setInterval i (beginerval (moment' i) (begin i)) - -{- | -The @'IntervalCombinable'@ typeclass provides methods for (possibly) combining -two @i a@s to form a @'Maybe' i a@, or in case of @><@, a possibly different -@Intervallic@ type. --} -class (Intervallic i a) => IntervalCombinable i a where - - -- | Maybe form a new @i a@ by the union of two @i a@s that 'meets'. - (.+.) :: i a -> i a -> Maybe (i a) - (.+.) x y - | x `meets` y = Just $ setInterval y $ Interval (b, e) - | otherwise = Nothing - where b = begin x - e = end y - {-# INLINABLE (.+.) #-} - - -- | If @x@ is 'before' @y@, then form a new @Just Interval a@ from the - -- interval in the "gap" between @x@ and @y@ from the 'end' of @x@ to the - -- 'begin' of @y@. Otherwise, 'Nothing'. - (><) :: i a -> i a -> Maybe (i a) - - -- | If @x@ is 'before' @y@, return @f x@ appended to @f y@. Otherwise, - -- return 'extenterval' of @x@ and @y@ (wrapped in @f@). This is useful for - -- (left) folding over an *ordered* container of @Interval@s and combining - -- intervals when @x@ is *not* 'before' @y@. - (<+>):: ( Semigroup (f (i a)), Applicative f) => - i a - -> i a - -> f (i a) - -{- -Misc --} - --- | Defines a predicate of two objects of type @a@. -type ComparativePredicateOf1 a = (a -> a -> Bool) - --- | Defines a predicate of two object of different types. -type ComparativePredicateOf2 a b = (a -> b -> Bool) - --- {- --- Instances --- -} - --- | Imposes a total ordering on @'Interval' a@ based on first ordering the --- 'begin's then the 'end's. -instance (Ord a) => Ord (Interval a) where - (<=) x y - | begin x < begin y = True - | begin x == begin y = end x <= end y - | otherwise = False - (<) x y - | begin x < begin y = True - | begin x == begin y = end x < end y - | otherwise = False - -instance (Ord a) => Intervallic Interval a where - getInterval = id - setInterval _ x = x - -instance (Ord a) => IntervalCombinable Interval a where - (><) x y - | x `before` y = Just $ Interval (end x, begin y) - | otherwise = Nothing - {-# INLINABLE (><) #-} - - (<+>) x y - | x `before` y = pure ( getInterval x ) <> pure ( getInterval y ) - | otherwise = pure ( extenterval x y ) - {-# INLINABLE (<+>) #-} - -instance IntervalSizeable Int Int where - moment = 1 - add = (+) - diff = (-) - -instance IntervalSizeable Integer Integer where - moment = 1 - add = (+) - diff = (-) - -instance IntervalSizeable DT.Day Integer where - moment = 1 - add = addDays - diff = diffDays +import safe IntervalAlgebra.Core +import safe IntervalAlgebra.IntervalUtilities +import safe IntervalAlgebra.PairedInterval diff --git a/src/IntervalAlgebra/Arbitrary.hs b/src/IntervalAlgebra/Arbitrary.hs --- a/src/IntervalAlgebra/Arbitrary.hs +++ b/src/IntervalAlgebra/Arbitrary.hs @@ -13,21 +13,50 @@ module IntervalAlgebra.Arbitrary() where -import Test.QuickCheck ( Arbitrary(arbitrary, shrink) ) +import Test.QuickCheck ( Arbitrary(arbitrary, shrink), + Gen, NonNegative ) import GHC.Int ( Int ) -import GHC.Num ( Num((+), negate) ) -import Control.Applicative ( (<$>) ) +import GHC.Num +import GHC.Real +import GHC.Float +import Control.Applicative ( (<$>), liftA2 ) import Control.Monad ( liftM2 ) import IntervalAlgebra (Interval, beginerval) -import Data.Function ( (.) ) -import Data.Time as DT ( Day(ModifiedJulianDay), toModifiedJulianDay) +import Data.Function ( (.), ($) ) +import Data.Fixed +import Data.Bool +import Data.Ord +import Data.Time as DT ( Day(ModifiedJulianDay) + , toModifiedJulianDay + , picosecondsToDiffTime + , secondsToDiffTime + , secondsToNominalDiffTime + , UTCTime(..), NominalDiffTime) instance Arbitrary (Interval Int) where arbitrary = liftM2 beginerval arbitrary arbitrary instance Arbitrary DT.Day where - arbitrary = DT.ModifiedJulianDay . (2000 +) <$> arbitrary + arbitrary = DT.ModifiedJulianDay <$> arbitrary shrink = (DT.ModifiedJulianDay <$>) . shrink . DT.toModifiedJulianDay + +withinDiffTimeRange :: Integer -> Integer +withinDiffTimeRange x + | x < 0 = 0 + | x > 86400 = 86400 + | otherwise = x + +instance Arbitrary DT.NominalDiffTime where + arbitrary = fromInteger . withinDiffTimeRange <$> (arbitrary :: Gen Integer) + +instance Arbitrary DT.UTCTime where + arbitrary = liftA2 UTCTime + arbitrary + (secondsToDiffTime . withinDiffTimeRange <$> (arbitrary :: Gen Integer) ) + instance Arbitrary (Interval DT.Day) where + arbitrary = liftM2 beginerval arbitrary arbitrary + +instance Arbitrary (Interval DT.UTCTime) where arbitrary = liftM2 beginerval arbitrary arbitrary diff --git a/src/IntervalAlgebra/Axioms.hs b/src/IntervalAlgebra/Axioms.hs new file mode 100644 --- /dev/null +++ b/src/IntervalAlgebra/Axioms.hs @@ -0,0 +1,342 @@ +{-| +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 Test.QuickCheck ( (===) + , (==>) + , Property + , Arbitrary (arbitrary) ) +import Data.Either ( isRight ) +import Data.Maybe ( fromJust, isJust, isNothing ) +import Data.Time as DT ( Day(..) + , UTCTime(..) + , DiffTime + , NominalDiffTime + ) +import Data.Set ( Set + , member + , disjointUnion + , fromList ) +import IntervalAlgebra.Core +import IntervalAlgebra.Arbitrary + + +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 diff --git a/src/IntervalAlgebra/Core.hs b/src/IntervalAlgebra/Core.hs new file mode 100644 --- /dev/null +++ b/src/IntervalAlgebra/Core.hs @@ -0,0 +1,795 @@ +{-| +Module : Interval Algebra +Description : Implementation of Allen's interval algebra +Copyright : (c) NoviSci, Inc 2020 +License : BSD3 +Maintainer : bsaul@novisci.com + +The @IntervalAlgebra@ module provides data types and related classes for the +interval-based temporal logic described in [Allen (1983)](https://doi.org/10.1145/182.358434) +and axiomatized in [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x). +A good primer on Allen's algebra can be [found here](https://thomasalspaugh.org/pub/fnd/allen.html). + += Design + +The module is built around three typeclasses designed to separate concerns of +constructing, relating, and combining types that contain @'Interval'@s: + +1. @'Intervallic'@ provides an interface to the data structures which contain an + @'Interval'@. +2. @'IntervalCombinable'@ provides an interface to methods of combining two + @'Interval's@. +3. @'IntervalSizeable'@ provides methods for measuring and modifying the size of + an interval. + +-} + +{-# LANGUAGE Safe #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE AllowAmbiguousTypes #-} + +module IntervalAlgebra.Core( + + -- * Intervals + Interval + , Intervallic(..) + , ParseErrorInterval(..) + , begin + , end + + -- ** Create new intervals + , parseInterval + , beginerval + , enderval + + -- ** Modify intervals + , expand + , expandl + , expandr + + -- * Interval Algebra + + -- ** Interval Relations and Predicates + , IntervalRelation(..) + + {- | + === Meets, Metby + + > x `meets` y + > y `metBy` x + + @ + x: |-----| + y: |-----| + @ + -} + , meets , metBy + + {- | + === Before, After + + > x `before` y + > y `after` x + + @ + x: |-----| + y: |-----| + @ + -} + , before , after + + {- | + === Overlaps, OverlappedBy + + > x `overlaps` y + > y `overlappedBy` x + + @ + x: |-----| + y: |-----| + @ + -} + , overlaps , overlappedBy + + {- | + === Finishes, FinishedBy + + > x `finishes` y + > y `finishedBy` x + + @ + x: |---| + y: |-----| + @ + -} + , finishedBy , finishes + + {- | + === During, Contains + + > x `during` y + > y `contains` x + + @ + x: |-| + y: |-----| + @ + -} + , contains , during + + {- | + === Starts, StartedBy + + > x `starts` y + > y `startedBy` x + + @ + x: |---| + y: |-----| + @ + -} + , starts , startedBy + + {- | + === Equal + + > x `equal` y + > y `equal` x + + @ + x: |-----| + y: |-----| + @ + -} + , equals + + -- ** Additional predicates and utilities + , precedes, precededBy + , disjoint , notDisjoint, concur + , within, enclose, enclosedBy + , (<|>) + , predicate, unionPredicates + , disjointRelations, withinRelations + , ComparativePredicateOf1 + , ComparativePredicateOf2 + , beginervalFromEnd + , endervalFromBegin + , diffFromBegin + , diffFromEnd + , momentize + + -- ** Algebraic operations + , intervalRelations + , relate + , compose + , complement + , union + , intersection + , converse + + -- * Combine two intervals + , IntervalCombinable(..) + , extenterval + + -- * Measure an interval + , IntervalSizeable(..) + +) where + +import Prelude ( Eq, Show, Enum(..), Bounded(..) + , Maybe(..), Either(..), String, Bool(..) + , Integer, Int, Num, Rational + , map, otherwise, show + , any, negate, not + , replicate + , fromRational + , toRational + , fromInteger + , toInteger + , (++), (==), (&&), (+), (-), (!!), realToFrac) +import Data.Function ( ($), id, (.), flip ) +import Data.Functor ( Functor(fmap) ) +import Data.Ord ( Ord(..), Ordering(..), min, max ) +import Data.Semigroup ( Semigroup((<>)) ) +import qualified Data.Set ( Set + , fromList + , difference + , intersection + , union + , map + , toList ) +import Data.Tuple ( fst, snd ) +import Data.Fixed ( Pico ) +import Data.Time as DT ( Day + , UTCTime + , NominalDiffTime + , DiffTime + , addUTCTime + , diffUTCTime + , secondsToNominalDiffTime + , nominalDiffTimeToSeconds + , addDays + , diffDays ) +import Control.Applicative ( Applicative(pure) ) + +{- | An @'Interval' a@ is a pair \( (x, y) \text{ such that } x < y\). To create +intervals use the @'parseInterval'@, @'beginerval'@, or @'enderval'@ functions. +-} +newtype Interval a = Interval (a, a) deriving (Eq) + +-- | A type identifying interval parsing errors. +newtype ParseErrorInterval = ParseErrorInterval String + deriving (Eq, Show) + +-- | Safely parse a pair of @a@s to create an @'Interval' a@. +-- +-- >>> parseInterval 0 1 +-- Right (0, 1) +-- +-- >>> parseInterval 1 0 +-- Left "0<1" +-- +parseInterval :: (Show a, Ord a) => a -> a -> Either ParseErrorInterval (Interval a) +parseInterval x y + | y < x = Left $ ParseErrorInterval $ show y ++ "<" ++ show x + | otherwise = Right $ Interval (x, y) + +intervalBegin :: (Ord a) => Interval a -> a +intervalBegin (Interval x) = fst x + +intervalEnd :: (Ord a) => Interval a -> a +intervalEnd (Interval x) = snd x + +instance Functor Interval where + fmap f (Interval (x, y)) = Interval (f x, f y) + +instance (Show a, Ord a) => Show (Interval a) where + show x = "(" ++ show (begin x) ++ ", " ++ show (end x) ++ ")" + +{- | +The @'Intervallic'@ typeclass defines how to get and set the 'Interval' content +of a data structure. It also includes functions for getting the endpoints of the +'Interval' via @'begin'@ and @'end'@. + +>>> getInterval (Interval (0, 10)) +(0, 10) + +>>> begin (Interval (0, 10)) +0 + +>>> end (Interval (0, 10)) +10 +-} +class (Ord a) => Intervallic i a where + + -- | Get the interval from an @i a@. + getInterval :: i a -> Interval a + + -- | Set the interval in an @i a@. + setInterval :: i a -> Interval a -> i a + +-- | Access the endpoints of an @i a@ . +begin, end :: Intervallic i a => i a -> a +begin = intervalBegin . getInterval +end = intervalEnd . getInterval + +{- | +The 'IntervalRelation' type and the associated predicate functions enumerate +the thirteen possible ways that two @'Interval'@ objects may 'relate' according +to Allen's interval algebra. Constructors are shown with their corresponding +predicate function. +-} +data IntervalRelation = + Before -- ^ `before` + | Meets -- ^ `meets` + | Overlaps -- ^ `overlaps` + | FinishedBy -- ^ `finishedBy` + | Contains -- ^ `contains` + | Starts -- ^ `starts` + | Equals -- ^ `equals` + | StartedBy -- ^ `startedBy` + | During -- ^ `during` + | Finishes -- ^ `finishes` + | OverlappedBy -- ^ `overlappedBy` + | MetBy -- ^ `metBy` + | After -- ^ `after` + deriving (Eq, Show, Enum) + +instance Bounded IntervalRelation where + minBound = Before + maxBound = After + +instance Ord IntervalRelation where + compare x y = compare (fromEnum x) (fromEnum y) + +-- | Does x `meets` y? Is x metBy y? +meets, metBy :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +meets x y = end x == begin y +metBy = flip meets + +-- | Is x before y? Is x after y? +before, after, precedes, precededBy :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +before x y = end x < begin y +after = flip before +precedes = before +precededBy = after +-- | Does x overlap y? Is x overlapped by y? +overlaps, overlappedBy :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +overlaps x y = begin x < begin y && end x < end y && end x > begin y +overlappedBy = flip overlaps + +-- | Does x start y? Is x started by y? +starts, startedBy :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +starts x y = begin x == begin y && end x < end y +startedBy = flip starts + +-- | Does x finish y? Is x finished by y? +finishes, finishedBy :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +finishes x y = begin x > begin y && end x == end y +finishedBy = flip finishes + +-- | Is x during y? Does x contain y? +during, contains :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +during x y = begin x > begin y && end x < end y +contains = flip during + +-- | Does x equal y? +equals :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +equals x y = begin x == begin y && end x == end y + +-- | Operator for composing the union of two predicates +(<|>) :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) + -> ComparativePredicateOf2 (i0 a) (i1 a) + -> ComparativePredicateOf2 (i0 a) (i1 a) +(<|>) f g = unionPredicates [f, g] + +-- | The set of @IntervalRelation@ meaning two intervals are disjoint. +disjointRelations :: Data.Set.Set IntervalRelation +disjointRelations = toSet [Before, After, Meets, MetBy] + +-- | The set of @IntervalRelation@ meaning one interval is within the other. +withinRelations :: Data.Set.Set IntervalRelation +withinRelations = toSet [Starts, During, Finishes, Equals] + +-- | Are x and y disjoint ('before', 'after', 'meets', or 'metBy')? +disjoint :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +disjoint = predicate disjointRelations + +-- | Are x and y not disjoint (concur); i.e. do they share any support? This is +-- the 'complement' of 'disjoint'. +notDisjoint, concur :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +notDisjoint = predicate (complement disjointRelations) +concur = notDisjoint + +-- | Is x entirely *within* (enclosed by) the endpoints of y? That is, 'during', +-- 'starts', 'finishes', or 'equals'? +within, enclosedBy:: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +within = predicate withinRelations +enclosedBy = within + +-- | Does x enclose y? That is, is y 'within' x? +enclose :: (Intervallic i0 a, Intervallic i1 a)=> + ComparativePredicateOf2 (i0 a) (i1 a) +enclose = flip enclosedBy + +-- | The 'Data.Set.Set' of all 'IntervalRelation's. +intervalRelations :: Data.Set.Set IntervalRelation +intervalRelations = Data.Set.fromList (Prelude.map toEnum [0..12] ::[IntervalRelation]) + +-- | Find the converse of a single 'IntervalRelation' +converseRelation :: IntervalRelation -> IntervalRelation +converseRelation x = toEnum (12 - fromEnum x) + +-- | Shortcut to creating a 'Set IntervalRelation' from a list. +toSet :: [IntervalRelation ] -> Data.Set.Set IntervalRelation +toSet = Data.Set.fromList + +-- | Compose a list of interval relations with _or_ to create a new +-- @'ComparativePredicateOf1' i a@. For example, +-- @unionPredicates [before, meets]@ creates a predicate function determining +-- if one interval is either before or meets another interval. +unionPredicates :: [ComparativePredicateOf2 a b] -> ComparativePredicateOf2 a b +unionPredicates fs x y = any (\ f -> f x y) fs + +-- | Maps an 'IntervalRelation' to its corresponding predicate function. +toPredicate :: (Intervallic i0 a, Intervallic i1 a) => + IntervalRelation + -> ComparativePredicateOf2 (i0 a) (i1 a) +toPredicate r = + case r of + Before -> before + Meets -> meets + Overlaps -> overlaps + FinishedBy -> finishedBy + Contains -> contains + Starts -> starts + Equals -> equals + StartedBy -> startedBy + During -> during + Finishes -> finishes + OverlappedBy -> overlappedBy + MetBy -> metBy + After -> after + +-- | Given a set of 'IntervalRelation's return a list of 'predicate' functions +-- corresponding to each relation. +predicates :: (Intervallic i0 a, Intervallic i1 a)=> + Data.Set.Set IntervalRelation + -> [ComparativePredicateOf2 (i0 a) (i1 a)] +predicates x = Prelude.map toPredicate (Data.Set.toList x) + +-- | Forms a predicate function from the union of a set of 'IntervalRelation's. +predicate :: (Intervallic i0 a, Intervallic i1 a)=> + Data.Set.Set IntervalRelation + -> ComparativePredicateOf2 (i0 a) (i1 a) +predicate = unionPredicates.predicates + +-- | The lookup table for the compositions of interval relations. +composeRelationLookup :: [[[IntervalRelation]]] +composeRelationLookup = + [ [p , p , p , p , p , p , p , p , pmosd, pmosd, pmosd, pmosd, full ] + , [p , p , p , p , p , m , m , m , osd , osd , osd , fef , dsomp] + , [p , p , pmo , pmo , pmofd, o , o , ofd , osd , osd , cncr , dso , dsomp] + , [p , m , o , f' , d' , o , f', d' , osd , fef , dso , dso , dsomp] + , [pmofd, ofd , ofd , d' , d' , ofd , d', d' , cncr , dso , dso , dso , dsomp] + , [p , p , pmo , pmo , pmofd, s , s , ses , d , d , dfo , m' , p' ] + , [p , m , o , f' , d' , s , e , s' , d , f , o' , m' , p' ] + , [pmofd, ofd , ofd , d' , d' , ses , s', s' , dfo , o' , o' , m' , p' ] + , [p , p , pmosd, pmosd, full , d , d , dfomp, d , d , dfomp, p' , p' ] + , [p , m , osd , fef , dsomp, d , f , omp , d , f , omp , p' , p' ] + , [pmofd, ofd , cncr , dso , dsomp, dfo , o', omp , dfo , o' , omp , p' , p' ] + , [pmofd, ses , dfo , m' , p' , dfo , m', p' , dfo , m' , p' , p' , p' ] + , [full , dfomp, dfomp, p' , p' , dfomp, p', p' , dfomp, p' , p' , p' , p' ] + ] + where p = [Before] + m = [Meets] + o = [Overlaps] + f' = [FinishedBy] + d' = [Contains] + s = [Starts] + e = [Equals] + s' = [StartedBy] + d = [During] + f = [Finishes] + o' = [OverlappedBy] + m' = [MetBy] + p' = [After] + ses = s ++ e ++ s' + fef = f' ++ e ++ f + pmo = p ++ m ++ o + pmofd = pmo ++ f' ++ d' + osd = o ++ s ++ d + ofd = o ++ f' ++ d' + omp = o' ++ m' ++ p' + dfo = d ++ f ++ o' + dfomp = dfo ++ m' ++ p' + dso = d' ++ s' ++ o' + dsomp = dso ++ m' ++ p' + pmosd = p ++ m ++ osd + cncr = o ++ f' ++ d' ++ s ++ e ++ s' ++ d ++ f ++ o' + full = p ++ m ++ cncr ++ m' ++ p' + +-- | Compare two @i a@ to determine their 'IntervalRelation'. +-- +-- >>> relate (Interval (0::Int, 1)) (Interval (1, 2)) +-- Meets +-- +-- >>> relate (Interval (1::Int, 2)) (Interval (0, 1)) +-- MetBy +-- +relate :: (Intervallic i0 a, Intervallic i1 a) => i0 a -> i1 a -> IntervalRelation +relate x y + | x `before` y = Before + | x `after` y = After + | x `meets` y = Meets + | x `metBy` y = MetBy + | x `overlaps` y = Overlaps + | x `overlappedBy` y = OverlappedBy + | x `starts` y = Starts + | x `startedBy` y = StartedBy + | x `finishes` y = Finishes + | x `finishedBy` y = FinishedBy + | x `during` y = During + | x `contains` y = Contains + | otherwise = Equals + +-- | Compose two interval relations according to the rules of the algebra. +-- The rules are enumerated according to . +compose :: IntervalRelation + -> IntervalRelation + -> Data.Set.Set IntervalRelation +compose x y = toSet (composeRelationLookup !! fromEnum x !! fromEnum y) + +-- | Finds the complement of a @'Data.Set.Set' 'IntervalRelation'@. +complement :: Data.Set.Set IntervalRelation -> Data.Set.Set IntervalRelation +complement = Data.Set.difference intervalRelations + +-- | Find the intersection of two 'Data.Set.Set's of 'IntervalRelation's. +intersection :: Data.Set.Set IntervalRelation + -> Data.Set.Set IntervalRelation + -> Data.Set.Set IntervalRelation +intersection = Data.Set.intersection + +-- | Find the union of two 'Data.Set.Set's of 'IntervalRelation's. +union :: Data.Set.Set IntervalRelation + -> Data.Set.Set IntervalRelation + -> Data.Set.Set IntervalRelation +union = Data.Set.union + +-- | Find the converse of a @'Data.Set.Set' 'IntervalRelation'@. +converse :: Data.Set.Set IntervalRelation + -> Data.Set.Set IntervalRelation +converse = Data.Set.map converseRelation + +{- | +The 'IntervalSizeable' typeclass provides functions to determine the size of an +'Intervallic' type and to resize an 'Interval a'. +-} +class (Ord a, Num b, Ord b) => IntervalSizeable a b | a -> b where + + -- | The smallest duration for an 'Interval a'. + moment :: b + moment = 1 + + -- | Gives back a 'moment' based on the input's type. + moment' :: Intervallic i a => i a -> b + moment' x = moment @a + + -- | Determine the duration of an @'i a'@. + duration :: Intervallic i a => i a -> b + duration x = diff (end x) (begin x) + + -- | Shifts an @a@. Most often, the @b@ will be the same type as @a@. + -- But for example, if @a@ is 'Day' then @b@ could be 'Int'. + add :: b -> a -> a + + -- | Takes the difference between two @a@ to return a @b@. + diff :: a -> a -> b + +-- | Resize an @i a@ to by expanding to "left" by @l@ and to the +-- "right" by @r@. In the case that @l@ or @r@ are less than a 'moment' +-- the respective endpoints are unchanged. +-- +-- >>> expand 0 0 (Interval (0::Int, 2::Int)) +-- (0, 2) +-- +-- >>> expand 1 1 (Interval (0::Int, 2::Int)) +-- (-1, 3) +-- +expand :: (IntervalSizeable a b, Intervallic i a) => + b -- ^ duration to subtract from the 'begin' + -> b -- ^ duration to add to the 'end' + -> i a + -> i a +expand l r p = setInterval p i + where s = if l < moment' p then 0 else negate l + e = if r < moment' p then 0 else r + i = Interval (add s $ begin p, add e $ end p) + +-- | Expands an @i a@ to "left". +-- +-- >>> expandl 2 (Interval (0::Int, 2::Int)) +-- (-2, 2) +-- +expandl :: (IntervalSizeable a b, Intervallic i a) => b -> i a -> i a +expandl i = expand i 0 + +-- | Expands an @i a@ to "right". +-- +-- >>> expandr 2 (Interval (0::Int, 2::Int)) +-- (0, 4) +-- +expandr :: (IntervalSizeable a b, Intervallic i a) => b -> i a -> i a +expandr = expand 0 + +-- | Safely creates an 'Interval a' using @x@ as the 'begin' and adding +-- @max 'moment' dur@ to @x@ as the 'end'. +-- +-- >>> beginerval (0::Int) (0::Int) +-- (0, 1) +-- +-- >>> beginerval (1::Int) (0::Int) +-- (0, 1) +-- +-- >>> beginerval (2::Int) (0::Int) +-- (0, 2) +-- +beginerval :: (IntervalSizeable a b) => + b -- ^ @dur@ation to add to the 'begin' + -> a -- ^ the 'begin' point of the 'Interval' + -> Interval a +beginerval dur x = Interval (x, y) + where i = Interval (x, x) + d = max (moment' i) dur + y = add d x +{-# INLINABLE beginerval #-} + +-- | Safely creates an 'Interval a' using @x@ as the 'end' and adding +-- @negate max 'moment' dur@ to @x@ as the 'begin'. +-- +-- >>> enderval (0::Int) (0::Int) +-- (-1, 0) +-- +-- >>> enderval (1::Int) (0::Int) +-- (-1, 0) +-- +-- >>> enderval (2::Int) (0::Int) +-- (-2, 0) +-- +enderval :: (IntervalSizeable a b) => + b -- ^ @dur@ation to subtract from the 'end' + -> a -- ^ the 'end' point of the 'Interval' + -> Interval a +enderval dur x = Interval (add (negate $ max (moment' i) dur) x, x) + where i = Interval (x, x) +{-# INLINABLE enderval #-} + +-- | Creates a new Interval from the 'end' of an @i a@. +beginervalFromEnd :: (IntervalSizeable a b, Intervallic i a) => + b -- ^ @dur@ation to add to the 'end' + -> i a -- ^ the @i a@ from which to get the 'end' + -> Interval a +beginervalFromEnd d i = beginerval d (end i) + +-- | Creates a new Interval from the 'begin' of an @i a@. +endervalFromBegin :: (IntervalSizeable a b, Intervallic i a) => + b -- ^ @dur@ation to subtract from the 'begin' + -> i a -- ^ the @i a@ from which to get the 'begin' + -> Interval a +endervalFromBegin d i = enderval d (begin i) + +-- | Creates a new @Interval@ spanning the extent x and y. +-- +-- >>> extenterval (Interval (0, 1)) (Interval (9, 10)) +-- (0, 10) +-- +extenterval :: Intervallic i a => i a -> i a -> Interval a +extenterval x y = Interval (s, e) + where s = min (begin x) (begin y) + e = max (end x) (end y) + +-- | Modifies the endpoints of second argument's interval by taking the difference +-- from the first's input's 'begin'. +-- >>> diffFromBegin (Interval ((5::Int), 6)) (Interval (10, 15)) +-- (5, 10) +-- +-- >>> diffFromBegin (Interval ((1::Int), 2)) (Interval (3, 15)) +-- (2, 14) +-- +diffFromBegin :: ( IntervalSizeable a b + , Functor i1 + , Intervallic i0 a ) => + i0 a -> i1 a -> i1 b +diffFromBegin i = fmap (`diff` begin i) + +-- | Modifies the endpoints of second argument's interval by taking the difference +-- from the first's input's 'end'. +-- >>> diffFromEnd (Interval ((5::Int), 6)) (Interval (10, 15)) +-- (4, 9) +-- +-- >>> diffFromEnd (Interval ((1::Int), 2)) (Interval (3, 15)) +-- (1, 13) +-- +diffFromEnd :: ( IntervalSizeable a b + , Functor i1 + , Intervallic i0 a ) => + i0 a -> i1 a -> i1 b +diffFromEnd i = fmap (`diff` end i) + +-- | Changes the duration of an 'Intervallic' value to a moment starting at the +-- 'begin' of the interval. +-- +-- >>> momentize (Interval (6, 10)) +-- (6, 7) +-- +momentize :: ( IntervalSizeable a b, Intervallic i a ) => + i a -> i a +momentize i = setInterval i (beginerval (moment' i) (begin i)) + +{- | +The @'IntervalCombinable'@ typeclass provides methods for (possibly) combining +two @i a@s to form a @'Maybe' i a@, or in case of @><@, a possibly different +@Intervallic@ type. +-} +class (Intervallic i a) => IntervalCombinable i a where + + -- | Maybe form a new @i a@ by the union of two @i a@s that 'meets'. + (.+.) :: i a -> i a -> Maybe (i a) + (.+.) x y + | x `meets` y = Just $ setInterval y $ Interval (b, e) + | otherwise = Nothing + where b = begin x + e = end y + {-# INLINABLE (.+.) #-} + + -- | If @x@ is 'before' @y@, then form a new @Just Interval a@ from the + -- interval in the "gap" between @x@ and @y@ from the 'end' of @x@ to the + -- 'begin' of @y@. Otherwise, 'Nothing'. + (><) :: i a -> i a -> Maybe (i a) + + -- | If @x@ is 'before' @y@, return @f x@ appended to @f y@. Otherwise, + -- return 'extenterval' of @x@ and @y@ (wrapped in @f@). This is useful for + -- (left) folding over an *ordered* container of @Interval@s and combining + -- intervals when @x@ is *not* 'before' @y@. + (<+>):: ( Semigroup (f (i a)), Applicative f) => + i a + -> i a + -> f (i a) + + +{- +Misc +-} + +-- | Defines a predicate of two objects of type @a@. +type ComparativePredicateOf1 a = (a -> a -> Bool) + +-- | Defines a predicate of two object of different types. +type ComparativePredicateOf2 a b = (a -> b -> Bool) + +-- {- +-- Instances +-- -} + +-- | Imposes a total ordering on @'Interval' a@ based on first ordering the +-- 'begin's then the 'end's. +instance (Ord a) => Ord (Interval a) where + (<=) x y + | begin x < begin y = True + | begin x == begin y = end x <= end y + | otherwise = False + (<) x y + | begin x < begin y = True + | begin x == begin y = end x < end y + | otherwise = False + +instance (Ord a) => Intervallic Interval a where + getInterval = id + setInterval _ x = x + +instance (Ord a) => IntervalCombinable Interval a where + (><) x y + | x `before` y = Just $ Interval (end x, begin y) + | otherwise = Nothing + {-# INLINABLE (><) #-} + + (<+>) x y + | x `before` y = pure x <> pure y + | otherwise = pure ( extenterval x y ) + {-# INLINABLE (<+>) #-} + +instance IntervalSizeable Int Int where + moment = 1 + add = (+) + diff = (-) + +instance IntervalSizeable Integer Integer where + moment = 1 + add = (+) + diff = (-) + +instance IntervalSizeable DT.Day Integer where + moment = 1 + add = addDays + diff = diffDays + +-- | Note that the @moment@ of this instance is a @'Data.Fixed.Pico'@ +instance IntervalSizeable DT.UTCTime NominalDiffTime where + moment = toEnum 1 :: NominalDiffTime + add = addUTCTime + diff = diffUTCTime diff --git a/src/IntervalAlgebra/IntervalUtilities.hs b/src/IntervalAlgebra/IntervalUtilities.hs --- a/src/IntervalAlgebra/IntervalUtilities.hs +++ b/src/IntervalAlgebra/IntervalUtilities.hs @@ -89,7 +89,7 @@ , Witherable(..) , mapMaybe , catMaybes ) -import safe IntervalAlgebra ( (<|>), +import safe IntervalAlgebra.Core ( (<|>), begin, end, after, diff --git a/src/IntervalAlgebra/PairedInterval.hs b/src/IntervalAlgebra/PairedInterval.hs --- a/src/IntervalAlgebra/PairedInterval.hs +++ b/src/IntervalAlgebra/PairedInterval.hs @@ -22,14 +22,14 @@ , trivialize ) where -import IntervalAlgebra ( Interval - , Intervallic(..) - , before - , IntervalCombinable(..) - , ComparativePredicateOf1 - , extenterval ) -import Witherable ( Filterable(filter) ) -import Data.Bifunctor ( Bifunctor(bimap) ) +import safe IntervalAlgebra.Core ( Interval + , Intervallic(..) + , before + , IntervalCombinable(..) + , ComparativePredicateOf1 + , extenterval ) +import safe Witherable ( Filterable(filter) ) +import safe Data.Bifunctor ( Bifunctor(bimap) ) -- | An @Interval a@ paired with some other data of type @b@. newtype PairedInterval b a = PairedInterval (Interval a, b) diff --git a/src/IntervalAlgebra/RelationProperties.hs b/src/IntervalAlgebra/RelationProperties.hs new file mode 100644 --- /dev/null +++ b/src/IntervalAlgebra/RelationProperties.hs @@ -0,0 +1,147 @@ +{-| +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.RelationProperties ( + IntervalRelationProperties(..) +) where + +import Test.QuickCheck ( (===) + , (==>) + , Property + , Arbitrary (arbitrary) ) +import Data.Maybe ( fromJust, isJust, isNothing ) +import Data.Time as DT ( Day + , UTCTime + , NominalDiffTime + ) +import Data.Set ( Set + , member + , disjointUnion + , fromList ) +import IntervalAlgebra.Core +import IntervalAlgebra.Arbitrary + +allIArelations:: (Ord a) => [ComparativePredicateOf1 (Interval a)] +allIArelations = [ equals + , meets + , metBy + , before + , after + , starts + , startedBy + , finishes + , finishedBy + , overlaps + , overlappedBy + , during + , 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 x y = + ( 1 == length (filter id $ map (\r -> r x y) allIArelations)) === 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 s pred i0 i1 = + pred i0 i1 === (relate i0 i1 `elem` s) + + prop_IAbefore :: Interval a -> Interval a -> Property + prop_IAbefore i j = + before i j ==> (i `meets` k) && (k `meets` j) + where k = beginerval (diff (begin j) (end i)) (end i) + + prop_IAstarts:: Interval a -> Interval a -> Property + prop_IAstarts i j + | starts i j = (j == fromJust (i .+. k)) === True + | otherwise = starts i j === False + where k = beginerval (diff (end j) (end i)) (end i) + + prop_IAfinishes:: Interval a -> Interval a -> Property + prop_IAfinishes i j + | finishes i j = (j == fromJust ( k .+. i)) === True + | otherwise = finishes i j === False + where k = beginerval (diff (begin i) (begin j)) (begin j) + + prop_IAoverlaps:: Interval a -> Interval a -> Property + prop_IAoverlaps i j + | overlaps i j = ((i == fromJust ( k .+. l )) && + (j == fromJust ( l .+. m ))) === True + | otherwise = overlaps i j === False + where k = beginerval (diff (begin j) (begin i)) (begin i) + l = beginerval (diff (end i) (begin j)) (begin j) + m = beginerval (diff (end j) (end i)) (end i) + + prop_IAduring:: Interval a -> Interval a-> Property + prop_IAduring i j + | during i j = (j == fromJust ( fromJust (k .+. i) .+. l)) === True + | otherwise = during i j === False + where k = beginerval (diff (begin i) (begin j)) (begin j) + l = beginerval (diff (end j) (end i)) (end i) + + prop_disjoint_predicate :: (Ord a) => + Interval a + -> Interval a + -> Property + prop_disjoint_predicate = prop_predicate_unions disjointRelations disjoint + + prop_notdisjoint_predicate :: (Ord a) => + Interval a + -> Interval a + -> Property + prop_notdisjoint_predicate = + prop_predicate_unions (complement disjointRelations) notDisjoint + + prop_concur_predicate :: (Ord a) => + Interval a + -> Interval a + -> Property + prop_concur_predicate = + prop_predicate_unions (complement disjointRelations) concur + + prop_within_predicate :: (Ord a) => + Interval a + -> Interval a + -> Property + prop_within_predicate = prop_predicate_unions withinRelations within + + prop_enclosedBy_predicate :: (Ord a) => + Interval a + -> Interval a + -> Property + prop_enclosedBy_predicate = prop_predicate_unions withinRelations enclosedBy + + prop_enclose_predicate :: (Ord a) => + Interval a + -> Interval a + -> Property + prop_enclose_predicate = prop_predicate_unions (converse withinRelations) enclose + +instance IntervalRelationProperties Int Int +instance IntervalRelationProperties Day Integer +instance IntervalRelationProperties UTCTime NominalDiffTime diff --git a/test-axioms/AxiomsSpec.hs b/test-axioms/AxiomsSpec.hs new file mode 100644 --- /dev/null +++ b/test-axioms/AxiomsSpec.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleContexts #-} +module AxiomsSpec (spec) where + +import Test.Hspec ( hspec, describe, it, Spec, ) +import Test.Hspec.QuickCheck ( modifyMaxSuccess ) +import Test.QuickCheck ( quickCheck + , generate + , Gen(..) + , Arbitrary(arbitrary) + , Property + , Testable(property) ) +import Data.Time ( Day, UTCTime ) +import IntervalAlgebra.Axioms ( IntervalAxioms(..) ) + + +spec :: Spec +spec = do + + describe "An Axiomatization of Interval Time" $ + modifyMaxSuccess (*1000) $ + do + it "M1" $ property (prop_IAaxiomM1 @Int) + it "M1" $ property (prop_IAaxiomM1 @Day) + it "M1" $ property (prop_IAaxiomM1 @UTCTime) + + it "M2" $ property (prop_IAaxiomM2 @Int) + it "M2" $ property (prop_IAaxiomM2 @Day) + it "M2" $ property (prop_IAaxiomM2 @UTCTime) + + it "ML1" $ property (prop_IAaxiomML1 @Int) + it "ML1" $ property (prop_IAaxiomML1 @Day) + it "ML1" $ property (prop_IAaxiomML1 @UTCTime) + + it "ML2" $ property (prop_IAaxiomML2 @Int) + it "ML2" $ property (prop_IAaxiomML2 @Day) + it "ML2" $ property (prop_IAaxiomML2 @UTCTime) + + it "M3" $ property (prop_IAaxiomM3 @Int) + it "M3" $ property (prop_IAaxiomM3 @Day) + it "M3" $ property (prop_IAaxiomM3 @UTCTime) + + it "M4" $ property (prop_IAaxiomM4 @Int) + it "M4" $ property (prop_IAaxiomM4 @Day) + it "M4" $ property (prop_IAaxiomM4 @UTCTime) + + it "M5" $ property (prop_IAaxiomM5 @Int) + it "M5" $ property (prop_IAaxiomM5 @Day) + it "M5" $ property (prop_IAaxiomM5 @UTCTime) + + it "M4.1" $ property (prop_IAaxiomM4_1 @Int) + it "M4.1" $ property (prop_IAaxiomM4_1 @Day) + it "M4.1" $ property (prop_IAaxiomM4_1 @UTCTime) + diff --git a/test-axioms/Main.hs b/test-axioms/Main.hs new file mode 100644 --- /dev/null +++ b/test-axioms/Main.hs @@ -0,0 +1,7 @@ +module Main where + +import Test.Hspec +import AxiomsSpec + +main :: IO () +main = hspec spec diff --git a/test-relation-properties/Main.hs b/test-relation-properties/Main.hs new file mode 100644 --- /dev/null +++ b/test-relation-properties/Main.hs @@ -0,0 +1,7 @@ +module Main where + +import Test.Hspec +import RelationPropertiesSpec + +main :: IO () +main = hspec spec diff --git a/test-relation-properties/RelationPropertiesSpec.hs b/test-relation-properties/RelationPropertiesSpec.hs new file mode 100644 --- /dev/null +++ b/test-relation-properties/RelationPropertiesSpec.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleContexts #-} +module RelationPropertiesSpec (spec) where + +import Test.Hspec ( hspec, describe, it, Spec, ) +import Test.Hspec.QuickCheck ( modifyMaxSuccess ) +import Test.QuickCheck +import Data.Time +import IntervalAlgebra.RelationProperties ( IntervalRelationProperties(..) ) + + + +spec :: Spec +spec = do + describe "Interval Algebra relation properties for Interval Int" $ + modifyMaxSuccess (*100) $ + do + it "before" $ property (prop_IAbefore @Int) + it "starts" $ property (prop_IAstarts @Int) + it "finishes" $ property (prop_IAfinishes @Int) + it "overlaps" $ property (prop_IAoverlaps @Int) + it "during" $ property (prop_IAduring @Int) + it "disjoint" $ property (prop_disjoint_predicate @Int) + it "within" $ property (prop_within_predicate @Int) + it "enclose" $ property (prop_enclose_predicate @Int) + it "enclosedBy" $ property (prop_enclosedBy_predicate @Int) + it "notDisjoint" $ property (prop_notdisjoint_predicate @Int) + it "concur" $ property (prop_concur_predicate @Int) + + describe "Interval Algebra relation properties for Interval Day" $ + modifyMaxSuccess (*100) $ + do + it "before" $ property (prop_IAbefore @Day) + it "starts" $ property (prop_IAstarts @Day) + it "finishes" $ property (prop_IAfinishes @Day) + it "overlaps" $ property (prop_IAoverlaps @Day) + it "during" $ property (prop_IAduring @Day) + it "disjoint" $ property (prop_disjoint_predicate @Day) + it "within" $ property (prop_within_predicate @Day) + it "enclose" $ property (prop_enclose_predicate @Day) + it "enclosedBy" $ property (prop_enclosedBy_predicate @Day) + it "notDisjoint" $ property (prop_notdisjoint_predicate @Day) + it "concur" $ property (prop_concur_predicate @Day) + + describe "Interval Algebra relation properties for Interval UTCTime" $ + modifyMaxSuccess (*100) $ + do + it "before" $ property (prop_IAbefore @UTCTime) + it "starts" $ property (prop_IAstarts @UTCTime) + it "finishes" $ property (prop_IAfinishes @UTCTime) + it "overlaps" $ property (prop_IAoverlaps @UTCTime) + it "during" $ property (prop_IAduring @UTCTime) + it "disjoint" $ property (prop_disjoint_predicate @UTCTime) + it "within" $ property (prop_within_predicate @UTCTime) + it "enclose" $ property (prop_enclose_predicate @UTCTime) + it "enclosedBy" $ property (prop_enclosedBy_predicate @UTCTime) + it "notDisjoint" $ property (prop_notdisjoint_predicate @UTCTime) + it "concur" $ property (prop_concur_predicate @UTCTime) + + describe "Interval Algebra relation uniqueness" $ + modifyMaxSuccess (*100) $ + do + it "exactly one relation must be true" $ + property (prop_exclusiveRelations @Int) + it "exactly one relation must be true" $ + property (prop_exclusiveRelations @Day) + it "exactly one relation must be true" $ + property (prop_exclusiveRelations @UTCTime) diff --git a/test/IntervalAlgebra/IntervalUtilitiesSpec.hs b/test/IntervalAlgebra/IntervalUtilitiesSpec.hs --- a/test/IntervalAlgebra/IntervalUtilitiesSpec.hs +++ b/test/IntervalAlgebra/IntervalUtilitiesSpec.hs @@ -8,9 +8,7 @@ import Test.Hspec ( Spec , it , shouldBe - , describe - , pending - , xcontext ) + , describe ) import Test.QuickCheck ( Property , Testable(property) , Arbitrary(arbitrary, shrink) @@ -71,6 +69,7 @@ import Control.Monad ( liftM2 ) import Data.Set ( Set, fromList, member ) import Witherable ( Filterable ) +import Data.Time ( Day, UTCTime ) -- Types for testing @@ -276,108 +275,112 @@ -> Set IntervalRelation -> Interval a -> [Interval a] - -> Property - prop_filtration fltr s x l = + -> Property + prop_filtration fltr s x l = not (null res) ==> and (fmap (predicate s x) res) === True where res = fltr x l prop_filterOverlaps :: Interval a -> [Interval a] - -> Property + -> Property prop_filterOverlaps = prop_filtration filterOverlaps (fromList [Overlaps]) prop_filterOverlappedBy :: Interval a -> [Interval a] - -> Property + -> Property prop_filterOverlappedBy = prop_filtration filterOverlappedBy (fromList [OverlappedBy]) prop_filterBefore :: Interval a -> [Interval a] - -> Property + -> Property prop_filterBefore = prop_filtration filterBefore (fromList [Before]) prop_filterAfter :: Interval a -> [Interval a] - -> Property + -> Property prop_filterAfter = prop_filtration filterAfter (fromList [After]) prop_filterStarts :: Interval a -> [Interval a] - -> Property + -> Property prop_filterStarts = prop_filtration filterStarts (fromList [Starts]) prop_filterStartedBy :: Interval a -> [Interval a] - -> Property + -> Property prop_filterStartedBy = prop_filtration filterStartedBy (fromList [StartedBy]) prop_filterFinishes :: Interval a -> [Interval a] - -> Property + -> Property prop_filterFinishes = prop_filtration filterFinishes (fromList [Finishes]) prop_filterFinishedBy :: Interval a -> [Interval a] - -> Property + -> Property prop_filterFinishedBy = prop_filtration filterFinishedBy (fromList [FinishedBy]) prop_filterMeets :: Interval a -> [Interval a] - -> Property + -> Property prop_filterMeets = prop_filtration filterMeets (fromList [Meets]) prop_filterMetBy :: Interval a -> [Interval a] - -> Property + -> Property prop_filterMetBy = prop_filtration filterMetBy (fromList [MetBy]) prop_filterDuring :: Interval a -> [Interval a] - -> Property + -> Property prop_filterDuring = prop_filtration filterDuring (fromList [During]) prop_filterContains :: Interval a -> [Interval a] - -> Property + -> Property prop_filterContains = prop_filtration filterContains (fromList [Contains]) prop_filterEquals :: Interval a -> [Interval a] - -> Property + -> Property prop_filterEquals = prop_filtration filterEquals (fromList [Equals]) prop_filterDisjoint :: Interval a -> [Interval a] - -> Property + -> Property prop_filterDisjoint = prop_filtration filterDisjoint disjointRelations prop_filterNotDisjoint :: Interval a -> [Interval a] - -> Property + -> Property prop_filterNotDisjoint = prop_filtration filterNotDisjoint (complement disjointRelations) prop_filterWithin :: Interval a -> [Interval a] - -> Property + -> Property prop_filterWithin = prop_filtration filterWithin withinRelations prop_filterEnclosedBy :: Interval a -> [Interval a] - -> Property + -> Property prop_filterEnclosedBy = prop_filtration filterEnclosedBy withinRelations prop_filterEnclose :: Interval a -> [Interval a] - -> Property + -> Property prop_filterEnclose = prop_filtration filterEnclose (converse withinRelations) prop_filterConcur :: Interval a -> [Interval a] - -> Property + -> Property prop_filterConcur = prop_filtration filterConcur (complement disjointRelations) instance FiltrationProperties Int +prop_clip_intersect :: (Show a, Ord a, IntervalSizeable a b) => + Interval a -> Interval a -> Property +prop_clip_intersect x y = + clip x y === intersect (min x y) (max x y) spec :: Spec spec = do @@ -409,7 +412,8 @@ it "clip Interval (4, 10) Interval (0, 10) should be Interval (4, 10)" $ clip noncontainmentInt containmentInt `shouldBe` Just (iv 6 4) - it "clip x y === intersect sort x y " pending + it "clip x y === intersect sort x y " $ + property (prop_clip_intersect @Int) describe "relationsL tests" $ do @@ -420,7 +424,8 @@ relationsL ([] :: [Interval Int]) `shouldBe` [] it "relationsL of singleton shouldBe []" $ relationsL [containmentInt] `shouldBe` [] - it "more relationsL tests" pending + it "length of relationsL result should be 1 less then length of input" $ + property (\x -> not (null x) ==> length (relationsL x) === length (x :: [Interval Int]) - 1 ) describe "gapsWithin tests" $ do @@ -430,13 +435,12 @@ it "gapsWithin (1, 10) [(-1, 0), (12,15)] should be [(5,7), (9,10)]" $ gapsWithin (iv 9 1) [iv 1 (-1), iv 3 12] `shouldBe` Nothing - it "gapsWithin (0, 455) [(0, 730), (731, 762), (763, 793)]" $ - gapsWithin (readInterval (0 :: Int, 455)) + it "gapsWithin (0, 455) [(0, 730), (731, 762), (763, 793)]" $ + gapsWithin (readInterval (0 :: Int, 455)) (fmap readInterval [(0, 730), (731, 762), (763, 793)]) `shouldBe` Just [] it "gapsWithin (1, 10) [] should be []" $ gapsWithin (iv 9 1) ([] :: [Interval a]) `shouldBe` Nothing - it "more gapsWithin tests" pending describe "emptyIf tests" $ do @@ -446,7 +450,6 @@ it "emptyIfNone (starts (3, 5)) [(3,6), (5,6)] shoiuld be input" $ nothingIfNone (starts (iv 2 3)) [iv 3 3, iv 1 5] `shouldBe` Just [ iv 3 3, iv 1 5] - it "more emptyif tests" pending describe "filtration tests" $ modifyMaxDiscardRatio (*2) $ @@ -478,16 +481,16 @@ it "filterEnclosedBy property" $ property (prop_filterEnclosedBy @Int) describe "nothingIf unit tests" $ - do - it "nothing from nothingIfAll" $ + do + it "nothing from nothingIfAll" $ nothingIfAll (starts (iv 2 3)) [iv 3 3, iv 4 3] `shouldBe` Nothing it "something from nothingIfAll" $ - nothingIfAll (starts (iv 2 3)) [iv 3 0, iv 4 3] `shouldBe` Just [iv 3 0, iv 4 3] - it "nothing from nothingIfAny" $ + nothingIfAll (starts (iv 2 3)) [iv 3 0, iv 4 3] `shouldBe` Just [iv 3 0, iv 4 3] + it "nothing from nothingIfAny" $ nothingIfAny (starts (iv 2 3)) [iv 3 3, iv 1 5] `shouldBe` Nothing it "something from nothingIfAny" $ nothingIfAny (starts (iv 2 3)) [iv 3 1, iv 1 5] `shouldBe` Just [iv 3 1, iv 1 5] - + describe "intersection tests" $ do it "intersection of (0, 2) (2, 4) should be Nothing" $ @@ -495,7 +498,7 @@ it "intersection of (0, 2) (3, 4) should be Nothing" $ intersect (iv 2 0) (iv 1 3) `shouldBe` Nothing it "intersection of (2, 4) (0, 2) should be Nothing" $ - intersect (iv 2 2) (iv 2 0) `shouldBe` Nothing + intersect (iv 2 2) (iv 2 0) `shouldBe` Nothing describe "intersection tests" $ do @@ -539,6 +542,10 @@ do it "after combining, only relation should be Before" $ property ( prop_combineIntervals1 @Int) + it "after combining, only relation should be Before" $ + property ( prop_combineIntervals1 @Day) + it "after combining, only relation should be Before" $ + property ( prop_combineIntervals1 @UTCTime) describe "foldMeets unit tests" $ do diff --git a/test/IntervalAlgebraSpec.hs b/test/IntervalAlgebraSpec.hs --- a/test/IntervalAlgebraSpec.hs +++ b/test/IntervalAlgebraSpec.hs @@ -1,506 +1,40 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleContexts #-} module IntervalAlgebraSpec (spec) where -import Test.Hspec ( hspec, describe, it, Spec, shouldBe, pending ) +import Test.Hspec ( hspec, describe, it, Spec, shouldBe ) import Test.Hspec.QuickCheck ( modifyMaxSuccess, modifyMaxDiscardRatio ) import Test.QuickCheck ( (===) , (==>) + , quickCheck + , generate + , Gen(..) , Arbitrary(arbitrary) , Property - , Testable(property) ) -import Data.Maybe ( fromJust ) + , Testable(property) ) +import GHC.Real ( Rational(..), Real(..) ) +import Data.Maybe ( fromJust, isJust, isNothing ) import Data.Either ( isRight ) +import Data.Fixed ( Pico ) import IntervalAlgebra.Arbitrary () import Data.Time as DT ( Day(..) + , UTCTime(..) + , DiffTime , fromGregorian + , secondsToDiffTime + , picosecondsToDiffTime, NominalDiffTime ) import Data.Set ( Set , member , disjointUnion , fromList ) -import IntervalAlgebra as IA ( enderval - , beginerval - , expandr - , expandl - , expand - , parseInterval - , before - , meets - , overlaps - , finishedBy - , contains - , starts - , precedes - , precededBy - , equals - , startedBy - , during - , finishes - , overlappedBy - , metBy - , after - , relate - , compose - , disjoint - , within - , concur - , notDisjoint - , enclose - , enclosedBy - , (<|>) - , begin - , end - , disjointRelations - , withinRelations - , converse - , union - , intersection - , complement - , diffFromBegin - , diffFromEnd - , IntervalCombinable((.+.)) - , IntervalSizeable(moment, moment', diff) - , ComparativePredicateOf1 - , ComparativePredicateOf2 - , Intervallic - , Interval - , IntervalRelation (..) - , intervalRelations - , notDisjoint - , momentize ) +import IntervalAlgebra as IA mkIntrvl :: Int -> Int -> Interval Int mkIntrvl = beginerval -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) - --- TODO: remove duplication like this: -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 - --- | 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 i,j,k,l s.t. (i:j & i:k & 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 - -prop_IAaxiomM1_Int :: M1set Int -> Property -prop_IAaxiomM1_Int = prop_IAaxiomM1 - -prop_IAaxiomM1_Day :: M1set DT.Day -> Property -prop_IAaxiomM1_Day = prop_IAaxiomM1 - --- | 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 - --- | 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 & 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) - -prop_IAaxiomM2_Int :: M2set Int -> Property -prop_IAaxiomM2_Int = prop_IAaxiomM2 - -prop_IAaxiomM2_Day :: M2set DT.Day -> Property -prop_IAaxiomM2_Day = prop_IAaxiomM2 - -{- - - ** 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 - -prop_IAaxiomML1_Int :: Interval Int -> Property -prop_IAaxiomML1_Int = prop_IAaxiomML1 - -prop_IAaxiomML1_Day :: Interval DT.Day -> Property -prop_IAaxiomML1_Day = prop_IAaxiomML1 - -{- - -** 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 - -prop_IAaxiomML2_Int :: M2set Int -> Property -prop_IAaxiomML2_Int = prop_IAaxiomML2 - -prop_IAaxiomML2_Day :: M2set DT.Day -> Property -prop_IAaxiomML2_Day = prop_IAaxiomML2 - -{- - -** 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) - -prop_IAaxiomM3_Int :: Interval Int -> Property -prop_IAaxiomM3_Int = prop_IAaxiomM3 1 - -prop_IAaxiomM3_Day :: Interval Day -> Property -prop_IAaxiomM3_Day = prop_IAaxiomM3 1 - -{- - -** 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 & 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) - -prop_IAaxiomM4_Int :: M2set Int -> Property -prop_IAaxiomM4_Int = prop_IAaxiomM4 1 - -prop_IAaxiomM4_Day :: M2set DT.Day -> Property -prop_IAaxiomM4_Day = prop_IAaxiomM4 1 - -{- - -** Axiom M5 - -If two meets are separated by intervals, then this sequence is a longer interval. - -\[ - \forall i,j,k,l (i:j:l & i:k:l) \seteq j = k -\] --} - --- | 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 - --- | 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 - - -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 - -prop_IAaxiomM5_Int :: M5set Int -> Property -prop_IAaxiomM5_Int = prop_IAaxiomM5 - -prop_IAaxiomM5_Day :: M5set DT.Day -> Property -prop_IAaxiomM5_Day = prop_IAaxiomM5 - -{- - -** Axiom M4.1 - -Ordered unions: - -\[ - \forall i,j i:j \implies (\exists m,n s.t. m:i:j:n & 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 - -prop_IAaxiomM4_1_Int :: M2set Int -> Property -prop_IAaxiomM4_1_Int = prop_IAaxiomM4_1 1 - -prop_IAaxiomM4_1_Day :: M2set DT.Day -> Property -prop_IAaxiomM4_1_Day = prop_IAaxiomM4_1 1 - -{- -* Interval Relation property testing --} - -class ( IntervalSizeable a b ) => IntervalRelationProperties a b where - - prop_IAbefore :: Interval a -> Interval a -> Property - prop_IAbefore i j = - IA.before i j ==> (i `meets` k) && (k `meets` j) - where k = beginerval (diff (begin j) (end i)) (end i) - - prop_IAstarts:: Interval a -> Interval a -> Property - prop_IAstarts i j - | IA.starts i j = (j == fromJust (i .+. k)) === True - | otherwise = IA.starts i j === False - where k = beginerval (diff (end j) (end i)) (end i) - - prop_IAfinishes:: Interval a -> Interval a -> Property - prop_IAfinishes i j - | IA.finishes i j = (j == fromJust ( k .+. i)) === True - | otherwise = IA.finishes i j === False - where k = beginerval (diff (begin i) (begin j)) (begin j) - - prop_IAoverlaps:: Interval a -> Interval a -> Property - prop_IAoverlaps i j - | IA.overlaps i j = ((i == fromJust ( k .+. l )) && - (j == fromJust ( l .+. m ))) === True - | otherwise = IA.overlaps i j === False - where k = beginerval (diff (begin j) (begin i)) (begin i) - l = beginerval (diff (end i) (begin j)) (begin j) - m = beginerval (diff (end j) (end i)) (end i) - - prop_IAduring:: Interval a -> Interval a-> Property - prop_IAduring i j - | IA.during i j = (j == fromJust ( fromJust (k .+. i) .+. l)) === True - | otherwise = IA.during i j === False - where k = beginerval (diff (begin i) (begin j)) (begin j) - l = beginerval (diff (end j) (end i)) (end i) - - -- | For any two pair of intervals exactly one 'IntervalRelation' should hold - prop_exclusiveRelations:: Interval a -> Interval a -> Property - prop_exclusiveRelations x y = - ( 1 == length (filter id $ map (\r -> r x y) allIArelations)) === 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 s pred i0 i1 = - pred i0 i1 === (relate i0 i1 `elem` s) - - prop_disjoint_predicate :: (Ord a) => - Interval a - -> Interval a - -> Property - prop_disjoint_predicate = prop_predicate_unions disjointRelations disjoint - - prop_notdisjoint_predicate :: (Ord a) => - Interval a - -> Interval a - -> Property - prop_notdisjoint_predicate = - prop_predicate_unions (complement disjointRelations) notDisjoint - - prop_concur_predicate :: (Ord a) => - Interval a - -> Interval a - -> Property - prop_concur_predicate = - prop_predicate_unions (complement disjointRelations) concur - - prop_within_predicate :: (Ord a) => - Interval a - -> Interval a - -> Property - prop_within_predicate = prop_predicate_unions withinRelations within - - prop_enclosedBy_predicate :: (Ord a) => - Interval a - -> Interval a - -> Property - prop_enclosedBy_predicate = prop_predicate_unions withinRelations enclosedBy - - prop_enclose_predicate :: (Ord a) => - Interval a - -> Interval a - -> Property - prop_enclose_predicate = prop_predicate_unions (converse withinRelations) enclose - -instance IntervalRelationProperties Int Int -instance IntervalRelationProperties Day Integer - -allIArelations:: (Ord a) => [ComparativePredicateOf1 (Interval a)] -allIArelations = [ IA.equals - , IA.meets - , IA.metBy - , IA.before - , IA.after - , IA.starts - , IA.startedBy - , IA.finishes - , IA.finishedBy - , IA.overlaps - , IA.overlappedBy - , IA.during - , IA.contains ] - prop_expandl_end ::(IntervalSizeable a b, Show a)=> b -> Interval a @@ -523,7 +57,26 @@ -> Property prop_compose x y z = member (relate x z) (compose (relate x y) (relate y z)) === True +-- | If two intervals are disjoint and not meeting, then there should be a gap +-- between the two (by ><), after the intervals are sorted. +prop_combinable_gap_exists :: Ord a => + Interval a + -> Interval a + -> Property +prop_combinable_gap_exists x y = + (before <|> after) x y ==> isJust (uncurry (><) (min x y, max x y)) +-- | If two intervals are not disjoint or meeting, then there should be NO gap +-- between the two (by ><), after the intervals are sorted. +prop_combinable_nogap_exists :: Ord a => + Interval a + -> Interval a + -> Property +prop_combinable_nogap_exists x y = + (predicate $ complement $ fromList [Before, After]) x y ==> + isNothing (uncurry (><) (min x y, max x y)) + + spec :: Spec spec = do describe "Basic Interval unit tests of typeclass and creation methods" $ @@ -534,7 +87,7 @@ it "not equality works" $ enderval 5 (2::Int) /= beginerval 1 1 `shouldBe` True it "parsing fails on bad inputs" $ - parseInterval 10 0 `shouldBe` Left "0<10" + parseInterval 10 0 `shouldBe` Left (IA.ParseErrorInterval "0<10") it "parsing works on good inputs" $ parseInterval 0 10 `shouldBe` Right (beginerval 10 (0::Int)) @@ -666,7 +219,7 @@ describe "Intervallic tests" $ - modifyMaxSuccess (*10000) $ + -- modifyMaxSuccess (*10000) $ do it "(startedBy <|> overlappedBy) Interval (0, 9) Interval (-1, 4) is True" $ (startedBy <|> overlappedBy) (mkIntrvl 9 0) (mkIntrvl 5 (-1)) @@ -691,61 +244,19 @@ it "join non-meeting intervals is Nothing" $ beginerval 2 (0::Int) .+. beginerval 6 5 `shouldBe` Nothing it "join meeting intervals is Just _" $ - beginerval 2 (0::Int) .+. beginerval 6 2 `shouldBe` Just (beginerval 8 0) - it "" pending - - describe "Interval Algebra Axioms for meets properties" $ - modifyMaxSuccess (*10) $ - do - it "M1 Int" $ property prop_IAaxiomM1_Int - it "M1 Day" $ property prop_IAaxiomM1_Day - it "M2_Int" $ property prop_IAaxiomM2_Int - it "M2_Day" $ property prop_IAaxiomM2_Day - it "ML1_Int" $ property prop_IAaxiomML1_Int - it "ML1_Day" $ property prop_IAaxiomML1_Day - it "ML2_Int" $ property prop_IAaxiomML2_Int - it "ML2_Day" $ property prop_IAaxiomML2_Day - {- - 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. - -} - --it "ML3" $ property prop_IAaxiomML3 - it "M3_Int" $ property prop_IAaxiomM3_Int - it "M3_Day" $ property prop_IAaxiomM3_Day - it "M4_Int" $ property prop_IAaxiomM4_Int - it "M4_Day" $ property prop_IAaxiomM4_Day - it "M5_Int" $ property prop_IAaxiomM5_Int - it "M5_Day" $ property prop_IAaxiomM5_Day - it "M4.1_Int" $ property prop_IAaxiomM4_1_Int - it "M4.1_Day" $ property prop_IAaxiomM4_1_Day + beginerval 2 (0::Int) .+. beginerval 6 2 `shouldBe` Just (beginerval 8 0) - describe "Interval Algebra relation properties" $ - modifyMaxSuccess (*10) $ - do - it "before" $ property (prop_IAbefore @Int) - it "starts" $ property (prop_IAstarts @Int) - it "finishes" $ property (prop_IAfinishes @Int) - it "overlaps" $ property (prop_IAoverlaps @Int) - it "during" $ property (prop_IAduring @Int) - it "before" $ property (prop_IAbefore @Day) - it "starts" $ property (prop_IAstarts @Day) - it "finishes" $ property (prop_IAfinishes @Day) - it "overlaps" $ property (prop_IAoverlaps @Day) - it "during" $ property (prop_IAduring @Day) + it "gap of disjoint intervals should be something" $ + property (prop_combinable_gap_exists @Int) + it "gap of disjoint intervals should be something" $ + property (prop_combinable_gap_exists @Day) + it "gap of disjoint intervals should be something" $ + property (prop_combinable_gap_exists @UTCTime) - it "disjoint" $ property (prop_disjoint_predicate @Int) - it "disjoint" $ property (prop_disjoint_predicate @Day) - it "within" $ property (prop_within_predicate @Int) - it "within" $ property (prop_within_predicate @Day) - it "enclose" $ property (prop_enclose_predicate @Int) - it "enclose" $ property (prop_enclose_predicate @Day) - it "enclosedBy" $ property (prop_enclosedBy_predicate @Int) - it "enclosedBy" $ property (prop_enclosedBy_predicate @Day) - it "notDisjoint" $ property (prop_notdisjoint_predicate @Int) - it "notDisjoint" $ property (prop_notdisjoint_predicate @Day) - it "concur" $ property (prop_concur_predicate @Int) - it "concur" $ property (prop_concur_predicate @Day) + it "gap of nondisjoint, nonmeeting intervals should be nothing" $ + property (prop_combinable_nogap_exists @Int) + it "gap of nondisjoint, nonmeeting intervals should be nothing" $ + property (prop_combinable_nogap_exists @Day) describe "Interval Algebra relation unit tests for synonyms" $ do @@ -766,11 +277,3 @@ concur (beginerval 1 0) (beginerval 10 (0::Int)) `shouldBe` notDisjoint (beginerval 1 0) (beginerval 10 (0::Int)) - - describe "Interval Algebra relation uniqueness" $ - modifyMaxSuccess (*100) $ - do - it "exactly one relation must be true" $ - property (prop_exclusiveRelations @Int) - it "exactly one relation must be true" $ - property (prop_exclusiveRelations @Day)