Commit 509fd75c authored by Sven Keidel's avatar Sven Keidel

use memoize in Abstract.FixT again

parent cd8570b2
......@@ -20,6 +20,7 @@ import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Const
import Control.Arrow.Trans
import Control.Arrow.Abstract.Terminating
import Control.Arrow.Transformer.Abstract.Stack
......@@ -75,7 +76,7 @@ import Text.Printf
-- evaluates to
-- 'Reader Env (State Store (LeastFix Stack (Store,(Env,Expr)) (Store)))'
type Cache a b = Map a (Terminating b)
newtype FixT s a b c x y = FixT (ConstT (Widening b) (StackT s a (ReaderT (Cache a b) (TerminatingT (StateT (Cache a b) c)))) x y)
newtype FixT s a b c x y = FixT { unFixT :: ConstT (Widening b) (StackT s a (ReaderT (Cache a b) (TerminatingT (StateT (Cache a b) c)))) x y }
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTerminating)
type instance Fix x y (FixT s () () c) = FixT s x y c
......@@ -101,17 +102,16 @@ liftFixT = lift'
instance ArrowLift (FixT s a b) where
lift' f = FixT (ConstT (StaticT (const (StackT (ConstT (StaticT (const (ReaderT (TerminatingT (StateT (lmap snd (second (rmap Terminating f)))))))))))))
#ifndef TRACE
instance (Identifiable x, PreOrd y, ArrowChoice c, Profunctor c) => ArrowFix x y (FixT s x y c) where
instance (Identifiable x, PreOrd y, ArrowChoice c, ArrowApply c, Profunctor c, ArrowFix (Cache x y, (Cache x y, x)) (Cache x y, Terminating y) c)
=> ArrowFix x y (FixT s x y c) where
fix f = proc x -> do
old <- getCache -< ()
-- reset the current fixpoint cache
setCache -< bottom
-- recompute the fixpoint cache by calling 'f' and memoize its results.
-- y <- localOldCache (F.fix (memoize . f)) -< (old,x)
y <- localOldCache (F.fix f) -< (old,x)
y <- localOldCache (FixT (fix (unFixT . memoize . f . FixT))) -< (old,x)
new <- getCache -< ()
......@@ -120,63 +120,103 @@ instance (Identifiable x, PreOrd y, ArrowChoice c, Profunctor c) => ArrowFix x y
-- overshot the fixpoint and stop recursion. Otherwise, we have
-- not reached the fixpoint yet and need to continue improving the
-- fixpoint cache.
if {-# SCC "Fix.Cache.comparison" #-}(new old)
if {-# SCC "Fix.Cache.comparison" #-} (new old)
then returnA -< y
else fix f -< x
-- | Memoizes the results of the interpreter function. In case a value
-- 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,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 -< (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 (x',stack') = runState (stackWidening x) stack
-- yOld = fromMaybe bottom (M.unsafeLookup x' oldCache)
-- newCache' = M.insert x' yOld newCache
-- (newCache'',y) <- f (stackWidening,widening) -< (((stack',oldCache), newCache'),x')
-- -- TODO: use insertLookup
-- let newCache''' = M.unsafeInsertWith (flip (T.widening widening)) x' y newCache''
-- y' = fromJust (M.unsafeLookup x' newCache''')
-- returnA -< (newCache''',y')
memoize :: (Identifiable x, PreOrd y, ArrowChoice c, Profunctor c) => FixT s x y c x y -> FixT s x y c x y
memoize f = proc x -> do
newCache <- getCache -< ()
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 -> throwTerminating -< 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
oldCache <- getOldCache -< ()
setCache -< M.insert x (fromMaybe bottom (M.unsafeLookup x oldCache)) newCache
y <- catchTerminating f -< x
(widening, newCache') <- (getWidening &&& getCache) -< ()
-- TODO: use insertLookup
let newCache'' = M.unsafeInsertWith (flip (T.widening widening)) x y newCache'
y' = fromJust (M.unsafeLookup x newCache'')
setCache -< newCache''
throwTerminating -< 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
instance (Show x, Show y, Identifiable x, PreOrd y, ArrowChoice c, ArrowApply c, Profunctor c, ArrowFix (Cache x y, (Cache x y, x)) (Cache x y, Terminating y) c)
=> ArrowFix x y (FixT s x y c) where
fix f = proc x -> do
old <- getCache -< ()
setOutCache -< bottom
y <- localInCache (F.fix (memoize . f)) -< trace "----- ITERATION -----" $ (old,x)
new <- getOutCache -< ()
if (new old)
setCache -< bottom
y <- localOldCache (FixT (fix (unFixT . memoize . f . FixT))) -< trace "----- ITERATION -----" (old,x)
new <- getCache -< ()
if {-# SCC "Fix.Cache.comparison" #-} (new old)
then returnA -< y
else fix f -< x
memoize :: (Show x, Show y, 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
Just y -> returnA -< trace (printf "HIT: %s -> %s" (show x) (show y))
(outCache,y)
-- | Memoizes the results of the interpreter function. In case a value
-- has been computed before, the cached value is returned and will not
-- be recomputed.
memoize :: (Show x, Show y,Identifiable x, PreOrd y, ArrowChoice c, Profunctor c) => FixT s x y c x y -> FixT s x y c x y
memoize f = proc x -> do
newCache <- getCache -< ()
case M.unsafeLookup x newCache of
Just y -> throwTerminating -< trace (printf "HIT: %s -> %s" (show x) (show y)) y
Nothing -> do
let yOld = fromMaybe bottom (M.unsafeLookup x inCache)
outCache' = M.insert x yOld outCache
(x',stack') = runState (stackWidening x) stack
(outCache'',y) <- f (stackWidening,widening) -< trace (printf "CALL: %s" (show x')) (((stack',inCache), outCache'),x')
let outCache''' = M.unsafeInsertWith (flip (T.widening widening)) x' y outCache''
y' = fromJust (M.unsafeLookup x' outCache''')
returnA -< trace (printf "CACHE: %s := (%s -> %s)\n" (show x) (show y) (show y') ++
printf "RET: %s -> %s" (show x') (show y'))
(M.unsafeInsertWith (flip (T.widening widening)) x y outCache'',y')
oldCache <- getOldCache -< ()
setCache -< M.insert x (fromMaybe bottom (M.unsafeLookup x oldCache)) newCache
y <- catchTerminating f -< x
(widening, newCache') <- (getWidening &&& getCache) -< ()
let newCache'' = M.unsafeInsertWith (flip (T.widening widening)) x y newCache'
y' = fromJust (M.unsafeLookup x newCache'')
setCache -< newCache''
throwTerminating -< trace (printf "RET: %s -> %s" (show x) (show y')) y'
-- 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 <- getCache -< ()
-- setOutCache -< bottom
-- y <- localInCache (F.fix (memoize . f)) -< trace "----- ITERATION -----" $ (old,x)
-- new <- getOutCache -< ()
-- if (new ⊑ old)
-- then returnA -< y
-- else fix f -< x
-- memoize :: (Show x, Show y, 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
-- Just y -> returnA -< trace (printf "HIT: %s -> %s" (show x) (show y))
-- (outCache,y)
-- Nothing -> do
-- let yOld = fromMaybe bottom (M.unsafeLookup x inCache)
-- outCache' = M.insert x yOld outCache
-- (x',stack') = runState (stackWidening x) stack
-- (outCache'',y) <- f (stackWidening,widening) -< trace (printf "CALL: %s" (show x')) (((stack',inCache), outCache'),x')
-- let outCache''' = M.unsafeInsertWith (flip (T.widening widening)) x' y outCache''
-- y' = fromJust (M.unsafeLookup x' outCache''')
-- returnA -< trace (printf "CACHE: %s := (%s -> %s)\n" (show x) (show y) (show y') ++
-- printf "RET: %s -> %s" (show x') (show y'))
-- (M.unsafeInsertWith (flip (T.widening widening)) x y outCache'',y')
#endif
getWidening :: (ArrowChoice c, Profunctor c) => FixT s x y c () (Widening y)
getWidening = FixT askConst
getOldCache :: (ArrowChoice c, Profunctor c) => FixT s x y c () (Cache x y)
getOldCache = FixT ask
getCache :: (ArrowChoice c, Profunctor c) => FixT s x y c () (Cache x y)
getCache = FixT get
......
......@@ -14,6 +14,7 @@ import Control.Arrow.Const
import Control.Arrow.Trans
import Control.Arrow.State
import Control.Arrow.Reader
import Control.Arrow.Fix
import Control.Arrow.Abstract.Terminating
import Control.Category
......@@ -74,6 +75,10 @@ instance (ArrowChoice c, ArrowReader r c) => ArrowReader r (TerminatingT c) wher
instance (ArrowChoice c, ArrowConst x c) => ArrowConst x (TerminatingT c) where
askConst = lift' askConst
type instance Fix x y (TerminatingT c) = TerminatingT (Fix (Dom TerminatingT x y) (Cod TerminatingT x y) c)
instance (ArrowChoice c, ArrowFix (Dom TerminatingT x y) (Cod TerminatingT x y) c) => ArrowFix x y (TerminatingT c) where
fix = liftFix
deriving instance PreOrd (c x (Terminating y)) => PreOrd (TerminatingT c x y)
deriving instance LowerBounded (c x (Terminating y)) => LowerBounded (TerminatingT c x y)
deriving instance Complete (c x (Terminating y)) => Complete (TerminatingT c x y)
......
......@@ -93,7 +93,7 @@ spec = do
f -< (m'- I.Interval 1 1, x)) -<< n)
-<< m
in it "ackerman ([0,inf], [0,inf]) should be [0,inf] " $ do
runFixT' (SW.stack (SW.reuse (const head) SW.topOut)) W.finite ackermann (I.Interval 0 Infinity, I.Interval 0 Infinity)
runFixT' (SW.stack (SW.reuse (const head) SW.topOut)) I.widening ackermann (I.Interval 0 Infinity, I.Interval 0 Infinity)
`shouldBe` return (I.Interval 1 Infinity)
describe "the analyis of a diverging program" $
......
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