module Feldspar.Range where
import Data.Bits
import Data.Int
import Data.Word
import Data.Typeable
import System.Random
import Test.QuickCheck hiding ((.&.))
import qualified Test.QuickCheck as QC
import Text.Printf
import Feldspar.Set
data Range a = Range
{ lowerBound :: a
, upperBound :: a
}
deriving (Eq, Show)
class (Eq a, Ord a, Show a, Num a, Bounded a, Integral a, Bits a) => BoundedInt a
instance (Eq a, Ord a, Show a, Num a, Bounded a, Integral a, Bits a) => BoundedInt a
handleSign :: forall a b . BoundedInt a =>
(Range a -> b) -> (Range a -> b) -> (Range a -> b)
handleSign u s
| isSigned (minBound::a) = s
| otherwise = u
showBound :: BoundedInt a => a -> String
showBound a
| a `elem` [maxBound,minBound] = "*"
| otherwise = show a
showRange :: BoundedInt a => Range a -> String
showRange r@(Range l u)
| isEmpty r = "[]"
| isSingleton r = show u
| otherwise = "[" ++ showBound l ++ "," ++ showBound u ++ "]"
mapMonotonic :: (a -> b) -> Range a -> Range b
mapMonotonic f (Range l u) = Range (f l) (f u)
mapMonotonic2 :: (a -> b -> c) -> Range a -> Range b -> Range c
mapMonotonic2 f (Range l1 u1) (Range l2 u2) = Range (f l1 l2) (f u1 u2)
instance BoundedInt a => Set (Range a)
where
empty = emptyRange
universal = fullRange
(\/) = rangeUnion
(/\) = rangeIntersection
emptyRange :: BoundedInt a => Range a
emptyRange = Range maxBound minBound
fullRange :: BoundedInt a => Range a
fullRange = Range minBound maxBound
range :: a -> a -> Range a
range = Range
rangeByRange :: Range a -> Range a -> Range a
rangeByRange r1 r2 = Range (lowerBound r1) (upperBound r2)
singletonRange :: a -> Range a
singletonRange a = Range a a
naturalRange :: BoundedInt a => Range a
naturalRange = Range 0 maxBound
negativeRange :: BoundedInt a => Range a
negativeRange = Range minBound (1)
rangeSize :: BoundedInt a => Range a -> a
rangeSize (Range l u) = ul+1
isEmpty :: BoundedInt a => Range a -> Bool
isEmpty (Range l u) = u < l
isFull :: BoundedInt a => Range a -> Bool
isFull r = lowerBound r == minBound && upperBound r == maxBound
isSingleton :: BoundedInt a => Range a -> Bool
isSingleton (Range l u) = l==u
isSubRangeOf :: BoundedInt a => Range a -> Range a -> Bool
isSubRangeOf r1@(Range l1 u1) r2@(Range l2 u2)
| isEmpty r1 = True
| isEmpty r2 = False
| otherwise = (l1>=l2) && (u1<=u2)
isNatural :: BoundedInt a => Range a -> Bool
isNatural = (`isSubRangeOf` naturalRange)
isNegative :: BoundedInt a => Range a -> Bool
isNegative = (`isSubRangeOf` negativeRange)
inRange :: BoundedInt a => a -> Range a -> Bool
inRange a r = singletonRange a `isSubRangeOf` r
rangeOp :: BoundedInt a => (Range a -> Range a) -> (Range a -> Range a)
rangeOp f r = if isEmpty r then r else f r
rangeOp2 :: BoundedInt 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
rangeUnion :: BoundedInt a => Range a -> Range a -> Range a
r1 `rangeUnion` r2
| isEmpty r1 = r2
| isEmpty r2 = r1
| otherwise = union r1 r2
where
union (Range l1 u1) (Range l2 u2) = Range (min l1 l2) (max u1 u2)
rangeIntersection :: BoundedInt a => Range a -> Range a -> Range a
rangeIntersection = rangeOp2 intersection
where
intersection (Range l1 u1) (Range l2 u2) = Range (max l1 l2) (min u1 u2)
disjoint :: BoundedInt a => Range a -> Range a -> Bool
disjoint r1 r2 = isEmpty (r1 /\ r2)
rangeGap :: BoundedInt a => Range a -> Range a -> Range a
rangeGap = rangeOp2 gap
where
gap (Range l1 u1) (Range l2 u2)
| u1 < l2 = range u1 l2
| u2 < l1 = range u2 l1
gap _ _ = emptyRange
rangeLess :: BoundedInt a => Range a -> Range a -> Bool
rangeLess r1 r2
| isEmpty r1 || isEmpty r2 = True
rangeLess (Range _ u1) (Range l2 _) = u1 < l2
rangeLessEq :: BoundedInt a => Range a -> Range a -> Bool
rangeLessEq (Range _ u1) (Range l2 _) = u1 <= l2
instance BoundedInt a => Num (Range a)
where
fromInteger = singletonRange . fromInteger
abs = rangeAbs
signum = rangeSignum
negate = rangeNeg
(+) = rangeAdd
(*) = rangeMul
rangeAbs :: BoundedInt a => Range a -> Range a
rangeAbs = rangeOp $ \r -> case r of
Range l u
| isNatural r -> r
| r == singletonRange minBound -> r
| minBound `inRange` r -> range minBound maxBound
| isNegative r -> range (abs u) (abs l)
| otherwise -> range 0 (abs l `max` abs u)
rangeSignum :: BoundedInt a => Range a -> Range a
rangeSignum = handleSign rangeSignumUnsigned rangeSignumSigned
rangeSignumSigned :: BoundedInt a => Range a -> Range a
rangeSignumSigned = 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
| inRange 0 r = 0
| isNatural r = 1
| isNegative r = 1
rangeSignumUnsigned :: BoundedInt a => Range a -> Range a
rangeSignumUnsigned = rangeOp sign
where
sign r
| r == singletonRange 0 = r
| not (0 `inRange` r) = singletonRange 1
| otherwise = range 0 1
rangeNeg :: BoundedInt a => Range a -> Range a
rangeNeg = handleSign rangeNegUnsigned rangeNegSigned
rangeNegUnsigned :: BoundedInt a => Range a -> Range a
rangeNegUnsigned (Range l u)
| l == 0 && u /= 0 = fullRange
| otherwise = range (u) (l)
rangeNegSigned :: BoundedInt a => Range a -> Range a
rangeNegSigned (Range l u)
| l == minBound && u == minBound = singletonRange minBound
| l == minBound = fullRange
| otherwise = range (u) (l)
rangeAdd :: BoundedInt a => Range a -> Range a -> Range a
rangeAdd = handleSign rangeAddUnsigned rangeAddSigned
rangeAddUnsigned :: BoundedInt a => Range a -> Range a -> Range a
rangeAddUnsigned (Range l1 u1) (Range l2 u2)
| s >= l1 && t < u1 = fullRange
| otherwise = range s t
where
s = l1 + l2
t = u1 + u2
rangeAddSigned :: BoundedInt a => Range a -> Range a -> Range a
rangeAddSigned (Range l1 u1) (Range l2 u2)
| (u .|. v) < 0 = fullRange
| otherwise = range s t
where
s = l1 + l2
t = u1 + u2
u = l1 .&. l2 .&. complement s .&.
complement (u1 .&. u2 .&. complement t)
v = ((xor l1 l2) .|. complement (xor l1 s)) .&.
(complement u1 .&. complement u2 .&. t)
rangeSub :: BoundedInt a => Range a -> Range a -> Range a
rangeSub = handleSign rangeSubUnsigned ()
rangeSubUnsigned :: BoundedInt a => Range a -> Range a -> Range a
rangeSubUnsigned (Range l1 u1) (Range l2 u2)
| s > l1 && t <= u1 = fullRange
| otherwise = range s t
where
s = l1 u2
t = u1 l2
rangeMul :: BoundedInt a => Range a -> Range a -> Range a
rangeMul = handleSign rangeMulUnsigned rangeMulSigned
rangeMulSigned :: forall a . BoundedInt a => Range a -> Range a -> Range a
rangeMulSigned r1 r2
| r1 == singletonRange 0 || r2 == singletonRange 0 = singletonRange 0
| lowerBound r1 == minBound || lowerBound r2 == minBound
= range minBound maxBound
| bits (maxAbs r1) + bits (maxAbs r2) <= bitSize (undefined :: a) 1
= range (minimum [b1,b2,b3,b4]) (maximum [b1,b2,b3,b4])
| otherwise = range minBound maxBound
where maxAbs (Range l u) = max (abs l) (abs u)
b1 = lowerBound r1 * lowerBound r2
b2 = lowerBound r1 * upperBound r2
b3 = upperBound r1 * lowerBound r2
b4 = upperBound r1 * upperBound r2
rangeMulUnsigned :: forall a . BoundedInt a => Range a -> Range a -> Range a
rangeMulUnsigned r1 r2
| bits (upperBound r1) + bits (upperBound r2)
<= bitSize (undefined :: a)
= mapMonotonic2 (*) r1 r2
| otherwise = universal
bits :: Bits b => b -> Int
bits b = loop b 0
where loop 0 c = c
loop n c = loop (n `shiftR` 1) (c+1)
rangeExp :: BoundedInt a => Range a -> Range a -> Range a
rangeExp = handleSign rangeExpUnsigned rangeExpSigned
rangeExpUnsigned :: BoundedInt a => Range a -> Range a -> Range a
rangeExpUnsigned m@(Range l1 u1) e@(Range l2 u2)
| toInteger (bits u1) * toInteger u2 > toInteger (bitSize l1) + 1 = universal
| toInteger u1 ^ toInteger u2 > toInteger (maxBound `asTypeOf` l1) = universal
| 0 `inRange` m && 0 `inRange` e = range 0 (max b1 b2)
| otherwise = range b1 b2
where b1 = (l1 ^ l2)
b2 = (u1 ^ u2)
rangeExpSigned :: BoundedInt a => Range a -> Range a -> Range a
rangeExpSigned _ _ = universal
rangeOr :: forall a . BoundedInt a => Range a -> Range a -> Range a
rangeOr = handleSign rangeOrUnsignedAccurate (\_ _ -> universal)
rangeOrUnsignedCheap :: BoundedInt a => Range a -> Range a -> Range a
rangeOrUnsignedCheap (Range l1 u1) (Range l2 u2) =
range (max l1 l2) (maxPlus u1 u2)
maxPlus :: BoundedInt a => a -> a -> a
maxPlus b d = if sum < b then maxBound
else sum
where sum = b + d
minOrUnsigned :: BoundedInt 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 :: BoundedInt 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 :: BoundedInt a => Range a -> Range a -> Range a
rangeOrUnsignedAccurate (Range l1 u1) (Range l2 u2) =
range (minOrUnsigned l1 u1 l2 u2) (maxOrUnsigned l1 u1 l2 u2)
rangeAnd :: forall a . BoundedInt a => Range a -> Range a -> Range a
rangeAnd = handleSign rangeAndUnsignedCheap (\_ _ -> universal)
rangeAndUnsignedCheap :: BoundedInt a => Range a -> Range a -> Range a
rangeAndUnsignedCheap (Range l1 u1) (Range l2 u2) = range 0 (min u1 u2)
rangeXor :: forall a . BoundedInt a => Range a -> Range a -> Range a
rangeXor = handleSign rangeXorUnsigned (\_ _ -> universal)
rangeXorUnsigned :: BoundedInt a => Range a -> Range a -> Range a
rangeXorUnsigned (Range l1 u1) (Range l2 u2) = range 0 (maxPlus u1 u2)
rangeShiftLU :: BoundedInt a => Range a -> Range Word32 -> Range a
rangeShiftLU = handleSign rangeShiftLUUnsigned (\_ _ -> universal)
rangeShiftLUUnsigned (Range l1 u1) (Range l2 u2)
| toInteger (bits u1) + fromIntegral u2 > toInteger (bitSize u1) = universal
rangeShiftLUUnsigned (Range l1 u1) (Range l2 u2)
= range (shiftL l1 (fromIntegral l2)) (shiftL u1 (fromIntegral u2))
rangeShiftRU :: BoundedInt a => Range a -> Range Word32 -> Range a
rangeShiftRU = handleSign rangeShiftRUUnsigned (\_ _ -> universal)
rangeShiftRUUnsigned (Range l1 u1) (Range l2 u2)
= range (correctShiftRU l1 u2) (correctShiftRU u1 l2)
correctShiftRU :: Bits a => a -> Word32 -> a
correctShiftRU a i | i > fromIntegral (maxBound :: Int) = 0
correctShiftRU a i = shiftR a (fromIntegral i)
rangeMax :: BoundedInt a => Range a -> Range a -> Range a
rangeMax r1 r2
| isEmpty r1 = r2
| isEmpty r2 = r1
| r1 `rangeLess` r2 = r2
| r2 `rangeLess` r1 = r1
| otherwise = mapMonotonic2 max r1 r2
rangeMin :: BoundedInt a => Range a -> Range a -> Range a
rangeMin r1 r2
| isEmpty r1 = r2
| isEmpty r2 = r1
| r1 `rangeLess` r2 = r1
| r2 `rangeLess` r1 = r2
| otherwise = mapMonotonic2 min r1 r2
rangeMod :: BoundedInt a => Range a -> Range a -> Range a
rangeMod d r
| isSigned (lowerBound d) &&
minBound `inRange` d && (1) `inRange` r = fullRange
| d `rangeLess` r && isNatural r && isNatural d = d
| isNatural r = range 0 (pred (upperBound r))
| r `rangeLess` d && isNeg r && isNeg d = d
| isNeg r = range (succ (lowerBound r)) 0
where
isNeg = (`isSubRangeOf` negs)
negs = negativeRange \/ 0
rangeMod d (Range l u) = Range (succ l) (pred u)
rangeRem :: BoundedInt a => Range a -> Range a -> Range a
rangeRem d r
| isSigned (lowerBound d) &&
minBound `inRange` d && (1) `inRange` r = fullRange
| d `rangeLessAbs` r && isNatural d = d
| isNatural d = range 0 (pred (upperBound (abs r)))
| d `absRangeLessAbs` r && isNeg d = d
| isNeg d = range (negate (upperBound (abs r))) 0
where
isNeg = (`isSubRangeOf` negs)
negs = negativeRange \/ 0
rangeRem d r@(Range l u)
| abs l >= abs u || l == minBound = range (succ $ negate $ abs l) (predAbs l)
| otherwise = range (succ $ negate $ abs u) (predAbs u)
predAbs l | l == minBound = abs (succ l)
| otherwise = pred (abs l)
rangeQuot :: BoundedInt a => Range a -> Range a -> Range a
rangeQuot = handleSign rangeQuotU (\_ _ -> universal)
rangeQuotU :: BoundedInt a => Range a -> Range a -> Range a
rangeQuotU (Range l1 u1) (Range l2 u2) | l2 == 0 || u2 == 0 = universal
rangeQuotU (Range l1 u1) (Range l2 u2) = Range (l1 `quot` u2) (u1 `quot` l2)
rangeLessAbs d r
| r == singletonRange minBound
= lowerBound d /= minBound
| lowerBound r == minBound
= d `rangeLess` (abs (range (succ (lowerBound r)) (upperBound r)))
| otherwise = d `rangeLess` (abs r)
absRangeLessAbs d r
| lowerBound d == minBound = False
| otherwise = abs d `rangeLessAbs` r
instance (BoundedInt a, Arbitrary a) => Arbitrary (Range a)
where
arbitrary = do
[bound1,bound2] <- vectorOf 2 $ oneof
[ arbitrary
, elements [minBound,1,0,1,maxBound]]
frequency
[ (10, return $
Range (min bound1 bound2) (max bound1 bound2))
, (1 , return $
Range (max bound1 bound2) (min bound1 bound2))
, (1 , return $
Range bound1 bound1)
]
shrink (Range x y) =
[ Range x' y | x' <- shrink x ] ++
[ Range x y' | y' <- shrink y ]
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 Random Int8 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 Random Word8 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
fromRange :: Random a => Range a -> Gen a
fromRange r = choose (lowerBound r, upperBound r)
rangeTy :: Range t -> t -> Range t
rangeTy r t = r
atAllTypes :: (Monad m) =>
(forall t . (BoundedInt t, Random t, Arbitrary t, Typeable t) =>
t -> m a)
-> m ()
atAllTypes test = sequence_ [test (undefined :: Int)
,test (undefined :: Int8)
,test (undefined :: Word32)
,test (undefined :: Word8)
]
prop_empty t = isEmpty (emptyRange `rangeTy` t)
prop_full t = isFull (fullRange `rangeTy` t)
prop_isEmpty t r = isEmpty r ==> (upperBound r < lowerBound (r `rangeTy` t))
prop_rangeByRange1 t r1 r2 =
lowerBound r1 < lowerBound r2 && upperBound r1 < upperBound r2 ==>
r1 `isSubRangeOf` rangeByRange r1 r2
where _ = r1 `rangeTy` t
prop_rangeByRange2 t r1 r2 =
lowerBound r1 < lowerBound r2 && upperBound r1 < upperBound r2 ==>
r2 `isSubRangeOf` rangeByRange r1 r2
where _ = r1 `rangeTy` t
prop_rangeByRange3 t r1 r2 =
lowerBound r1 < lowerBound r2 && upperBound r1 < upperBound r2 ==>
(r1 `rangeUnion` r2) `isSubRangeOf` rangeByRange r1 r2
where _ = r1 `rangeTy` t
prop_singletonRange t a = isSingleton (singletonRange (a `asTypeOf` t))
prop_singletonSize t r = isSingleton (r `rangeTy` t) ==> (rangeSize r == 1)
prop_emptySubRange1 t r1 r2 =
isEmpty (r1 `rangeTy` t) ==> (not (isEmpty r2) ==>
not (r2 `isSubRangeOf` r1))
prop_emptySubRange2 t r1 r2 =
isEmpty (r1 `rangeTy` t) ==> (not (isEmpty r2) ==> (r1 `isSubRangeOf` r2))
prop_rangeGap t r1 r2 =
(isEmpty gap1 && isEmpty gap2) || (gap1 == gap2)
where
gap1 = rangeGap r1 r2
gap2 = rangeGap r2 r1
_ = r1 `rangeTy` t
prop_union1 t x r1 r2 =
((x `inRange` r1) || (x `inRange` r2)) ==> (x `inRange` (r1\/r2))
where _ = x `asTypeOf` t
prop_union2 t x r1 r2 =
(x `inRange` (r1\/r2)) ==>
((x `inRange` r1) || (x `inRange` r2) || (x `inRange` rangeGap r1 r2))
where _ = x `asTypeOf` t
prop_union3 t r1 r2 = (r1 `rangeTy` t) `isSubRangeOf` (r1\/r2)
prop_union4 t r1 r2 = (r2 `rangeTy` t) `isSubRangeOf` (r1\/r2)
prop_intersect1 t x r1 r2 =
((x `inRange` r1) && (x `inRange` r2)) ==> (x `inRange` (r1/\r2))
where _ = x `asTypeOf` t
prop_intersect2 t x r1 r2 =
(x `inRange` (r1/\r2)) ==> ((x `inRange` r1) && (x `inRange` r2))
where _ = x `asTypeOf` t
prop_intersect3 t r1 r2 = (r1/\r2) `isSubRangeOf` (r1 `rangeTy` t)
prop_intersect4 t r1 r2 = (r1/\r2) `isSubRangeOf` (r2 `rangeTy` t)
prop_intersect5 t r1 r2 =
isEmpty r1 || isEmpty r2 ==> isEmpty (r1/\r2)
where _ = r1 `rangeTy` t
prop_disjoint t x r1 r2 =
disjoint r1 r2 ==> (x `inRange` r1) ==> not (x `inRange` r2)
where _ = x `asTypeOf` t
prop_rangeLess1 t r1 r2 =
rangeLess r1 r2 ==> disjoint r1 (r2 `rangeTy` t)
prop_rangeLess2 t r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
forAll (fromRange r1) $ \x ->
forAll (fromRange r2) $ \y ->
rangeLess r1 r2 ==> x < y
where _ = r1 `rangeTy` t
prop_rangeLessEq t r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
forAll (fromRange r1) $ \x ->
forAll (fromRange r2) $ \y ->
rangeLessEq r1 r2 ==> x <= y
where _ = r1 `rangeTy` t
prop_propagation1 :: (BoundedInt t, Random t) =>
t -> (forall a . Num a => a -> a) -> Range t -> Property
prop_propagation1 t op r =
not (isEmpty r) ==>
forAll (fromRange r) $ \x ->
op x `inRange` op r
rangePropagationSafetyPre :: (Random t, BoundedInt t, BoundedInt a) =>
t ->
(t -> t -> a) -> (Range t -> Range t -> Range a) ->
(t -> t -> Bool) ->
Range t -> Range t -> Property
rangePropagationSafetyPre t 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
rangePropagationSafetyPre2 ::
(Random t, BoundedInt t, Random t2, BoundedInt t2, BoundedInt a) =>
t ->
(t -> t2 -> a) -> (Range t -> Range t2 -> Range a) ->
(t -> t2 -> Bool) ->
Range t -> Range t2 -> Property
rangePropagationSafetyPre2 t 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 t op rop = rangePropagationSafetyPre t op rop noPre
where
noPre _ _ = True
rangePropSafety1 t op rop ran =
not (isEmpty ran) ==>
forAll (fromRange ran) $ \val ->
op val `inRange` rop ran
where _ = ran `rangeTy` t
prop_propagation2
:: (BoundedInt t, Random t) => t -> (forall a . Num a => a -> a -> a)
-> Range t -> Range t -> Property
prop_propagation2 t op r1 r2 = rangePropagationSafety t op op r1 r2
prop_fromInteger t a = isSingleton (fromInteger a `rangeTy` t)
prop_abs t = prop_propagation1 t abs
prop_sign t = prop_propagation1 t signum
prop_neg t = prop_propagation1 t negate
prop_add t = prop_propagation2 t (+)
prop_sub t = prop_propagation2 t ()
prop_mul t = prop_propagation2 t (*)
prop_exp t = rangePropagationSafetyPre t (^) rangeExp (\_ e -> e >= 0)
prop_mulU t = rangePropagationSafety t (*) rangeMulUnsigned
prop_isNegative (r::Range Int) =
not (isEmpty r) ==> (isNegative r ==> not (isNegative $ negate r))
prop_abs2 t r =
(if isSigned (minBound `asTypeOf` t) then
lowerBound r /= (minBound `asTypeOf` t)
else True)
==> isNatural (abs r)
prop_or t = rangePropagationSafety t (.|.) rangeOr
prop_and t = rangePropagationSafety t (.&.) rangeAnd
prop_xor t = rangePropagationSafety t xor rangeXor
prop_shiftLU t
= rangePropagationSafetyPre2 t fixShiftL rangeShiftLU (\_ _ -> True)
where fixShiftL a b = shiftL a (fromIntegral b)
prop_shiftRU t
= rangePropagationSafetyPre2 t fixShiftR rangeShiftRU (\_ _ -> True)
where fixShiftR a b = correctShiftRU a (fromIntegral b)
prop_rangeMax1 t r1 = rangeMax r1 r1 == (r1 `rangeTy` t)
prop_rangeMax2 t r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
upperBound r1 <= upperBound max && upperBound r2 <= upperBound max
where
max = rangeMax r1 (r2 `rangeTy` t)
prop_rangeMax3 t r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
lowerBound (rangeMax r1 r2) == max (lowerBound r1) (lowerBound r2)
where _ = r1 `rangeTy` t
prop_rangeMax4 t r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
rangeMax r1 r2 == rangeMax r2 r1
where _ = r1 `rangeTy` t
prop_rangeMax5 t r1 r2 =
(isEmpty r1 && not (isEmpty r2) ==>
rangeMax r1 r2 == r2)
QC..&.
(isEmpty r2 && not (isEmpty r1) ==>
rangeMax r1 r2 == r1)
where _ = r1 `rangeTy` t
prop_rangeMax6 t v1 v2 =
max v1 v2 `inRange` rangeMax (singletonRange v1) (singletonRange v2)
where _ = v1 `asTypeOf` t
prop_rangeMax7 a r1 r2 =
rangePropagationSafety a max rangeMax r1 r2
prop_rangeMin1 t r1 = rangeMin r1 r1 == (r1 `rangeTy` t)
prop_rangeMin2 t r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
lowerBound min <= lowerBound r1 && lowerBound min <= lowerBound r2
where
min = rangeMin r1 (r2 `rangeTy` t)
prop_rangeMin3 t r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
upperBound (rangeMin r1 r2) == min (upperBound r1) (upperBound r2)
where _ = r1 `rangeTy` t
prop_rangeMin4 t r1 r2 =
not (isEmpty r1) && not (isEmpty r2) ==>
rangeMin r1 r2 == rangeMin r2 r1
where _ = r1 `rangeTy` t
prop_rangeMin5 t r1 r2 =
(isEmpty r1 && not (isEmpty r2) ==>
rangeMin r1 r2 == r2)
QC..&.
(isEmpty r2 && not (isEmpty r1) ==>
rangeMin r1 r2 == r1)
where _ = r1 `rangeTy` t
prop_rangeMin6 t v1 v2 =
min v1 v2 `inRange` rangeMin (singletonRange v1) (singletonRange v2)
where _ = v1 `asTypeOf` t
prop_rangeMin7 t r1 r2 =
rangePropagationSafety t min rangeMin r1 r2
prop_rangeMod1 t v1 v2 =
v2 /= 0 ==>
mod v1 v2 `inRange` rangeMod (singletonRange v1) (singletonRange v2)
where _ = v1 `asTypeOf` t
prop_rangeMod2 t =
rangePropagationSafetyPre t mod rangeMod divPre
prop_rangeMod3 t =
if isSigned t then
isFull $ rangeMod (singletonRange (minBound `asTypeOf` t))
(singletonRange (1))
else
True
prop_rangeRem t =
rangePropagationSafetyPre t rem rangeRem divPre
prop_rangeRem1 t =
if isSigned t then
isFull $ rangeRem (singletonRange (minBound `asTypeOf` t))
(singletonRange (1))
else
True
prop_rangeQuot t =
rangePropagationSafetyPre t quot rangeQuot divPre
prop_rangeQuot1 t =
if isSigned t then
isFull $ rangeQuot (singletonRange (minBound `asTypeOf` t))
(singletonRange (1))
else
True
divPre v1 v2 = v2 /= 0 && not (v1 == minBound && v2 == (1))
data TestCase = forall t. Testable t => TC String t
typedTests :: forall a. (BoundedInt a, Random a, Arbitrary a, Integral a) =>
a -> [TestCase]
typedTests a =
[TC "prop_empty" (prop_empty a)
,TC "prop_full" (prop_full a)
,TC "prop_isEmpty" (prop_isEmpty a)
,TC "prop_rangeByRange1" (prop_rangeByRange1 a)
,TC "prop_rangeByRange2" (prop_rangeByRange2 a)
,TC "prop_rangeByRange3" (prop_rangeByRange3 a)
,TC "prop_singletonRange" (prop_singletonRange a)
,TC "prop_singletonSize" (prop_singletonSize a)
,TC "prop_emptySubRange1" (prop_emptySubRange1 a)
,TC "prop_emptySubRange2" (prop_emptySubRange2 a)
,TC "prop_rangeGap" (prop_rangeGap a)
,TC "prop_union1" (prop_union1 a)
,TC "prop_union2" (prop_union2 a)
,TC "prop_union3" (prop_union3 a)
,TC "prop_union4" (prop_union4 a)
,TC "prop_intersect1" (prop_intersect1 a)
,TC "prop_intersect2" (prop_intersect2 a)
,TC "prop_intersect3" (prop_intersect3 a)
,TC "prop_intersect4" (prop_intersect4 a)
,TC "prop_intersect5" (prop_intersect5 a)
,TC "prop_disjoint" (prop_disjoint a)
,TC "prop_rangeLess1" (prop_rangeLess1 a)
,TC "prop_rangeLess2" (prop_rangeLess2 a)
,TC "prop_rangeLessEq" (prop_rangeLessEq a)
,TC "prop_fromInteger" (prop_fromInteger a)
,TC "prop_abs" (prop_abs a)
,TC "prop_sign" (prop_sign a)
,TC "prop_neg" (prop_neg a)
,TC "prop_add" (prop_add a)
,TC "prop_sub" (prop_sub a)
,TC "prop_mul" (prop_mul a)
,TC "prop_exp" (prop_exp a)
,TC "prop_abs2" (prop_abs2 a)
,TC "prop_and" (prop_and a)
,TC "prop_or" (prop_or a)
,TC "prop_xor" (prop_xor a)
,TC "prop_shiftLU" (prop_shiftLU a)
,TC "prop_shiftRU" (prop_shiftRU a)
,TC "prop_rangeMax1" (prop_rangeMax1 a)
,TC "prop_rangeMax2" (prop_rangeMax2 a)
,TC "prop_rangeMax3" (prop_rangeMax3 a)
,TC "prop_rangeMax4" (prop_rangeMax4 a)
,TC "prop_rangeMax5" (prop_rangeMax5 a)
,TC "prop_rangeMax6" (prop_rangeMax6 a)
,TC "prop_rangeMax7" (prop_rangeMax7 a)
,TC "prop_rangeMin1" (prop_rangeMin1 a)
,TC "prop_rangeMin2" (prop_rangeMin2 a)
,TC "prop_rangeMin3" (prop_rangeMin3 a)
,TC "prop_rangeMin4" (prop_rangeMin4 a)
,TC "prop_rangeMin5" (prop_rangeMin5 a)
,TC "prop_rangeMin6" (prop_rangeMin6 a)
,TC "prop_rangeMin7" (prop_rangeMin7 a)
,TC "prop_rangeMod1" (prop_rangeMod1 a)
,TC "prop_rangeMod2" (prop_rangeMod2 a)
,TC "prop_rangeMod3" (prop_rangeMod3 a)
,TC "prop_rangeRem" (prop_rangeRem a)
,TC "prop_rangeRem1" (prop_rangeRem1 a)
,TC "prop_rangeQuot" (prop_rangeQuot a)
,TC "prop_rangeQuot1" (prop_rangeQuot1 a)
]
testAll = do testAtType (undefined :: Int)
testAtType (undefined :: Int8)
testAtType (undefined :: Word32)
testAtType (undefined :: Word8)
myCheck (TC name test) =
do printf "%-25s" name
quickCheckWith stdArgs {maxDiscard = 10000} test
testAtType t = do let tn = tyConString $ typeRepTyCon $ typeOf t
putStrLn $ "Testing using type: " ++ tn
mapM_ myCheck (typedTests t)