Interval.hs 3.93 KB
Newer Older
Sven Keidel's avatar
Sven Keidel committed
1
{-# LANGUAGE MultiWayIf #-}
2
{-# LANGUAGE DeriveGeneric #-}
3 4
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
Sven Keidel's avatar
Sven Keidel committed
5
module Data.Abstract.Interval where
6

Sven Keidel's avatar
Sven Keidel committed
7
import Prelude hiding (div,Bool(..),(==),(/),(<),Ordering)
8
import qualified Prelude as P
Sven Keidel's avatar
Sven Keidel committed
9 10 11

import Control.DeepSeq

12
import Data.Hashable
13
import Data.Order
Sven Keidel's avatar
Sven Keidel committed
14
import Data.Metric
15 16 17 18
import Data.Numeric

import Data.Abstract.Boolean
import Data.Abstract.Equality
Sven Keidel's avatar
Sven Keidel committed
19
import Data.Abstract.Ordering
Sven Keidel's avatar
Sven Keidel committed
20
import Data.Abstract.Failure
21 22
import Data.Abstract.InfiniteNumbers
import Data.Abstract.Widening
Sven Keidel's avatar
Sven Keidel committed
23
import Data.Abstract.Stable
24

25
import GHC.Generics
26

Sven Keidel's avatar
Sven Keidel committed
27
-- | Intervals represent ranges of numbers. Bot represents the empty interval
28
data Interval n = Interval n n
Sven Keidel's avatar
Sven Keidel committed
29 30 31 32
  deriving (Eq,Generic)

instance Show n => Show (Interval n) where
  show (Interval n m) = "["++ show n ++ "," ++ show m ++"]"
33

34 35
instance Ord x => PreOrd (Interval x) where
  Interval i1 i2  Interval j1 j2 = j1 <= i1 && i2 <= j2
36

37 38
instance Ord x => Complete (Interval x) where
  Interval i1 i2   Interval j1 j2 = Interval (min i1 j1) (max i2 j2)
39

Sven Keidel's avatar
Sven Keidel committed
40 41
instance NFData x => NFData (Interval x)

42
instance (Num n, Ord n) => Num (Interval n) where
Sven Keidel's avatar
Sven Keidel committed
43
  Interval i1 i2 + Interval j1 j2 = Interval (i1 + j1) (i2 + j2)
44
  (*) = withBounds2 (*)
Sven Keidel's avatar
Sven Keidel committed
45
  negate (Interval i1 i2) = Interval (negate i2) (negate i1)
46
  abs (Interval i j)
47 48
    | 0 <= i = Interval i j
    | otherwise = Interval 0 (max i j)
49 50 51
  signum = withBounds1 signum
  fromInteger = constant . fromInteger

52
instance (Integral n, Num n, Ord n) => Numeric (Interval (InfiniteNumber n)) (Failure String) where
Sven Keidel's avatar
Sven Keidel committed
53
  Interval i1 i2 / Interval j1 j2
Sven Keidel's avatar
Sven Keidel committed
54 55 56
    | 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)
Sven Keidel's avatar
Sven Keidel committed
57 58
    | 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))
59 60 61

instance Ord n => Equality (Interval n) where
  Interval i1 i2 == Interval j1 j2
Sven Keidel's avatar
Sven Keidel committed
62 63 64 65 66 67 68
    | 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
69
    | j2 P.<= i1 = False
Sven Keidel's avatar
Sven Keidel committed
70
    | otherwise = Top
71

72 73
instance Hashable n => Hashable (Interval n)

74
constant :: n -> Interval n
Sven Keidel's avatar
Sven Keidel committed
75
constant x = Interval x x
76

77 78
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))
79

80
withBounds2 :: Ord n => (n -> n -> n) -> Interval n -> Interval n -> Interval n
Sven Keidel's avatar
Sven Keidel committed
81
withBounds2 f (Interval i1 i2) (Interval j1 j2) =
Sven Keidel's avatar
Sven Keidel committed
82
    Interval (minimum [ f x y | x <- [i1,i2], y <- [j1,j2]])
83
             (maximum [ f x y | x <- [i1,i2], y <- [j1,j2]])
Sven Keidel's avatar
Sven Keidel committed
84

85 86
instance (Ord n, Bounded n) => UpperBounded (Interval n) where
  top = Interval minBound maxBound
87

Sven Keidel's avatar
Sven Keidel committed
88
bounded :: Ord n => Interval (InfiniteNumber n) -> Widening (Interval (InfiniteNumber n))
Sven Keidel's avatar
Sven Keidel committed
89
bounded (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
Sven Keidel's avatar
Sven Keidel committed
90 91 92
  ( if (i1,i2) P.== (r1,r2) || (j1,j2) P.== (r1,r2) then Stable else Unstable
  , Interval r1 r2
  )
Sven Keidel's avatar
Sven Keidel committed
93 94 95
  where
    lower = min i1 j1
    upper = max i2 j2
Sven Keidel's avatar
Sven Keidel committed
96

Sven Keidel's avatar
Sven Keidel committed
97 98
    r1 = if | lower P.< lowerBound -> NegInfinity
            | upperBound P.< lower -> upperBound
Sven Keidel's avatar
Sven Keidel committed
99
            | otherwise -> lower
Sven Keidel's avatar
Sven Keidel committed
100 101
    r2 = if | upperBound P.< upper -> Infinity
            | upper P.< lowerBound -> lowerBound
Sven Keidel's avatar
Sven Keidel committed
102 103
            | otherwise -> upper

Sven Keidel's avatar
Sven Keidel committed
104 105
widening :: Ord n => Widening (Interval (InfiniteNumber n))
widening (Interval i1 i2) (Interval j1 j2) =
Sven Keidel's avatar
Sven Keidel committed
106 107
  let (r1,r2) = (if i1 P./= j1 then NegInfinity else i1, if i2 P./= j2 then Infinity else i2)
  in (if (i1,i2) P.== (r1,r2) || (j1,j2) P.== (r1,r2) then Stable else Unstable, Interval r1 r2)
Sven Keidel's avatar
Sven Keidel committed
108

Sven Keidel's avatar
Sven Keidel committed
109 110 111
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 #-}