use ArrowFix to expose inputs and outputs for fixpoint algorithm.

parent c200468f
......@@ -7,6 +7,7 @@
{-# LANGUAGE StandaloneDeriving #-}
module Control.Arrow.Transformer.BoundedEnvironment(BoundedEnv,runBoundedEnv,liftBoundedEnv,Alloc) where
import Prelude hiding ((.))
import Control.Category
import Control.Arrow
import Control.Arrow.Class.Environment
......@@ -14,6 +15,7 @@ import Control.Arrow.Class.Reader
import Control.Arrow.Class.State
import Control.Arrow.Class.Fail
import Control.Arrow.Class.Config
import Control.Arrow.Class.Fix
import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.State
import Control.Arrow.Utils
......@@ -86,6 +88,20 @@ instance (Eq a, Hashable a, Eq addr, Hashable addr, Complete b, ArrowConfig cIn
getOutConfig = getStore &&& liftBoundedEnv getOutConfig
setOutConfig = voidA $ putStore *** liftBoundedEnv setOutConfig
instance (ArrowApply c, ArrowFix (HashMap a addr,Store addr b,x) (Store addr b,y) c) => ArrowFix x y (BoundedEnv a addr b c) where
fixA f = lift $ proc (a,e,s,x) -> do
fixA (unlift a . f . lift') -<< (e,s,x)
where
lift :: Arrow c => c (Alloc a addr b c, HashMap a addr,Store addr b,x) (Store addr b,y) -> BoundedEnv a addr b c x y
lift g = BoundedEnv (ReaderArrow (StateArrow ((\(s,((a,e),x)) -> (a,e,s,x)) ^>> g)))
lift' :: Arrow c => c (HashMap a addr,Store addr b,x) (Store addr b,y) -> BoundedEnv a addr b c x y
lift' g = BoundedEnv (ReaderArrow (StateArrow ((\(s,((_,e),x)) -> (e,s,x)) ^>> g)))
unlift :: Arrow c => Alloc a addr b c -> BoundedEnv a addr b c x y -> c (HashMap a addr,Store addr b,x) (Store addr b,y)
unlift a (BoundedEnv (ReaderArrow (StateArrow g))) = (\(s,e,x) -> (e,((a,s),x))) ^>> g
deriving instance PreOrd (c (Store addr b,((Alloc a addr b c,HashMap a addr),x)) (Store addr b,y)) => PreOrd (BoundedEnv a addr b c x y)
deriving instance Complete (c (Store addr b,((Alloc a addr b c,HashMap a addr),x)) (Store addr b,y)) => Complete (BoundedEnv a addr b c x y)
deriving instance CoComplete (c (Store addr b,((Alloc a addr b c,HashMap a addr),x)) (Store addr b,y)) => CoComplete (BoundedEnv a addr b c x y)
......
......@@ -7,6 +7,8 @@
{-# LANGUAGE Arrows #-}
module Control.Arrow.Transformer.Environment where
import Prelude hiding ((.))
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as H
import Data.Hashable
......@@ -20,6 +22,7 @@ import Control.Arrow.Class.State
import Control.Arrow.Class.Fail
import Control.Arrow.Class.Environment
import Control.Arrow.Class.Config
import Control.Arrow.Class.Fix
newtype Environment a b c x y = Environment (ReaderArrow (HashMap a b) c x y)
deriving (Category,Arrow,ArrowChoice)
......@@ -57,6 +60,8 @@ instance (Eq a, Hashable a, ArrowConfig cIn cOut c) => ArrowConfig (HashMap a b,
getOutConfig = liftEnv getOutConfig
setOutConfig = liftEnv setOutConfig
instance (ArrowFix (HashMap a b,x) y c) => ArrowFix x y (Environment a b c) where
fixA f = Environment (ReaderArrow (fixA (runEnvironment . f . Environment . ReaderArrow)))
deriving instance PreOrd (c (HashMap a b,x) y) => PreOrd (Environment a b c x y)
deriving instance Complete (c (HashMap a b,x) y) => Complete (Environment a b c x y)
......
......@@ -5,7 +5,7 @@
{-# LANGUAGE StandaloneDeriving #-}
module Control.Arrow.Transformer.Fail(ErrorArrow(..),liftError) where
import Prelude hiding (id,lookup)
import Prelude hiding (id,(.),lookup)
import Control.Category
import Control.Arrow
......@@ -14,6 +14,7 @@ import Control.Arrow.Class.Reader
import Control.Arrow.Class.State
import Control.Arrow.Class.Environment
import Control.Arrow.Class.Config
import Control.Arrow.Class.Fix
import Control.Monad (join)
import Data.Error
......@@ -89,6 +90,9 @@ instance (ArrowChoice c, ArrowConfig cIn cOut c) => ArrowConfig cIn cOut (ErrorA
getOutConfig = liftError getOutConfig
setOutConfig = liftError setOutConfig
instance (ArrowChoice c, ArrowFix x (Error e y) c) => ArrowFix x y (ErrorArrow e c) where
fixA f = ErrorArrow (fixA (runErrorArrow . f . ErrorArrow))
deriving instance PreOrd (c x (Error e y)) => PreOrd (ErrorArrow e c x y)
deriving instance LowerBounded (c x (Error e y)) => LowerBounded (ErrorArrow e c x y)
deriving instance Complete (c x (Error e y)) => Complete (ErrorArrow e c x y)
......
......@@ -7,7 +7,7 @@
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonoLocalBinds #-}
module Control.Arrow.Transformer.FixpointCache(CacheArrow,runCacheArrow,liftCache) where
module Control.Arrow.Transformer.FixpointCache(CacheArrow,runCacheArrow,runCacheArrow',liftCache) where
import Prelude hiding (id,(.),lookup)
import Data.Function (fix)
......@@ -31,7 +31,10 @@ import qualified Data.Store as S
newtype CacheArrow a b c x y = CacheArrow (c ((Store a b,Store a b),x) (Store a b,y))
runCacheArrow :: Arrow c => CacheArrow a b c x y -> c x y
runCacheArrow (CacheArrow f) = (\x -> ((S.empty,S.empty),x)) ^>> f >>^ snd
runCacheArrow f = runCacheArrow' f >>^ snd
runCacheArrow' :: Arrow c => CacheArrow a b c x y -> c x (Store a b,y)
runCacheArrow' (CacheArrow f) = (\x -> ((S.empty,S.empty),x)) ^>> f
liftCache :: Arrow c => c x y -> CacheArrow a b c x y
liftCache f = CacheArrow ((\((_,o),x) -> (o,x)) ^>> second f)
......@@ -72,30 +75,50 @@ instance ArrowEnv a b env c => ArrowEnv a b env (CacheArrow x y c) where
localEnv (CacheArrow f) = CacheArrow $ (\(s,(env,a)) -> (env,(s,a))) ^>> localEnv f
instance ArrowConfig cIn cOut c => ArrowConfig cIn cOut (CacheArrow cIn cOut c) where
getInConfig = liftCache getInConfig
getOutConfig = liftCache getOutConfig
setOutConfig = liftCache setOutConfig
instance (Eq x, Eq cIn, Hashable x, Hashable cIn, LowerBounded y, Complete y, LowerBounded cOut, Complete cOut, ArrowConfig cIn cOut c, ArrowChoice c) => ArrowFix x y (CacheArrow (x,cIn) (y,cOut) c) where
instance (Show x, Show y, Eq x, Hashable x, LowerBounded y, Complete y, ArrowChoice c) => ArrowFix x y (CacheArrow x y c) where
fixA f = proc x -> do
(y,fp) <- retireCache (fix (f . memoize) &&& reachedFixpoint) -< x
if fp
then returnA -< y
else fixA f -< x
memoize :: (Eq (x,cIn), Hashable (x,cIn), LowerBounded (y,cOut), Complete (y,cOut), ArrowConfig cIn cOut c, ArrowChoice c) => CacheArrow (x,cIn) (y,cOut) c x y -> CacheArrow (x,cIn) (y,cOut) c x y
memoize :: (Eq x, Hashable x, LowerBounded y, Complete y, ArrowChoice c) => CacheArrow x y c x y -> CacheArrow x y c x y
memoize f = proc x -> do
cIn <- liftCache getInConfig -< ()
m <- askCache -< (x,cIn)
m <- askCache -< x
case m of
Just (y,cOut) -> do
liftCache setOutConfig -< cOut
returnA -< y
Just y -> returnA -< y
Nothing -> do
initializeCache -< (x,cIn)
initializeCache -< x
y <- f -< x
cOut <- liftCache getOutConfig -< ()
updateCache -< ((x,cIn),(y,cOut))
updateCache -< (x,y)
returnA -< y
-- instance (Eq (x,cIn), Hashable (x,cIn), LowerBounded (y,cOut), Complete (y,cOut), ArrowConfig cIn cOut c, ArrowChoice c) => ArrowFix x y (CacheArrow (x,cIn) (y,cOut) c) where
-- fixA f = proc x -> do
-- (y,fp) <- retireCache (fix (f . memoize) &&& reachedFixpoint) -< x
-- if fp
-- then returnA -< y
-- else fixA f -< x
-- memoize :: (Eq (x,cIn), Hashable (x,cIn), LowerBounded (y,cOut), Complete (y,cOut), ArrowConfig cIn cOut c, ArrowChoice c) => CacheArrow (x,cIn) (y,cOut) c x y -> CacheArrow (x,cIn) (y,cOut) c x y
-- memoize f = proc x -> do
-- cIn <- liftCache getInConfig -< ()
-- m <- askCache -< (x,cIn)
-- case m of
-- Just (y,cOut) -> do
-- liftCache setOutConfig -< cOut
-- returnA -< y
-- Nothing -> do
-- initializeCache -< (x,cIn)
-- y <- f -< x
-- cOut <- liftCache getOutConfig -< ()
-- updateCache -< ((x,cIn),(y,cOut))
-- returnA -< y
askCache :: (Eq x, Hashable x, Arrow c) => CacheArrow x y c x (Maybe y)
askCache = CacheArrow $ arr $ \((_,o),x) -> (o,S.lookup x o)
......@@ -108,7 +131,7 @@ initializeCache = CacheArrow $ arr $ \((i,o),x) -> (S.insert x (fromMaybe bottom
updateCache :: (Eq a, Hashable a, Complete b, Arrow c) => CacheArrow a b c (a,b) ()
updateCache = CacheArrow $ arr $ \((_,o),(x,y)) -> (S.insertWith () x y o,())
reachedFixpoint :: (Eq a, Hashable a, LowerBounded b, Arrow c) => CacheArrow a b c x Bool
reachedFixpoint :: (Show a, Show b, Eq a, Hashable a, LowerBounded b, Arrow c) => CacheArrow a b c x Bool
reachedFixpoint = CacheArrow $ arr $ \((i,o),_) -> (o,o i)
deriving instance PreOrd (c ((Store a b,Store a b),x) (Store a b,y)) => PreOrd (CacheArrow a b c x y)
......
......@@ -15,6 +15,7 @@ import Control.Arrow.Class.Reader
import Control.Arrow.Class.State
import Control.Arrow.Class.Environment
import Control.Arrow.Class.Config
import Control.Arrow.Class.Fix
import Control.Arrow.Utils
import Data.Order
......@@ -62,6 +63,9 @@ instance ArrowConfig cIn cOut c => ArrowConfig (r,cIn) cOut (ReaderArrow r c) wh
getOutConfig = liftReader getOutConfig
setOutConfig = liftReader setOutConfig
instance ArrowFix (r,x) y c => ArrowFix x y (ReaderArrow r c) where
fixA f = ReaderArrow (fixA (runReaderArrow . f . ReaderArrow))
deriving instance PreOrd (c (r,x) y) => PreOrd (ReaderArrow r c x y)
deriving instance LowerBounded (c (r,x) y) => LowerBounded (ReaderArrow r c x y)
deriving instance Complete (c (r,x) y) => Complete (ReaderArrow r c x y)
......
......@@ -14,6 +14,7 @@ import Control.Arrow.Class.State
import Control.Arrow.Class.Reader
import Control.Arrow.Class.Environment
import Control.Arrow.Class.Config
import Control.Arrow.Class.Fix
import Control.Arrow.Utils
import Data.Order
......@@ -62,6 +63,9 @@ instance ArrowConfig cIn cOut c => ArrowConfig (s,cIn) (s,cOut) (StateArrow s c)
getOutConfig = getA &&& liftState getOutConfig
setOutConfig = voidA (putA *** liftState setOutConfig)
instance ArrowFix (s,x) (s,y) c => ArrowFix x y (StateArrow s c) where
fixA f = StateArrow (fixA (runStateArrow . f . StateArrow))
deriving instance PreOrd (c (s,x) (s,y)) => PreOrd (StateArrow s c x y)
deriving instance LowerBounded (c (s,x) (s,y)) => LowerBounded (StateArrow s c x y)
deriving instance Complete (c (s,x) (s,y)) => Complete (StateArrow s c x y)
......
......@@ -33,6 +33,9 @@ instance Complete a => Complete (Error e a) where
instance PreOrd a => LowerBounded (Error String a) where
bottom = Error "Bottom"
instance (PreOrd b, LowerBounded a) => LowerBounded (Error a b) where
bottom = Error bottom
instance UpperBounded a => UpperBounded (Error e a) where
top = Success top
......
......@@ -9,7 +9,6 @@ import Data.Map (Map)
import qualified Data.Map as Map
import Data.Order
import Data.Powerset
import Data.Functor.Identity
-- | A galois connection consisting of an abstraction function alpha
-- and a concretization function gamma between two pre-ordered sets
......
......@@ -31,6 +31,8 @@ instance (Num n, Complete n, LowerBounded n, CoComplete n, UpperBounded n) => Nu
fromInteger = constant . fromInteger
instance (Fractional n, Complete n, LowerBounded n, CoComplete n, UpperBounded n) => Fractional (Interval n) where
Bot / _ = Bot
_ / Bot = Bot
Interval i1 i2 / Interval j1 j2
| j1 0 && 0 j2 = Interval bottom top
| otherwise = withBounds2 (/) (Interval i1 i2) (Interval j1 j2)
......@@ -43,12 +45,15 @@ 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
withBounds2 :: (Complete n, LowerBounded n, CoComplete n, UpperBounded 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
instance PreOrd n => LowerBounded (Interval n) where
bottom = Bot
......
......@@ -73,7 +73,7 @@ instance PreOrd a => PreOrd [a] where
(a:as) (b:bs) = a b && as bs
_ _ = False
instance (PreOrd a) => PreOrd (Set a) where
instance PreOrd a => PreOrd (Set a) where
s1 s2 = all (\x -> any (\y -> x y) s2) s1
instance (Ord a, PreOrd a) => Complete (Set a) where
......@@ -85,6 +85,12 @@ instance (Ord a, PreOrd a) => CoComplete (Set a) where
instance PreOrd () where
() () = True
instance LowerBounded () where
bottom = ()
instance UpperBounded () where
top = ()
instance Complete () where
() () = ()
......@@ -94,6 +100,9 @@ instance (PreOrd a,PreOrd b) => PreOrd (a,b) where
instance (LowerBounded a,LowerBounded b) => LowerBounded (a,b) where
bottom = (bottom,bottom)
instance (UpperBounded a,UpperBounded b) => UpperBounded (a,b) where
top = (top,top)
instance (Complete a, Complete b) => Complete (a,b) where
(a1,b1) (a2,b2) = (a1 a2, b1 b2)
......@@ -158,7 +167,7 @@ instance Complete Double where
instance CoComplete Double where
() = min
instance (Ord a, PreOrd a) => LowerBounded (Set a) where
instance PreOrd a => LowerBounded (Set a) where
bottom = S.empty
instance (Ord k, PreOrd v) => LowerBounded (Map k v) where
......
......@@ -51,6 +51,9 @@ instance Num Sign where
instance PreOrd Sign where
Bot _ = True
_ Top = True
Negative Negative = True
Zero Zero = True
Positive Positive = True
_ _ = False
instance Complete Sign where
......
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
module Data.Store(Store,subsetKeys,empty,lookup,insert,insertWith,(!),keys,toList) where
module Data.Store(Store,subsetKeys,empty,lookup,insert,insertWith,(!),keys,toList,fromList) where
import Prelude hiding (lookup)
......@@ -12,7 +12,7 @@ import Data.HashSet (HashSet)
import qualified Data.HashSet as S
import Text.Printf
newtype Store a b = Store (HashMap a b) deriving (Functor,Foldable,Traversable)
newtype Store a b = Store (HashMap a b) deriving (Eq,Functor,Foldable,Traversable)
instance (Show a,Show b) => Show (Store a b) where
show (Store h)
......@@ -58,3 +58,6 @@ keys (Store m) = H.keys m
toList :: Store a b -> [(a,b)]
toList (Store m) = H.toList m
fromList :: (Eq a, Hashable a) => [(a,b)] -> Store a b
fromList l = Store (H.fromList l)
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
module FixpointCacheSpec where
import Prelude hiding (lookup)
......@@ -7,25 +11,45 @@ import Data.Function
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Fail
import Data.Interval (Interval)
import Data.Sign (Sign)
import Data.Order
import Data.Error
import qualified Data.Store as S
import Test.Hspec
main :: IO ()
main = hspec spec
type Cache x y = CacheArrow x y (->) x y
type CacheError x y = CacheArrow x y (ErrorArrow () (->)) x y
-- CacheArrow x y (ErrorArrow () (->)) a b
-- = (ErrorArrow () (->)) ((Store x y,Store x y),a) (Store x y,b)
-- = ((Store x y,Store x y),a) -> Error () (Store x y,b)
type ErrorCache x y = ErrorArrow () (CacheArrow x (Error () y) (->)) x y
-- ErrorArrow () (CacheArrow x (Error () y) (->)) a b
-- = (CacheArrow x (Error () y) (->)) a (Error () b)
-- = (CacheArrow x (Error () y) (->)) ((Store x y,Store x y),a) (Store x y,Error () b)
spec :: Spec
spec = do
it "fib" $ do
runCacheArrow (fixA fib) 10 `shouldBe` fix fib 10
runCacheArrow (fixA fib) 15 `shouldBe` fix fib 15
runCacheArrow (fixA fib :: Cache Int (Interval Int)) 10 `shouldBe` fix fib 10
runCacheArrow (fixA fib :: Cache Int (Interval Int)) 15 `shouldBe` fix fib 15
describe "the analyis of a diverging program" $
it "should terminate with bottom" $ do
runCacheArrow (fixA diverge) 5 `shouldBe` bottom
runCacheArrow (fixA diverge :: Cache Int Sign) 5 `shouldBe` bottom
describe "the analysis of a failing program" $
it "should" $ do
runErrorArrow (runCacheArrow (fixA recurseFail :: CacheError Int Sign)) 5 `shouldBe` Success 0
runCacheArrow' (runErrorArrow (fixA recurseFail :: ErrorCache Int Sign)) 5 `shouldBe` (S.fromList [(n,Success 0) | n <- [0..4]], Success 0)
where
fib :: ArrowChoice c => c Int (Interval Int) -> c Int (Interval Int)
......@@ -42,4 +66,8 @@ spec = do
0 -> f -< 0
_ -> f -< (n-1)
recurseFail :: (ArrowFail () c, Complete (c ((),Sign) Sign), ArrowChoice c) => c Int Sign -> c Int Sign
recurseFail f = proc n -> case n of
0 -> joined failA returnA -< ((),0)
_ -> f -< (n-1)
......@@ -20,7 +20,7 @@ import Data.Hashable
import Data.Order
import Data.Powerset
import qualified Data.Sign as Sign
import Data.Sign hiding (Top)
import Data.Sign hiding (Bot,Top)
import Data.Text (Text)
import GHC.Generics
......
{-# LANGUAGE OverloadedStrings #-}
module IntervalAnalysisSpec where
import SharedSpecs
import Data.Bounded
import Data.Error
import qualified Data.HashMap.Lazy as M
import qualified Data.Interval as I
import qualified Data.Powerset as P
import qualified Data.Text as T
import IntervalAnalysis
import qualified PCF as E
import PCF
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec = describe "evalInterval" $ do
it "should look up a bound variable" $
let k = "x"; v = NumVal 5
in evalInterval lim (M.singleton k v) (E.Var k) `shouldBe` Success v
it "should fail when looking up an unbound variable" $
evalInterval lim M.empty (E.Var "x") `shouldBe` Error "Variable \"x\" not bound"
it "should create a closure" $
let v = E.Succ (E.Var "x")
in evalInterval lim M.empty (E.Lam "x" v) `shouldBe` Success (ClosureVal (P.singleton (Closure "x" v M.empty)))
it "should apply a function" $
evalInterval lim M.empty (E.App (E.Lam "x" (E.Succ "x")) E.Zero) `shouldBe` Success (NumVal (Bounded lim 1))
it "should fail when applying something other than a function" $
evalInterval lim M.empty (E.App E.Zero E.Zero) `shouldBe` Error "Expected a closure"
--it "will recurse infinitely when using Y" $
-- evalInterval M.empty (E.Y (E.Succ E.Zero)) `shouldBe` Success (NumVal (IV (1, 1)))
it "should correctly give the interval of zero" $
evalInterval lim M.empty E.Zero `shouldBe` Success (NumVal (Bounded lim 0))
it "should correctly give the interval of succ of 0" $
evalInterval lim M.empty (E.Succ E.Zero) `shouldBe` Success (NumVal (Bounded lim 1))
it "should correctly give the interval of succ of succ of 0" $
evalInterval lim M.empty (E.Succ (E.Succ E.Zero)) `shouldBe` Success (NumVal (Bounded lim 2))
it "should correctly give the interval of pred of 0" $
evalInterval lim M.empty (E.Pred E.Zero) `shouldBe` Success (NumVal (Bounded lim (-1)))
it "should correctly give the interval of pred of pred of 0" $
evalInterval lim M.empty (E.Pred (E.Pred E.Zero)) `shouldBe` Success (NumVal (Bounded lim (-2)))
it "should correctly give the interval of pred of succ of 0" $
evalInterval lim M.empty (E.Pred (E.Succ E.Zero)) `shouldBe` Success (NumVal (Bounded lim 0))
it "should correctly give the interval of succ of pred of 0" $
evalInterval lim M.empty (E.Succ (E.Pred E.Zero)) `shouldBe` Success (NumVal (Bounded lim 0))
it "should fail when using succ on something other than a number" $
let bogus = E.Lam (T.singleton 'x') E.Zero
in evalInterval lim M.empty (E.Succ bogus) `shouldBe` Error "Expected a number as argument for 'succ'"
it "should fail when using pred on something other than a number" $
let bogus = E.Lam (T.singleton 'x') E.Zero
in evalInterval lim M.empty (E.Pred bogus) `shouldBe` Error "Expected a number as argument for 'pred'"
it "should execute the then branch on IfZero on zero" $
evalInterval lim M.empty (E.IfZero E.Zero (E.Succ E.Zero) E.Zero)
`shouldBe` Success (NumVal (Bounded lim 1))
it "should execute the else branch on IfZero on completely non-zero" $
evalInterval lim M.empty (E.IfZero (E.Succ E.Zero) (E.Succ E.Zero) E.Zero)
`shouldBe` Success (NumVal (Bounded lim 0))
-- TODO: it seems that the current implementation cannot ever get here.
spec = do
sharedSpec (evalInterval lim) (NumVal . Bounded lim . fromIntegral)
describe "behavior specific to interval analysis" $ do
it "should execute both branches on IfZero on interval containing zero" $
-- evalInterval M.empty (E.IfZero (E.Succ E.Zero) (E.Succ E.Zero) E.Zero)
-- `shouldBe` Success (NumVal (IV (0, 0)))
pendingWith "it seems that the current implementation cannot ever get here"
let intervalWithZero = NumVal (Bounded lim (I.Interval (-5) 5))
in evalInterval lim (M.fromList [("x", intervalWithZero)])
(IfZero "x" (Succ E.Zero) (E.Pred E.Zero))
`shouldBe` Success (NumVal (Bounded lim (I.Interval (-1) 1)))
it "should fail when using a non-number condition for IfZero" $
let bogus = E.Lam (T.singleton 'x') E.Zero
in evalInterval lim M.empty (E.IfZero bogus E.Zero E.Zero) `shouldBe` Error "Expected a number as condition for 'ifZero'"
it "should compute 0 + -1 + 1 = 0" $
evalInterval lim M.empty (E.Succ (E.Pred E.Zero)) `shouldBe`
Success (NumVal (Bounded lim 0))
where
lim = I.Interval (-100) 100
where
lim = I.Interval (-100) 100
{-# LANGUAGE OverloadedStrings #-}
module SharedSpecs where
import Data.Error
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Text (Text)
import PCF (Expr)
import qualified PCF as E
import Test.Hspec
sharedSpec :: (Show v, Eq v) => (HashMap Text v -> Expr -> Error String v) -> (Int -> v)-> Spec
sharedSpec eval fromInt = describe "shared language behavior" $ do
it "should look up a bound variable" $
eval (M.singleton "x" (fromInt 5)) "x" `shouldBe` Success (fromInt 5)
it "should fail when looking up an unbound variable" $
eval M.empty "x" `shouldBe` Error "Variable \"x\" not bound"
it "should apply a function" $
eval M.empty (E.App (E.Lam "x" (E.Succ "x")) E.Zero) `shouldBe` Success (fromInt 1)
it "should fail when applying something other than a function" $
eval M.empty (E.App E.Zero E.Zero) `shouldBe` Error "Expected a closure"
it "should compute 0 + 1 + 1 = 2" $
eval M.empty (E.Succ (E.Succ E.Zero)) `shouldBe` Success (fromInt 2)
it "should fail when using succ on something other than a number" $
eval M.empty (E.Succ (E.Lam "x" E.Zero)) `shouldBe` Error "Expected a number as argument for 'succ'"
it "should fail when using pred on something other than a number" $
eval M.empty (E.Pred (E.Lam "x" E.Zero)) `shouldBe` Error "Expected a number as argument for 'pred'"
it "should execute the then branch on IfZero on zero" $
eval M.empty (E.IfZero E.Zero (E.Succ E.Zero) E.Zero)
`shouldBe` Success (fromInt 1)
it "should execute the else branch on IfZero on completely non-zero" $
eval M.empty (E.IfZero (E.Succ E.Zero) (E.Succ E.Zero) E.Zero)
`shouldBe` Success (fromInt 0)
it "should fail when using a non-number condition for IfZero" $
eval M.empty (E.IfZero (E.Lam "x" E.Zero) E.Zero E.Zero) `shouldBe` Error "Expected a number as condition for 'ifZero'"
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