Commit 75999f29 authored by Sven Keidel's avatar Sven Keidel

implement interval division

parent c148cca1
......@@ -57,6 +57,18 @@ instance (Num a, Ord a) => Num (InfiniteNumber a) where
negate NegInfinity = Infinity
negate (Number n) = Number (negate n)
divInf :: Integral n => InfiniteNumber n -> InfiniteNumber n -> InfiniteNumber n
divInf n m = case (n,m) of
(Number _,Infinity) -> Number 0
(Number _,NegInfinity) -> Number 0
(Infinity,Number _) -> signum n * Infinity
(NegInfinity,Number _) -> signum n * NegInfinity
(Number x,Number y) -> Number (x `div` y)
(Infinity,Infinity) -> Infinity
(NegInfinity,Infinity) -> NegInfinity
(Infinity,NegInfinity) -> NegInfinity
(NegInfinity,NegInfinity) -> Infinity
instance Ord a => PreOrd (InfiniteNumber a) where
NegInfinity _ = True
_ NegInfinity = False
......
......@@ -32,7 +32,7 @@ instance Ord x => Complete (Interval x) where
Interval i1 i2 Interval j1 j2 = Interval (min i1 j1) (max i2 j2)
instance (Num n, Ord n) => Num (Interval n) where
Interval i1 i2 + Interval j1 j2 = Interval (i1 + j1) (i2+ j2)
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)
......@@ -41,13 +41,13 @@ instance (Num n, Ord n) => Num (Interval n) where
signum = withBounds1 signum
fromInteger = constant . fromInteger
instance Numeric (Interval Int) (Error String) where
instance (Integral n, Num n, Ord n) => Numeric (Interval (InfiniteNumber n)) (Error 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 (P.div) (Interval i1 i2) (Interval j1 j2))
| otherwise = Success (withBounds2 (P.div) (Interval i1 i2) (Interval j1 j2))
| 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
......
......@@ -33,6 +33,7 @@ import qualified Data.Abstract.Map as M
import Data.Abstract.Terminating hiding(widening)
import Data.Abstract.Widening (Widening)
import Data.Abstract.FreeCompletion(FreeCompletion)
import Data.Abstract.InfiniteNumbers
import Data.Monoidal (Iso(..))
import qualified Data.Abstract.Widening as W
import qualified Data.Abstract.StackWidening as S
......@@ -64,7 +65,7 @@ import Control.Arrow.Transformer.Abstract.Failure
import GHC.Generics
type Addr = FreeCompletion Label
type IV = Interval Int
type IV = Interval (InfiniteNumber Int)
data Val = BoolVal Bool | NumVal IV | Top deriving (Eq,Generic)
run :: (?bound :: IV) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error String (Map Addr Val))
......@@ -116,7 +117,7 @@ instance (ArrowChoice c, ArrowFail String c, Complete (c (Val,String) Val)) => I
BoolVal b -> returnA -< BoolVal (B.not b)
Top -> joined returnA fail -< (BoolVal top, "Expected a boolean as argument for 'not'")
NumVal _ -> fail -< "Expected a boolean as argument for 'not'"
numLit = proc (x,_) -> returnA -< NumVal (I.Interval x x)
numLit = proc (x,_) -> returnA -< NumVal (I.Interval (Number x) (Number x))
add = proc (v1,v2,_) -> case (v1,v2) of
(NumVal n1,NumVal n2) -> returnA -< NumVal (n1 + n2)
_ | v1 == Top || v2 == Top -> joined returnA fail -< (NumVal top, "Expected two numbers as arguments for 'add'")
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment