module Feldspar.Range where
import Control.Monad
import Data.Maybe
import Data.Monoid
import Test.QuickCheck
data Ord a => Range a = Range
{ lowerBound :: Maybe a
, upperBound :: Maybe a
}
deriving (Eq, Show)
instance (Ord a, Num a) => Num (Range a)
where
fromInteger = singletonRange . fromInteger
negate = rangeOp neg
where
neg (Range l u) = Range (liftM negate u) (liftM negate l)
(+) = rangeOp2 add
where
add (Range l1 u1) (Range l2 u2) =
Range (liftM2 (+) l1 l2) (liftM2 (+) u1 u2)
(*) = rangeMul
abs = rangeOp abs'
where
abs' (Range l u) =
Range (Just 0) (liftM2 max (liftM abs l) (liftM abs u))
signum = rangeOp sign
where
sign r
| range (1) 1 `isSubRangeOf` r = range (1) 1
| range (1) 0 `isSubRangeOf` r = range (1) 0
| range 0 1 `isSubRangeOf` r = range 0 1
| singletonRange 0 `isSubRangeOf` r = singletonRange 0
| isNatural r = singletonRange 1
| isNegative r = singletonRange (1)
instance (Ord a, Num a) => Monoid (Range a)
where
mempty = emptyRange
mappend = (\/)
rangeOp :: Ord a => (Range a -> Range a) -> (Range a -> Range a)
rangeOp f r = if isEmpty r then r else f r
rangeOp2 :: Ord a =>
(Range a -> Range a -> Range a) -> (Range a -> Range a -> Range a)
rangeOp2 f r1 r2
| isEmpty r1 = r1
| isEmpty r2 = r2
| otherwise = f r1 r2
mapMonotonic :: (Ord a, Ord b) => (a -> b) -> Range a -> Range b
mapMonotonic f (Range l u) = Range (liftM f l) (liftM f u)
rangeMul :: (Ord a, Num a) => Range a -> Range a -> Range a
rangeMul r1 r2 = p1 \/ p2 \/ p3 \/ p4
where
split r = (r /\ negativeRange, r /\ naturalRange)
(r1neg,r1pos) = split r1
(r2neg,r2pos) = split r2
p1 = mul (negate r1neg) (negate r2neg)
p2 = negate $ mul (negate r1neg) r2pos
p3 = negate $ mul r1pos (negate r2neg)
p4 = mul r1pos r2pos
mul = rangeOp2 mul'
where
mul' (Range l1 u1) (Range l2 u2) =
Range (liftM2 (*) l1 l2) (liftM2 (*) u1 u2)
emptyRange :: (Ord a, Num a) => Range a
emptyRange = Range (Just 0) (Just (1))
fullRange :: Ord a => Range a
fullRange = Range Nothing Nothing
range :: Ord a => a -> a -> Range a
range l u = Range (Just l) (Just u)
rangeByRange :: Ord a => Range a -> Range a -> Range a
rangeByRange r1 r2 = Range (lowerBound r1) (upperBound r2)
singletonRange :: Ord a => a -> Range a
singletonRange a = Range (Just a) (Just a)
naturalRange :: (Ord a, Num a) => Range a
naturalRange = Range (Just 0) Nothing
negativeRange :: (Ord a, Num a) => Range a
negativeRange = Range Nothing (Just (1))
rangeSize :: (Ord a, Num a) => Range a -> Maybe a
rangeSize (Range l u) = do
l' <- l
u' <- u
return (u'l'+1)
isEmpty :: Ord a => Range a -> Bool
isEmpty (Range Nothing _) = False
isEmpty (Range _ Nothing) = False
isEmpty (Range (Just l) (Just u)) = u < l
isFull :: Ord a => Range a -> Bool
isFull (Range Nothing Nothing) = True
isFull _ = False
isBounded :: Ord a => Range a -> Bool
isBounded (Range Nothing _) = False
isBounded (Range _ Nothing) = False
isBounded (Range _ _) = True
isSingleton :: Ord a => Range a -> Bool
isSingleton (Range (Just l) (Just u)) = l==u
isSingleton _ = False
isSubRangeOf :: Ord a => Range a -> Range a -> Bool
isSubRangeOf r1@(Range l1 u1) r2@(Range l2 u2)
| isEmpty r1 = True
| isEmpty r2 = False
| otherwise
= (isNothing l2 || (isJust l1 && l1>=l2))
&& (isNothing u2 || (isJust u1 && u1<=u2))
isNatural :: (Ord a, Num a) => Range a -> Bool
isNatural = (`isSubRangeOf` naturalRange)
isNegative :: (Ord a, Num a) => Range a -> Bool
isNegative = (`isSubRangeOf` negativeRange)
inRange :: Ord a => a -> Range a -> Bool
inRange a r = singletonRange a `isSubRangeOf` r
rangeGap :: (Ord a, Num a) => Range a -> Range a -> Range a
rangeGap = rangeOp2 gap
where
gap (Range _ (Just u1)) (Range (Just l2) _)
| u1 < l2 = Range (Just u1) (Just l2)
gap (Range (Just l1) _) (Range _ (Just u2))
| u2 < l1 = Range (Just u2) (Just l1)
gap _ _ = emptyRange
(\/) :: Ord a => Range a -> Range a -> Range a
r1 \/ r2
| isEmpty r1 = r2
| isEmpty r2 = r1
| otherwise = or r1 r2
where
or (Range l1 u1) (Range l2 u2) =
Range (liftM2 min l1 l2) (liftM2 max u1 u2)
liftMaybe2 :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
liftMaybe2 f Nothing b = b
liftMaybe2 f a Nothing = a
liftMaybe2 f (Just a) (Just b) = Just (f a b)
(/\) :: Ord a => Range a -> Range a -> Range a
(/\) = rangeOp2 and
where
and (Range l1 u1) (Range l2 u2) =
Range (liftMaybe2 max l1 l2) (liftMaybe2 min u1 u2)
disjoint :: (Ord a, Num a) => Range a -> Range a -> Bool
disjoint r1 r2 = isEmpty (r1 /\ r2)
rangeLess :: Ord a => Range a -> Range a -> Bool
rangeLess r1 r2
| isEmpty r1 || isEmpty r2 = True
rangeLess (Range _ (Just u1)) (Range (Just l2) _) = u1 < l2
rangeLess _ _ = False
rangeLessEq :: Ord a => Range a -> Range a -> Bool
rangeLessEq (Range _ (Just u1)) (Range (Just l2) _) = u1 <= l2
rangeLessEq _ _ = False
showBound :: Show a => Maybe a -> String
showBound (Just a) = show a
showBound _ = "*"
showRange :: (Show a, Ord a) => Range a -> String
showRange r@(Range l u)
| isEmpty r = "[]"
| isSingleton r = let Just a = upperBound r in show [a]
| otherwise = "[" ++ showBound l ++ "," ++ showBound u ++ "]"
instance (Arbitrary a, Ord a, Num a) => Arbitrary (Range a)
where
coarbitrary = error "coarbitrary not defined for (Range a)"
arbitrary = do
lower <- arbitrary
size <- liftM abs arbitrary
upper <- frequency [(6, return (lower+size)), (1, return (lowersize))]
liftM2 Range (arbMaybe lower) (arbMaybe upper)
where
arbMaybe a = frequency [(5, return (Just a)), (1, return Nothing)]
prop_arith1 :: (forall a . Num a => a -> a) -> Int -> Range Int -> Property
prop_arith1 op x r = (x `inRange` r) ==> (op x `inRange` op r)
prop_arith2
:: (forall a . Num a => a -> a -> a)
-> Int -> Int -> Range Int -> Range Int -> Property
prop_arith2 op x y r1 r2 =
(inRange x r1 && inRange y r2) ==> (op x y `inRange` op r1 r2)
prop_fromInteger = isSingleton . fromInteger
prop_neg = prop_arith1 negate
prop_add = prop_arith2 (+)
prop_sub = prop_arith2 ()
prop_mul = prop_arith2 (*)
prop_abs = prop_arith1 abs
prop_sign = prop_arith1 signum
prop_abs2 (r::Range Int) = isNatural (abs r)
prop_empty = isEmpty (emptyRange :: Range Int)
prop_full = isFull (fullRange :: Range Int)
prop_isEmpty1 (r::Range Int) = isEmpty r ==> isBounded r
prop_isEmpty2 (r::Range Int) = isEmpty r ==> (upperBound r < lowerBound r)
prop_isFull (r::Range Int) = isFull r ==> not (isBounded r)
prop_fullRange = not $ isBounded (fullRange :: Range Int)
prop_range (a::Int) (b::Int) = isBounded $ range a b
prop_rangeByRange (r1::Range Int) (r2::Range Int) =
(rangeLess r1 r2 && not (isEmpty (r1/\r2))) ==> isEmpty (rangeByRange r1 r2)
prop_singletonRange1 (a::Int) = isSingleton (singletonRange a)
prop_singletonRange2 (a::Int) = isBounded (singletonRange a)
prop_singletonSize (r::Range Int) = isSingleton r ==> (rangeSize r == Just 1)
prop_subRange (r1::Range Int) (r2::Range Int) =
((r1 < r2) && (r2 < r1) && not (isEmpty r1)) ==> r1==r2
where
(<) = isSubRangeOf
prop_emptySubRange1 (r1::Range Int) (r2::Range Int) =
isEmpty r1 ==> (not (isEmpty r2) ==> not (r2 `isSubRangeOf` r1))
prop_emptySubRange2 (r1::Range Int) (r2::Range Int) =
isEmpty r1 ==> (not (isEmpty r2) ==> (r1 `isSubRangeOf` r2))
prop_isNegative (r::Range Int) =
not (isEmpty r) ==> (isNegative r ==> not (isNegative $ negate r))
prop_rangeGap (r1::Range Int) (r2::Range Int) =
(isEmpty gap1 && isEmpty gap2) || (gap1 == gap2)
where
gap1 = rangeGap r1 r2
gap2 = rangeGap r2 r1
prop_union1 x (r1::Range Int) (r2::Range Int) =
((x `inRange` r1) || (x `inRange` r2)) ==> (x `inRange` (r1\/r2))
prop_union2 x (r1::Range Int) (r2::Range Int) =
(x `inRange` (r1\/r2)) ==>
((x `inRange` r1) || (x `inRange` r2) || (x `inRange` rangeGap r1 r2))
prop_union3 (r1::Range Int) (r2::Range Int) = r1 `isSubRangeOf` (r1\/r2)
prop_union4 (r1::Range Int) (r2::Range Int) = r2 `isSubRangeOf` (r1\/r2)
prop_intersect1 x (r1::Range Int) (r2::Range Int) =
((x `inRange` r1) && (x `inRange` r2)) ==> (x `inRange` (r1/\r2))
prop_intersect2 x (r1::Range Int) (r2::Range Int) =
(x `inRange` (r1/\r2)) ==> ((x `inRange` r1) && (x `inRange` r2))
prop_intersect3 (r1::Range Int) (r2::Range Int) = (r1/\r2) `isSubRangeOf` r1
prop_intersect4 (r1::Range Int) (r2::Range Int) = (r1/\r2) `isSubRangeOf` r2
prop_disjoint x (r1::Range Int) (r2::Range Int) =
disjoint r1 r2 ==> (x `inRange` r1) ==> not (x `inRange` r2)
prop_rangeLess1 (r1::Range Int) (r2::Range Int) =
rangeLess r1 r2 ==> disjoint r1 r2
prop_rangeLess2 x y (r1::Range Int) (r2::Range Int) =
(rangeLess r1 r2 && inRange x r1 && inRange y r2) ==> x < y
prop_rangeLessEq x y (r1::Range Int) (r2::Range Int) =
(rangeLessEq r1 r2 && inRange x r1 && inRange y r2) ==> x <= y
testAll = do
myCheck prop_neg
myCheck prop_add
myCheck prop_sub
myCheck prop_mul
myCheck prop_abs
myCheck prop_sign
myCheck prop_abs2
myCheck prop_fromInteger
myCheck prop_empty
myCheck prop_full
myCheck prop_isEmpty1
myCheck prop_isEmpty2
myCheck prop_isFull
myCheck prop_fullRange
myCheck prop_range
myCheck prop_singletonRange1
myCheck prop_singletonRange2
myCheck prop_singletonSize
myCheck prop_subRange
myCheck prop_emptySubRange1
myCheck prop_emptySubRange2
myCheck prop_isNegative
myCheck prop_rangeGap
myCheck prop_union1
myCheck prop_union2
myCheck prop_union3
myCheck prop_union4
myCheck prop_intersect1
myCheck prop_intersect2
myCheck prop_intersect3
myCheck prop_intersect4
myCheck prop_disjoint
myCheck prop_rangeLess1
myCheck prop_rangeLess2
myCheck prop_rangeLessEq
where
myCheck = check defaultConfig {configMaxFail = 100000}