module Feldspar.Range where
import Control.Monad
import Data.Maybe
import Data.Monoid
import Data.Bits
import Data.Word
import Test.QuickCheck hiding ((.&.))
import qualified Test.QuickCheck as QC
import System.Random
import Text.Printf
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' r@(Range l u)
| isNatural r = r
| isNegative r = Range (liftM abs u) (liftM abs l)
| otherwise =
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
rangeAddUnsigned :: (Ord a, Num a, Bounded a) => Range a -> Range a -> Range a
rangeAddUnsigned =
rangeProp2 $ \a b c d ->
if a + c >= a && b + d < b
then fullRange
else range (a + c) (b + d)
rangeAddSigned :: (Ord a, Num a, Bounded a, Bits a) =>
Range a -> Range a -> Range a
rangeAddSigned =
rangeProp2 $ \a b c d ->
let s = a + c
t = b + d
u = a .&. c .&. complement s .&.
complement (b .&. d .&. complement t)
v = ((xor a c) .|. complement (xor a s)) .&.
(complement b .&. complement d .&. t)
in if (u .|. v) < 0
then fullRange
else range s t
rangeSubUnsigned :: (Ord a, Num a, Bounded a) => Range a -> Range a -> Range a
rangeSubUnsigned =
rangeProp2 $ \a b c d ->
let s = a d
t = b c
in if s > a && t <= b
then fullRange
else range s t
rangeNegUnsigned :: (Ord a, Num a, Bounded a) => Range a -> Range a
rangeNegUnsigned =
rangeProp1 $ \a b ->
if a == 0 && b /= 0
then fullRange
else range (b) (a)
rangeNegSigned :: (Ord a, Num a, Bounded a) => Range a -> Range a
rangeNegSigned =
rangeProp1 $ \a b ->
if a == minBound && b == minBound
then singletonRange minBound
else if a == minBound
then fullRange
else range (b) (a)
rangeOrUnsignedCheap :: (Ord a, Num a, Bounded a) =>
Range a -> Range a -> Range a
rangeOrUnsignedCheap =
rangeProp2 $ \a b c d -> range (max a c) (maxPlus b d)
maxPlus b d = if sum < b then maxBound
else sum
where sum = b + d
minOrUnsigned :: (Ord a, Num a, Bits a) => a -> a -> a -> a -> a
minOrUnsigned a b c d = loop (bit (bitSize a 1))
where loop 0 = a .|. c
loop m
| complement a .&. c .&. m > 0 =
let temp = (a .|. m) .&. negate m
in if temp <= b
then temp .|. c
else loop (shiftR m 1)
| a .&. complement c .&. m > 0=
let temp = (c .|. m) .&. negate m
in if temp <= d
then a .|. temp
else loop (shiftR m 1)
| otherwise = loop (shiftR m 1)
maxOrUnsigned :: (Ord a, Num a, Bits a) => a -> a -> a -> a -> a
maxOrUnsigned a b c d= loop (bit (bitSize a 1))
where loop 0 = b .|. d
loop m
| b .&. d .&. m > 0 =
let temp = (b m) .|. (m 1)
in if temp >= a
then temp .|. d
else let temp = (d m) .|. (m 1)
in if temp >= c
then b .|. temp
else loop (shiftR m 1)
| otherwise = loop (shiftR m 1)
rangeOrUnsignedAccurate :: (Ord a, Num a, Bits a, Bounded a) =>
Range a -> Range a -> Range a
rangeOrUnsignedAccurate =
rangeProp2 $ \a b c d ->
range (minOrUnsigned a b c d) (maxOrUnsigned a b c d)
rangeAndUnsignedCheap :: (Ord a, Num a, Bounded a) =>
Range a -> Range a -> Range a
rangeAndUnsignedCheap = rangeProp2 $ \a b c d -> range 0 (min b d)
rangeXorUnsigned :: (Ord a, Num a, Bounded a) => Range a -> Range a -> Range a
rangeXorUnsigned = rangeProp2 (\a b c d -> range 0 (maxPlus b d))
rangeProp1 :: (Ord a, Bounded a) => (a -> a -> Range a) -> Range a -> Range a
rangeProp1 f (Range l u) = f a b
where toUpper Nothing = maxBound
toUpper (Just u) = u
toLower Nothing = minBound
toLower (Just l) = l
a = toLower l
b = toUpper u
rangeProp2 :: (Ord a, Bounded a) =>
(a -> a -> a -> a -> Range a) -> Range a -> Range a -> Range a
rangeProp2 f (Range l1 u1) (Range l2 u2) =
f a b c d
where toUpper Nothing = maxBound
toUpper (Just u) = u
toLower Nothing = minBound
toLower (Just l) = l
a = toLower l1
b = toUpper u1
c = toLower l2
d = toUpper u2
rangeMax :: Ord a => Range a -> Range a -> Range a
rangeMax r1 r2
| isEmpty r1 = r2
| isEmpty r2 = r1
rangeMax r1 r2
| r1 `rangeLess` r2 = r2
| r2 `rangeLess` r1 = r1
rangeMax (Range (Just l1) u1) (Range (Just l2) u2)
| l1 < l2 = Range (Just l2) (liftM2 max u1 u2)
| otherwise = Range (Just l1) (liftM2 max u1 u2)
rangeMax (Range Nothing u1) (Range (Just l2) u2)
= Range (Just l2) (liftM2 max u1 u2)
rangeMax (Range (Just l1) u1) (Range Nothing u2)
= Range (Just l1) (liftM2 max u1 u2)
rangeMax (Range Nothing u1) (Range Nothing u2)
= Range Nothing (liftM2 max u1 u2)
rangeMin :: Ord a => Range a -> Range a -> Range a
rangeMin r1 r2
| isEmpty r1 = r2
| isEmpty r2 = r1
rangeMin r1 r2
| r1 `rangeLess` r2 = r1
| r2 `rangeLess` r1 = r2
rangeMin (Range l1 (Just u1)) (Range l2 (Just u2))
| u1 < u2 = Range (liftM2 min l1 l2) (Just u1)
| otherwise = Range (liftM2 min l1 l2) (Just u2)
rangeMin (Range l1 Nothing) (Range l2 (Just u2))
= Range (liftM2 min l1 l2) (Just u2)
rangeMin (Range l1 (Just u1)) (Range l2 Nothing)
= Range (liftM2 min l1 l2) (Just u1)
rangeMin (Range l1 Nothing) (Range l2 Nothing)
= Range (liftM2 min l1 l2) Nothing
rangeMod :: (Num a, Ord a, Enum a) => Range a -> Range a -> Range a
rangeMod d r
| d `rangeLess` r && isNatural r && isNatural d = d
| isNatural r = Range (Just 0) (fmap pred (upperBound r))
| r `rangeLess` d && isNegative r && isNegative d = d
| isNegative r = Range (fmap succ (lowerBound r)) (Just 0)
where
isNegative = (`isSubRangeOf` negativeRange)
negativeRange = Range Nothing (Just 0)
rangeMod d (Range l u)
= Range (fmap succ l) (fmap pred u)
rangeRem :: (Num a, Ord a, Enum a) => Range a -> Range a -> Range a
rangeRem d r
| d `rangeLess` abs r && isNatural d = d
| isNatural d = Range (Just 0) (fmap pred (upperBound (abs r)))
| abs d `rangeLess` abs r && isNegative d = d
| isNegative d = Range (fmap negate (upperBound (abs r))) (Just 0)
where
isNegative = (`isSubRangeOf` negativeRange)
negativeRange = Range Nothing (Just 0)
rangeRem d r@(Range l u)
| l `betterThan` u =
Range (fmap (succ . negate .abs) l) (fmap (pred . abs) l)
| otherwise =
Range (fmap (succ . negate . abs) u) (fmap (pred . abs) upper)
where lower = lowerBound r
upper = upperBound r
betterThan (Just a) (Just b) = abs a >= abs b
betterThan Nothing (Just b) = True
betterThan (Just a) Nothing = False
betterThan Nothing Nothing = True
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
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)]
instance Random Word32 where
random g = (fromIntegral i,g')
where (i :: Int,g') = random g
randomR (l,u) g = (fromIntegral i,g')
where (i :: Integer, g') = randomR (fromIntegral l,fromIntegral u) g
instance Arbitrary Word32 where
arbitrary = choose (0,maxBound)
shrink i = [i `div` 2, i `div` 2 1, i 1]
prop_arith1 :: (forall a . Num a => a -> a) -> Range Int -> Property
prop_arith1 op r =
not (isEmpty r) ==>
forAll (fromRange r) $ \x ->
op x `inRange` op r
prop_arith2
:: (forall a . Num a => a -> a -> a)
-> Range Int -> Range Int -> Property
prop_arith2 op r1 r2 = rangePropagationSafety op 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_addU = rangePropagationSafety ((+) :: Word32 -> Word32 -> Word32)
rangeAddUnsigned
prop_addS = rangePropagationSafety ((+) :: Int -> Int -> Int)
rangeAddSigned
prop_subU = rangePropagationSafety (() :: Word32 -> Word32 -> Word32)
rangeSubUnsigned
prop_negU = rangePropSafety1 (negate :: Word32 -> Word32) rangeNegUnsigned
prop_negS = rangePropSafety1 (negate :: Int -> Int) rangeNegSigned
prop_andUCheap = rangePropagationSafety ((.&.) :: Word32 -> Word32 -> Word32)
rangeAndUnsignedCheap
prop_orUCheap = rangePropagationSafety ((.|.) :: Word32 -> Word32 -> Word32)
rangeOrUnsignedCheap
prop_xorU = rangePropagationSafety (xor :: Word32 -> Word32 -> Word32)
rangeXorUnsigned
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_intersect5 (r1::Range Int) (r2::Range Int) =
isEmpty r1 || isEmpty r2 ==> isEmpty (r1/\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 (r1::Range Int) (r2::Range Int) =
not (isEmpty r1) && not (isEmpty r2) ==>
forAll (fromRange r1) $ \x ->
forAll (fromRange r2) $ \y ->
rangeLess r1 r2 ==> x < y
prop_rangeLessEq (r1::Range Int) (r2::Range Int) =
not (isEmpty r1) && not (isEmpty r2) ==>
forAll (fromRange r1) $ \x ->
forAll (fromRange r2) $ \y ->
rangeLessEq r1 r2 ==> x <= y
prop_rangeMax1 (r1::Range Int) = rangeMax r1 r1 == r1
prop_rangeMax2 (r1::Range Int) r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
upperBound r1 <= upperBound max && upperBound r2 <= upperBound max
where
max = rangeMax r1 r2
Nothing <= Nothing = True
Just _ <= Nothing = True
Just a <= Just b = a Prelude.<= b
_ <= _ = False
prop_rangeMax3 (r1::Range Int) r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
lowerBound (rangeMax r1 r2) == liftMaybe2 max (lowerBound r1) (lowerBound r2)
prop_rangeMax4 (r1::Range Int) r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
rangeMax r1 r2 == rangeMax r2 r1
prop_rangeMax5 (r1::Range Int) r2 =
(isEmpty r1 && not (isEmpty r2) ==>
rangeMax r1 r2 == r2)
QC..&.
(isEmpty r2 && not (isEmpty r1) ==>
rangeMax r1 r2 == r1)
prop_rangeMax6 (v1::Int) v2 =
max v1 v2 `inRange` rangeMax (singletonRange v1) (singletonRange v2)
prop_rangeMax7 (r1::Range Int) r2 =
rangePropagationSafety max rangeMax r1 r2
prop_rangeMin1 (r1::Range Int) = rangeMin r1 r1 == r1
prop_rangeMin2 (r1::Range Int) r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
lowerBound min <= lowerBound r1 && lowerBound min <= lowerBound r2
where
min = rangeMin r1 r2
Nothing <= Nothing = True
Nothing <= Just _ = True
Just a <= Just b = a Prelude.<= b
_ <= _ = False
prop_rangeMin3 (r1::Range Int) r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
upperBound (rangeMin r1 r2) == liftMaybe2 min (upperBound r1) (upperBound r2)
prop_rangeMin4 (r1::Range Int) r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
rangeMin r1 r2 == rangeMin r2 r1
prop_rangeMin5 (r1::Range Int) r2 =
(isEmpty r1 && not (isEmpty r2) ==>
rangeMin r1 r2 == r2)
QC..&.
(isEmpty r2 && not (isEmpty r1) ==>
rangeMin r1 r2 == r1)
prop_rangeMin6 (v1::Int) v2 =
min v1 v2 `inRange` rangeMin (singletonRange v1) (singletonRange v2)
prop_rangeMin7 (r1::Range Int) r2 =
rangePropagationSafety min rangeMin r1 r2
prop_rangeMod1 (v1::Int) v2 =
v2 /= 0 ==>
mod v1 v2 `inRange` rangeMod (singletonRange v1) (singletonRange v2)
prop_rangeMod2 =
rangePropagationSafetyPre mod rangeMod (\v1 (v2::Int) -> v2 /= 0)
prop_rangeRem =
rangePropagationSafetyPre rem rangeRem (\v1 (v2::Int) -> v2 /= 0)
rangePropagationSafetyPre :: (Random a, Ord a, Show a, Bounded a,
Random b, Ord b, Show b, Bounded b,
Ord c) =>
(a -> b -> c) -> (Range a -> Range b -> Range c) ->
(a -> b -> Bool) ->
Range a -> Range b -> Property
rangePropagationSafetyPre op rop pre r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
forAll (fromRange r1) $ \v1 ->
forAll (fromRange r2) $ \v2 ->
pre v1 v2 ==>
op v1 v2 `inRange` rop r1 r2
rangePropagationSafety op rop r1 r2 =
rangePropagationSafetyPre op rop noPre r1 r2
noPre _ _ = True
rangePropSafety1 :: (Ord a, Show a, Random a, Bounded a, Ord b) =>
(a -> b) -> (Range a -> Range b) -> Range a -> Property
rangePropSafety1 op rop ran =
not (isEmpty ran) ==>
forAll (fromRange ran) $ \val ->
op val `inRange` rop ran
lowBound,uppBound :: (Bounded a, Ord a) => Range a -> a
lowBound r | Just l <- lowerBound r = l
lowBound r = minBound
uppBound r | Just u <- upperBound r = u
uppBound r = maxBound
fromRange :: (Random a, Bounded a, Ord a) => Range a -> Gen a
fromRange r = choose (lowBound r,uppBound r)
testAll = do
myCheck "prop_neg" prop_neg
myCheck "prop_negU" prop_negU
myCheck "prop_negS" prop_negS
myCheck "prop_add" prop_add
myCheck "prop_sub" prop_sub
myCheck "prop_mul" prop_mul
myCheck "prop_addU" prop_addU
myCheck "prop_addS" prop_addS
myCheck "prop_subU" prop_subU
myCheck "prop_andUCheap" prop_andUCheap
myCheck "prop_orUCheap" prop_orUCheap
myCheck "prop_xorU" prop_xorU
myCheck "prop_abs" prop_abs
myCheck "prop_sign" prop_sign
myCheck "prop_abs2" prop_abs2
myCheck "prop_fromInteger" prop_fromInteger
myCheck "prop_empty" prop_empty
myCheck "prop_full" prop_full
myCheck "prop_isEmpty1" prop_isEmpty1
myCheck "prop_isEmpty2" prop_isEmpty2
myCheck "prop_isFull" prop_isFull
myCheck "prop_fullRange" prop_fullRange
myCheck "prop_range" prop_range
myCheck "prop_singletonRange1" prop_singletonRange1
myCheck "prop_singletonRange2" prop_singletonRange2
myCheck "prop_singletonSize" prop_singletonSize
myCheck "prop_subRange" prop_subRange
myCheck "prop_emptySubRange1" prop_emptySubRange1
myCheck "prop_emptySubRange2" prop_emptySubRange2
myCheck "prop_isNegative" prop_isNegative
myCheck "prop_rangeGap" prop_rangeGap
myCheck "prop_union1" prop_union1
myCheck "prop_union2" prop_union2
myCheck "prop_union3" prop_union3
myCheck "prop_union4" prop_union4
myCheck "prop_intersect1" prop_intersect1
myCheck "prop_intersect2" prop_intersect2
myCheck "prop_intersect3" prop_intersect3
myCheck "prop_intersect4" prop_intersect4
myCheck "prop_intersect5" prop_intersect5
myCheck "prop_disjoint" prop_disjoint
myCheck "prop_rangeLess1" prop_rangeLess1
myCheck "prop_rangeLess2" prop_rangeLess2
myCheck "prop_rangeLessEq" prop_rangeLessEq
myCheck "prop_rangeMax1" prop_rangeMax1
myCheck "prop_rangeMax2" prop_rangeMax2
myCheck "prop_rangeMax3" prop_rangeMax3
myCheck "prop_rangeMax4" prop_rangeMax4
myCheck "prop_rangeMax5" prop_rangeMax5
myCheck "prop_rangeMax6" prop_rangeMax6
myCheck "prop_rangeMax7" prop_rangeMax7
myCheck "prop_rangeMin1" prop_rangeMin1
myCheck "prop_rangeMin2" prop_rangeMin2
myCheck "prop_rangeMin3" prop_rangeMin3
myCheck "prop_rangeMin4" prop_rangeMin4
myCheck "prop_rangeMin5" prop_rangeMin5
myCheck "prop_rangeMin6" prop_rangeMin6
myCheck "prop_rangeMin7" prop_rangeMin7
myCheck "prop_rangeMod1" prop_rangeMod1
myCheck "prop_rangeMod2" prop_rangeMod2
myCheck "prop_rangeRem" prop_rangeRem
where
myCheck name test =
do printf "%-25s" name
quickCheckWith stdArgs {maxDiscard = 10000} test