-- 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 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))

-- | 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

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 (lower-size))]
        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_rangeByRange
    -- XXX "Arguments exhausted after 0 test"
    --     Something must be wrong with generator...
    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}