content: {-# LANGUAGE MultiWayIf #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE OverloadedStrings #-}
  module Data.Abstract.Interval where
  
  import Prelude hiding (div,Bool(..),(==),(/),(<),Ordering)
  import qualified Prelude as P
  
  import Control.DeepSeq
  
  import Data.Hashable
  import Data.Order
  import Data.Metric
  import Data.Numeric
  import Prettyprinter
  
  import Data.Abstract.Boolean
  import Data.Abstract.Equality
  import Data.Abstract.Ordering
  import Data.Abstract.Failure
  import Data.Abstract.InfiniteNumbers
  import Data.Abstract.Widening
  import Data.Abstract.Stable
  import Data.Abstract.Terminating
  
  import GHC.Generics
  
  -- | Intervals represent ranges of numbers. Bot represents the empty interval
  data Interval n = Interval n n
    deriving (Eq,Generic)
  
  instance Pretty n => Show (Interval n) where show = show . pretty
  instance Pretty n => Pretty (Interval n) where
    pretty (Interval n m) = "[" <> pretty n <> "," <> pretty m <> "]"
  
  instance Ord x => PreOrd (Interval x) where
    Interval i1 i2 ⊑ Interval j1 j2 = j1 <= i1 && i2 <= j2
  
  instance Ord x => Complete (Interval x) where
    Interval i1 i2 ⊔ Interval j1 j2 = Interval (min i1 j1) (max i2 j2)
  
  instance Ord x => CoComplete (Terminating (Interval x)) where
    NonTerminating ⊓ _ = NonTerminating
    _ ⊓ NonTerminating = NonTerminating
    Terminating (Interval i1 i2) ⊓ Terminating (Interval j1 j2) = if x <= y then Terminating iv else NonTerminating
      where iv@(Interval x y) = Interval (max i1 j1) (min i2 j2)
  
  instance NFData x => NFData (Interval x)
  
  instance (Num n, Ord n) => Num (Interval n) where
    Interval i1 i2 + Interval j1 j2 = Interval (i1 + j1) (i2 + j2)
    (*) = withBounds2 (*)
    negate (Interval i1 i2) = Interval (negate i2) (negate i1)
    abs (Interval i j)
      | 0 <= i = Interval i j
      | otherwise = Interval 0 (max i j)
    signum = withBounds1 signum
    fromInteger = constant . fromInteger
  
  instance (Integral n) => Numeric (Interval (InfiniteNumber n)) (Failure String) where
    Interval i1 i2 / Interval j1 j2
      | j1 P.== 0 && j2 P.== 0 = Fail "divided by 0 error"
      | j1 P.== 0 && 0  P.< j2 = Fail "divided by 0 error" ⊔ Interval i1 i2 / Interval (j1+1) j2
      | j1 P.<  0 && j2 P.== 0 = Fail "divided by 0 error" ⊔ Interval i1 i2 / Interval j1 (j2-1)
      | j1 P.<  0 && 0  P.< j2 = Fail "divided by 0 error" ⊔ Success (withBounds2 divInf (Interval i1 i2) (Interval j1 j2))
      | otherwise = Success (withBounds2 divInf (Interval i1 i2) (Interval j1 j2))
  
  instance Ord n => Equality (Interval n) where
    Interval i1 i2 == Interval j1 j2
      | i1 P.== i2 && j1 P.== j2 && i1 P.== j1 = True
      | j2 P.< i1 || i2 P.< j1 = False
      | otherwise = Top
  
  instance Ord n => Ordering (Interval n) where
    Interval i1 i2 < Interval j1 j2
      | i2 P.< j1 = True
      | j2 P.<= i1 = False
      | otherwise = Top
  
  instance Hashable n => Hashable (Interval n)
  
  constant :: n -> Interval n
  constant x = Interval x x
  
  withBounds1 :: Ord n => (n -> n) -> Interval n -> Interval n
  withBounds1 f (Interval i1 i2) = Interval (min (f i1) (f i2)) (max (f i1) (f i2))
  
  withBounds2 :: Ord n => (n -> n -> n) -> Interval n -> Interval n -> Interval n
  withBounds2 f (Interval i1 i2) (Interval j1 j2) =
      Interval (minimum [ f x y | x <- [i1,i2], y <- [j1,j2]])
               (maximum [ f x y | x <- [i1,i2], y <- [j1,j2]])
  
  instance (Ord n, Bounded n) => UpperBounded (Interval n) where
    top = Interval minBound maxBound
  
  bounded :: Ord n => Interval (InfiniteNumber n) -> Widening (Interval (InfiniteNumber n))
  bounded (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
    ( if (i1,i2) P.== (r1,r2) || (j1,j2) P.== (r1,r2) then Stable else Unstable
    , Interval r1 r2
    )
    where
      lower = min i1 j1
      upper = max i2 j2
  
      r1 = if | lower P.< lowerBound -> NegInfinity
              | upperBound P.< lower -> upperBound
              | otherwise -> lower
      r2 = if | upperBound P.< upper -> Infinity
              | upper P.< lowerBound -> lowerBound
              | otherwise -> upper
  
  widening :: Ord n => Widening (Interval (InfiniteNumber n))
  widening old@(Interval i1 i2) (Interval j1 j2) =
      let r1 = if j1 >= i1 then i1 else NegInfinity in
      let r2 = if j2 <= i2 then i2 else Infinity in
      let new = Interval r1 r2 in
      (if new ⊑ old then Stable else Unstable, new)
  
  metric :: Metric m n -> Metric (Interval m) (Product n n)
  metric m (Interval i1 i2) (Interval j1 j2) = Product (m i1 j1) (m i2 j2)
  {-# INLINE metric #-}
  