Commit 34e3e4b3 authored by Sven Keidel's avatar Sven Keidel

move bottom element from abstract domain into arrow

parent f70af8bd
{ mkDerivation, base, containers, hashable, hspec, mtl
, numeric-limits, stdenv, text, unordered-containers
, stdenv, text, unordered-containers
}:
mkDerivation {
pname = "sturdy-lib";
version = "0.1.0.0";
src = ./.;
libraryHaskellDepends = [
base containers hashable mtl numeric-limits text
unordered-containers
base containers hashable mtl text unordered-containers
];
testHaskellDepends = [ base hspec text unordered-containers ];
license = stdenv.lib.licenses.bsd3;
......
......@@ -5,14 +5,14 @@ let
inherit (nixpkgs) pkgs;
f = { mkDerivation, base, containers, hashable, hspec, mtl
, numeric-limits, stdenv, text, unordered-containers, cabal-install
, stdenv, text, unordered-containers, cabal-install
}:
mkDerivation {
pname = "sturdy-lib";
version = "0.1.0.0";
src = ./.;
libraryHaskellDepends = [
base containers hashable mtl numeric-limits text
base containers hashable mtl text
unordered-containers cabal-install
];
testHaskellDepends = [ base hspec text unordered-containers ];
......
......@@ -6,19 +6,20 @@
{-# LANGUAGE Arrows #-}
module Control.Arrow.Transformer.Abstract.Except(Except(..)) where
import Prelude hiding (id,(.),lookup)
import Prelude hiding (id,(.),lookup)
import Control.Category
import Control.Arrow
import Control.Arrow.Environment
import Control.Arrow.Fail
import Control.Arrow.Lift
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Category
import Control.Arrow
import Control.Arrow.Environment
import Control.Arrow.Fail
import Control.Arrow.Lift
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Data.Abstract.Error
import Data.Order
import Data.Abstract.Error
import Data.Order
import Data.Utils
newtype Except e c x y = Except { runExcept :: c x (Error e y) }
......@@ -36,42 +37,12 @@ instance ArrowChoice c => Category (Except r c) where
instance ArrowChoice c => Arrow (Except r c) where
arr f = lift (arr f)
first (Except f) = Except $ first f >>^ injectRight
second (Except f) = Except $ second f >>^ injectLeft
injectRight :: (Error e a,x) -> Error e (a,x)
injectRight (er,x) = case er of
Bot -> Bot
Fail e -> Fail e
Success a -> Success (a,x)
{-# INLINE injectRight #-}
injectLeft :: (x, Error e a) -> Error e (x,a)
injectLeft (x,er) = case er of
Bot -> Bot
Fail e -> Fail e
Success a -> Success (x,a)
{-# INLINE injectLeft #-}
first (Except f) = Except $ first f >>^ strength1
second (Except f) = Except $ second f >>^ strength2
instance ArrowChoice c => ArrowChoice (Except r c) where
left (Except f) = Except $ left f >>^ commuteLeft
right (Except f) = Except $ right f >>^ commuteRight
commuteLeft :: Either (Error e x) y -> Error e (Either x y)
commuteLeft e0 = case e0 of
Left Bot -> Bot
Left (Fail e) -> Fail e
Left (Success x) -> Success (Left x)
Right y -> Success (Right y)
{-# INLINE commuteLeft #-}
commuteRight :: Either x (Error e y) -> Error e (Either x y)
commuteRight e0 = case e0 of
Left x -> Success (Left x)
Right Bot -> Bot
Right (Fail e) -> Fail e
Right (Success x) -> Success (Right x)
{-# INLINE commuteRight #-}
left (Except f) = Except $ left f >>^ costrength1
right (Except f) = Except $ right f >>^ costrength2
instance (ArrowChoice c, ArrowApply c) => ArrowApply (Except e c) where
app = Except $ first runExcept ^>> app
......
......@@ -63,8 +63,8 @@ instance ArrowApply (Fix i o) where
app = Fix $ (\(io,(Fix f,x)) -> (f,(io,x))) ^>> app
#ifdef TRACE
instance (Show x, Show y, Eq x, Hashable x, LowerBounded y, Widening y)
=> ArrowFix x y (CacheArrow x y) where
instance (Show x, Show y, Identifiable x, LowerBounded y, Widening y)
=> ArrowFix x y (Fix x y) where
fixA f = trace (printf "fixA f") $ proc x -> do
old <- getOutCache -< ()
setOutCache -< bottom
......@@ -74,22 +74,24 @@ instance (Show x, Show y, Eq x, Hashable x, LowerBounded y, Widening y)
then returnA -< y
else fixA f -< x
memoize :: (Show x, Show y, Eq x, Hashable x, LowerBounded y, Widening y) => CacheArrow x y x y -> CacheArrow x y x y
memoize :: (Show x, Show y, Identifiable x, LowerBounded y, Widening y) => Fix x y x y -> Fix x y x y
memoize f = proc x -> do
m <- lookupOutCache -< trace (printf "\tmemoize -< %s" (show x)) x
case m of
Just y -> do
Success y -> do
returnA -< trace (printf "\t%s <- memoize -< %s" (show y) (show x)) y
Nothing -> do
Fail _ -> do
yOld <- lookupInCache -< x
writeOutCache -< trace (printf "\tout(%s) := %s" (show x) (show (fromMaybe bottom yOld))) (x, fromMaybe bottom yOld)
writeOutCache -< trace (printf "\tout(%s) := %s" (show x) (show (fromError bottom yOld))) (x, fromError bottom yOld)
y <- f -< trace (printf "\tf -< %s" (show x)) x
yCached <- lookupOutCache -< x
updateOutCache -< (x, y)
yNew <- lookupOutCache -< x
returnA -< trace (printf "\t%s <- f -< %s\n" (show y) (show x) ++
printf "\tout(%s) := %s ▽ %s = %s\n" (show x) (show (fromJust yCached)) (show y) (show yNew) ++
printf "\tout(%s) := %s ▽ %s = %s\n" (show x) (show yCached) (show y) (show yNew) ++
printf "\t%s <- memoize -< %s" (show y) (show x)) y
Bot -> bottom -< ()
#else
instance (Identifiable x, LowerBounded y, Widening y)
......
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Arrows #-}
module Control.Arrow.Transformer.Abstract.Floor where
import Prelude hiding (id,(.),lookup)
import Control.Category
import Control.Arrow
import Control.Arrow.Environment
import Control.Arrow.Fail
import Control.Arrow.Lift
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Data.Abstract.Floored
import Data.Order
import Data.Utils
newtype Floor c x y = Floor { runFloor :: c x (Floored y) }
instance ArrowLift Floor where
lift f = Floor (f >>> arr Greater)
instance ArrowChoice c => Category (Floor c) where
id = lift id
Floor f . Floor g = Floor $ proc x -> do
ey <- g -< x
case ey of
Bottom -> returnA -< Bottom
Greater y -> f -< y
instance ArrowChoice c => Arrow (Floor c) where
arr f = lift (arr f)
first (Floor f) = Floor $ first f >>^ strength1
second (Floor f) = Floor $ second f >>^ strength2
instance ArrowChoice c => ArrowChoice (Floor c) where
left (Floor f) = Floor $ left f >>^ costrength1
right (Floor f) = Floor $ right f >>^ costrength2
instance (ArrowChoice c, ArrowApply c) => ArrowApply (Floor c) where
app = Floor $ first runFloor ^>> app
instance (ArrowChoice c, ArrowState s c) => ArrowState s (Floor c) where
getA = lift getA
putA = lift putA
instance (ArrowChoice c, ArrowFail e c) => ArrowFail e (Floor c) where
failA = lift failA
instance (ArrowChoice c, ArrowReader r c) => ArrowReader r (Floor c) where
askA = lift askA
localA (Floor f) = Floor (localA f)
instance (ArrowChoice c, ArrowEnv x y env c) => ArrowEnv x y env (Floor c) where
lookup = lift lookup
getEnv = lift getEnv
extendEnv = lift extendEnv
localEnv (Floor f) = Floor (localEnv f)
instance (ArrowChoice c, ArrowFix x (Floored y) c) => ArrowFix x y (Floor c) where
fixA f = Floor (fixA (runFloor . f . Floor))
deriving instance PreOrd (c x (Floored y)) => PreOrd (Floor c x y)
deriving instance LowerBounded (c x (Floored y)) => LowerBounded (Floor c x y)
deriving instance Complete (c x (Floored y)) => Complete (Floor c x y)
deriving instance CoComplete (c x (Floored y)) => CoComplete (Floor c x y)
deriving instance UpperBounded (c x (Floored y)) => UpperBounded (Floor c x y)
......@@ -11,10 +11,9 @@ import Data.Order
import GHC.Generics
data Bool = Bot | True | False | Top deriving (Eq,Generic)
data Bool = True | False | Top deriving (Eq,Generic)
instance Show Bool where
show Bot = "⊥"
show True = "True"
show False = "False"
show Top = "⊤"
......@@ -23,44 +22,33 @@ instance Logic Bool where
true = True
false = False
and b1 b2 = case (b1,b2) of
(Bot,_) -> Bot
(_,Bot) -> Bot
(True,True) -> true
(False,_) -> false
(_,False) -> false
(_,_) -> Top
or b1 b2 = case (b1,b2) of
(Bot,_) -> Bot
(_,Bot) -> Bot
(True,_) -> true
(_,True) -> true
(False,False) -> false
(_,_) -> Top
not b = case b of
Bot -> Bot
True -> false
False -> true
Top -> Top
instance PreOrd Bool where
Bot _ = P.True
_ Top = P.True
True True = P.True
False False = P.True
_ _ = P.False
instance Complete Bool where
Bot b = b
b Bot = b
Top _ = Top
_ Top = Top
True True = True
False False = False
_ _ = Top
instance LowerBounded Bool where
bottom = Bot
instance UpperBounded Bool where
top = Top
......
......@@ -35,7 +35,7 @@ instance LowerBounded a => LowerBounded (Bounded a) where
bottom = Bounded bottom bottom
-- | Arithmetic operations are lifted to the elements and bounds are joined. This makes all operations associative.
instance (Num a, LowerBounded a, Complete a, UpperBounded a) => Num (Bounded a) where
instance (Num a, Complete a, UpperBounded a) => Num (Bounded a) where
(+) = lift2 (+)
(*) = lift2 (*)
abs = lift abs
......
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
module Data.Abstract.FreeCoCompletion where
module Data.Abstract.Floored where
import Data.Order
import Control.Monad
import Control.Applicative
data FreeCoCompletion a = Bottom | Greater a deriving (Functor,Traversable,Foldable)
import Data.Order
import Data.Abstract.Widening
-- Free cocompletion of a type
data Floored a = Bottom | Greater a deriving (Eq,Functor,Traversable,Foldable)
instance Show a => Show (FreeCoCompletion a) where
instance Show a => Show (Floored a) where
show Bottom = "⊥"
show (Greater a) = show a
instance Applicative FreeCoCompletion where
instance Applicative Floored where
pure = return
(<*>) = ap
instance Monad FreeCoCompletion where
instance Monad Floored where
return = Greater
Greater x >>= k = k x
Bottom >>= _ = Bottom
instance PreOrd a => PreOrd (FreeCoCompletion a) where
Bottom _ = False
instance PreOrd a => PreOrd (Floored a) where
Bottom _ = True
_ Bottom = False
Greater a Greater b = a b
......@@ -30,12 +33,17 @@ instance PreOrd a => PreOrd (FreeCoCompletion a) where
Greater a Greater b = a b
_ _ = False
instance Complete a => Complete (FreeCoCompletion a) where
instance Complete a => Complete (Floored a) where
Greater a Greater b = Greater (a b)
x Bottom = x
Bottom y = y
instance PreOrd a => CoComplete (FreeCoCompletion a) where
instance Widening a => Widening (Floored a) where
Greater a Greater b = Greater (a b)
x Bottom = x
Bottom y = y
instance PreOrd a => CoComplete (Floored a) where
Greater a Greater b
| a b = Greater a
| b a = Greater b
......@@ -43,13 +51,13 @@ instance PreOrd a => CoComplete (FreeCoCompletion a) where
Bottom _ = Bottom
_ Bottom = Bottom
instance UpperBounded a => UpperBounded (FreeCoCompletion a) where
instance UpperBounded a => UpperBounded (Floored a) where
top = Greater top
instance PreOrd a => LowerBounded (FreeCoCompletion a) where
instance PreOrd a => LowerBounded (Floored a) where
bottom = Bottom
instance Num a => Num (FreeCoCompletion a) where
instance Num a => Num (Floored a) where
(+) = liftA2 (+)
(*) = liftA2 (*)
negate = fmap negate
......@@ -57,6 +65,6 @@ instance Num a => Num (FreeCoCompletion a) where
signum = fmap signum
fromInteger = pure . fromInteger
instance Fractional a => Fractional (FreeCoCompletion a) where
instance Fractional a => Fractional (Floored a) where
(/) = liftA2 (/)
fromRational = pure . fromRational
......@@ -57,31 +57,35 @@ instance (Num a, Ord a) => Num (InfiniteNumber a) where
negate NegInfinity = Infinity
negate (Number n) = Number (negate n)
instance PreOrd a => PreOrd (InfiniteNumber a) where
instance Ord a => PreOrd (InfiniteNumber a) where
NegInfinity _ = True
_ NegInfinity = False
_ Infinity = True
Infinity _ = False
Number n Number m = n m
Number n Number m = n <= m
instance PreOrd a => LowerBounded (InfiniteNumber a) where
instance Ord a => LowerBounded (InfiniteNumber a) where
bottom = NegInfinity
instance PreOrd a => UpperBounded (InfiniteNumber a) where
instance Ord a => UpperBounded (InfiniteNumber a) where
top = Infinity
instance (PreOrd a, Complete a) => Complete (InfiniteNumber a) where
instance Ord a => Complete (InfiniteNumber a) where
NegInfinity x = x
x NegInfinity = x
Infinity _ = Infinity
_ Infinity = Infinity
Number n Number m = Number (n m)
Number n Number m = Number (max n m)
instance (PreOrd a, CoComplete a) => CoComplete (InfiniteNumber a) where
instance Ord a => CoComplete (InfiniteNumber a) where
NegInfinity _ = NegInfinity
_ NegInfinity = NegInfinity
Infinity x = x
x Infinity = x
Number n Number m = Number (n m)
Number n Number m = Number (min n m)
instance Bounded (InfiniteNumber n) where
minBound = NegInfinity
maxBound = Infinity
instance Hashable a => Hashable (InfiniteNumber a)
......@@ -6,42 +6,31 @@ import Data.Order
import GHC.Generics
-- | Intervals represent ranges of numbers. Bot represents the empty interval
data Interval n = Bot | Interval n n
data Interval n = Interval n n
deriving (Eq,Generic)
instance Show n => Show (Interval n) where
show Bot = "⊥"
show (Interval n m) = "["++ show n ++ "," ++ show m ++"]"
instance PreOrd x => PreOrd (Interval x) where
Bot _ = True
_ Bot = False
Interval i1 i2 Interval j1 j2 = j1 i1 && i2 j2
instance Ord x => PreOrd (Interval x) where
Interval i1 i2 Interval j1 j2 = j1 <= i1 && i2 <= j2
instance (Complete x, CoComplete x) => Complete (Interval x) where
Bot x = x
x Bot = x
Interval i1 i2 Interval j1 j2 = Interval (i1 j1) (i2 j2)
instance Ord x => Complete (Interval x) where
Interval i1 i2 Interval j1 j2 = Interval (min i1 j1) (max i2 j2)
instance (Num n, Complete n, LowerBounded n, CoComplete n, UpperBounded n) => Num (Interval n) where
Bot + _ = Bot
_ + Bot = Bot
Interval i1 i2 + Interval j1 j2 = Interval (i1+ j1) (i2+ j2)
instance (Num n, Ord n) => Num (Interval n) where
Interval i1 i2 + Interval j1 j2 = Interval (i1 + j1) (i2+ j2)
(*) = withBounds2 (*)
negate Bot = Bot
negate (Interval i1 i2) = Interval (negate i2) (negate i1)
abs Bot = Bot
abs (Interval i j)
| 0 i = Interval i j
| otherwise = Interval 0 (i j)
| 0 <= i = Interval i j
| otherwise = Interval 0 (max i j)
signum = withBounds1 signum
fromInteger = constant . fromInteger
instance (Fractional n, Complete n, LowerBounded n, CoComplete n, UpperBounded n) => Fractional (Interval n) where
Bot / _ = Bot
_ / Bot = Bot
instance (Fractional n, Ord n, LowerBounded n, UpperBounded n) => Fractional (Interval n) where
Interval i1 i2 / Interval j1 j2
| j1 0 && 0 j2 = Interval bottom top
| j1 <= 0 && 0 <= j2 = Interval bottom top
| otherwise = withBounds2 (/) (Interval i1 i2) (Interval j1 j2)
fromRational = constant . fromRational
......@@ -50,20 +39,13 @@ instance Hashable n => Hashable (Interval n)
constant :: n -> Interval n
constant x = Interval x x
withBounds1 :: (Complete n, CoComplete n) => (n -> n) -> Interval n -> Interval n
withBounds1 f (Interval i1 i2) = Interval (f i1 f i2) (f i1 f i2)
withBounds1 _ Bot = Bot
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 :: (Complete n, LowerBounded n, CoComplete n, UpperBounded n) =>
(n -> n -> n) -> Interval n -> Interval n -> Interval n
withBounds2 :: Ord n => (n -> n -> n) -> Interval n -> Interval n -> Interval n
withBounds2 f (Interval i1 i2) (Interval j1 j2) =
Interval (glb [ f x y | x <- [i1,i2], y <- [j1,j2]])
(lub [ f x y | x <- [i1,i2], y <- [j1,j2]])
withBounds2 _ Bot _ = Bot
withBounds2 _ _ Bot = Bot
Interval (minimum [ f x y | x <- [i1,i2], y <- [j1,j2]])
(maximum [ f x y | x <- [i1,i2], y <- [j1,j2]])
instance PreOrd n => LowerBounded (Interval n) where
bottom = Bot
instance (LowerBounded n, UpperBounded n) => UpperBounded (Interval n) where
top = Interval bottom top
instance (Ord n, Bounded n) => UpperBounded (Interval n) where
top = Interval minBound maxBound
......@@ -7,20 +7,16 @@ import Data.Abstract.Widening
import GHC.Generics
data Sign = Bot | Negative | Zero | Positive | Top
data Sign = Negative | Zero | Positive | Top
deriving (Show,Eq,Generic)
instance Num Sign where
Bot + _ = Bot
_ + Bot = Bot
Negative + Negative = Negative
Positive + Positive = Positive
Zero + x = x
x + Zero = x
_ + _ = Top
Bot * _ = Bot
_ * Bot = Bot
Negative * Negative = Positive
Positive * Negative = Negative
Negative * Positive = Negative
......@@ -34,7 +30,6 @@ instance Num Sign where
negate Positive = Negative
negate Negative = Positive
negate Top = Top
negate Bot = Bot
abs Zero = Zero
abs _ = Positive
......@@ -43,7 +38,6 @@ instance Num Sign where
signum Positive = Positive
signum Zero = Zero
signum Top = Top
signum Bot = Bot
fromInteger n
| n == 0 = Zero
......@@ -51,16 +45,12 @@ instance Num Sign where
| otherwise = Positive
instance PreOrd Sign where
Bot _ = True
_ Top = True
Negative Negative = True
Zero Zero = True
Positive Positive = True
_ _ = False
instance Complete Sign where
Bot y = y
x Bot = x
Negative Negative = Negative
Zero Zero = Zero
Positive Positive = Positive
......@@ -68,9 +58,6 @@ instance Complete Sign where
instance Widening Sign
instance LowerBounded Sign where
bottom = Bot
instance UpperBounded Sign where
top = Top
......
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
module Data.Abstract.FreeCompletion where
module Data.Abstract.Topped where
import Data.Order
import Control.Monad
import Control.Applicative
data FreeCompletion a = Lower a | Top deriving (Functor,Traversable,Foldable)
data Topped a = Lower a | Top deriving (Functor,Traversable,Foldable)
instance Show a => Show (FreeCompletion a) where
instance Show a => Show (Topped a) where
show Top = "⊤"
show (Lower a) = show a
instance Applicative FreeCompletion where
instance Applicative Topped where
pure = return
(<*>) = ap
instance Monad FreeCompletion where
instance Monad Topped where
return = Lower
Lower x >>= k = k x
Top >>= _ = Top
instance PreOrd a => PreOrd (FreeCompletion a) where
instance PreOrd a => PreOrd (Topped a) where
_ Top = True
Top _ = False
Lower a Lower b = a b
......@@ -30,7 +30,7 @@ instance PreOrd a => PreOrd (FreeCompletion a) where
Lower a Lower b = a b
_ _ = False
instance PreOrd a => Complete (FreeCompletion a) where
instance PreOrd a => Complete (Topped a) where
Lower a Lower b
| a b = Lower b