merge branch with master

parent 0ed49a19
......@@ -8,7 +8,7 @@ module Control.Arrow.Fix.Chaotic where
import Prelude hiding (head,iterate,map)
import Control.Arrow
import Control.Arrow hiding (loop)
import Control.Arrow.Trans
import Control.Arrow.Fix
import Control.Arrow.Fix.Stack as Stack
......@@ -36,13 +36,20 @@ chaotic :: forall a b c. (ArrowStack a c, ArrowCache a b c, ArrowChoice c) => Fi
chaotic f = proc a -> do
m <- Cache.lookup -< a
case m of
Just (_,b) -> returnA -< b
Nothing -> do
Cache.initialize -< a
iterate -< a
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> do
loop <- Stack.elem -< a
if loop
then returnA -< b
else Stack.push iterate -< a
Nothing -> do
loop <- Stack.elem -< a
if loop
then initialize -< a
else Stack.push iterate -< a
where
iterate = proc a -> do
b <- Stack.push f -< a
b <- f -< a
(stable,b') <- Cache.update -< (a,b)
case stable of
Stable -> returnA -< b'
......@@ -52,17 +59,10 @@ chaotic f = proc a -> do
-- | Iterate on the innermost fixpoint component.
iterateInner :: forall a b c. (Identifiable a, ArrowChaotic a c, ArrowStack a c, ArrowCache a b c, ArrowChoice c) => FixpointCombinator c a b
{-# INLINE iterateInner #-}
iterateInner f = proc a -> do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> setComponent -< (mempty { head = H.singleton a }, b)
Nothing -> do
Cache.initialize -< a
iterate -< a
iterateInner f = detectLoop iterate
where
iterate = proc a -> do
(component,b) <- getComponent (Stack.push f) -< a
(component,b) <- getComponent f -< a
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
......@@ -87,17 +87,10 @@ iterateInner f = proc a -> do
-- | Iterate on the outermost fixpoint component.
iterateOuter :: forall a b c. (Identifiable a, ArrowChaotic a c, ArrowStack a c, ArrowCache a b c, ArrowChoice c) => FixpointCombinator c a b
{-# INLINE iterateOuter #-}
iterateOuter f = proc a -> do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> setComponent -< (mempty { head = H.singleton a }, b)
Nothing -> do
Cache.initialize -< a
iterate -< a
iterateOuter f = detectLoop iterate
where
iterate = proc a -> do
(component,b) <- getComponent (Stack.push f) -< a
(component,b) <- getComponent f -< a
case () of
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
......@@ -128,6 +121,25 @@ iterateOuter f = proc a -> do
setComponent -< (component { head = H.delete a (head component)
, body = H.insert a (body component) }, b)
detectLoop :: (Identifiable a, ArrowChaotic a c, ArrowStack a c, ArrowCache a b c, ArrowChoice c) => c a b -> c a b
detectLoop iterate = proc a -> do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> do
loop <- Stack.elem -< a
if loop
then setComponent -< (mempty { head = H.singleton a }, b)
else Stack.push iterate -< a
Nothing -> do
loop <- Stack.elem -< a
if loop
then do
b <- Cache.initialize -< a
setComponent -< (mempty { head = H.singleton a }, b)
else Stack.push iterate -< a
{-# INLINE detectLoop #-}
data Component a = Component { head :: HashSet a, body :: HashSet a } deriving (Eq)
instance Identifiable a => PreOrd (Component a) where
......
......@@ -19,14 +19,17 @@ import Text.Printf
class (Arrow c, Profunctor c) => ArrowStack a c | c -> a where
push :: c a b -> c a b
elem :: c a Bool
elems :: c () [a]
peek :: c () (Maybe a)
size :: c () Int
default elem :: (c ~ t c', ArrowLift t, ArrowStack a c') => c a Bool
default elems :: (c ~ t c', ArrowLift t, ArrowStack a c') => c () [a]
default peek :: (c ~ t c', ArrowLift t, ArrowStack a c') => c () (Maybe a)
default size :: (c ~ t c', ArrowLift t, ArrowStack a c') => c () Int
elem = lift' elem
elems = lift' elems
peek = lift' peek
size = lift' size
......@@ -69,13 +72,13 @@ reuseFirst = reuse find
reuseByMetric :: (PreOrd a, Ord n, ArrowChoice c, ArrowStack a c) => Metric a n -> FixpointCombinator c a b
reuseByMetric metric = reuse find
where
find a xs = elem <$> foldMap (\a' -> if a a' then Just (Measured a' (metric a a')) else Nothing) xs
find a xs = element <$> foldMap (\a' -> if a a' then Just (Measured a' (metric a a')) else Nothing) xs
{-# INLINE reuseByMetric #-}
data Measured a n = Measured { elem :: a, measured :: n }
data Measured a n = Measured { element :: a, measured :: n }
instance (Show a, Show n) => Show (Measured a n) where
show m = printf "%s@%s" (show (elem m)) (show (measured m))
show m = printf "%s@%s" (show (element m)) (show (measured m))
instance Ord n => Semigroup (Measured a n) where
m1 <> m2
......
......@@ -225,26 +225,37 @@ newCache f = lift $ \widen ->
------ Monotone Cache ------
data Monotone a b where
Monotone :: s -> Monotone s s
Monotone :: s -> HashMap a b -> Monotone (s,a) (s,b)
type instance Widening (Monotone s s) = W.Widening s
type instance Widening (Monotone (s,a) (s,b)) = (W.Widening s,W.Widening b)
instance IsEmpty s => IsEmpty (Monotone s s) where
empty = Monotone empty
instance IsEmpty s => IsEmpty (Monotone (s,a) (s,b)) where
empty = Monotone empty empty
instance Show s => Show (Monotone s s) where
show (Monotone s) = show s
instance (Show s, Show a, Show b) => Show (Monotone (s,a) (s,b)) where
show (Monotone s m) = show (s,m)
instance (Arrow c, Profunctor c) => ArrowParallel (CacheT Monotone a b c) where
nextIteration = id
{-# INLINE nextIteration #-}
instance (ArrowChoice c, Profunctor c) => ArrowCache s s (CacheT Monotone s s c) where
initialize = id
lookup = CacheT $ proc s -> returnA -< Just (Unstable, s)
update = CacheT $ askConst $ \widening -> modify' $ \((_,sNew), Monotone sOld) ->
let y@(_,sWiden) = widening sOld sNew
in (y,Monotone sWiden)
instance (Identifiable a, LowerBounded b, ArrowChoice c, Profunctor c) => ArrowCache (s,a) (s,b) (CacheT Monotone (s,a) (s,b) c) where
initialize = CacheT $ modify' $ \((s,a),Monotone s' cache) ->
let cache' = M.insertWith (\_ _old -> _old) a bottom cache
b = M.lookupDefault bottom a cache
in ((s,b),Monotone s' cache')
lookup = CacheT $ proc (s,a) -> do
m <- get -< ()
case m of
Monotone _ cache ->
returnA -< (\b -> (Unstable,(s,b))) <$> M.lookup a cache
update = CacheT $ askConst $ \(widenS,widenB) -> modify' $ \(((_,a),(sNew,b)),Monotone sOld cache) ->
let (stable1,sWiden) = widenS sOld sNew
in case M.lookup a cache of
Just b' ->
let ~(stable2,b'') = widenB b' b
in ((stable1 stable2, (sWiden,b'')), Monotone sWiden (M.insert a b'' cache))
Nothing -> ((Unstable,(sWiden,b)),Monotone sWiden (M.insert a b cache))
write = CacheT $ proc _ -> returnA -< ()
setStable = CacheT $ proc _ -> returnA -< ()
{-# INLINE initialize #-}
......
......@@ -28,6 +28,9 @@ import Data.Profunctor
import Data.Profunctor.Unsafe ((.#))
import Data.Coerce
import Data.Empty
import Data.HashSet (HashSet)
import qualified Data.HashSet as Set
import Data.Identifiable
newtype StackT stack a c x y = StackT (ReaderT (stack a) c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowJoin,ArrowComplete z,
......@@ -35,18 +38,25 @@ newtype StackT stack a c x y = StackT (ReaderT (stack a) c x y)
ArrowParallel,ArrowControlFlow stmt)
data Stack a = Stack
{ elems :: [a]
{ elems :: HashSet a
, stack :: [a]
, size :: !Int
}
instance IsEmpty (Stack a) where
empty = Stack { elems = [], size = 0 }
empty = Stack { elems = empty, stack = empty, size = 0 }
{-# INLINE empty #-}
instance (Arrow c, Profunctor c) => ArrowStack a (StackT Stack a c) where
push f = lift $ proc (st,a) -> unlift f -< (st { elems = a : elems st, size = size st + 1 }, a)
peek = lift $ proc (st,()) -> returnA -< case elems st of [] -> Nothing; (x:_) -> Just x
elems = lift $ proc (st,()) -> returnA -< elems st
instance (Identifiable a, Arrow c, Profunctor c) => ArrowStack a (StackT Stack a c) where
push f = lift $ proc (st,a) -> do
let st' = st { elems = Set.insert a (elems st)
, stack = a : stack st
, size = size st + 1
}
unlift f -< (st', a)
elem = lift $ proc (st,a) -> returnA -< Set.member a (elems st)
peek = lift $ proc (st,()) -> returnA -< case stack st of [] -> Nothing; (x:_) -> Just x
elems = lift $ proc (st,()) -> returnA -< stack st
size = lift $ proc (st,()) -> returnA -< size st
{-# INLINE peek #-}
{-# INLINE push #-}
......
......@@ -85,7 +85,7 @@ withBounds2 f (Interval i1 i2) (Interval j1 j2) =
instance (Ord n, Bounded n) => UpperBounded (Interval n) where
top = Interval minBound maxBound
bounded :: Ord n => Interval n -> Widening (Interval (InfiniteNumber n))
bounded :: Ord n => Interval (InfiniteNumber n) -> Widening (Interval (InfiniteNumber n))
bounded (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
( if (i1,i2) P.== (r1,r2) || (j1,j2) P.== (r1,r2) then Stable else Unstable
, Interval r1 r2
......@@ -94,11 +94,11 @@ bounded (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
lower = min i1 j1
upper = max i2 j2
r1 = if | lower P.< Number lowerBound -> NegInfinity
| Number upperBound P.< lower -> Number upperBound
r1 = if | lower P.< lowerBound -> NegInfinity
| upperBound P.< lower -> upperBound
| otherwise -> lower
r2 = if | Number upperBound P.< upper -> Infinity
| upper P.< Number lowerBound -> Number lowerBound
r2 = if | upperBound P.< upper -> Infinity
| upper P.< lowerBound -> lowerBound
| otherwise -> upper
widening :: Ord n => Widening (Interval (InfiniteNumber n))
......
......@@ -59,6 +59,10 @@ instance (ArrowClosure Expr Cls c, ArrowChoice c, ArrowFail String c) => IsVal V
NumVal n -> returnA -< NumVal (n - 1)
_ -> fail -< "Expected a number as argument for 'pred'"
mult = proc x -> case x of
(NumVal n, NumVal m) -> returnA -< NumVal (n * m)
_ -> fail -< "Expected two numbers as argument for 'mult'"
zero = arr $ const (NumVal 0)
if_ f g = proc (v1, (x, y)) -> case v1 of
......
......@@ -40,6 +40,10 @@ eval = fix $ \ev -> proc e0 -> case e0 of
Pred e _ -> do
v <- ev -< e
pred -< v
Mult e1 e2 _ -> do
v1 <- ev -< e1
v2 <- ev -< e2
mult -< (v1,v2)
IfZero e1 e2 e3 _ -> do
v1 <- ev -< e1
if_ ev ev -< (v1, (e2, e3))
......@@ -70,4 +74,6 @@ class IsVal v c | c -> v where
-- | creates the numeric value zero.
zero :: c () v
mult :: c (v,v) v
if_ :: Join z c => c x z -> c y z -> c (v, (x, y)) z
......@@ -24,7 +24,7 @@ import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Environment(extend')
import Control.Arrow.Fix
import Control.Arrow.Fix.Parallel(parallel)
import Control.Arrow.Fix.Chaotic(chaotic)
import qualified Control.Arrow.Fix.Context as Ctx
import Control.Arrow.Trans
import Control.Arrow.Closure (ArrowClosure,IsClosure(..))
......@@ -34,10 +34,11 @@ import Control.Arrow.Transformer.Value
import Control.Arrow.Transformer.Abstract.FiniteEnvironment
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.Chaotic
import Control.Arrow.Transformer.Abstract.Fix.Context
import Control.Arrow.Transformer.Abstract.Fix.Stack
-- import Control.Arrow.Transformer.Abstract.Fix.Trace
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable(CacheT,Cache,Parallel,Monotone,type (**),Group)
import Control.Arrow.Transformer.Abstract.Fix.Trace
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable(CacheT,Monotone)
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Monad.State hiding (lift,fail)
......@@ -92,7 +93,7 @@ type Out = (Store, Terminating (Error (Pow String) Val))
-- | Run the abstract interpreter for an interval analysis. The arguments are the
-- maximum interval bound, the depth @k@ of the longest call string,
-- an environment, and the input of the computation.
evalInterval :: (?sensitivity :: Int, ?bound :: Interval Int) => [(Text,Val)] -> State Label Expr -> (Store, Terminating (Error (Pow String) Val))
evalInterval :: (?sensitivity :: Int, ?bound :: IV) => [(Text,Val)] -> State Label Expr -> (Store, Terminating (Error (Pow String) Val))
evalInterval env0 e = snd $
run (extend' (Generic.eval ::
Fix'
......@@ -101,10 +102,10 @@ evalInterval env0 e = snd $
(TerminatingT
(EnvT Text Addr Val
(FixT _ _
(-- ChaoticT In
(ChaoticT In
(-- TraceT
(StackT Stack In
(CacheT (Monotone ** Parallel (Group Cache)) In Out
(CacheT Monotone In Out
(ContextT Ctx
(->))))))))))) Expr Val))
(alloc, widenVal)
......@@ -122,12 +123,12 @@ evalInterval env0 e = snd $
traceShow .
-- traceCache show .
Ctx.recordCallsite ?sensitivity (\(_,(_,expr)) -> case expr of App _ _ l -> Just l; _ -> Nothing) .
filter apply parallel
filter apply chaotic
widenVal :: Widening Val
widenVal = widening (I.bounded ?bound)
evalInterval' :: (?sensitivity :: Int, ?bound :: Interval Int) => [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval' :: (?sensitivity :: Int, ?bound :: IV) => [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval' env expr = snd $ evalInterval env expr
{-# INLINE evalInterval' #-}
......@@ -142,6 +143,10 @@ instance (IsString e, ArrowChoice c, ArrowFail e c) => IsVal Val (ValueT Val c)
NumVal n -> returnA -< NumVal $ n - 1
_ -> fail -< "Expected a number as argument for 'pred'"
mult = proc x -> case x of
(NumVal n, NumVal m) -> returnA -< NumVal $ n * m
_ -> fail -< "Expected two numbers as argument for 'mult'"
zero = proc _ -> returnA -< NumVal 0
if_ f g = proc v -> case v of
......
......@@ -25,6 +25,7 @@ data Expr
| Lam [Text] Expr Label
| App Expr [Expr] Label
| Zero Label
| Mult Expr Expr Label
| Succ Expr Label
| Pred Expr Label
| IfZero Expr Expr Expr Label
......@@ -52,6 +53,9 @@ succ e = Succ <$> e <*> fresh
pred :: State Label Expr -> State Label Expr
pred e = Pred <$> e <*> fresh
mult :: State Label Expr -> State Label Expr -> State Label Expr
mult e1 e2 = Mult <$> e1 <*> e2 <*> fresh
ifZero :: State Label Expr -> State Label Expr -> State Label Expr -> State Label Expr
ifZero e1 e2 e3 = IfZero <$> e1 <*> e2 <*> e3 <*> fresh
......@@ -78,6 +82,10 @@ instance Show Expr where
$ showsPrec (app_prec + 1) e1
. showString " "
. showsPrec (app_prec + 1) e2
Mult e1 e2 _ -> showParen (d > mult_prec)
$ showsPrec (mult_prec + 1) e1
. showString " * "
. showsPrec (mult_prec + 1) e2
Lam x e2 _ -> showParen (d > lam_prec)
$ showString "λ"
. showString (unwords (map unpack x))
......@@ -86,6 +94,7 @@ instance Show Expr where
where
app_prec = 10
lam_prec = 9
mult_prec = 8
instance HasLabel Expr where
label e = case e of
......@@ -95,6 +104,7 @@ instance HasLabel Expr where
Zero l -> l
Succ _ l -> l
Pred _ l -> l
Mult _ _ l -> l
IfZero _ _ _ l -> l
Let _ _ l -> l
Apply _ l -> l
......@@ -123,6 +133,7 @@ freeVars e0 = execState (go e0) M.empty
Zero _ -> return H.empty
Succ e1 _ -> go e1
Pred e1 _ -> go e1
Mult e1 e2 _ -> H.union <$> go e1 <*> go e2
IfZero e1 e2 e3 _ -> do
m1 <- go e1
m2 <- go e2
......
......@@ -9,6 +9,7 @@ import Data.Abstract.DiscretePowerset(Pow)
import Data.Abstract.Error hiding (toEither)
import qualified Data.Abstract.Interval as I
import Data.Abstract.Terminating hiding (toEither)
import Data.Abstract.InfiniteNumbers(InfiniteNumber(..))
import Test.Hspec
import SharedSpecs
......@@ -51,7 +52,14 @@ spec = do
evalInterval' [("x", num 0 1)] (let_ [("add",add)] (app "add" ["x",two]))
-- Most precise would be [2,3], however, the analysis does not refine
-- `x` and therefore introduces some imprecision.
`shouldBe` Terminating (Success (num 2 5))
`shouldBe` Terminating (Success (num 2 7))
context "the factorial function" $
it "should only return positive numbers" $
let ?bound = I.Interval 0 Infinity
?sensitivity = 1
in evalInterval' [("x", num 0 Infinity)] (let_ [("fact", lam ["n"] (ifZero "n" (succ zero) (mult (app "fact" [pred "n"]) "n")))] (app "fact" ["x"])) `shouldBe`
Terminating (Success (num NegInfinity Infinity))
it "context sensitivity" $
let diamond = let_ [("second",second),("id",id)] (app "second" [app "id" [one],app "id" [two]]) in
......
......@@ -96,7 +96,7 @@ newtype Exception = Exception (Map Text Val) deriving (PreOrd,Complete,Show,Eq)
-- 'Generic.run' with the components for fixpoint computation
-- ('FixT'), termination ('TerminatingT'), failure ('ErrorT'), store
-- ('StoreT'), environments ('EnvT'), and values ('IntervalT').
run :: (?bound :: Interval Int) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (Except Exception (M.Map Addr Val)))
run :: (?bound :: IV) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (Except Exception (M.Map Addr Val)))
run k env ss = fmap (fmap (fmap fst)) <$> snd $
Trans.run
(Generic.run ::
......
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