gitlab.rlp.net will be temporarily unavailable for maintenance reasons on 2021-01-15 21:00 - 23:00

gitlab.rlp.net will be temporarily unavailable for maintenance reasons on 2021-01-15 21:00 - 23:00

Add tracing to fixpoint algorithm

parent f451adf3
...@@ -10,6 +10,7 @@ ...@@ -10,6 +10,7 @@
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE CPP #-}
module Control.Arrow.Transformer.Abstract.Fixpoint(Fix,FixT,runFixT,runFixT',runFixT'',liftFixT) where module Control.Arrow.Transformer.Abstract.Fixpoint(Fix,FixT,runFixT,runFixT',runFixT'',liftFixT) where
import Prelude hiding (id,(.),lookup) import Prelude hiding (id,(.),lookup)
...@@ -35,6 +36,13 @@ import qualified Data.Abstract.Widening as W ...@@ -35,6 +36,13 @@ import qualified Data.Abstract.Widening as W
import Data.Abstract.StackWidening (StackWidening) import Data.Abstract.StackWidening (StackWidening)
import qualified Data.Abstract.StackWidening as SW import qualified Data.Abstract.StackWidening as SW
#define TRACE
#ifdef TRACE
import Debug.Trace
import Text.Printf
#endif
-- | Fixpoint algorithm that computes the least fixpoint of an arrow computation. -- | Fixpoint algorithm that computes the least fixpoint of an arrow computation.
-- This fixpoint caching algorithm is due to /Abstract Definitional -- This fixpoint caching algorithm is due to /Abstract Definitional
-- Interpreters, David Darais et. al., ICFP' 17/. We made some -- Interpreters, David Darais et. al., ICFP' 17/. We made some
...@@ -75,6 +83,8 @@ runFixT'' sw w (FixT f) = (\x -> (((mempty,M.empty),M.empty),x)) ^>> f (sw,w) ...@@ -75,6 +83,8 @@ runFixT'' sw w (FixT f) = (\x -> (((mempty,M.empty),M.empty),x)) ^>> f (sw,w)
liftFixT :: Arrow c => c x y -> FixT s a b c x y liftFixT :: Arrow c => c x y -> FixT s a b c x y
liftFixT f = FixT $ \_ -> ((\((_,o),x) -> (o,x)) ^>> second (f >>^ Terminating)) 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 instance (Identifiable x, PreOrd y, ArrowChoice c) => ArrowFix x y (FixT s x y c) where
fix f = proc x -> do fix f = proc x -> do
old <- getOutCache -< () old <- getOutCache -< ()
...@@ -113,7 +123,39 @@ memoize (FixT f) = FixT $ \(stackWidening,widening) -> proc (((stack,inCache), o ...@@ -113,7 +123,39 @@ memoize (FixT f) = FixT $ \(stackWidening,widening) -> proc (((stack,inCache), o
outCache' = M.insert x yOld outCache outCache' = M.insert x yOld outCache
(x',stack') = runState (stackWidening x) stack (x',stack') = runState (stackWidening x) stack
(outCache'',y) <- f (stackWidening,widening) -< (((stack',inCache), outCache'),x') (outCache'',y) <- f (stackWidening,widening) -< (((stack',inCache), outCache'),x')
returnA -< (M.unsafeInsertWith (flip (T.widening widening)) x y outCache'',y) let outCache''' = M.unsafeInsertWith (flip (T.widening widening)) x' y outCache''
let y' = outCache''' M.! x'
returnA -< (outCache''',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 -< ()
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' = fromMaybe (error "x not in cache") (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
getOutCache :: Arrow c => FixT s x y c () (Map x (Terminating y)) getOutCache :: Arrow c => FixT s x y c () (Map x (Terminating y))
getOutCache = FixT $ \_ -> arr $ \((_,o),()) -> (o,return o) getOutCache = FixT $ \_ -> arr $ \((_,o),()) -> (o,return o)
......
...@@ -24,7 +24,7 @@ toEither (Terminating a) = Right a ...@@ -24,7 +24,7 @@ toEither (Terminating a) = Right a
toEither NonTerminating = Left () toEither NonTerminating = Left ()
instance Show a => Show (Terminating a) where instance Show a => Show (Terminating a) where
show NonTerminating = "" show NonTerminating = "NonTerminating"
show (Terminating a) = show a show (Terminating a) = show a
instance Applicative Terminating where instance Applicative Terminating where
......
...@@ -248,7 +248,7 @@ spec = do ...@@ -248,7 +248,7 @@ spec = do
let ?ctx = Ctx.empty in let ?ctx = Ctx.empty in
let t = term "Exp" let t = term "Exp"
tenv = termEnv [("x",t)] tenv = termEnv [("x",t)]
in seval 2 (Let [("swap", swap)] (Match "x" `Seq` Call "swap" [] [])) t `shouldBe` success (tenv, t) in seval 2 (Let [("swap", swap)] (Match "x" `Seq` Call "swap" [] ["x"])) t `shouldBe` success (tenv, t)
it "should support recursion" $ it "should support recursion" $
let ?ctx = Ctx.empty in let ?ctx = Ctx.empty in
......
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