module SoPSat.Internal.Range (
  Range (..),
  Bound (..),
  boundSoP,
  rangeAdd,
  rangeMul,
  rangeExp,
)
where

import SoPSat.SoP

data Bound f c
  = Bound (SoP f c)
  | Inf
  deriving (Bound f c -> Bound f c -> Bool
(Bound f c -> Bound f c -> Bool)
-> (Bound f c -> Bound f c -> Bool) -> Eq (Bound f c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f c. (Eq f, Eq c) => Bound f c -> Bound f c -> Bool
$c== :: forall f c. (Eq f, Eq c) => Bound f c -> Bound f c -> Bool
== :: Bound f c -> Bound f c -> Bool
$c/= :: forall f c. (Eq f, Eq c) => Bound f c -> Bound f c -> Bool
/= :: Bound f c -> Bound f c -> Bool
Eq, Int -> Bound f c -> ShowS
[Bound f c] -> ShowS
Bound f c -> String
(Int -> Bound f c -> ShowS)
-> (Bound f c -> String)
-> ([Bound f c] -> ShowS)
-> Show (Bound f c)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f c. (Show f, Show c) => Int -> Bound f c -> ShowS
forall f c. (Show f, Show c) => [Bound f c] -> ShowS
forall f c. (Show f, Show c) => Bound f c -> String
$cshowsPrec :: forall f c. (Show f, Show c) => Int -> Bound f c -> ShowS
showsPrec :: Int -> Bound f c -> ShowS
$cshow :: forall f c. (Show f, Show c) => Bound f c -> String
show :: Bound f c -> String
$cshowList :: forall f c. (Show f, Show c) => [Bound f c] -> ShowS
showList :: [Bound f c] -> ShowS
Show)

boundSoP :: Bound f c -> Maybe (SoP f c)
boundSoP :: forall f c. Bound f c -> Maybe (SoP f c)
boundSoP (Bound SoP f c
s) = SoP f c -> Maybe (SoP f c)
forall a. a -> Maybe a
Just SoP f c
s
boundSoP Bound f c
Inf = Maybe (SoP f c)
forall a. Maybe a
Nothing

data Range f c
  = Range
  { forall f c. Range f c -> Bound f c
lower :: Bound f c
  , forall f c. Range f c -> Bound f c
upper :: Bound f c
  }
  deriving (Range f c -> Range f c -> Bool
(Range f c -> Range f c -> Bool)
-> (Range f c -> Range f c -> Bool) -> Eq (Range f c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f c. (Eq f, Eq c) => Range f c -> Range f c -> Bool
$c== :: forall f c. (Eq f, Eq c) => Range f c -> Range f c -> Bool
== :: Range f c -> Range f c -> Bool
$c/= :: forall f c. (Eq f, Eq c) => Range f c -> Range f c -> Bool
/= :: Range f c -> Range f c -> Bool
Eq, Int -> Range f c -> ShowS
[Range f c] -> ShowS
Range f c -> String
(Int -> Range f c -> ShowS)
-> (Range f c -> String)
-> ([Range f c] -> ShowS)
-> Show (Range f c)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f c. (Show f, Show c) => Int -> Range f c -> ShowS
forall f c. (Show f, Show c) => [Range f c] -> ShowS
forall f c. (Show f, Show c) => Range f c -> String
$cshowsPrec :: forall f c. (Show f, Show c) => Int -> Range f c -> ShowS
showsPrec :: Int -> Range f c -> ShowS
$cshow :: forall f c. (Show f, Show c) => Range f c -> String
show :: Range f c -> String
$cshowList :: forall f c. (Show f, Show c) => [Range f c] -> ShowS
showList :: [Range f c] -> ShowS
Show)

boundAdd :: (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundAdd :: forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundAdd Bound f c
Inf Bound f c
_ = Bound f c
forall f c. Bound f c
Inf
boundAdd Bound f c
_ Bound f c
Inf = Bound f c
forall f c. Bound f c
Inf
boundAdd (Bound SoP f c
a) (Bound SoP f c
b) = SoP f c -> Bound f c
forall f c. SoP f c -> Bound f c
Bound (SoP f c
a SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
|+| SoP f c
b)

boundMul :: (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundMul :: forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundMul Bound f c
Inf Bound f c
_ = Bound f c
forall f c. Bound f c
Inf
boundMul Bound f c
_ Bound f c
Inf = Bound f c
forall f c. Bound f c
Inf
boundMul (Bound SoP f c
a) (Bound SoP f c
b) = SoP f c -> Bound f c
forall f c. SoP f c -> Bound f c
Bound (SoP f c
a SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
|*| SoP f c
b)

boundExp :: (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundExp :: forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundExp Bound f c
Inf Bound f c
_ = Bound f c
forall f c. Bound f c
Inf
boundExp Bound f c
_ Bound f c
Inf = Bound f c
forall f c. Bound f c
Inf
boundExp (Bound SoP f c
a) (Bound SoP f c
b) = SoP f c -> Bound f c
forall f c. SoP f c -> Bound f c
Bound (SoP f c
a SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
|^| SoP f c
b)

rangeAdd :: (Ord f, Ord c) => Range f c -> Range f c -> Maybe (Range f c)
-- Subtraction of unbounded functions
rangeAdd :: forall f c.
(Ord f, Ord c) =>
Range f c -> Range f c -> Maybe (Range f c)
rangeAdd (Range Bound f c
_ Bound f c
Inf) (Range Bound f c
Inf Bound f c
_) = Maybe (Range f c)
forall a. Maybe a
Nothing
rangeAdd (Range Bound f c
Inf Bound f c
_) (Range Bound f c
_ Bound f c
Inf) = Maybe (Range f c)
forall a. Maybe a
Nothing
rangeAdd (Range Bound f c
low1 Bound f c
up1) (Range Bound f c
low2 Bound f c
up2) =
  Range f c -> Maybe (Range f c)
forall a. a -> Maybe a
Just (Range f c -> Maybe (Range f c)) -> Range f c -> Maybe (Range f c)
forall a b. (a -> b) -> a -> b
$
    Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundAdd Bound f c
low1 Bound f c
low2) (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundAdd Bound f c
up1 Bound f c
up2)

rangeMul :: (Ord f, Ord c) => Range f c -> Range f c -> Maybe (Range f c)
-- Multiplication of unbounded functions
rangeMul :: forall f c.
(Ord f, Ord c) =>
Range f c -> Range f c -> Maybe (Range f c)
rangeMul (Range Bound f c
Inf Bound f c
Inf) Range f c
_ = Maybe (Range f c)
forall a. Maybe a
Nothing
rangeMul Range f c
_ (Range Bound f c
Inf Bound f c
Inf) = Maybe (Range f c)
forall a. Maybe a
Nothing
-- Multiplication with infinitely increasing/decresing functions
rangeMul (Range Bound f c
low1 Bound f c
Inf) (Range Bound f c
low2 Bound f c
_) =
  Range f c -> Maybe (Range f c)
forall a. a -> Maybe a
Just (Range f c -> Maybe (Range f c)) -> Range f c -> Maybe (Range f c)
forall a b. (a -> b) -> a -> b
$
    Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundMul Bound f c
low1 Bound f c
low2) Bound f c
forall f c. Bound f c
Inf
rangeMul (Range Bound f c
low1 Bound f c
_) (Range Bound f c
low2 Bound f c
Inf) =
  Range f c -> Maybe (Range f c)
forall a. a -> Maybe a
Just (Range f c -> Maybe (Range f c)) -> Range f c -> Maybe (Range f c)
forall a b. (a -> b) -> a -> b
$
    Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundMul Bound f c
low1 Bound f c
low2) Bound f c
forall f c. Bound f c
Inf
rangeMul (Range Bound f c
Inf Bound f c
up1) (Range Bound f c
low2 Bound f c
_) =
  Range f c -> Maybe (Range f c)
forall a. a -> Maybe a
Just (Range f c -> Maybe (Range f c)) -> Range f c -> Maybe (Range f c)
forall a b. (a -> b) -> a -> b
$
    Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range Bound f c
forall f c. Bound f c
Inf (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundMul Bound f c
up1 Bound f c
low2)
rangeMul (Range Bound f c
low1 Bound f c
_) (Range Bound f c
Inf Bound f c
up2) =
  Range f c -> Maybe (Range f c)
forall a. a -> Maybe a
Just (Range f c -> Maybe (Range f c)) -> Range f c -> Maybe (Range f c)
forall a b. (a -> b) -> a -> b
$
    Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range Bound f c
forall f c. Bound f c
Inf (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundMul Bound f c
up2 Bound f c
low1)
rangeMul (Range Bound f c
low1 Bound f c
up1) (Range Bound f c
low2 Bound f c
up2) =
  Range f c -> Maybe (Range f c)
forall a. a -> Maybe a
Just (Range f c -> Maybe (Range f c)) -> Range f c -> Maybe (Range f c)
forall a b. (a -> b) -> a -> b
$
    Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundMul Bound f c
low1 Bound f c
low2) (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundMul Bound f c
up1 Bound f c
up2)

-- rangeMul (Range low1 up1) (Range low2 up2)
-- --   | sopSign low1 == sopSign low2
-- --   = Range
-- rangeMul (Range low1 up1) (Range low2 up2) = let
--     low1Sign = sopSign =<< boundSoP low1
--     low2Sign = sopSign =<< boundSoP low2
--   in case (low1Sign,low2Sign) of
--        (Just Positive, Just Positive) -> Just $
--          Range (boundMul low1 low2) (boundMul up1 up2)
--        (Just Negative, Just Positive) -> Just $
--          Range (boundMul low1 up2) (boundMul up1 low2)
--        (Just Positive, Just Negative) -> Just $
--          Range (boundMul up1 low2) (boundMul low1 up2)
--        (Just Negative, Just Negative) -> Just $
--          Range (boundMul
-- rangeMul _ _ = Nothing

rangeExp :: (Ord f, Ord c) => Range f c -> Range f c -> Maybe (Range f c)
rangeExp :: forall f c.
(Ord f, Ord c) =>
Range f c -> Range f c -> Maybe (Range f c)
rangeExp (Range Bound f c
Inf Bound f c
_) (Range Bound f c
Inf Bound f c
_) = Maybe (Range f c)
forall a. Maybe a
Nothing
rangeExp (Range Bound f c
_ Bound f c
up1) (Range Bound f c
Inf Bound f c
up2) =
  Range f c -> Maybe (Range f c)
forall a. a -> Maybe a
Just (Range f c -> Maybe (Range f c)) -> Range f c -> Maybe (Range f c)
forall a b. (a -> b) -> a -> b
$
    Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range (SoP f c -> Bound f c
forall f c. SoP f c -> Bound f c
Bound (Integer -> SoP f c
forall f c. Integer -> SoP f c
int Integer
0)) (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundExp Bound f c
up1 Bound f c
up2)
rangeExp (Range Bound f c
low1 Bound f c
up1) (Range Bound f c
low2 Bound f c
up2) =
  Range f c -> Maybe (Range f c)
forall a. a -> Maybe a
Just (Range f c -> Maybe (Range f c)) -> Range f c -> Maybe (Range f c)
forall a b. (a -> b) -> a -> b
$
    Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundExp Bound f c
low1 Bound f c
low2) (Bound f c -> Bound f c -> Bound f c
forall f c. (Ord f, Ord c) => Bound f c -> Bound f c -> Bound f c
boundExp Bound f c
up1 Bound f c
up2)