Commit 4c416392 authored by Sven Keidel's avatar Sven Keidel

add tests for fixpoint cache and bounded environment

parent 071a73fc
{ mkDerivation, base, containers, hashable, mtl, numeric-limits
, stdenv, text, unordered-containers
{ mkDerivation, base, containers, hashable, hspec, mtl
, numeric-limits, stdenv, text, unordered-containers
}:
mkDerivation {
pname = "sturdy-lib";
......@@ -9,5 +9,6 @@ mkDerivation {
base containers hashable mtl numeric-limits text
unordered-containers
];
testHaskellDepends = [ base hspec text unordered-containers ];
license = stdenv.lib.licenses.bsd3;
}
......@@ -4,8 +4,8 @@ let
inherit (nixpkgs) pkgs;
f = { mkDerivation, base, containers, hashable, mtl
, numeric-limits, stdenv, text, unordered-containers, hlint, cabal-install
f = { mkDerivation, base, containers, hashable, hspec, mtl
, numeric-limits, stdenv, text, unordered-containers, cabal-install
}:
mkDerivation {
pname = "sturdy-lib";
......@@ -13,8 +13,9 @@ let
src = ./.;
libraryHaskellDepends = [
base containers hashable mtl numeric-limits text
unordered-containers hlint cabal-install
unordered-containers cabal-install
];
testHaskellDepends = [ base hspec text unordered-containers ];
license = stdenv.lib.licenses.bsd3;
};
......
......@@ -25,6 +25,9 @@ import Data.Order
import Data.Store (Store)
import qualified Data.Store as S
import Debug.Trace
import Text.Printf
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
......@@ -68,15 +71,14 @@ instance ArrowEnv a b env c => ArrowEnv a b env (CacheArrow x y c) where
extendEnv = liftCache extendEnv
localEnv (CacheArrow f) = CacheArrow $ (\(s,(env,a)) -> (env,(s,a))) ^>> localEnv f
instance (Eq a, Hashable a, LowerBounded b, Complete b, ArrowChoice c) => ArrowFix a b (CacheArrow a b c) where
instance (Show a, Show b, Eq a, Hashable a, LowerBounded b, Complete b, ArrowChoice c) => ArrowFix a b (CacheArrow a b c) where
fixA f = proc x -> do
y <- retireCache (fix (f . memoize)) -< x
fp <- reachedFixpoint -< ()
(y,fp) <- retireCache (fix (f . memoize) &&& reachedFixpoint) -< x
if fp
then returnA -< y
else fix f -< x
else fixA f -< x
memoize :: (Eq a, Hashable a, LowerBounded b, Complete b, ArrowChoice c) => CacheArrow a b c a b -> CacheArrow a b c a b
memoize :: (Show a, Show b, Eq a, Hashable a, LowerBounded b, Complete b, ArrowChoice c) => CacheArrow a b c a b -> CacheArrow a b c a b
memoize f = proc x -> do
m <- askCache -< x
case m of
......@@ -99,8 +101,8 @@ 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 () Bool
reachedFixpoint = CacheArrow $ arr $ \((i,o),()) -> (o,o i)
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)
deriving instance Complete (c ((Store a b,Store a b),x) (Store a b,y)) => Complete (CacheArrow a b c x y)
......
......@@ -5,16 +5,20 @@ import Data.Order
import Data.Hashable
import GHC.Generics
data Sign = Negative | Zero | Positive | Top
data Sign = Bot | 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
......@@ -28,6 +32,7 @@ instance Num Sign where
negate Positive = Negative
negate Negative = Positive
negate Top = Top
negate Bot = Bot
abs Zero = Zero
abs _ = Positive
......@@ -36,6 +41,7 @@ instance Num Sign where
signum Positive = Positive
signum Zero = Zero
signum Top = Top
signum Bot = Bot
fromInteger n
| n == 0 = Zero
......@@ -43,13 +49,22 @@ instance Num Sign where
| otherwise = Positive
instance PreOrd Sign where
Bot _ = True
_ Top = True
_ _ = False
instance Complete Sign where
Bot y = y
x Bot = x
Negative Negative = Negative
Zero Zero = Zero
Positive Positive = Positive
_ _ = Top
instance LowerBounded Sign where
bottom = Bot
instance UpperBounded Sign where
top = Top
instance Hashable Sign
......@@ -10,9 +10,15 @@ import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as H
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)
instance (Show a,Show b) => Show (Store a b) where
show (Store h)
| H.null h = "[]"
| otherwise = "[" ++ init (unwords [ printf "%s -> %s," (show k) (show v) | (k,v) <- H.toList h]) ++ "]"
instance (Eq a, Hashable a, PreOrd b) => PreOrd (Store a b) where
Store m1 Store m2 = subsetKeys m1 m2 && all (\(k,v1) -> v1 (m2 H.! k)) (H.toList m1)
Store m1 Store m2 = H.keys m1 == H.keys m2 && all (\(k,v_o) -> v_o (m2 H.! k)) (H.toList m1)
......
......@@ -65,5 +65,17 @@ library
unordered-containers
hs-source-dirs: src/
default-language: Haskell2010
test-suite specs
type: exitcode-stdio-1.0
ghc-options: -Wall
hs-source-dirs: test
main-is: Spec.hs
build-depends: base,
hspec,
sturdy-lib,
unordered-containers,
text
default-language: Haskell2010
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
module BoundedEnvironmentSpec where
import Prelude hiding (lookup)
import Control.Arrow
import Control.Arrow.Environment
import Control.Arrow.State
import Data.Interval
import qualified Data.HashMap.Lazy as M
import Data.Text (Text)
import Test.Hspec
main :: IO ()
main = hspec spec
type Val = Interval Int
type Addr = Int
type Ar = BoundedEnv Text Addr Val (StateArrow Addr (->))
spec :: Spec
spec = do
context "env = [a -> 1, b -> 2, c -> 3, d -> 4, e -> 5, f -> 6, g -> 7] with allocation strategy (addr+1)%5" $ do
let setup :: Ar x y -> Ar x y
setup f = proc x -> do
env0 <- getEnv -< ()
env1 <- extendEnv -< ("a",1,env0)
env2 <- extendEnv -< ("b",2,env1)
env3 <- extendEnv -< ("c",3,env2)
env4 <- extendEnv -< ("d",4,env3)
env5 <- extendEnv -< ("e",5,env4)
env6 <- extendEnv -< ("f",6,env5)
env7 <- extendEnv -< ("g",7,env6)
localEnv f -< (env7,x)
it "env(a) = [1,6]" $ runTests setup "a" `shouldBe` Just (Interval 1 6)
it "env(b) = [2,6]" $ runTests setup "b" `shouldBe` Just (Interval 2 7)
it "env(c) = [3,3]" $ runTests setup "c" `shouldBe` Just (Interval 3 3)
it "env(d) = [4,4]" $ runTests setup "d" `shouldBe` Just (Interval 4 4)
it "env(e) = [5,5]" $ runTests setup "e" `shouldBe` Just (Interval 5 5)
it "env(f) = [1,6]" $ runTests setup "f" `shouldBe` Just (Interval 1 6)
it "env(g) = [2,7]" $ runTests setup "g" `shouldBe` Just (Interval 2 7)
context "env = [a -> 1, d -> 4, g -> 7] with allocation strategy (addr+1)%5" $ do
let setup :: Ar x y -> Ar x y
setup f = proc x -> do
env0 <- getEnv -< ()
env1 <- extendEnv -< ("a",1,env0)
localEnv
(proc env1 -> do
env2 <- extendEnv -< ("b",2,env1)
extendEnv -< ("c",3,env2))
-< (env1,env1)
env4 <- extendEnv -< ("d",4,env1)
localEnv
(proc env4 -> do
env5 <- extendEnv -< ("e",5,env4)
extendEnv -< ("f",6,env5))
-< (env4,env4)
env7 <- extendEnv -< ("g",7,env4)
localEnv f -< (env7,x)
it "env(a) = [1,6]" $ runTests setup "a" `shouldBe` Just (Interval 1 6)
it "env(b) = Nothing" $ runTests setup "b" `shouldBe` Nothing
it "env(c) = Nothing" $ runTests setup "c" `shouldBe` Nothing
it "env(d) = [4,4]" $ runTests setup "d" `shouldBe` Just (Interval 4 4)
it "env(e) = Nothing" $ runTests setup "e" `shouldBe` Nothing
it "env(f) = Nothing" $ runTests setup "f" `shouldBe` Nothing
it "env(g) = [2,7]" $ runTests setup "g" `shouldBe` Just (Interval 2 7)
where
runTests s x = snd (runStateArrow (runBoundedEnv (s lookup)) (0,(alloc,M.empty,x)))
alloc :: Alloc Text Addr Val (StateArrow Addr (->))
alloc = proc _ -> do
addr <- getA -< ()
putA -< (succ addr `mod` 5)
returnA -< addr
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
module FixpointCacheSpec where
import Prelude hiding (lookup)
import Data.Function
import Control.Arrow
import Control.Arrow.Fix
import Data.Interval (Interval)
import Data.Sign (Sign)
import Data.Order
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec = do
it "fib" $ do
runCacheArrow (fixA fib) 10 `shouldBe` fix fib 10
runCacheArrow (fixA fib) 15 `shouldBe` fix fib 15
describe "the analyis of a diverging program" $
it "should terminate with bottom" $ do
runCacheArrow (fixA diverge) 5 `shouldBe` bottom
where
fib :: ArrowChoice c => c Int (Interval Int) -> c Int (Interval Int)
fib f = proc n -> case n of
0 -> returnA -< 0
1 -> returnA -< 1
_ -> do
x <- f -< n-1
y <- f -< n-2
returnA -< x + y
diverge :: ArrowChoice c => c Int Sign -> c Int Sign
diverge f = proc n -> case n of
0 -> f -< 0
_ -> f -< (n-1)
{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
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