--
-- Copyright (c) 2009-2010, ERICSSON AB All rights reserved.
-- 
-- Redistribution and use in source and binary forms, with or without
-- modification, are permitted provided that the following conditions are met:
-- 
--     * Redistributions of source code must retain the above copyright notice,
--       this list of conditions and the following disclaimer.
--     * 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.
--     * Neither the name of the ERICSSON AB nor the names of its contributors
--       may be used to endorse or promote products derived from this software
--       without specific prior written permission.
-- 
-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "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 COPYRIGHT HOLDER OR CONTRIBUTORS
-- 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.
--

{-# LANGUAGE NoMonomorphismRestriction #-}

-- | Ranged values

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 -- Should maybe be exported from QuickCheck
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))

-- | Checks whether a range is a sub-range of the natural numbers.
isNatural :: (Ord a, Num a) => Range a -> Bool
isNatural = (`isSubRangeOf` naturalRange)

-- | Checks whether a range is a sub-range of the negative numbers.
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
  -- If the result is non-empty, it will include the boundary elements from the
  -- two ranges.



(\/) :: 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)

-- | @r1 \`rangeLess\` r2:@
--
-- Checks if all elements of @r1@ are less than all elements of @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

-- | @r1 \`rangeLessEq\` r2:@
--
-- Checks if all elements of @r1@ are less than or equal to all elements of
-- @r2@.
rangeLessEq :: Ord a => Range a -> Range a -> Bool
rangeLessEq (Range _ (Just u1)) (Range (Just l2) _) = u1 <= l2
rangeLessEq _ _                                     = False

-- | @rangeAddUnsigned@ correctly and accurately propagates range
-- information through an unsigned addition. Code is borrowed from
-- Hacker's Delight.
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@ correctly and accurately propagates range
-- information through a signed addition. Code is borrowed from
-- Hacker's Delight.
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@ propagates range information through unsigned
--   subtraction. Code is borrowed from Hacker's Delight
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

-- | Propagates range information through unsigned negation. Code from
--   Hacker's Delight
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)

-- | Propagates range information through signed negation. Code from
--   Hacker's Delight.
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)

-- | Cheap and inaccurate range propagation for '.|.' on unsigned numbers.
-- Code from Hacker's Delight
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

-- | Accurate lower bound for '.|.' on unsigned numbers.
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)

-- | Accurate upper bound for '.|.' on unsigned numbers.
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)

-- | Cheap and inaccurate range propagation for '.&.' on unsigned numbers.
-- Code from Hacker's Delight
rangeAndUnsignedCheap :: (Ord a, Num a, Bounded a) => 
                         Range a -> Range a -> Range a
rangeAndUnsignedCheap = rangeProp2 $ \a b c d -> range 0 (min b d)

-- | Range propagation for 'xor' on unsigned numbers.
-- Code from Hacker's Delight
rangeXorUnsigned :: (Ord a, Num a, Bounded a) => Range a -> Range a -> Range a
rangeXorUnsigned = rangeProp2 (\a b c d -> range 0 (maxPlus b d))

-- | Auxiliary function for writing range propagation
-- functions. Especially suitable for the code borrowed from Hacker's
-- Delight.
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

-- | Auxiliary function for writing range propagation functions for
-- two argument functions. Especially suitable for the code borrowed
-- from Hacker's Delight.
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

-- | Propagates range information through @max@.
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)

-- | Analogous to 'rangeMax'
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

-- | Propagates range information through 'mod'.
-- Note that we assume Haskell semantics for 'mod'.
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)

-- | Propagates range information through 'rem'.
-- Note that we assume Haskell semantics for 'rem'.
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 (lower-size))]
        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

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)

-- This function is useful for range propagation functions like
-- rangeMax, rangeMod etc. 
-- It takes two ranges, picks an element out of either ranges and
-- checks if applying the operation to the individual elements is in
-- the resulting range after range propagation 
-- The third argument is a precondition that is satisfied before the test is run
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
    -- This one is wrong but QuickCheck doesn't spot it
    myCheck "prop_neg"             prop_neg

    myCheck "prop_negU"            prop_negU
    myCheck "prop_negS"            prop_negS

    -- These three suffer from overflow behaviour
    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_rangeByRange
    -- XXX "Arguments exhausted after 0 test"
    --     Something must be wrong with generator...
    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