packages feed

data-interval (empty) → 0.1.0

raw patch · 7 files changed

+1063/−0 lines, 7 filesdep +HUnitdep +QuickCheckdep +basesetup-changed

Dependencies added: HUnit, QuickCheck, base, containers, data-interval, lattices, test-framework, test-framework-hunit, test-framework-quickcheck2, test-framework-th

Files

+ .travis.yml view
@@ -0,0 +1,1 @@+language: haskell
+ COPYING view
@@ -0,0 +1,27 @@+Copyright 2010-2013 Masahiro Sakai. All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++   1. Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.+   2. Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.+   3. The name of the author may not be used to endorse or promote+      products derived from this software without specific prior+      written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,+INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING+IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,4 @@+data-interval+=============++Interval datatype and interval arithmetic for Haskell
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell
+
+> import Distribution.Simple
+> main = defaultMain
+ data-interval.cabal view
@@ -0,0 +1,43 @@+Name:		data-interval+Version:	0.1.0+License:	BSD3+License-File:	COPYING+Author:		Masahiro Sakai (masahiro.sakai@gmail.com)+Maintainer:	masahiro.sakai@gmail.com+Category:	Data+Cabal-Version:	>= 1.8+Synopsis:	Interval Arithmetic+Description:+   Unlike the intervals package (<http://hackage.haskell.org/package/intervals>),+   this module provides both open and closed intervals and is intended to be used+   with @Rational@.+Bug-Reports:	https://github.com/msakai/data-interval/issues+Extra-Source-Files:+   README.md+   COPYING+   .travis.yml+Build-Type: Simple++source-repository head+  type:     git+  location: git://github.com/msakai/data-interval.git++Library+  Exposed: False+  Hs-source-dirs: src+  Build-Depends:+     base >=4 && <5, lattices >=1.2.1.1+  Extensions:+     ScopedTypeVariables+     FlexibleInstances+     MultiParamTypeClasses+     DeriveDataTypeable+  Exposed-Modules:+     Data.Interval++Test-suite TestInterval+  Type:              exitcode-stdio-1.0+  HS-Source-Dirs:    test+  Main-is:           TestInterval.hs+  Build-depends:     base >=4 && <5, containers, data-interval, test-framework, test-framework-th, test-framework-hunit, test-framework-quickcheck2, HUnit, QuickCheck >=2 && <3+  Extensions: TemplateHaskell, DoAndIfThenElse
+ src/Data/Interval.hs view
@@ -0,0 +1,504 @@+{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses, DeriveDataTypeable #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Interval+-- Copyright   :  (c) Masahiro Sakai 2011-2013+-- License     :  BSD-style+-- +-- Maintainer  :  masahiro.sakai@gmail.com+-- Stability   :  provisional+-- Portability :  non-portable (ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses, DeriveDataTypeable)+--+-- Interval datatype and interval arithmetic.+--+-- Unlike the intervals package (<http://hackage.haskell.org/package/intervals>),+-- this module provides both open and closed intervals and is intended to be used+-- with @Rational@.+-- +-----------------------------------------------------------------------------+module Data.Interval+  (+  -- * Interval type+    Interval+  , EndPoint (..)++  -- * Construction+  , interval+  , (<=..<=)+  , (<..<=)+  , (<=..<)+  , (<..<)+  , whole+  , empty+  , singleton++  -- * Query+  , null+  , member+  , notMember+  , isSubsetOf+  , isProperSubsetOf+  , lowerBound+  , upperBound+  , lowerBound'+  , upperBound'+  , width++  -- * Comparison+  , (<!), (<=!), (==!), (>=!), (>!)+  , (<?), (<=?), (==?), (>=?), (>?)++  -- * Combine+  , intersection+  , hull++  -- * Operations+  , pickup+  ) where++import Algebra.Lattice+import Control.Exception (assert)+import Control.Monad hiding (join)+import Data.List hiding (null)+import Data.Maybe+import Data.Monoid+import Data.Typeable+import Prelude hiding (null)++-- | Interval+data Interval r = Interval !(EndPoint r, Bool) !(EndPoint r, Bool)+  deriving (Eq, Typeable)  ++-- | Lower bound of the interval+lowerBound :: Num r => Interval r -> EndPoint r+lowerBound (Interval (lb,_) _) = lb++-- | Upper bound of the interval+upperBound :: Num r => Interval r -> EndPoint r+upperBound (Interval _ (ub,_)) = ub++-- | Lower bound of the interval and whether it is included in the interval+lowerBound' :: Num r => Interval r -> (EndPoint r, Bool)+lowerBound' (Interval lb _) = lb++-- | Upper bound of the interval and whether it is included in the interval+upperBound' :: Num r => Interval r -> (EndPoint r, Bool)+upperBound' (Interval _ ub) = ub++instance (Num r, Ord r) => JoinSemiLattice (Interval r) where+  join = hull++instance (Num r, Ord r) => MeetSemiLattice (Interval r) where+  meet = hull++instance (Num r, Ord r) => Lattice (Interval r)++instance (Num r, Ord r) => BoundedJoinSemiLattice (Interval r) where+  bottom = empty++instance (Num r, Ord r) => BoundedMeetSemiLattice (Interval r) where+  top = whole++instance (Num r, Ord r) => BoundedLattice (Interval r)++instance (Num r, Ord r, Show r) => Show (Interval r) where+  showsPrec p x | null x = showString "empty"+  showsPrec p x = showParen (p > appPrec) $+    showString "interval " .+    showsPrec appPrec1 (lowerBound' x) .+    showChar ' ' . +    showsPrec appPrec1 (upperBound' x)++instance (Num r, Ord r, Read r) => Read (Interval r) where+  readsPrec p r =+    (readParen (p > appPrec) $ \s0 -> do+      ("interval",s1) <- lex s0+      (lb,s2) <- readsPrec (appPrec+1) s1+      (ub,s3) <- readsPrec (appPrec+1) s2+      return (interval lb ub, s3)) r+    +++    (do ("empty", s) <- lex r+        return (empty, s))++-- | smart constructor for 'Interval'+interval+  :: (Ord r, Num r)+  => (EndPoint r, Bool) -- ^ lower bound and whether it is included +  -> (EndPoint r, Bool) -- ^ upper bound and whether it is included+  -> Interval r+interval lb@(x1,in1) ub@(x2,in2) =+  case x1 `compare` x2 of+    GT -> empty --  empty interval+    LT -> Interval (normalize lb) (normalize ub)+    EQ -> if in1 && in2 && isFinite x1 then Interval lb ub else empty+  where+    normalize x@(Finite _, _) = x+    normalize (x, _) = (x, False)++-- | closed interval [@l@,@u@]+(<=..<=)+  :: (Ord r, Num r)+  => EndPoint r -- ^ lower bound @l@+  -> EndPoint r -- ^ upper bound @u@+  -> Interval r+(<=..<=) lb ub = interval (lb, True) (ub, True)++-- | left-open right-closed interval (@l@,@u@]+(<..<=)+  :: (Ord r, Num r)+  => EndPoint r -- ^ lower bound @l@+  -> EndPoint r -- ^ upper bound @u@+  -> Interval r+(<..<=) lb ub = interval (lb, False) (ub, True)++-- | left-closed right-open interval [@l@, @u@)+(<=..<)+  :: (Ord r, Num r)+  => EndPoint r -- ^ lower bound @l@+  -> EndPoint r -- ^ upper bound @u@+  -> Interval r+(<=..<) lb ub = interval (lb, True) (ub, False)++-- | open interval (@l@, @u@)+(<..<)+  :: (Ord r, Num r)+  => EndPoint r -- ^ lower bound @l@+  -> EndPoint r -- ^ upper bound @u@+  -> Interval r+(<..<) lb ub = interval (lb, False) (ub, False)++-- | whole real number line (-∞, ∞)+whole :: (Num r, Ord r) => Interval r+whole = Interval (NegInf, False) (PosInf, False)++-- | empty (contradicting) interval+empty :: Num r => Interval r+empty = Interval (PosInf, False) (NegInf, False)++-- | singleton set \[x,x\]+singleton :: (Num r, Ord r) => r -> Interval r+singleton x = interval (Finite x, True) (Finite x, True)++-- | intersection (greatest lower bounds) of two intervals+intersection :: forall r. (Ord r, Num r) => Interval r -> Interval r -> Interval r+intersection (Interval l1 u1) (Interval l2 u2) = interval (maxLB l1 l2) (minUB u1 u2)+  where+    maxLB :: (EndPoint r, Bool) -> (EndPoint r, Bool) -> (EndPoint r, Bool)+    maxLB (x1,in1) (x2,in2) =+      ( max x1 x2+      , case x1 `compare` x2 of+          EQ -> in1 && in2+          LT -> in2+          GT -> in1+      )+    minUB :: (EndPoint r, Bool) -> (EndPoint r, Bool) -> (EndPoint r, Bool)+    minUB (x1,in1) (x2,in2) =+      ( min x1 x2+      , case x1 `compare` x2 of+          EQ -> in1 && in2+          LT -> in1+          GT -> in2+      )++-- | convex hull of two intervals+hull :: forall r. (Ord r, Num r) => Interval r -> Interval r -> Interval r+hull x1 x2+  | null x1 = x2+  | null x2 = x1+hull (Interval l1 u1) (Interval l2 u2) = interval (minLB l1 l2) (maxUB u1 u2)+  where+    maxUB :: (EndPoint r, Bool) -> (EndPoint r, Bool) -> (EndPoint r, Bool)+    maxUB (x1,in1) (x2,in2) =+      ( max x1 x2+      , case x1 `compare` x2 of+          EQ -> in1 || in2+          LT -> in2+          GT -> in1+      )+    minLB :: (EndPoint r, Bool) -> (EndPoint r, Bool) -> (EndPoint r, Bool)+    minLB (x1,in1) (x2,in2) =+      ( min x1 x2+      , case x1 `compare` x2 of+          EQ -> in1 || in2+          LT -> in1+          GT -> in2+      )++-- | Is the interval empty?+null :: Ord r => Interval r -> Bool+null (Interval (x1,in1) (x2,in2)) = +  case x1 `compare` x2 of+    EQ -> assert (in1 && in2) False+    LT -> False+    GT -> True++-- | Is the element in the interval?+member :: Ord r => r -> Interval r -> Bool+member x (Interval (x1,in1) (x2,in2)) = condLB && condUB+  where+    condLB = if in1 then x1 <= Finite x else x1 < Finite x+    condUB = if in2 then Finite x <= x2 else Finite x < x2++-- | Is the element not in the interval?+notMember :: Ord r => r -> Interval r -> Bool+notMember a i = not $ member a i++-- | Is this a subset?+-- @(i1 `isSubsetOf` i2)@ tells whether @i1@ is a subset of @i2@.+isSubsetOf :: Ord r => Interval r -> Interval r -> Bool+isSubsetOf (Interval lb1 ub1) (Interval lb2 ub2) = testLB lb1 lb2 && testUB ub1 ub2+  where+    testLB (x1,in1) (x2,in2) =+      case x1 `compare` x2 of+        GT -> True+        LT -> False+        EQ -> not in1 || in2 -- in1 => in2+    testUB (x1,in1) (x2,in2) =+      case x1 `compare` x2 of+        LT -> True+        GT -> False+        EQ -> not in1 || in2 -- in1 => in2++-- | Is this a proper subset? (ie. a subset but not equal).+isProperSubsetOf :: Ord r => Interval r -> Interval r -> Bool+isProperSubsetOf i1 i2 = i1 /= i2 && i1 `isSubsetOf` i2++-- | Width of a interval. Width of an unbounded interval is @undefined@.+width :: (Num r, Ord r) => Interval r -> r+width x | null x = 0+width (Interval (Finite l, _) (Finite u, _)) = u - l+width _ = error "Data.Interval.width: unbounded interval"++-- | pick up an element from the interval if the interval is not empty.+pickup :: (Real r, Fractional r) => Interval r -> Maybe r+pickup (Interval (NegInf,in1) (PosInf,in2))   = Just 0+pickup (Interval (Finite x1, in1) (PosInf,_)) = Just $ if in1 then x1 else x1+1+pickup (Interval (NegInf,_) (Finite x2, in2)) = Just $ if in2 then x2 else x2-1+pickup (Interval (Finite x1, in1) (Finite x2, in2)) =+  case x1 `compare` x2 of+    GT -> Nothing+    LT -> Just $ (x1+x2) / 2+    EQ -> if in1 && in2 then Just x1 else Nothing+pickup x = Nothing++-- | For all @x@ in @X@, @y@ in @Y@. @x '<' y@+(<!) :: Real r => Interval r -> Interval r -> Bool+a <! b =+  case ub_a `compare` lb_b of+    LT -> True+    GT -> False+    EQ ->+      case ub_a of+        NegInf   -> True -- a is empty, so it holds vacuously+        PosInf   -> True -- b is empty, so it holds vacuously+        Finite x -> not (in1 && in2)+  where+    (ub_a, in1) = upperBound' a+    (lb_b, in2) = lowerBound' b++-- | For all @x@ in @X@, @y@ in @Y@. @x '<=' y@+(<=!) :: Real r => Interval r -> Interval r -> Bool+a <=! b = upperBound a <= lowerBound b++-- | For all @x@ in @X@, @y@ in @Y@. @x '==' y@+(==!) :: Real r => Interval r -> Interval r -> Bool+a ==! b = a <=! b && a >=! b++-- | For all @x@ in @X@, @y@ in @Y@. @x '>=' y@+(>=!) :: Real r => Interval r -> Interval r -> Bool+(>=!) = flip (<=!)++-- | For all @x@ in @X@, @y@ in @Y@. @x '>' y@+(>!) :: Real r => Interval r -> Interval r -> Bool+(>!) = flip (<!)++-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '<' y@?+(<?) :: Real r => Interval r -> Interval r -> Bool+a <? b = lb_a < ub_b+  where+    lb_a = lowerBound a+    ub_b = upperBound b++-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '<=' y@?+(<=?) :: Real r => Interval r -> Interval r -> Bool+a <=? b　=+  case lb_a `compare` ub_b of+    LT -> True+    GT -> False+    EQ -> +      case lb_a of+        NegInf -> False -- b is empty+        PosInf -> True  -- a is empty+        Finite x -> in1 && in2+  where+    (lb_a, in1) = lowerBound' a+    (ub_b, in2) = upperBound' b++-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '==' y@?+(==?) :: Real r => Interval r -> Interval r -> Bool+a ==? b = not $ null $ intersection a b++-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '>=' y@?+(>=?) :: Real r => Interval r -> Interval r -> Bool+(>=?) = flip (<=?)++-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '>' y@?+(>?) :: Real r => Interval r -> Interval r -> Bool+(>?) = flip (<?)++appPrec, appPrec1 :: Int+appPrec = 10+appPrec1 = appPrec + 1++scaleInterval :: (Num r, Ord r) => r -> Interval r -> Interval r+scaleInterval _ x | null x = empty+scaleInterval c (Interval lb ub) =+  case compare c 0 of+    EQ -> singleton 0+    LT -> interval (scaleInf' c ub) (scaleInf' c lb)+    GT -> interval (scaleInf' c lb) (scaleInf' c ub)++instance (Num r, Ord r) => Num (Interval r) where+  a + b | null a || null b = empty+  Interval lb1 ub1 + Interval lb2 ub2 = interval (f lb1 lb2) (g ub1 ub2)+    where+      f (Finite x1, in1) (Finite x2, in2) = (Finite (x1+x2), in1 && in2)+      f (NegInf,_) _ = (NegInf, False)+      f _ (NegInf,_) = (NegInf, False)+      f _ _ = error "Interval.(+) should not happen"++      g (Finite x1, in1) (Finite x2, in2) = (Finite (x1+x2), in1 && in2)+      g (PosInf,_) _ = (PosInf, False)+      g _ (PosInf,_) = (PosInf, False)+      g _ _ = error "Interval.(+) should not happen"++  negate a = scaleInterval (-1) a++  fromInteger i = singleton (fromInteger i)++  abs x = ((x `intersection` nonneg) `hull` (negate x `intersection` nonneg))+    where+      nonneg = Finite 0 <=..< PosInf++  signum x = zero `hull` pos `hull` neg+    where+      zero = if member 0 x then singleton 0 else empty+      pos = if null $ (Finite 0 <..< PosInf) `intersection` x+            then empty+            else singleton 1+      neg = if null $ (NegInf <..< Finite 0) `intersection` x+            then empty+            else singleton (-1)++  a * b | null a || null b = empty+  Interval lb1 ub1 * Interval lb2 ub2 = interval lb3 ub3+    where+      xs = [ mulInf' x1 x2 | x1 <- [lb1, ub1], x2 <- [lb2, ub2] ]+      ub3 = maximumBy cmpUB xs+      lb3 = minimumBy cmpLB xs++instance forall r. (Real r, Fractional r) => Fractional (Interval r) where+  fromRational r = singleton (fromRational r)+  recip a | null a = empty+  recip i | 0 `member` i = whole -- should be error?+  recip (Interval lb ub) = interval lb3 ub3+    where+      ub3 = maximumBy cmpUB xs+      lb3 = minimumBy cmpLB xs+      xs = [recipLB lb, recipUB ub]++cmpUB, cmpLB :: Ord r => (EndPoint r, Bool) -> (EndPoint r, Bool) -> Ordering+cmpUB (x1,in1) (x2,in2) = compare x1 x2 `mappend` compare in1 in2+cmpLB (x1,in1) (x2,in2) = compare x1 x2 `mappend` flip compare in1 in2++-- | Endpoints of intervals+data EndPoint r+  = NegInf    -- ^ negative infinity (-∞)+  | Finite !r -- ^ finite value+  | PosInf    -- ^ positive infinity (+∞)+  deriving (Ord, Eq, Show, Read, Typeable)++instance Bounded (EndPoint r) where+  minBound = NegInf+  maxBound = PosInf++instance Functor EndPoint where+  fmap f NegInf = NegInf+  fmap f (Finite x) = Finite (f x)+  fmap f PosInf = PosInf++isFinite :: EndPoint r -> Bool+isFinite (Finite _) = True+isFinite _ = False++negateEndPoint :: Num r => EndPoint r -> EndPoint r+negateEndPoint NegInf = PosInf+negateEndPoint PosInf = NegInf+negateEndPoint (Finite x) = Finite (negate x)++scaleInf' :: (Num r, Ord r) => r -> (EndPoint r, Bool) -> (EndPoint r, Bool)+scaleInf' a (x1, in1) = (scaleEndPoint a x1, in1)++scaleEndPoint :: (Num r, Ord r) => r -> EndPoint r -> EndPoint r+scaleEndPoint a inf =+  case a `compare` 0 of+    EQ -> Finite 0+    GT ->+      case inf of+        NegInf   -> NegInf+        Finite b -> Finite (a*b)+        PosInf   -> PosInf+    LT ->+      case inf of+        NegInf   -> PosInf+        Finite b -> Finite (a*b)+        PosInf   -> NegInf++mulInf' :: (Num r, Ord r) => (EndPoint r, Bool) -> (EndPoint r, Bool) -> (EndPoint r, Bool)+mulInf' (Finite 0, True) _ = (Finite 0, True)+mulInf' _ (Finite 0, True) = (Finite 0, True)+mulInf' (x1,in1) (x2,in2) = (mulEndPoint x1 x2, in1 && in2)++mulEndPoint :: (Num r, Ord r) => EndPoint r -> EndPoint r -> EndPoint r+mulEndPoint (Finite x1) (Finite x2) = Finite (x1 * x2)+mulEndPoint inf (Finite x2) =+  case compare x2 0 of+    EQ -> Finite 0+    GT -> inf+    LT -> negateEndPoint inf+mulEndPoint (Finite x1) inf =+  case compare x1 0 of+    EQ -> Finite 0+    GT -> inf+    LT -> negateEndPoint inf+mulEndPoint PosInf PosInf = PosInf+mulEndPoint PosInf NegInf = NegInf+mulEndPoint NegInf PosInf = NegInf+mulEndPoint NegInf NegInf = PosInf++recipLB :: (Fractional r, Ord r) => (EndPoint r, Bool) -> (EndPoint r, Bool)+recipLB (Finite 0, _) = (PosInf, False)+recipLB (x1, in1) = (recipEndPoint x1, in1)++recipUB :: (Fractional r, Ord r) => (EndPoint r, Bool) -> (EndPoint r, Bool)+recipUB (Finite 0, _) = (NegInf, False)+recipUB (x1, in1) = (recipEndPoint x1, in1)++recipEndPoint :: (Fractional r, Ord r) => EndPoint r -> EndPoint r+recipEndPoint PosInf = Finite 0+recipEndPoint NegInf = Finite 0+recipEndPoint (Finite x) = Finite (1/x)++-- | Combining two @Maybe@ values using given function.+combineMaybe :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a+combineMaybe _ Nothing y = y+combineMaybe _ x Nothing = x+combineMaybe f (Just x) (Just y) = Just (f x y)++-- | is the number integral?+--+-- @+--    isInteger x = fromInteger (round x) == x+-- @+isInteger :: RealFrac a => a -> Bool+isInteger x = fromInteger (round x) == x
+ test/TestInterval.hs view
@@ -0,0 +1,480 @@+{-# LANGUAGE TemplateHaskell #-}++import Control.Monad+import Data.Maybe+import Data.Ratio+import Test.HUnit hiding (Test)+import Test.QuickCheck+import Test.Framework (Test, defaultMain, testGroup)+import Test.Framework.TH+import Test.Framework.Providers.HUnit+import Test.Framework.Providers.QuickCheck2++import Data.Interval (Interval, EndPoint (..), (<=..<=), (<=..<), (<..<=), (<..<), (<!), (<=!), (==!), (>=!), (>!), (<?), (<=?), (==?), (>=?), (>?))+import qualified Data.Interval as Interval++{--------------------------------------------------------------------+  empty+--------------------------------------------------------------------}++prop_empty_is_bottom =+  forAll intervals $ \a ->+    Interval.isSubsetOf Interval.empty a++prop_null_empty =+  forAll intervals $ \a ->+    Interval.null a == (a == Interval.empty)++case_null_empty =+  Interval.null (Interval.empty :: Interval Rational) @?= True++{--------------------------------------------------------------------+  whole+--------------------------------------------------------------------}++prop_whole_is_top =+  forAll intervals $ \a ->+    Interval.isSubsetOf a Interval.whole++case_nonnull_top =+  Interval.null (Interval.whole :: Interval Rational) @?= False++{--------------------------------------------------------------------+  singleton+--------------------------------------------------------------------}++prop_singleton_member =+  forAll arbitrary $ \r ->+    Interval.member (r::Rational) (Interval.singleton r)++prop_singleton_member_intersection =+  forAll intervals $ \a ->+  forAll arbitrary $ \r ->+    let b = Interval.singleton r+    in Interval.member (r::Rational) a+       ==> Interval.intersection a b == b++prop_singleton_nonnull =+  forAll arbitrary $ \r1 ->+    not $ Interval.null $ Interval.singleton (r1::Rational)++prop_distinct_singleton_intersection =+  forAll arbitrary $ \r1 ->+  forAll arbitrary $ \r2 ->+    (r1::Rational) /= r2 ==>+      Interval.intersection (Interval.singleton r1) (Interval.singleton r2)+      == Interval.empty++{--------------------------------------------------------------------+  Intersection+--------------------------------------------------------------------}++prop_intersection_comm =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    Interval.intersection a b == Interval.intersection b a++prop_intersection_assoc =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+  forAll intervals $ \c ->+    Interval.intersection a (Interval.intersection b c) ==+    Interval.intersection (Interval.intersection a b) c++prop_intersection_unitL =+  forAll intervals $ \a ->+    Interval.intersection Interval.whole a == a++prop_intersection_unitR =+  forAll intervals $ \a ->+    Interval.intersection a Interval.whole == a++prop_intersection_empty =+  forAll intervals $ \a ->+    Interval.intersection a Interval.empty == Interval.empty++prop_intersection_isSubsetOf =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    Interval.isSubsetOf (Interval.intersection a b) a++prop_intersection_isSubsetOf_equiv =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    (Interval.intersection a b == a)+    == Interval.isSubsetOf a b++{--------------------------------------------------------------------+  Hull+--------------------------------------------------------------------}++prop_hull_comm =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    Interval.hull a b == Interval.hull b a++prop_hull_assoc =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+  forAll intervals $ \c ->+    Interval.hull a (Interval.hull b c) ==+    Interval.hull (Interval.hull a b) c++prop_hull_unitL =+  forAll intervals $ \a ->+    Interval.hull Interval.empty a == a++prop_hull_unitR =+  forAll intervals $ \a ->+    Interval.hull a Interval.empty == a++prop_hull_whole =+  forAll intervals $ \a ->+    Interval.hull a Interval.whole == Interval.whole++prop_hull_isSubsetOf =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    Interval.isSubsetOf a (Interval.hull a b)++prop_hull_isSubsetOf_equiv =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    (Interval.hull a b == b)+    == Interval.isSubsetOf a b++{--------------------------------------------------------------------+  member+--------------------------------------------------------------------}++prop_member_isSubsetOf =+  forAll arbitrary $ \r ->+  forAll intervals $ \a ->+    Interval.member r a == Interval.isSubsetOf (Interval.singleton r) a++{--------------------------------------------------------------------+  isSubsetOf+--------------------------------------------------------------------}++prop_isSubsetOf_refl =+  forAll intervals $ \a ->+    Interval.isSubsetOf a a++prop_isSubsetOf_trans =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+  forAll intervals $ \c ->+    Interval.isSubsetOf a b && Interval.isSubsetOf b c+    ==> Interval.isSubsetOf a c++-- prop_isSubsetOf_antisym =+--   forAll intervals $ \a ->+--   forAll intervals $ \b ->+--     Interval.isSubsetOf a b && Interval.isSubsetOf b a+--     ==> a == b++{--------------------------------------------------------------------+  pickup+--------------------------------------------------------------------}++prop_pickup_member_null =+  forAll intervals $ \a ->+    case Interval.pickup a of+      Nothing -> Interval.null a+      Just x -> Interval.member x a++case_pickup_empty =+  Interval.pickup (Interval.empty :: Interval Rational) @?= Nothing++case_pickup_whole =+  isJust (Interval.pickup (Interval.whole :: Interval Rational)) @?= True++{--------------------------------------------------------------------+  Comparison+--------------------------------------------------------------------}++case_lt_all_1 = (a <! b) @?= False+  where+    a, b :: Interval Rational+    a = NegInf <..<= Finite 0+    b = Finite 0 <=..< PosInf++case_lt_all_2 = (a <! b) @?= True+  where+    a, b :: Interval Rational+    a = NegInf <..< Finite 0+    b = Finite 0 <=..< PosInf++case_lt_all_3 = (a <! b) @?= True+  where+    a, b :: Interval Rational+    a = NegInf <..<= Finite 0+    b = Finite 0 <..< PosInf++case_lt_all_4 = (a <! b) @?= False+  where+    a, b :: Interval Rational+    a = Finite 0 <=..< PosInf+    b = Finite 1 <=..< PosInf++case_lt_some_1 = (a <? b) @?= False+  where+    a, b :: Interval Rational+    a = Finite 0 <=..< PosInf+    b = NegInf <..<= Finite 0++case_lt_some_2 = (a <? b) @?= False+  where+    a, b :: Interval Rational+    a = Finite 0 <..< PosInf+    b = NegInf <..<= Finite 0++case_lt_some_3 = (a <? b) @?= False+  where+    a, b :: Interval Rational+    a = Finite 0 <=..< PosInf+    b = NegInf <..< Finite 0++case_lt_some_4 = (a <! b) @?= False+  where+    a, b :: Interval Rational+    a = Finite 0 <=..< PosInf+    b = Finite 1 <=..< PosInf++case_le_some_1 = (a <=? b) @?= True+  where+    a, b :: Interval Rational+    a = Finite 0 <=..< PosInf+    b = NegInf <..<= Finite 0++case_le_some_2 = (a <=? b) @?= False+  where+    a, b :: Interval Rational+    a = Finite 0 <..< PosInf+    b = NegInf <..<= Finite 0++case_le_some_3 = (a <=? b) @?= False+  where+    a, b :: Interval Rational+    a = Finite 0 <=..< PosInf+    b = NegInf <..< Finite 0++prop_lt_all_not_refl =+  forAll intervals $ \a -> not (Interval.null a) ==> not (a <! a)++prop_le_some_refl =+  forAll intervals $ \a -> not (Interval.null a) ==> a <=? a++prop_lt_all_singleton =+  forAll arbitrary $ \a ->+  forAll arbitrary $ \b ->+    (a::Rational) < b ==> Interval.singleton a <! Interval.singleton b++prop_lt_all_singleton_2 =+  forAll arbitrary $ \a ->+    not $ Interval.singleton (a::Rational) <! Interval.singleton a++prop_le_all_singleton =+  forAll arbitrary $ \a ->+  forAll arbitrary $ \b ->+    (a::Rational) <= b ==> Interval.singleton a <=! Interval.singleton b++prop_le_all_singleton_2 =+  forAll arbitrary $ \a ->+    Interval.singleton (a::Rational) <=! Interval.singleton a++prop_lt_some_singleton =+  forAll arbitrary $ \a ->+  forAll arbitrary $ \b ->+    (a::Rational) < b ==> Interval.singleton a <? Interval.singleton b++prop_lt_some_singleton_2 =+  forAll arbitrary $ \a ->+    not $ Interval.singleton (a::Rational) <? Interval.singleton a++prop_le_some_singleton =+  forAll arbitrary $ \a ->+  forAll arbitrary $ \b ->+    (a::Rational) <= b ==> Interval.singleton a <=? Interval.singleton b++prop_le_some_singleton_2 =+  forAll arbitrary $ \a ->+    Interval.singleton (a::Rational) <=? Interval.singleton a++{--------------------------------------------------------------------+  Num+--------------------------------------------------------------------}++prop_scale_empty =+  forAll arbitrary $ \r ->+    Interval.singleton (r::Rational) * Interval.empty == Interval.empty++prop_add_comm =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    a + b == b + a++prop_add_assoc =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+  forAll intervals $ \c ->+    a + (b + c) == (a + b) + c++prop_add_unitL =+  forAll intervals $ \a ->+    Interval.singleton 0 + a == a++prop_add_unitR =+  forAll intervals $ \a ->+    a + Interval.singleton 0 == a++prop_add_member =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    and [ (x+y) `Interval.member` (a+b)+        | x <- maybeToList $ Interval.pickup a+        , y <- maybeToList $ Interval.pickup b+        ]++prop_mult_comm =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    a * b == b * a++prop_mult_assoc =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+  forAll intervals $ \c ->+    a * (b * c) == (a * b) * c++prop_mult_unitL =+  forAll intervals $ \a ->+    Interval.singleton 1 * a == a++prop_mult_unitR =+  forAll intervals $ \a ->+    a * Interval.singleton 1 == a++prop_mult_dist =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+  forAll intervals $ \c ->+    (a * (b + c)) `Interval.isSubsetOf` (a * b + a * c)++prop_mult_empty =+  forAll intervals $ \a ->+    Interval.empty * a == Interval.empty++prop_mult_zero = +  forAll intervals $ \a ->+    not (Interval.null a) ==> Interval.singleton 0 * a ==  Interval.singleton 0++prop_mult_member =+  forAll intervals $ \a ->+  forAll intervals $ \b ->+    and [ (x*y) `Interval.member` (a*b)+        | x <- maybeToList $ Interval.pickup a+        , y <- maybeToList $ Interval.pickup b+        ]++case_mult_test1 = ival1 * ival2 @?= ival3+  where+    ival1 = Finite 1 <=..<= Finite 2+    ival2 = Finite 1 <=..<= Finite 2+    ival3 = Finite 1 <=..<= Finite 4++case_mult_test2 = ival1 * ival2 @?= ival3+  where+    ival1 = Finite 1 <=..<= Finite 2+    ival2 = Finite 1 <..< Finite 2+    ival3 = Finite 1 <..< Finite 4++case_mult_test3 = ival1 * ival2 @?= ival3+  where+    ival1 = Finite 1 <..< Finite 2+    ival2 = Finite 1 <..< Finite 2+    ival3 = Finite 1 <..< Finite 4++case_mult_test4 = ival1 * ival2 @?= ival3+  where+    ival1 = Finite 2 <..< PosInf+    ival2 = Finite 3 <..< PosInf+    ival3 = Finite 6 <..< PosInf++case_mult_test5 = ival1 * ival2 @?= ival3+  where+    ival1 = NegInf <..< Finite (-3)+    ival2 = NegInf <..< Finite (-2)+    ival3 = Finite 6 <..< PosInf++case_mult_test6 = ival1 * ival2 @?= ival3+  where+    ival1 = Finite 2 <..< PosInf+    ival2 = NegInf <..< Finite (-2)+    ival3 = NegInf <..< Finite (-4)++{--------------------------------------------------------------------+  Fractional+--------------------------------------------------------------------}++prop_recip_singleton =+  forAll arbitrary $ \r ->+    let n = fromIntegral (numerator r)+        d = fromIntegral (denominator r)+    in Interval.singleton n / Interval.singleton d == Interval.singleton (r::Rational)++case_recip_pos =+  recip pos @?= pos++case_recip_neg =+  recip neg @?= neg++case_recip_test1 = recip i1 @?= i2+  where+    i1, i2 :: Interval Rational+    i1 = Finite 2 <=..< PosInf+    i2 = Finite 0 <..<= Finite (1/2)++{--------------------------------------------------------------------+  Read+--------------------------------------------------------------------}++prop_show_read_invariance =+  forAll intervals $ \i -> do+    i == read (show i)++{--------------------------------------------------------------------+  Generators+--------------------------------------------------------------------}++instance Arbitrary r => Arbitrary (EndPoint r) where+  arbitrary = +    oneof+    [ return NegInf+    , return PosInf+    , liftM Finite arbitrary+    ]++intervals :: Gen (Interval Rational)+intervals = do+  lb <- arbitrary+  ub <- arbitrary+  return $ Interval.interval lb ub++pos :: Interval Rational+pos = Finite 0 <..< PosInf++neg :: Interval Rational+neg = NegInf <..< Finite 0++nonpos :: Interval Rational+nonpos = NegInf <..<= Finite 0++nonneg :: Interval Rational+nonneg = Finite 0 <=..< PosInf++------------------------------------------------------------------------+-- Test harness++main :: IO ()+main = $(defaultMainGenerator)