Commit 03b3c623 authored by Sven Keidel's avatar Sven Keidel

add benchmark of example

parent 9b976af2
{-# LANGUAGE Arrows #-}
module Control.Arrow.Abstract.Join where
import Prelude hiding ((.))
import Control.Arrow
import Control.Arrow.Utils
import Data.Order(Complete(..))
class Arrow c => ArrowJoin c where
-- | Join two arrow computation with the provided upper bound operator.
......@@ -11,7 +14,25 @@ class Arrow c => ArrowJoin c where
-- @
-- joinWith (⊔) f g = joined f g
-- @
joinWith :: (z -> z -> z) -> c x z -> c y z -> c (x,y) z
joinWith :: (y -> y -> y) -> c x y -> c x y -> c x y
joinWith' :: ArrowJoin c => (y -> y -> y) -> c x y -> c x' y -> c (x,x') y
joinWith' lub f g = joinWith lub (f <<< pi1) (g <<< pi2)
(<>) :: (ArrowJoin c, Complete y) => c x y -> c x y -> c x y
(<>) = joinWith ()
-- | Joins a list of arguments. Use it with idiom brackets:
-- @
-- let a = ...; b = ...; xs = ...
-- (| joinList (returnA -< a) (\x -> f -< x+b) |) xs
-- @
joinList :: (ArrowChoice c, ArrowJoin c, Complete y) => c (e,s) y -> c (e,(x,s)) y -> c (e,([x],s)) y
joinList empty f = proc (e,(l,s)) -> case l of
[] -> empty -< (e,s)
[x] -> f -< (e,(x,s))
(x:xs) -> (f -< (e,(x,s))) <> (joinList empty f -< (e,(xs,s)))
instance ArrowJoin (->) where
joinWith lub f g = \(x,y) -> lub (f x) (g y)
joinWith lub f g = \x -> lub (f x) (g x)
......@@ -13,5 +13,6 @@ class Arrow c => ArrowCond v c | c -> v where
-- | Type class constraint used by the abstract instances to join arrow computations.
type family Join (c :: * -> * -> *) x y :: Constraint
-- TODO: Change type to if_ :: Join c (e,s) y => c (e,s) y -> c (e,s) y -> c (e, (v, s)) y
-- | @'if_' f g -< (v,(x,y))@ performs a case distinction on the given value @v@ and executes either @(f -< x)@ or @(g -< y)@. Abstract instances might join the results of @f@ and @g@.
if_ :: Join c (x,y) z => c x z -> c y z -> c (v, (x, y)) z
......@@ -26,6 +26,7 @@ class Arrow c => ArrowEnv var val env c | c -> var, c -> val, c -> env where
-- | Type class constraint used by the abstract instances to join arrow computations.
type family Join (c :: * -> * -> *) x y :: Constraint
-- TODO: Change type to lookup (Join c x y) => c (e,(val,s)) y -> c (e,s) y -> c (e,(var,s)) y
-- | Lookup a variable in the current environment. If the
-- environment contains a binding of the variable, the first
-- continuation is called and the second computation otherwise.
......
......@@ -24,3 +24,4 @@ instance ArrowFix x y (->) where
liftFix :: (ArrowFix (Dom t x y) (Cod t x y) c,ArrowTrans t) => (t c x y -> t c x y) -> t c x y
liftFix f = lift $ fix (unlift . f . lift)
{-# INLINE liftFix #-}
......@@ -20,6 +20,7 @@ import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Const
import Control.Arrow.Transformer.Static
import Control.Arrow.Transformer.Reader
......@@ -89,6 +90,7 @@ deriving instance ArrowChoice c => ArrowChoice (EnvT var addr val c)
deriving instance ArrowState s c => ArrowState s (EnvT var addr val c)
deriving instance ArrowFail e c => ArrowFail e (EnvT var addr val c)
deriving instance ArrowExcept e c => ArrowExcept e (EnvT var addr val c)
deriving instance ArrowJoin c => ArrowJoin (EnvT var addr val c)
deriving instance PreOrd (c ((Map var addr val),x) y) => PreOrd (EnvT var addr val c x y)
deriving instance Complete (c ((Map var addr val),x) y) => Complete (EnvT var addr val c x y)
......
......@@ -19,6 +19,7 @@ import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Reader
import Control.Category
......@@ -69,6 +70,7 @@ deriving instance ArrowState s c => ArrowState s (ContourT lab c)
deriving instance ArrowEnv x y env c => ArrowEnv x y env (ContourT lab c)
deriving instance ArrowFail e c => ArrowFail e (ContourT lab c)
deriving instance ArrowExcept e c => ArrowExcept e (ContourT lab c)
deriving instance ArrowJoin c => ArrowJoin (ContourT lab c)
deriving instance PreOrd (c (CallString lab,x) y) => PreOrd (ContourT lab c x y)
deriving instance LowerBounded (c (CallString lab,x) y) => LowerBounded (ContourT lab c x y)
......
......@@ -49,22 +49,22 @@ instance (ArrowChoice c, ArrowJoin c, Complete e) => Category (ExceptT e c) wher
SuccessOrFail e y' -> do
-- Ideally we would like to write '(returnA -< Fail e) ⊔ (f -< y)',
-- however this is not possible, because the result type of
-- 'f', 'UncertainError e z', is not 'Complete' because 'z' is not
-- 'f', 'Error e z', is not 'Complete' because 'z' is not
-- 'Complete'. However, in '(returnA -< Fail e) ⊔ (f -< y)' we
-- actually never join to values of type 'z'.
joinWith (\(Fail e) er -> case er of
joinWith' (\(Fail e) er -> case er of
Success z -> SuccessOrFail e z
Fail e' -> Fail (e e')
SuccessOrFail e' z -> SuccessOrFail (e e') z)
id (unlift f) -< (Fail e,y')
instance (ArrowChoice c, ArrowJoin c, Complete e) => Arrow (ExceptT e c) where
arr f = lift' (arr f)
first f = lift $ first (unlift f) >>^ strength1
arr f = lift' (arr f)
first f = lift $ first (unlift f) >>^ strength1
second f = lift $ second (unlift f) >>^ strength2
instance (Complete e, ArrowJoin c, ArrowChoice c) => ArrowChoice (ExceptT e c) where
left f = lift $ left (unlift f) >>^ strength1
left f = lift $ left (unlift f) >>^ strength1
right f = lift $ right (unlift f) >>^ strength2
instance (Complete e, ArrowJoin c, ArrowApply c, ArrowChoice c) => ArrowApply (ExceptT e c) where
......
......@@ -85,21 +85,21 @@ liftFixT f = FixT $ \_ -> ((\((_,o),x) -> (o,x)) ^>> second (f >>^ Terminating))
#ifndef TRACE
instance (Identifiable x, PreOrd y, ArrowChoice c) => ArrowFix x y (FixT s x y c) where
fix f = proc x -> do
old <- getOutCache -< ()
old <- getCache -< ()
-- reset the current fixpoint cache
setOutCache -< bottom
setCache -< bottom
-- recompute the fixpoint cache by calling 'f' and memoize its results.
y <- localInCache (F.fix (memoize . f)) -< (old,x)
y <- localOldCache (F.fix (memoize . f)) -< (old,x)
new <- getOutCache -< ()
new <- getCache -< ()
-- In case the new fixpoint cache contains less information than
-- the old cache, we are in the reductive set of `f` and have
-- overshot the fixpoint and stop recursion. Otherwise, we have
-- not reached the fixpoint yet and need to continue improving the
-- fixpoint cache.
if (new old)
if {-# SCC "Fix.Cache.comparison" #-}(new old)
then returnA -< y
else fix f -< x
......@@ -107,29 +107,29 @@ instance (Identifiable x, PreOrd y, ArrowChoice c) => ArrowFix x y (FixT s x y c
-- has been computed before, the cached value is returned and will not
-- be recomputed.
memoize :: (Identifiable x, PreOrd y, ArrowChoice c) => FixT s x y c x y -> FixT s x y c x y
memoize (FixT f) = FixT $ \(stackWidening,widening) -> proc (((stack,inCache), outCache),x) -> do
case M.unsafeLookup x outCache of
memoize (FixT f) = FixT $ \(stackWidening,widening) -> proc (((stack,oldCache), newCache),x) -> do
case M.unsafeLookup x newCache of
-- In case the input was in the fixpoint cache, short-cut
-- recursion and return the cached value.
Just y -> returnA -< (outCache,y)
Just y -> returnA -< (newCache,y)
-- In case the input was not in the fixpoint cache, initialize the
-- cache with previous knowledge about the result or ⊥, compute
-- the result of the function and update the fixpoint cache.
Nothing -> do
let yOld = fromMaybe bottom (M.unsafeLookup x inCache)
outCache' = M.insert x yOld outCache
let yOld = fromMaybe bottom (M.unsafeLookup x oldCache)
newCache' = M.insert x yOld newCache
(x',stack') = runState (stackWidening x) stack
(outCache'',y) <- f (stackWidening,widening) -< (((stack',inCache), outCache'),x')
let outCache''' = M.unsafeInsertWith (flip (T.widening widening)) x' y outCache''
y' = fromJust (M.unsafeLookup x' outCache''')
returnA -< (outCache''',y')
(newCache'',y) <- f (stackWidening,widening) -< (((stack',oldCache), newCache'),x')
let newCache''' = M.unsafeInsertWith (flip (T.widening widening)) x' y newCache''
y' = fromJust (M.unsafeLookup x' newCache''')
returnA -< (newCache''',y')
#else
instance (Show x, Show y, Identifiable x, PreOrd y, ArrowChoice c) => ArrowFix x y (FixT s x y c) where
fix f = proc x -> do
old <- getOutCache -< ()
old <- getCache -< ()
setOutCache -< bottom
y <- localInCache (F.fix (memoize . f)) -< trace "----- ITERATION -----" $ (old,x)
new <- getOutCache -< ()
......@@ -155,14 +155,14 @@ memoize (FixT f) = FixT $ \(stackWidening,widening) -> proc (((stack,inCache), o
#endif
getOutCache :: Arrow c => FixT s x y c () (Map x (Terminating y))
getOutCache = FixT $ \_ -> arr $ \((_,o),()) -> (o,return o)
getCache :: Arrow c => FixT s x y c () (Map x (Terminating y))
getCache = FixT $ \_ -> arr $ \((_,o),()) -> (o,return o)
setOutCache :: Arrow c => FixT s x y c (Map x (Terminating y)) ()
setOutCache = FixT $ \_ -> arr $ \((_,_),o) -> (o,return ())
setCache :: Arrow c => FixT s x y c (Map x (Terminating y)) ()
setCache = FixT $ \_ -> arr $ \((_,_),o) -> (o,return ())
localInCache :: Arrow c => FixT s x y c x y -> FixT s x y c (Map x (Terminating y),x) y
localInCache (FixT f) = FixT $ \w -> proc (((s,_),o),(i,x)) -> f w -< (((s,i),o),x)
localOldCache :: Arrow c => FixT s x y c x y -> FixT s x y c (Map x (Terminating y),x) y
localOldCache (FixT f) = FixT $ \w -> proc (((s,_),o),(i,x)) -> f w -< (((s,i),o),x)
instance ArrowChoice c => Category (FixT s i o c) where
id = liftFixT id
......@@ -191,9 +191,9 @@ instance (ArrowChoice c, ArrowApply c) => ArrowApply (FixT s i o c) where
app = FixT $ \w -> (\(io,(FixT f,x)) -> (f w,(io,x))) ^>> app
instance (Identifiable i, Complete o, ArrowJoin c, ArrowChoice c) => ArrowJoin (FixT s i o c) where
joinWith lub (FixT f) (FixT g) = FixT $ \w -> proc ((i,o),(x,y)) -> do
joinWith lub (FixT f) (FixT g) = FixT $ \w -> proc ((i,o),x) -> do
(o',t1) <- f w -< ((i,o),x)
(o'',t2) <- g w -< ((i,o'),y)
(o'',t2) <- g w -< ((i,o'),x)
returnA -< (o'',case (t1,t2) of
(Terminating y',Terminating v') -> Terminating (lub y' v')
(Terminating y',NonTerminating) -> Terminating y'
......
......@@ -31,6 +31,7 @@ import Control.Arrow.Fail
import Control.Arrow.Random
import Control.Arrow.Store as Store
import Control.Arrow.Environment
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Reader
import Data.Identifiable
......@@ -88,6 +89,7 @@ deriving instance ArrowExcept e c => ArrowExcept e (ReachingDefsT lab c)
deriving instance ArrowState s c => ArrowState s (ReachingDefsT lab c)
deriving instance ArrowEnv x y env c => ArrowEnv x y env (ReachingDefsT lab c)
deriving instance ArrowCond val c => ArrowCond val (ReachingDefsT lab c)
deriving instance ArrowJoin c => ArrowJoin (ReachingDefsT lab c)
deriving instance PreOrd (c (Dom (ReachingDefsT lab) x y) (Cod (ReachingDefsT lab) x y)) => PreOrd (ReachingDefsT lab c x y)
deriving instance LowerBounded (c (Dom (ReachingDefsT lab) x y) (Cod (ReachingDefsT lab) x y)) => LowerBounded (ReachingDefsT lab c x y)
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module Control.Arrow.Transformer.Abstract.Stack(StackT,runStackT,runStackT') where
import Prelude hiding ((.))
import Control.Category
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Const
import Control.Arrow.Transformer.Static
import qualified Control.Monad.State as M
import Data.Order
import Data.Abstract.StackWidening (StackWidening)
newtype StackT s a c x y = StackT (ConstT (StackWidening s a,s a) c x y)
deriving (Category,Arrow,ArrowChoice,ArrowLift,ArrowJoin,PreOrd,Complete)
instance ArrowApply c => ArrowApply (StackT s a c) where app = StackT ((\(StackT f,x) -> (f,x)) ^>> app)
runStackT :: Arrow c => (StackWidening s a,s a) -> StackT s a c x y -> c x y
runStackT s (StackT f) = runConstT s f
runStackT' :: (Arrow c, Monoid (s a)) => StackWidening s a -> StackT s a c x y -> c x y
runStackT' s = runStackT (s,mempty)
stackT :: ((StackWidening s a,s a) -> c x y) -> StackT s a c x y
stackT f = StackT $ ConstT $ StaticT $ f
type instance Fix x y (StackT s () c) = StackT s x (Fix x y c)
instance (ArrowApply c, ArrowFix x y c) => ArrowFix x y (StackT s x c) where
fix f = stackT $ \(stackWidening,stack) -> proc x -> do
let (x',stack') = M.runState (stackWidening x) stack
fix (runStackT (stackWidening,stack') . f . lift') -<< x'
......@@ -93,23 +93,23 @@ instance ArrowFix (Dom (ReaderT r) x y) (Cod (ReaderT r) x y) c => ArrowFix x y
fix = liftFix
instance ArrowExcept e c => ArrowExcept e (ReaderT r c) where
type instance Join (ReaderT r c) (x,(x,e)) y = Exc.Join c ((r,x),((r,x),e)) y
type instance Join (ReaderT r c) (x,(x,e)) y = Exc.Join c (Dom (ReaderT r) x y,(Dom (ReaderT r) x y,e)) (Cod (ReaderT r) x y)
throw = lift' throw
catch (ReaderT f) (ReaderT g) = ReaderT $ catch f (from assoc ^>> g)
finally (ReaderT f) (ReaderT g) = ReaderT $ finally f g
catch f g = lift $ catch (unlift f) (from assoc ^>> unlift g)
finally f g = lift $ finally (unlift f) (unlift g)
instance ArrowDeduplicate (r, x) y c => ArrowDeduplicate x y (ReaderT r c) where
dedup (ReaderT f) = ReaderT (dedup f)
dedup f = lift (dedup (unlift f))
instance ArrowJoin c => ArrowJoin (ReaderT r c) where
joinWith lub (ReaderT f) (ReaderT g) = ReaderT $ (\(r,(x,y)) -> ((r,x),(r,y))) ^>> joinWith lub f g
joinWith lub f g = lift $ joinWith lub (unlift f) (unlift g)
instance ArrowConst x c => ArrowConst x (ReaderT r c) where
askConst = lift' askConst
instance ArrowCond v c => ArrowCond v (ReaderT r c) where
type instance Join (ReaderT r c) (x,y) z = Cond.Join c ((r,x),(r,y)) z
if_ (ReaderT f) (ReaderT g) = ReaderT $ (\(r,(v,(x,y))) -> (v,((r,x),(r,y)))) ^>> if_ f g
type instance Join (ReaderT r c) (x,y) z = Cond.Join c (Dom (ReaderT r) x z,Dom (ReaderT r) y z) (Cod (ReaderT r) (x,y) z)
if_ f g = lift $ (\(r,(v,(x,y))) -> (v,((r,x),(r,y)))) ^>> if_ (unlift f) (unlift g)
deriving instance PreOrd (c (r,x) y) => PreOrd (ReaderT r c x y)
deriving instance LowerBounded (c (r,x) y) => LowerBounded (ReaderT r c x y)
......
......@@ -113,7 +113,7 @@ instance (Eq s, Hashable s, ArrowDeduplicate (Dom (StateT s) x y) (Cod (StateT s
instance (ArrowJoin c, Complete s) => ArrowJoin (StateT s c) where
joinWith lub f g =
lift $ (\(s,(x,y)) -> ((s,x),(s,y))) ^>> joinWith (\(s1,z1) (s2,z2) -> (s1s2,lub z1 z2)) (unlift f) (unlift g)
lift $ joinWith (\(s1,z1) (s2,z2) -> (s1s2,lub z1 z2)) (unlift f) (unlift g)
instance ArrowConst x c => ArrowConst x (StateT s c) where
askConst = lift' askConst
......
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE TypeFamilies #-}
......@@ -7,16 +8,20 @@ module Data.Abstract.FreeCompletion where
import Control.Applicative
import Control.Monad
import Control.DeepSeq
import Data.Abstract.Widening
import Data.Hashable
import Data.Order
import GHC.Generics(Generic)
data FreeCompletion a = Lower a | Top deriving (Eq,Functor,Traversable,Foldable)
data FreeCompletion a = Lower a | Top deriving (Eq,Functor,Traversable,Foldable,Generic)
instance Show a => Show (FreeCompletion a) where
show Top = "⊤"
show (Lower a) = show a
instance NFData a => NFData (FreeCompletion a)
instance Hashable a => Hashable (FreeCompletion a) where
hashWithSalt s (Lower a) = s `hashWithSalt` a
hashWithSalt s Top = s `hashWithSalt` (2::Int)
......@@ -52,6 +57,15 @@ instance (PreOrd a, UpperBounded (FreeCompletion a),
(Lower a, Lower b) -> Lower (a,b)
(_,_) -> Top
instance (PreOrd x, Complete (FreeCompletion x)) => Complete (FreeCompletion [x]) where
Lower xs Lower ys | eqLength xs ys = zipWithM (\x y -> Lower x Lower y) xs ys
where
eqLength :: [a] -> [b] -> Bool
eqLength [] [] = True
eqLength (_:as) (_:bs) = eqLength as bs
eqLength _ _ = False
_ _ = Top
instance CoComplete a => CoComplete (FreeCompletion a) where
Lower a Lower b = Lower (a b)
......
......@@ -10,8 +10,8 @@ import Prelude hiding (lookup,map,Either(..),(**))
import Control.Arrow
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as H
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as H
import Data.Hashable
import Data.Order
import Data.Identifiable
......@@ -35,16 +35,19 @@ instance (Show a,Show b) => Show (Map a b) where
| otherwise = "[" ++ init (unwords [ printf "%s%s -> %s," (show k) (show t) (show v) | (k,(t,v)) <- H.toList h]) ++ "]"
instance (Identifiable a, PreOrd b) => PreOrd (Map a b) where
Map m1 m2 = all (\(k,(t,v)) -> (case t of Must -> M.Just v; May -> M.JustNothing v) lookup k m2) (H.toList m1)
Map m1 m2 = {-# SCC "Data.Abstract.Map.lt" #-} all (\(k,(t,v)) -> (case t of Must -> M.Just v; May -> M.JustNothing v) lookup k m2) (H.toList m1)
instance (Identifiable a, Complete b) => Complete (Map a b) where
Map m1 Map m2 = Map $ H.map join $ H.unionWith () (H.map Left m1) (H.map Right m2)
m1 m2 = {-# SCC "Data.Abstract.Map.join" #-} widening () m1 m2
widening :: Identifiable a => Widening b -> Widening (Map a b)
widening w (Map m1) (Map m2) = Map $ H.map join $ H.unionWith (E.widening (finite ** w) (finite ** w)) (H.map Left m1) (H.map Right m2)
where
join :: Complete a => Either (There,a) (There,a) -> (There,a)
join e = case e of
Left (_,a) -> (May,a)
Right (_,b) -> (May,b)
LeftRight (t1,a) (t2,b) -> (t1 t2,a b)
LeftRight (t1,a) (t2,b) -> (t1 t2,a `w` b)
{-# SCC widening #-}
instance (Identifiable a, PreOrd b) => LowerBounded (Map a b) where
bottom = empty
......@@ -100,14 +103,6 @@ adjust f a (Map m) = Map (H.adjust (second f) a m)
compose :: (Identifiable a, Identifiable b, Complete c) => [(a,b)] -> Map b c -> Map a c
compose f (Map g) = Map $ H.fromListWith () [ (a,c) | (a,b) <- f, Just c <- return $ H.lookup b g ]
widening :: Identifiable a => Widening b -> Widening (Map a b)
widening w (Map m1) (Map m2) = Map $ H.map join $ H.unionWith (E.widening (finite ** w) (finite ** w)) (H.map Left m1) (H.map Right m2)
where
join e = case e of
Left (_,a) -> (May,a)
Right (_,b) -> (May,b)
LeftRight (t1,a) (t2,b) -> (t1 t2,a `w` b)
instance Identifiable a => IsList (Map a b) where
type Item (Map a b) = (a,b)
toList (Map m) = H.toList (H.map snd m)
......
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
module Data.Abstract.Terminating where
import Control.Monad
import Control.Applicative
import Control.DeepSeq
import Data.Order
import Data.Abstract.Widening
import GHC.Generics
-- Free cocompletion of a type
data Terminating a = NonTerminating | Terminating a deriving (Eq,Functor,Traversable,Foldable)
data Terminating a = NonTerminating | Terminating a deriving (Eq,Functor,Traversable,Foldable,Generic)
instance NFData a => NFData (Terminating a)
fromTerminating :: a -> Terminating a -> a
fromTerminating _ (Terminating a) = a
......
......@@ -37,23 +37,14 @@ lub = foldr1 (⊔)
joined :: (Arrow c, Complete (c (a1,a2) b)) => c a1 b -> c a2 b -> c (a1,a2) b
joined f1 f2 = (arr fst >>> f1) (arr snd >>> f2)
-- What we actually would like to write is this:
-- joined f1 f2 = proc (x1,x2) -> (f1 -< x1) ⊔ (f2 -< x2)
-- This is what the compiler desugars it to (we simplified it):
-- joined =
-- (arr (\(x1, x2) -> ((x2, x1), ())) )
-- >>>
-- (op
-- (arr (\((x2,x1), b) -> (x1, b))) >>> arr fst >>> f1 :: c ((x2,x1,b)) r
-- (arr (\((x2,x1),b) -> (x2,b)) >>> arr fst >>> f2 :: c ((x2,x1),b) r
{-# DEPRECATED joined "Use Control.Arrow.Abstract.ArrowJoin.<⊔>" #-}
lubA :: (ArrowChoice c, Complete (c (x,[x]) y), LowerBounded (c () y)) => c x y -> c [x] y
lubA f = proc l -> case l of
[] -> bottom -< ()
-- (x:xs) -> (f -< x) ⊔ (lubA f -< xs) causes an type error.
(x:xs) -> joined f (lubA f) -< (x, xs)
{-# DEPRECATED lubA "Use Control.Arrow.Abstract.ArrowJoin.joinList" #-}
-- | Order with all greatest lower bounds
class PreOrd x => CoComplete x where
......
{ pkgs ? import <nixpkgs> {} }:
let
hsEnv = pkgs.haskellPackages.ghcWithPackages(p: with p; [
Cabal cabal-install hlint text containers hspec mtl numeric-limits criterion fgl
(p.callPackage ../lib/default.nix { })
]);
in pkgs.stdenv.mkDerivation {
name = "sturdy-pcf";
version = "0.0.1";
src = ./.;
buildInputs = [
hsEnv
];
}
......@@ -28,6 +28,7 @@ import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Conditional as Cond
import Control.Arrow.Environment
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Abstract.Contour
import Control.Arrow.Transformer.Abstract.BoundedEnvironment
import Control.Arrow.Transformer.Abstract.Failure
......@@ -96,7 +97,7 @@ evalInterval k env e = -- runInterp eval ?bound k env (generate e)
$ SW.reuse (\_ l -> head l)
$ SW.fromWidening (F.widening widenVal)
newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Category,Arrow,ArrowChoice,ArrowFail e, PreOrd, Complete, LowerBounded)
newtype IntervalT c x y = IntervalT { runIntervalT :: c x y } deriving (Category,Arrow,ArrowChoice,ArrowFail e,ArrowJoin)
type instance Fix x y (IntervalT c) = IntervalT (Fix x y c)
deriving instance ArrowFix x y c => ArrowFix x y (IntervalT c)
deriving instance ArrowEnv var val env c => ArrowEnv var val env (IntervalT c)
......@@ -107,35 +108,36 @@ instance ArrowTrans IntervalT where
lift = IntervalT
unlift = runIntervalT
instance (ArrowChoice c, ArrowFail String c) => IsVal Val (IntervalT c) where
instance (ArrowChoice c, ArrowFail String c, ArrowJoin c) => IsVal Val (IntervalT c) where
succ = proc x -> case x of
Top -> returnA -< Top
Top -> (returnA -< NumVal top) <> (fail -< "Expected a number as argument for 'succ'")
NumVal n -> returnA -< NumVal $ n + 1 -- uses the `Num` instance of intervals
ClosureVal _ -> fail -< "Expected a number as argument for 'succ'"
pred = proc x -> case x of
Top -> returnA -< Top
Top -> (returnA -< NumVal top) <> (fail -< "Expected a number as argument for 'pred'")
NumVal n -> returnA -< NumVal $ n - 1
ClosureVal _ -> fail -< "Expected a number as argument for 'pred'"
zero = proc _ -> returnA -< (NumVal 0)
instance (ArrowChoice c, ArrowFail String c) => ArrowCond Val (IntervalT c) where
type Join (IntervalT c) x y = Complete (IntervalT c x y)
instance (ArrowChoice c, ArrowJoin c, ArrowFail String c) => ArrowCond Val (IntervalT c) where
type Join (IntervalT c) x y = Complete y
if_ f g = proc v -> case v of
(Top, (x,y)) -> joined f g -< (x,y)
(Top, (x,y)) -> (f -< x) <> (g -< y) <> (fail -< "Expected a number as condition for 'ifZero'")
(NumVal (I.Interval i1 i2), (x, y))
| (i1, i2) == (0, 0) -> f -< x -- case the interval is exactly zero
| i1 > 0 || i2 < 0 -> g -< y -- case the interval does not contain zero
| otherwise -> joined f g -< (x,y) -- case the interval contains zero and other numbers.
(ClosureVal _, _) -> fail -< "Expected a number as condition for 'ifZero'"
| (i1, i2) == (0, 0) -> f -< x -- case the interval is exactly zero
| i1 > 0 || i2 < 0 -> g -< y -- case the interval does not contain zero
| otherwise -> (f -< x) <> (g -< y) -- case the interval contains zero and other numbers.
(ClosureVal _, _) -> fail -< "Expected a number as condition for 'ifZero'"
instance (ArrowChoice c, ArrowFail String c, LowerBounded (IntervalT c () Val), Complete (IntervalT c (((Expr, F.Map Text Addr Val),Val),[((Expr, F.Map Text Addr Val), Val)]) Val))
instance (ArrowChoice c, ArrowFail String c, ArrowJoin c)
=> IsClosure Val (F.Map Text Addr Val) (IntervalT c) where
closure = arr $ \(e, env) -> ClosureVal (Closure [(e,env)])
applyClosure f = proc (fun, arg) -> case fun of
Top -> returnA -< Top
ClosureVal (Closure cls) ->
-- Apply the interpreter function `f` on all closures and join their results.
lubA (proc ((e,env),arg) -> f -< ((e,env),arg)) -< [ (c,arg) | c <- toList cls]
(| joinList (returnA -< Top) (\(e,env) -> f -< ((e,env),arg)) |)
(toList cls)
NumVal _ -> fail -< "Expected a closure"
instance PreOrd Val where
......
......@@ -8,6 +8,7 @@ import SharedSpecs
import Data.Abstract.Failure hiding (toEither)
import qualified Data.Abstract.Interval as I
import Data.Abstract.Terminating hiding (toEither)
import Data.Order
import IntervalAnalysis
import Syntax
import Test.Hspec
......@@ -37,7 +38,8 @@ spec = do
in do
evalInterval 10 [] (app (app add zero) two) `shouldBe` Terminating (Success (num 2 2))
evalInterval 10 [] (app (app add one) two) `shouldBe` Terminating (Success (num 3 3))
evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 7))
-- evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (num 2 7))
evalInterval 10 [("x", num 0 1)] (app (app add "x") two) `shouldBe` Terminating (Success (NumVal top))
it "should terminate for the non-terminating program" $
let ?bound = I.Interval 0 5
......
......@@ -2,6 +2,8 @@
{-# LANGUAGE ImplicitParams #-}
module Main where
import Prelude hiding (exp)
import SortSemantics -- hiding (sortContext)
import Syntax hiding (Fail)
......@@ -10,21 +12,28 @@ import qualified SortContext as Ctx
import qualified Data.Abstract.Map as S
import qualified Data.HashMap.Lazy as M
import Data.Abstract.Failure(Failure)
import Data.Abstract.Error(Error)
import Data.Abstract.FreeCompletion(fromCompletion)
import Data.Abstract.Terminating(fromTerminating)
import Criterion
import Criterion.Main
main :: IO ()
main = defaultMain [
bench "build" $
let ?ctx = Ctx.empty
in nf (seval 0 (Build (StringLiteral "foo"))) bottom
bgroup "Least Fixpoint" [
bench "reduce Add(Zero,y)" $
let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in
let exp = term "Exp"
reduce = Match (Cons "Add" [Cons "Zero" [], "y"]) `Seq` Build "y"
in nf (eval 0 10 reduce M.empty ?ctx emptyEnv) exp
],
bgroup "Greatest Fixpoint" [
bench "reduce Add(Zero,y)" $
let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in