Commit 25de95c1 authored by Sven Keidel's avatar Sven Keidel

implement chaotic fixpoint iteration

parent 702cf84a
module Control.Arrow.Abstract.Terminating where
import Control.Arrow
import Data.Abstract.Terminating
import Data.Profunctor
class (Arrow c, Profunctor c) => ArrowTerminating c where
throwTerminating :: c (Terminating x) x
catchTerminating :: c x y -> c x (Terminating y)
......@@ -6,12 +6,7 @@
module Control.Arrow.State where
import Prelude hiding (id,(.),const)
import qualified Prelude as P
import Control.Category
import Control.Arrow
import Control.Arrow.Utils
import Control.Monad.State (MonadState)
import qualified Control.Monad.State as M
import Data.Profunctor
-- | Arrow-based interface to describe stateful computations.
......@@ -21,14 +16,9 @@ class (Arrow c, Profunctor c) => ArrowState s c | c -> s where
-- | Sets the current state.
put :: c s ()
-- | run computation that modifies the current state.
modify :: ArrowState s c => c (x,s) s -> c x ()
modify f = put <<< f <<< (id &&& const get)
-- | run computation that modifies the current state.
modify' :: ArrowState s c => c (s,x) s -> c x ()
modify' f = put <<< f <<< (const get &&& id)
instance MonadState s m => ArrowState s (Kleisli m) where
get = Kleisli (P.const M.get)
put = Kleisli M.put
modify :: c (x,s) (y,s) -> c x y
modify f = proc x -> do
s <- get -< ()
(y,s') <- f -< (x,s)
put -< s'
returnA -< y
{-# LANGUAGE Arrows #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Abstract.Fix(FixT,runFixT) where
import Control.Arrow hiding (loop)
import Control.Arrow.Const
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Const
import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.State
import Control.Category
import qualified Control.Monad.State as S
import Data.Identifiable
import Data.Order
import Data.Abstract.Widening (Widening)
import Data.Abstract.StackWidening (StackWidening,Loop(..))
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.HashSet (HashSet)
import qualified Data.HashSet as H
import Data.Profunctor
#ifdef TRACE
import Debug.Trace
import Text.Printf
#endif
type Cache a b = HashMap a b
type Component a = HashSet a
newtype FixT s a b c x y = FixT { unFixT :: ConstT (StackWidening s a, Widening b) (ReaderT (s a) (StateT (Cache a b, Component a) c)) x y }
deriving (Profunctor,Category,Arrow,ArrowChoice)
type instance Fix x y (FixT s () () c) = FixT s x y c
runFixT :: (Identifiable a, PreOrd b, Monoid (s a),ArrowChoice c, Profunctor c) => StackWidening s a -> Widening b -> FixT s a b c x y -> c x y
runFixT sw w f = dimap (\x -> ((M.empty,H.empty),(mempty,x))) snd $ runStateT $ runReaderT $ runConstT (sw,w) $ unFixT f
#ifndef TRACE
instance (Identifiable a, LowerBounded b, Profunctor c,ArrowChoice c) => ArrowFix a b (FixT s a b c) where
fix f = FixT $ proc x -> do
(stackWiden,stack) <- getStackWidening -< ()
let ((loop,x'),stack') = S.runState (stackWiden x) stack
case loop of
-- If we are not in a loop, continue recursing.
NoLoop -> do
y <- local (unFixT (f (fix f))) -< (stack',x')
comp <- getComponent -< ()
if not (H.null comp) && x' `H.member` comp
then do
yOld <- updateCache -< (x',bottom)
yNew <- updateCache -< (x',y)
deleteFromComponent -< x'
-- If we did not reach a fixpoint of f(x'), keep iterating.
if x' `isHeadOf` comp && yOld yNew
then unFixT (fix f) -< x
else returnA -< yNew
else do
returnA -< y
-- If we are in a loop, return the cached value or bottom otherwise.
-- Furthermore, add x' to the current component.
Loop -> do
addToComponent -< x'
updateCache -< (x',bottom)
where
y y' = {- y ⊑ y' && -} not (y' y)
#else
instance (Show a, Show b, Show (s a), Identifiable a, LowerBounded b, Profunctor c,ArrowChoice c) => ArrowFix a b (FixT s a b c) where
fix f = FixT $ proc x -> do
(stackWiden,stack) <- getStackWidening -< ()
let ((loop,x'),stack') = S.runState (stackWiden x) stack
case loop of
NoLoop -> do
y <- local (unFixT (f (fix f))) -< trace (printf "call [%s -> %s, %s]" (show x) (show x') (show stack)) $ (stack',x')
comp <- getComponent -< ()
if not (H.null comp) && x' `H.member` comp
then do
yOld <- updateCache -< (x',bottom)
yNew <- updateCache -< (x',y)
deleteFromComponent -< x'
if x' `isHeadOf` comp && yOld yNew
then unFixT (fix f) -< trace (printf "iterate [%s -> %s, %s] = [%s -> %s]" (show x) (show x') (show stack) (show yOld) (show yNew)) $ x
else returnA -< if x' `isHeadOf` comp then trace (printf "fixed [%s -> %s] = %s" (show x) (show x') (show yNew)) yNew else yNew
else do
returnA -< y
-- returnA -< trace (printf "return [%s -> %s] = %s" (show x) (show x') (show y)) y
-- If we are in a loop, return the cached value or bottom otherwise.
-- Furthermore, add x' to the current component.
Loop -> do
addToComponent -< x'
y <- updateCache -< (x',bottom)
-- returnA -< y
returnA -< trace (printf "loop [%s -> %s, %s] = %s" (show x) (show x') (show stack) (show y)) y
where
y y' = {- y ⊑ y' && -} not (y' y)
#endif
instance (ArrowJoin c, ArrowChoice c) => ArrowJoin (FixT s a b c) where
-- | The join operation of the 'FixT' arrow *does not* join the
-- cache for efficiency. This assumes that the cache is extended
-- only monotonically. Furthermore, this join operation *is not*
-- commutative, but it is still associative and computes an upper
-- bound.
joinWith lub_ f g = rmap (uncurry lub_) (f &&& g)
instance (ArrowJoin (FixT s a b c), Profunctor c, Complete y, PreOrd (c x y)) => Complete (FixT s a b c x y) where
f g = joinWith () f g
instance PreOrd (c x y) => PreOrd (FixT s a b c x y) where
() = error "f ⊑ g iff forall x. snd (f x) ⊑ snd (g x)"
instance (ArrowApply c, Profunctor c) => ArrowApply (FixT s a b c) where
app = FixT (lmap (first unFixT) app)
----- Helper functions -----
getStackWidening :: (ArrowConst (StackWidening s a,r) c, ArrowReader (s a) c) => c () (StackWidening s a,s a)
getStackWidening = rmap (first fst) (askConst &&& ask)
updateCache :: (Identifiable a, LowerBounded b, ArrowState (Cache a b,Component a) c) => ConstT (r,Widening b) c (a,b) b
updateCache = constT $ \(_,widen) -> modify' (\(x,y) -> insertWithLookup (\new old -> if new bottom then old else widen old new) x y) (curry snd)
getComponent :: ArrowState (Cache a b,Component a) c => c () (Component a)
getComponent = rmap snd get
addToComponent :: (Identifiable a,ArrowState (Cache a b,Component a) c) => c a ()
addToComponent = modify (arr (\(x,(cache,comp)) -> ((),(cache,H.insert x comp))))
isHeadOf :: Identifiable a => a -> Component a -> Bool
isHeadOf x comp = H.singleton x == comp
deleteFromComponent :: (Identifiable a,ArrowState (Cache a b,Component a) c) => c a ()
deleteFromComponent = modify (arr (\(x,(cache,comp)) -> ((),(cache,H.delete x comp))))
modify' :: ArrowState (Cache a b,Component a) c => (x -> Cache a b -> (y,Cache a b)) -> (x -> Component a -> Component a) -> c x y
modify' f g = modify (arr $ \(x,(cache,comp)) -> let (y,cache') = f x cache in (y,(cache',g x comp)))
insertWithLookup :: Identifiable a => (b -> b -> b) -> a -> b -> HashMap a b -> (b,HashMap a b)
insertWithLookup w a b m =
let m' = M.insertWith w a b m
in (m' M.! a, m')
This diff is collapsed.
......@@ -28,7 +28,6 @@ import Control.Arrow.Trans
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Fail
import Control.Arrow.Random
import Control.Arrow.Store as Store
import Control.Arrow.Environment
import Control.Arrow.Abstract.Join
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Abstract.Stack(StackT(..),runStackT,runStackT',stackT) where
import Prelude hiding ((.))
import Control.Category
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.State
import Control.Arrow.Reader
import Control.Arrow.Const
import Control.Arrow.Abstract.Join
import Control.Arrow.Abstract.Terminating
import Control.Arrow.Transformer.Const
import Control.Arrow.Transformer.Static
import Control.Arrow.Transformer.Reader
import qualified Control.Monad.State as M
import Data.Order
import Data.Profunctor
import Data.Abstract.StackWidening (StackWidening)
newtype StackT s a c x y = StackT { unStackT :: ConstT (StackWidening s a) (ReaderT (s a) c) x y }
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowJoin, ArrowState r,ArrowTerminating)
runStackT :: (Arrow c, Profunctor c) => (StackWidening s a,s a) -> StackT s a c x y -> c x y
runStackT (w,s) (StackT f) = lmap (s,) (runReaderT (runConstT w f))
runStackT' :: (Arrow c, Profunctor 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 -> c (s a,x) y) -> StackT s a c x y
stackT f = StackT $ ConstT $ StaticT $ \w -> ReaderT (f w)
type instance Fix x y (StackT s () c) = StackT s x (Fix x y c)
instance (Profunctor c,ArrowFix (s x,x) y c) => ArrowFix x y (StackT s x c) where
fix f = StackT $ fix (unStackT . widen . f . StackT)
where
widen :: (Arrow c, Profunctor c) => StackT s x c x y -> StackT s x c x y
widen (StackT f') = proc x -> do
stackWiden <- StackT askConst -< ()
stack <- StackT ask -< ()
let (x',stack') = M.runState (stackWiden x) stack
StackT (local f') -< (stack',x')
instance (ArrowApply c,Profunctor c) => ArrowApply (StackT s a c) where
app = StackT (lmap (\(StackT f,x) -> (f,x)) app)
instance ArrowLift (StackT s a) where
lift' = StackT . lift' . lift'
deriving instance PreOrd (c (s a,x) y) => PreOrd (StackT s a c x y)
deriving instance Complete (c (s a,x) y) => Complete (StackT s a c x y)
deriving instance CoComplete (c (s a,x) y) => CoComplete (StackT s a c x y)
deriving instance LowerBounded (c (s a,x) y) => LowerBounded (StackT s a c x y)
deriving instance UpperBounded (c (s a,x) y) => UpperBounded (StackT s a c x y)
......@@ -55,7 +55,7 @@ instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (
Just val -> f -< (val,x)
JustNothing val -> joined f g -< ((val,x),x)
Nothing -> g -< x
write = StoreT $ modify $ arr $ \((var,val),st) -> M.insert var val st
write = StoreT $ modify $ arr $ \((var,val),st) -> ((),M.insert var val st)
instance ArrowState s c => ArrowState s (StoreT var val c) where
get = lift' get
......
......@@ -16,7 +16,7 @@ import Control.Arrow.State
import Control.Arrow.Reader
import Control.Arrow.Fix
import Control.Arrow.Utils(duplicate)
import Control.Arrow.Abstract.Terminating
import Control.Arrow.Abstract.Join
import Control.Category
import Data.Abstract.Terminating
......@@ -27,10 +27,6 @@ import Data.Profunctor
-- | Arrow that propagates non-terminating computations.
newtype TerminatingT c x y = TerminatingT { runTerminatingT :: c x (Terminating y) }
instance (ArrowChoice c,Profunctor c) => ArrowTerminating (TerminatingT c) where
throwTerminating = lift id
catchTerminating f = lift $ rmap Terminating (unlift f)
instance ArrowTrans TerminatingT where
type Dom TerminatingT x y = x
type Cod TerminatingT x y = (Terminating y)
......@@ -80,6 +76,9 @@ type instance Fix x y (TerminatingT c) = TerminatingT (Fix (Dom TerminatingT x y
instance (ArrowChoice c, ArrowFix (Dom TerminatingT x y) (Cod TerminatingT x y) c) => ArrowFix x y (TerminatingT c) where
fix = liftFix
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (TerminatingT c) where
joinWith lub' f g = lift $ joinWith (widening lub') (unlift f) (unlift g)
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)
......
......@@ -52,7 +52,7 @@ instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (
case S.lookup var s of
Just v -> f -< (v,x)
Nothing -> g -< x
write = StoreT $ modify $ arr (\((x,v),s) -> S.insert x v s)
write = StoreT $ modify $ arr (\((x,v),s) -> ((),S.insert x v s))
instance ArrowState s c => ArrowState s (StoreT var val c) where
get = lift' get
......
......@@ -25,7 +25,6 @@ import Control.Arrow.Store
import Control.Arrow.Const
import Control.Arrow.Writer
import Control.Arrow.Abstract.Join
import Control.Arrow.Abstract.Terminating
import Control.Arrow.Transformer.Static
......@@ -37,7 +36,7 @@ newtype ConstT r c x y = ConstT (StaticT ((->) r) c x y)
deriving (Category,Profunctor,Arrow,ArrowChoice,ArrowJoin,ArrowLift,
ArrowState s,ArrowReader r',ArrowWriter w,
ArrowEnv var val env, ArrowStore var val,
ArrowFail e, ArrowExcept e, ArrowTerminating,
ArrowFail e, ArrowExcept e,
PreOrd, Complete, CoComplete, UpperBounded, LowerBounded)
runConstT :: r -> ConstT r c x y -> c x y
......
......@@ -26,7 +26,6 @@ import Control.Arrow.Trans
import Control.Arrow.Writer
import Control.Arrow.Utils
import Control.Arrow.Abstract.Join
import Control.Arrow.Abstract.Terminating
import Control.Category
import Data.Profunctor
......@@ -77,6 +76,7 @@ instance (Arrow c, Profunctor c) => ArrowReader r (ReaderT r c) where
instance ArrowState s c => ArrowState s (ReaderT r c) where
get = lift' get
put = lift' put
modify f = lift (modify (lmap assoc2 (unlift f)))
instance ArrowWriter w c => ArrowWriter w (ReaderT r c) where
tell = lift' tell
......@@ -84,10 +84,6 @@ instance ArrowWriter w c => ArrowWriter w (ReaderT r c) where
instance ArrowFail e c => ArrowFail e (ReaderT r c) where
fail = lift' fail
instance ArrowTerminating c => ArrowTerminating (ReaderT r c) where
throwTerminating = lift' throwTerminating
catchTerminating f = lift $ catchTerminating (unlift f)
instance ArrowEnv var val env c => ArrowEnv var val env (ReaderT r c) where
type instance Join (ReaderT r c) ((val,x),x) y = Env.Join c ((val,Dom (ReaderT r) x y),Dom (ReaderT r) x y) (Cod (ReaderT r) x y)
lookup f g = lift $ lmap (\(r,(v,a)) -> (v,(r,a)))
......
......@@ -81,7 +81,7 @@ instance (ArrowApply c, Profunctor c) => ArrowApply (StateT s c) where
instance (Arrow c, Profunctor c) => ArrowState s (StateT s c) where
get = lift (arr (\(a,()) -> (a,a)))
put = lift (arr (\(_,s) -> (s,())))
modify f = lift (dimap (\(s,x) -> (s,(x,s))) (\(_,(y,s)) -> (s,y)) (unlift f))
instance (ArrowFail e c, Profunctor c) => ArrowFail e (StateT s c) where
fail = lift' fail
......
......@@ -24,7 +24,6 @@ import Control.Arrow.State
import Control.Arrow.Store as Store
import Control.Arrow.Writer
import Control.Arrow.Abstract.Join
import Control.Arrow.Abstract.Terminating
import Data.Profunctor
import Data.Order hiding (lub)
......@@ -61,6 +60,7 @@ instance (Applicative f, ArrowChoice c, Profunctor c) => ArrowChoice (StaticT f
instance (Applicative f, ArrowState s c) => ArrowState s (StaticT f c) where
get = lift' get
put = lift' put
modify (StaticT f) = StaticT $ modify <$> f
instance (Applicative f, ArrowReader r c) => ArrowReader r (StaticT f c) where
ask = lift' ask
......@@ -72,10 +72,6 @@ instance (Applicative f, ArrowWriter w c) => ArrowWriter w (StaticT f c) where
instance (Applicative f, ArrowFail e c) => ArrowFail e (StaticT f c) where
fail = lift' fail
instance (Applicative f, ArrowTerminating c) => ArrowTerminating (StaticT f c) where
throwTerminating = lift' throwTerminating
catchTerminating (StaticT f) = StaticT $ catchTerminating <$> f
instance (Applicative f, ArrowExcept e c) => ArrowExcept e (StaticT f c) where
type Join (StaticT f c) x y = Exc.Join c x y
throw = lift' throw
......
......@@ -72,6 +72,7 @@ instance (Monoid w, ArrowApply c, Profunctor c) => ArrowApply (WriterT w c) wher
instance (Monoid w, ArrowState s c) => ArrowState s (WriterT w c) where
get = lift' get
put = lift' put
modify f = lift $ modify (rmap assoc1 (unlift f))
instance (Monoid w, Arrow c, Profunctor c) => ArrowWriter w (WriterT w c) where
tell = lift (arr (\w -> (w,())))
......
......@@ -4,7 +4,7 @@
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
module Data.Abstract.Map (Map,singleton,empty,lookup,unsafeLookup,insert,insertWith,unsafeInsertWith,delete,union,adjust,toList,fromList,mapMaybe,map,compose,widening,fromThereList) where
module Data.Abstract.Map (Map,singleton,empty,lookup,unsafeLookup,insert,insertWith,unsafeInsertWith,unsafeInsertWithLookup,delete,union,adjust,toList,fromList,mapMaybe,map,compose,widening,fromThereList) where
import Prelude hiding (lookup,map,Either(..),(**))
......@@ -15,6 +15,7 @@ import qualified Data.HashMap.Lazy as H
import Data.Hashable
import Data.Order
import Data.Identifiable
import Data.Maybe (fromJust)
import qualified Data.Abstract.Maybe as M
import qualified Data.Abstract.Either as E
import Data.Abstract.Either(Either(..))
......@@ -87,6 +88,10 @@ insertWith f a b (Map m) = Map (H.insertWith (\(_,new) (here,old) -> case here o
unsafeInsertWith :: (Identifiable a) => (b -> b -> b) -> a -> b -> Map a b -> Map a b
unsafeInsertWith f a b (Map m) = Map (H.insertWith (\(_,new) (_,old) -> (Must,f new old)) a (Must,b) m)
unsafeInsertWithLookup :: (Identifiable a) => (b -> b -> b) -> a -> b -> Map a b -> (b,Map a b)
unsafeInsertWithLookup f a b m =
let m' = unsafeInsertWith f a b m
in (fromJust (unsafeLookup a m'),m')
delete :: Identifiable a => a -> Map a b -> Map a b
delete a (Map m) = Map (H.delete a m)
......
......@@ -19,21 +19,29 @@ import Data.Maybe
import Data.Abstract.Widening(Widening)
import Debug.Trace
-- | A stack widening operator (▽ :: s -> a -> (s,a)) follows the same
-- | A stack widening operator @(▽ :: s -> a -> (s,a))@ follows the same
-- idea as a regular widening operator, but does not have the
-- restriction that the input chain has to be ascending:
-- Given an infinite series x1, x2, x3, x4 ..., the stack widening
-- Given an infinite series @x1, x2, x3, x4 ...@, the stack widening
-- operator produces a series
-- s1 ▽ x1 = (s2,x1') & x1 ⊑ x1'
-- s2 ▽ x2 = (s3,x2') & x2 ⊑ x2'
-- s3 ▽ x3 = (s4,x3') & x3 ⊑ x3'
-- s4 ▽ x4 = (s5,x4') & x4 ⊑ x4'
-- ...
-- such that x1', x2', x3' ... repeats itself, i.e. there exists n,m
-- with n /= m and xn' = xm'.
type StackWidening s a = a -> State (s a) a
data Unit a = Unit
-- @
-- s1 ▽ x1 = (s2,x1') & x1 ⊑ x1'
-- s2 ▽ x2 = (s3,x2') & x2 ⊑ x2'
-- s3 ▽ x3 = (s4,x3') & x3 ⊑ x3'
-- s4 ▽ x4 = (s5,x4') & x4 ⊑ x4'
-- ...
-- @
-- such that @x1', x2', x3' ...@ repeats itself, i.e. there exists @n,m@
-- with @n /= m@ and @xn' = xm'@.
--
-- Furthermore, a stack widening operator has to be monotone in the
-- second argument, i.e., for all @x ⊑ y@, @snd (s ▽ x) ⊑ snd (s ▽ y)@.
type StackWidening s a = a -> State (s a) (Loop,a)
-- | Datatype that signals that we are in a loop.
data Loop = Loop | NoLoop deriving (Show,Eq)
data Unit a = Unit deriving (Show)
instance Semigroup (Unit a) where (<>) = mappend
instance Monoid (Unit a) where
mempty = Unit
......@@ -41,88 +49,120 @@ instance Monoid (Unit a) where
-- | Trivial stack widening if the abstract domain is finite.
finite :: StackWidening Unit a
finite a = return a
finite a = return (NoLoop,a)
finite' :: StackWidening s a
finite' a = return a
finite' a = return (NoLoop,a)
data Stack a = Stack Int [a]
instance Semigroup (Stack a) where (<>) = mappend
instance Monoid (Stack a) where
mempty = Stack 0 []
mappend (Stack n st) (Stack n' st') = Stack (n+n') (st ++ st')
instance Show a => Show (Stack a) where show (Stack _ xs) = show xs
-- | Pushes elements onto a stack and increases its size. Always calls
-- the given widening.
stack :: StackWidening Stack a -> StackWidening Stack a
stack f x = state $ \s@(Stack n st) -> let x' = evalState (f x) s in (x',Stack (n+1) (x':st))
stack f x = state $ \s@(Stack n st) -> let (w,x') = evalState (f x) s in ((w,x'),Stack (n+1) (x':st))
traceStack :: Show a => StackWidening Stack a -> StackWidening Stack a
traceStack f x = state $ \s@(Stack n st) -> let x' = evalState (f x) s in traceShow x' (x',Stack (n+1) (x':st))
traceStack f x = state $ \s@(Stack n st) -> let (w,x') = evalState (f x) s in traceShow (w,x') ((w,x'),Stack (n+1) (x':st))
-- | Return the same elements until the specified maximum stack size
-- is reached, then call the fallback widening.
maxSize :: Int -> StackWidening Stack a -> StackWidening Stack a
maxSize limit fallback x = do
Stack n _ <- get
if n <= limit
then return x
if n < limit
then return (NoLoop,x)
else fallback x
-- | Reuse an element from the stack that is greater than the current
-- element. If no such elements exist, call the fallback widening.
reuse :: (Show a, PreOrd a) => (a -> [a] -> a) -> StackWidening Stack a -> StackWidening Stack a
reuse :: PreOrd a => (a -> [a] -> a) -> StackWidening Stack a -> StackWidening Stack a
reuse bestChoice fallback x = do
Stack _ st <- get
-- All elements in the stack that are greater than the current
-- element are potential candidates.
let candidates = [ y | y <- st, x y ]
if | null st -> return x
| not (null candidates) -> return $ bestChoice x candidates
if | null st -> return (NoLoop,x)
| not (null candidates) -> return (Loop,bestChoice x candidates)
| otherwise -> fallback x
reuse' :: PreOrd a => StackWidening Stack a -> StackWidening Stack a
reuse' = reuse (\_ -> head)
data Categories k b s a = Categories (HashMap k (s b))
instance (Identifiable k, Monoid (s b)) => Semigroup (Categories k b s a) where (<>) = mappend
instance (Identifiable k, Monoid (s b)) => Monoid (Categories k b s a) where
mempty = Categories M.empty
mappend (Categories m) (Categories m') = Categories (m `mappend` m')
instance (Show k, Show (s b)) => Show (Categories k b s a) where
show (Categories m) = show (M.toList m)
categorize :: (Monoid (s b), Identifiable k) => Iso a (k,b) -> StackWidening s b -> StackWidening (Categories k b s) a
categorize iso w a = do
Categories m <- get
let (k,b) = to iso a
s = fromMaybe mempty (M.lookup k m)
(b',s') = runState (w b) s
((l,b'),s') = runState (w b) s
put $ Categories $ M.insert k s' m
return (from iso (k,b'))
return (l,from iso (k,b'))
fromWidening :: Complete a => Widening a -> StackWidening Stack a
fromWidening w a = do
Stack _ s <- get
case s of
[] -> return a
[] -> return (NoLoop,a)
x:_ -> do
let x' = a `w` (x a)
return x'
let x' = x `w` (x a)
return (if (x' x) then Loop else NoLoop,x')
data Product s1 s2 x where
Product :: s1 a -> s2 b -> Product s1 s2 (a,b)
instance (Monoid (s1 a), Monoid (s2 b)) => Semigroup (Product s1 s2 (a,b)) where (<>) = mappend
instance (Monoid (s1 a), Monoid (s2 b)) => Monoid (Product s1 s2 (a,b)) where
mempty = Product mempty mempty
mappend (Product s1 s2) (Product s1' s2') = Product (s1 <> s1') (s2 <> s2')
instance (Show (s1 a), Show (s2 b)) => Show (Product s1 s2 (a,b)) where
show (Product s1 s2) = show (s1,s2)
(**) :: StackWidening s1 a -> StackWidening s2 b -> StackWidening (Product s1 s2) (a,b)
(**) f g (a,b) = do
Product s1 s2 <- get
let (a',s1') = runState (f a) s1
(b',s2') = runState (g b) s2
let ((la,a'),s1') = runState (f a) s1
((lb,b'),s2') = runState (g b) s2
put $ Product s1' s2'
return (a',b')
return (la lb,(a',b'))
(***) :: StackWidening Stack a -> StackWidening Stack b -> StackWidening Stack (a,b)
(***) f g (a,b) = do
Stack i st <- get
let (a',Stack i' as') = runState (f a) (Stack i (map fst st))
(b',Stack i'' bs') = runState (g b) (Stack i' (map snd st))
let ((la,a'),Stack i' as') = runState (f a) (Stack i (map fst st))
((lb,b'),Stack i'' bs') = runState (g b) (Stack i' (map snd st))
put (Stack i'' (zip as' bs'))
return (a',b')
return (la lb,(a',b'))
topOut :: UpperBounded a => StackWidening s a
topOut _ = return top
topOut :: (Eq a,UpperBounded a) => StackWidening Stack a
topOut = topOut' top
topOut' :: Eq a => a -> StackWidening Stack a
topOut' t x = do