Commit 277199d3 authored by Sven Keidel's avatar Sven Keidel

add support for method summaries

parent aa4d8a3a
Pipeline #14110 passed with stages
in 28 minutes and 2 seconds
......@@ -18,12 +18,6 @@ dependencies:
- deepseq
- profunctors
flags:
trace:
description: Enable tracing of the abstract intepreter
default: False
manual: True
library:
ghc-options: -Wall
source-dirs:
......@@ -38,9 +32,9 @@ tests:
source-dirs:
- test
dependencies:
- sturdy-lib
- hspec
- QuickCheck
- sturdy-lib
benchmarks:
arrow-transformers:
......
......@@ -5,20 +5,20 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DefaultSignatures #-}
module Control.Arrow.Fix(ArrowFix(..),Fix,liftFix,IterationStrategy) where
module Control.Arrow.Fix(Fix,ArrowFix(..),liftFix,IterationStrategy) where
import Control.Arrow
import Control.Arrow.Trans
import Data.Profunctor
-- | Arrow-based interface for describing fixpoint computations.
class (Arrow c, Profunctor c) => ArrowFix x y c where
-- | Type family that computes the type of the fixpoint.
type family Fix x y (c :: * -> * -> *) :: * -> * -> *
-- | Interface for describing fixpoint computations.
class (Arrow c, Profunctor c) => ArrowFix x y c where
-- | Computes the fixpoint of an arrow computation.
fix :: (c x y -> c x y) -> c x y
type family Fix x y (c :: * -> * -> *) :: * -> * -> *
type instance Fix x y (->) = (->)
instance ArrowFix x y (->) where
fix f = f (fix f)
......
......@@ -20,6 +20,21 @@ class (Arrow c, Profunctor c) => ArrowComplete y c where
instance Complete y => ArrowComplete y (->) where
(<>) f g = \x -> f x g x
-- | An arrow computation @c@ is effect commutative iff for all @f, g :: c x y@,
--
-- > (f ⊔ g) ⊑ (proc x -> do y1 <- f -< x
-- > y2 <- g -< x
-- > returnA -< y1 ⊔ y2)
--
-- and
--
-- > (f ⊔ g) ⊑ (proc x -> do y1 <- g -< x
-- > y2 <- f -< x
-- > returnA -< y1 ⊔ y2)
--
class (Arrow c, Profunctor c) => ArrowEffectCommutative c
instance ArrowEffectCommutative (->)
class (Arrow c, Profunctor c) => ArrowJoin c where
join :: (y -> y -> y) -> c x y -> c x y -> c x y
......
......@@ -54,6 +54,8 @@ instance (Profunctor c,ArrowApply c) => ArrowApply (FixT a b c) where
instance ArrowLift (FixT a b) where
lift' = FixT . lift'
instance ArrowEffectCommutative c => ArrowEffectCommutative (FixT a b c)
----- Helper functions -----
iterationStrategy :: FixT a b c a b -> FixT a b c a b
iterationStrategy (FixT (ConstT (StaticT f))) = FixT $ ConstT $ StaticT $ \strat -> strat (f strat)
......@@ -15,90 +15,99 @@ import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.Trans
import Control.Arrow.Order(ArrowComplete(..),ArrowJoin(..))
import Control.Arrow.Order(ArrowComplete(..),ArrowJoin(..),ArrowEffectCommutative)
import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.State
import Control.Arrow.Transformer.Writer
import Data.Profunctor
import Data.Order
import Data.HashMap.Lazy(HashMap)
import qualified Data.HashMap.Lazy as M
import Data.HashSet(HashSet)
import qualified Data.HashSet as H
import Data.Identifiable
import Data.Empty
import Data.Coerce
import Data.Abstract.Cache (IsCache)
import qualified Data.Abstract.Cache as Cache
import Data.Abstract.StackWidening(Stack(..))
import Data.Abstract.Widening(Widening,Stable(..))
import Data.Abstract.Widening(Stable(..))
newtype ChaoticT a b c x y =
newtype ChaoticT cache a b c x y =
ChaoticT (
WriterT (Component a)
(StateT (HashMap a (b,Stable))
(StateT (cache a b)
(ReaderT (Stack a) c)) x y)
deriving (Profunctor,Category,Arrow,ArrowChoice)
runChaoticT :: Profunctor c => ChaoticT a b c x y -> c x (HashMap a (b,Stable),y)
runChaoticT (ChaoticT f) = dimap (\a -> (empty,(M.empty,a))) (second snd) (runReaderT (runStateT (runWriterT f)))
runChaoticT :: (IsCache cache a b, Profunctor c) => ChaoticT cache a b c x y -> c x (cache a b,y)
runChaoticT (ChaoticT f) = dimap (\a -> (empty,(empty,a))) (second snd) (runReaderT (runStateT (runWriterT f)))
runChaoticT' :: Profunctor c => ChaoticT a b c x y -> c x y
runChaoticT' :: (IsCache cache a b, Profunctor c) => ChaoticT cache a b c x y -> c x y
runChaoticT' f = rmap snd (runChaoticT f)
chaotic :: (Identifiable a, LowerBounded b, Profunctor c, ArrowChoice c, ArrowApply c) => Widening b -> IterationStrategy (ChaoticT a b c) a b
chaotic :: (Identifiable a, IsCache cache a b, Profunctor c, ArrowChoice c, ArrowApply c) => Cache.Widening cache a b -> IterationStrategy (ChaoticT cache a b c) a b
chaotic widen (ChaoticT (WriterT (StateT f))) = ChaoticT $ WriterT $ StateT $ push $ proc (stack,cache,a) -> do
case M.lookup a cache of
Just (b,Stable) ->
case Cache.lookup a cache of
-- If the cache contains a stable entry, just return it.
Just (Stable,b) ->
returnA -< (cache,(mempty,b))
Just (b,Instable) | H.member a stack ->
-- If the entry has appeared on the stack, stop recursion and
-- return the cached entry. Remember with the fixpoint component
-- set that we need to iterate on this entry.
Just (Instable,b) | H.member a stack ->
returnA -< (cache,(Component {head = H.singleton a, body = H.empty},b))
-- If we did not encounter the entry, register the entry and keep
-- recursing.
_ ->
iterate -<< (M.insertWith (\_ o -> o) a (bottom,Instable) cache,a)
iterate -<< (Cache.initialize a cache,a)
where
iterate = proc (cache,a) -> do
(cache',(component,b)) <- f -< (cache,a)
case () of
-- The call did not depend on any unstable calls. This means we are done and don't need to iterate.
-- The call did not depend on any unstable calls. This means
-- we are done and don't need to iterate.
() | H.null (head component) -> do
returnA -< (M.insert a (b,Stable) cache',(mempty,b))
returnA -< (Cache.insert a b Stable cache',(mempty,b))
-- We are at the head of a fixpoint component. This means, we have to iterate until the head stabilized.
-- We are at the head of a fixpoint component. This means, we
-- have to iterate until the head stabilized.
| head component == H.singleton a -> do
-- Cache.update a b cache
let (bOld,_) = M.lookupDefault (bottom,Instable) a cache
(stable,bNew) = widen bOld b
let cache'' = M.insert a (bNew,stable) cache'
let ((stable,bNew),cache'') = Cache.update widen a b cache'
case stable of
-- If the head of a fixpoint component is stable, flag all elements in the body of the component as stable too and return.
-- If the head of a fixpoint component is stable, set
-- all elements in the body of the component as stable
-- too and return.
Stable -> do
returnA -< (foldr (M.adjust (second (\_ -> Stable))) cache'' (body component),(mempty,bNew))
returnA -< (foldr Cache.setStable cache'' (body component),(mempty,bNew))
-- If the head of a fixpoint component is not stable, keep iterating.
Instable ->
iterate -<< (cache'',a)
-- We are in an unstable fixpoint component, but not at its head. This means, we have to wait until the head stabilized.
-- We are inside an fixpoint component, but its head has not stabilized.
| otherwise -> do
returnA -< (M.insert a (b,Instable) cache,(Component {head = H.delete a (head component), body = H.insert a (body component)}, b))
returnA -< (Cache.insert a b Instable cache',
(Component { head = H.delete a (head component),
body = H.insert a (body component) }, b))
push g = proc (cache,a) -> do
Stack xs <- ask -< ()
local g -< (Stack (H.insert a xs),(xs,cache,a))
instance (Identifiable a, ArrowRun c) => ArrowRun (ChaoticT a b c) where
type Rep (ChaoticT a b c) x y = Rep c x (HashMap a (b,Stable),y)
instance (Identifiable a,IsCache cache a b, ArrowRun c) => ArrowRun (ChaoticT cache a b c) where
type Rep (ChaoticT cache a b c) x y = Rep c x (cache a b,y)
run = run . runChaoticT
instance (Identifiable a,Profunctor c,ArrowApply c) => ArrowApply (ChaoticT a b c) where app = ChaoticT (lmap (first coerce) app)
instance (Identifiable a,Profunctor c,Arrow c) => ArrowJoin (ChaoticT a b c) where
instance (Identifiable a,Profunctor c,ArrowApply c) => ArrowApply (ChaoticT cache a b c) where app = ChaoticT (lmap (first coerce) app)
instance (Identifiable a,Profunctor c,Arrow c) => ArrowJoin (ChaoticT cache a b c) where
join _lub (ChaoticT f) (ChaoticT g) = ChaoticT $ rmap (uncurry _lub) (f &&& g)
instance (Identifiable a,Profunctor c,Arrow c, Complete y) => ArrowComplete y (ChaoticT a b c) where
instance (Identifiable a,Profunctor c,Arrow c, Complete y) => ArrowComplete y (ChaoticT cache a b c) where
ChaoticT f <> ChaoticT g = ChaoticT $ rmap (uncurry ()) (f &&& g)
data Component a = Component { head :: HashSet a, body :: HashSet a }
......@@ -106,3 +115,5 @@ instance Identifiable a => Semigroup (Component a) where (<>) = mappend
instance Identifiable a => Monoid (Component a) where
mempty = Component { head = H.empty, body = H.empty }
c1 `mappend` c2 = Component { head = head c1 <> head c2, body = body c1 <> body c2 }
instance (Identifiable a, ArrowEffectCommutative c) => ArrowEffectCommutative (ChaoticT cache a b c) where
......@@ -30,8 +30,8 @@ import Text.Printf
trace :: (Show a, Show b, Arrow c) => IterationStrategy c a b -> IterationStrategy c a b
trace strat f = proc x -> do
y <- strat f -< x
returnA -< Debug.trace (printf "CALL\nx: %s\nf(x) = %s\n\n" (show x) (show y)) y
y <- strat f -< Debug.trace (printf "CALL\n%s\n\n" (show x)) x
returnA -< Debug.trace (printf "RETURN\neval(%s)\n\t= %s\n\n" (show x) (show y)) y
filter :: (Profunctor c, ArrowChoice c, ArrowApply c) => Prism' a a' -> IterationStrategy c a' b -> IterationStrategy c a b
filter pred strat f = proc a -> case getMaybe pred a of
......
......@@ -16,7 +16,7 @@ import Control.Arrow.Fix
import Control.Arrow.State
import Control.Arrow.Reader
import Control.Arrow.Trans
import Control.Arrow.Order(ArrowComplete(..),ArrowJoin(..))
import Control.Arrow.Order(ArrowComplete(..),ArrowJoin(..),ArrowEffectCommutative)
import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.State
......@@ -27,26 +27,26 @@ import Data.Identifiable
import Data.Empty
import Data.Coerce
import Data.Abstract.Cache(IsCache,Cache)
import Data.Abstract.Cache(IsCache)
import qualified Data.Abstract.Cache as Cache
import Data.Abstract.StackWidening(Stack(..))
import Data.Abstract.Widening(Stable(..))
import qualified Data.Abstract.Widening as W
data Iteration cache a b = Iteration { old :: cache a b, new :: cache a b, stable :: !Stable }
newtype ParallelT a b c x y = ParallelT (ReaderT (Stack a) (StateT (Iteration Cache a b) c) x y)
data Iteration cache a b = Iteration { old :: cache a b, new :: cache a b, stable :: Stable }
newtype ParallelT cache a b c x y = ParallelT (ReaderT (Stack a) (StateT (Iteration cache a b) c) x y)
deriving (Profunctor,Category,Arrow,ArrowChoice)
runParallelT :: (Profunctor c) => ParallelT a b c x y -> c x (Cache a b,y)
runParallelT :: (IsCache cache a b, Profunctor c) => ParallelT cache a b c x y -> c x (cache a b,y)
runParallelT (ParallelT f) = dimap (\a -> (empty,(empty,a))) (first new) (runStateT (runReaderT f))
execParallelT :: (Profunctor c) => ParallelT a b c x y -> c x (Cache a b)
execParallelT :: (IsCache cache a b, Profunctor c) => ParallelT cache a b c x y -> c x (cache a b)
execParallelT f = rmap fst (runParallelT f)
evalParallelT :: (Profunctor c) => ParallelT a b c x y -> c x y
evalParallelT :: (IsCache cache a b, Profunctor c) => ParallelT cache a b c x y -> c x y
evalParallelT f = rmap snd (runParallelT f)
parallel :: (Identifiable a, LowerBounded b, Profunctor c, ArrowChoice c) => Cache.Widening (Iteration Cache) a b -> IterationStrategy (ParallelT a b c) a b
parallel :: (Identifiable a, IsCache cache a b, Profunctor c, ArrowChoice c) => Cache.Widening (Iteration cache) a b -> IterationStrategy (ParallelT cache a b c) a b
parallel widen (ParallelT f) = ParallelT $ push $ proc (xs,a) -> do
cache <- get -< ()
case Cache.lookup a cache of
......@@ -54,15 +54,16 @@ parallel widen (ParallelT f) = ParallelT $ push $ proc (xs,a) -> do
_ -> iterate -< (xs,a)
where
iterate = proc (xs,a) -> do
modify' (\(a,cache) -> ((),Cache.initialize a bottom Instable cache)) -< a
modify' (\(a,cache) -> ((),Cache.initialize a cache)) -< a
b <- f -< a
(st,b') <- modify' (\((a,b),cache) -> Cache.update widen a b cache) -< (a,b)
cache <- get -< ()
if not (H.null xs) || st == Stable
then returnA -< b'
else do
if H.null xs && st == Instable
then do
put -< cache { new = empty, old = new cache, stable = Stable }
iterate -< (xs,a)
else
returnA -< b'
push g = proc a -> do
Stack xs <- ask -< ()
......@@ -70,34 +71,37 @@ parallel widen (ParallelT f) = ParallelT $ push $ proc (xs,a) -> do
instance IsCache cache a b => IsCache (Iteration cache) a b where
type Widening (Iteration cache) a b = Cache.Widening cache a b
lookup a cache = do
(st,b) <- Cache.lookup a (new cache)
return (st stable cache,b)
initialize a b st cache =
case Cache.lookup a (old cache) of
Just (st',b') ->
let new' = Cache.initialize a b' st' (new cache)
in cache { new = new', stable = st' stable cache }
Nothing ->
let new' = Cache.initialize a b st (new cache)
initialize a cache =
case (Cache.lookup a (old cache), Cache.lookup a (new cache)) of
(Just (st,b), Nothing) ->
let new' = Cache.insert a b st (new cache)
in cache { new = new', stable = stable cache st }
(Nothing, Nothing) ->
let new' = Cache.initialize a (new cache)
in cache { new = new', stable = Instable }
(_,_) -> cache
insert a b st cache = cache { new = Cache.insert a b st (new cache)
, stable = stable cache st }
setStable a cache = cache { new = Cache.setStable a (new cache)}
update widen a b cache =
let ((st,b'),new') = Cache.update widen a b (new cache)
st' = st stable cache
st' = stable cache st
in ((st',b'),cache { new = new', stable = st' })
lookup a cache = do
(st,b) <- Cache.lookup a (new cache)
return (stable cache st, b)
instance (ArrowRun c) => ArrowRun (ParallelT a b c) where
type Rep (ParallelT a b c) x y = Rep c x (Cache a b, y)
instance (IsCache cache a b, ArrowRun c) => ArrowRun (ParallelT cache a b c) where
type Rep (ParallelT cache a b c) x y = Rep c x (cache a b, y)
run = run . runParallelT
{-# INLINE run #-}
type instance Fix x y (ParallelT _ _ c) = ParallelT x y c
instance (Profunctor c,ArrowApply c) => ArrowApply (ParallelT a b c) where app = ParallelT (lmap (first coerce) app)
instance (Profunctor c,ArrowApply c) => ArrowApply (ParallelT cache a b c) where app = ParallelT (lmap (first coerce) app)
instance IsEmpty (cache a b) => IsEmpty (Iteration cache a b) where empty = Iteration empty empty W.Stable
instance (Profunctor c,Arrow c) => ArrowJoin (ParallelT a b c) where
instance (ArrowEffectCommutative c) => ArrowJoin (ParallelT cache a b c) where
join _lub (ParallelT f) (ParallelT g) = ParallelT $ rmap (uncurry _lub) (f &&& g)
instance (Profunctor c,Arrow c, Complete y) => ArrowComplete y (ParallelT a b c) where
instance (ArrowEffectCommutative c, Complete y) => ArrowComplete y (ParallelT cache a b c) where
ParallelT f <> ParallelT g = ParallelT $ rmap (uncurry ()) (f &&& g)
instance ArrowEffectCommutative c => ArrowEffectCommutative (ParallelT cache a b c)
......@@ -14,7 +14,7 @@ import Control.Category
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Order(ArrowJoin(..),ArrowComplete(..))
import Control.Arrow.Order(ArrowJoin(..),ArrowComplete(..),ArrowEffectCommutative)
import Control.Arrow.Transformer.Reader
import Data.Profunctor
......@@ -41,3 +41,5 @@ instance (IsEmpty (stack a), ArrowRun c) => ArrowRun (StackWideningT stack a c)
instance (Profunctor c,ArrowApply c) => ArrowApply (StackWideningT stack a c) where
app = StackWideningT (app .# first coerce)
instance ArrowEffectCommutative c => ArrowEffectCommutative (StackWideningT stack a c)
......@@ -12,6 +12,7 @@ import Prelude hiding (id,(.),lookup,fail)
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Environment
import Control.Arrow.Store
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
......@@ -31,7 +32,7 @@ import Data.Coerce
newtype TerminatingT c x y = TerminatingT (KleisliT Terminating c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun,
ArrowConst r, ArrowState s, ArrowReader r,
ArrowEnv var val, ArrowClosure var val env)
ArrowEnv var val, ArrowClosure var val env, ArrowStore addr val)
runTerminatingT :: TerminatingT c x y -> c x (Terminating y)
runTerminatingT = coerce
......
......@@ -165,3 +165,5 @@ instance ArrowComplete y c => ArrowComplete y (ReaderT r c) where
instance ArrowConst x c => ArrowConst x (ReaderT r c) where
askConst f = lift (askConst (unlift . f))
{-# INLINE askConst #-}
instance ArrowEffectCommutative c => ArrowEffectCommutative (ReaderT r c)
......@@ -6,32 +6,34 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE DataKinds #-}
module Control.Arrow.Transformer.State(StateT(..),evalStateT,execStateT) where
import Prelude hiding (id,(.),lookup,read,fail)
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Environment as Env
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Random
import Control.Arrow.Reader as Reader
import Control.Arrow.State as State
import Control.Arrow.Store as Store
import Control.Arrow.Except as Exc
import Control.Arrow.Writer
import Control.Arrow.Order
import Control.Category
import Prelude hiding (id,(.),lookup,read,fail)
import Control.Category
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Environment as Env
import Control.Arrow.Fail as Fail
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Random
import Control.Arrow.Reader as Reader
import Control.Arrow.State as State
import Control.Arrow.Store as Store
import Control.Arrow.Except as Exc
import Control.Arrow.Writer
import Control.Arrow.Order
import Data.Coerce
import Unsafe.Coerce
import qualified Data.Order as O
import Data.Monoidal
import Data.Profunctor hiding (Strong(..))
import Data.Profunctor.Unsafe
import Data.Coerce
import Unsafe.Coerce
import Data.Monoidal
import Data.Profunctor hiding (Strong(..))
import Data.Profunctor.Unsafe
import GHC.TypeLits
-- Due to "Generalising Monads to Arrows", by John Hughes, in Science of Computer Programming 37.
newtype StateT s c x y = StateT { runStateT :: c (s,x) (s,y) }
......@@ -184,6 +186,9 @@ instance ArrowRand v c => ArrowRand v (StateT s c) where
random = lift' random
{-# INLINE random #-}
instance (TypeError ('Text "StateT is not effect commutative since it allows non-monotonic changes to the state."), Arrow c, Profunctor c)
=> ArrowEffectCommutative (StateT s c)
second' :: (x -> y) -> ((z,x) -> (z,y))
second' f (x,y) = (x,f y)
{-# INLINE second' #-}
......@@ -4,83 +4,110 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Abstract.Cache where
import Prelude hiding (lookup)
import Control.Arrow
import Data.Empty
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Identifiable
import Data.Order
import Data.Abstract.Widening (Stable(..))
import qualified Data.Abstract.Widening as W
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Empty
class IsEmpty (cache a b) => IsCache cache a b where
type Widening cache a b :: *
lookup :: a -> cache a b -> Maybe (Stable,b)
initialize :: a -> b -> Stable -> cache a b -> cache a b
-- | Initializes a cache entry with a start value. Initializing the
-- same entry subsequently does not change the cache ('initialize'
-- is idempotent).
initialize :: a -> cache a b -> cache a b
-- | Overwrites a cache entry.
insert :: a -> b -> Stable -> cache a b -> cache a b
-- | Set a cache entry to stable.
-- adjust :: ((Stable,b) -> (Stable,b)) -> a -> cache a b -> cache a b
setStable :: a -> cache a b -> cache a b
-- | Updates a cache entry with a widening operator and returns the widened result.
update :: Widening cache a b -> a -> b -> cache a b -> ((Stable,b),cache a b)
-- | Looks up a cache entry.
lookup :: a -> cache a b -> Maybe (Stable,b)
newtype Cache a b = Cache (HashMap a (Stable,b))
instance IsEmpty (Cache a b) where
empty = Cache M.empty
instance (Identifiable a, LowerBounded b) => IsCache Cache a b where
type Widening Cache a b = a -> W.Widening b
initialize a b st (Cache m) = Cache (M.insertWith (\_ old -> old) a (st,b) m)
lookup a (Cache m) = M.lookup a m
type Widening Cache a b = W.Widening b
initialize a (Cache m) = Cache (M.insertWith (\_ old -> old) a (Instable,bottom) m)
insert a b st (Cache m) = Cache (M.insert a (st,b) m)
setStable a (Cache m) = Cache (M.adjust (first (\_ -> Stable)) a m)
update widen x y (Cache cache) = case M.lookup x cache of
Just (_,yOld) -> let yNew = widen x yOld y in (yNew,Cache (M.insert x yNew cache))
Just (_,yOld) -> let yNew = widen yOld y in (yNew,Cache (M.insert x yNew cache))
Nothing -> ((Instable,y),Cache (M.insert x (Instable,y) cache))
lookup a (Cache m) = M.lookup a m
data Monotone s a b where
Monotone :: Stable -> s -> Monotone s a s
instance IsEmpty s => IsEmpty (Monotone s a s) where
empty = Monotone Instable empty
instance IsEmpty s => IsCache (Monotone s) a s where
type Widening (Monotone s) a s = (W.Widening s)
initialize _ m = m
insert _ s _ _ = (Monotone Instable s)
setStable _ m = m
update widen _ sNew (Monotone _ sOld) =
let (st,s') = widen sOld sNew
in ((st,s'), Monotone st s')
lookup _ (Monotone _ s) = Just (Instable,s)
data (**) c1 c2 a b where
Product :: c1 a1 b1 -> c2 a2 b2 -> (**) c1 c2 (a1,a2) (b1,b2)
instance (IsEmpty (c1 a1 b1), IsEmpty (c2 a2 b2)) => IsEmpty ((**) c1 c2 (a1,a2) (b1,b2)) where
empty = Product empty empty
instance (IsCache c1 a1 b1, IsCache c2 a2 b2) => IsCache ((**) c1 c2) (a1,a2) (b1,b2) where
type Widening ((**) c1 c2) (a1,a2) (b1,b2) = (Widening c1 a1 b1,Widening c2 a2 b2)
initialize (a1,a2) (Product c1 c2) =
let c1' = initialize a1 c1
c2' = initialize a2 c2
in Product c1' c2'
insert (a1,a2) (b1,b2) s (Product c1 c2) = Product (insert a1 b1 s c1) (insert a2 b2 s c2)
setStable (a1,a2) (Product c1 c2) = Product (setStable a1 c1) (setStable a2 c2)
update (w1,w2) (a1,a2) (b1,b2) (Product c1 c2) =
let ((s1,b1'),c1') = update w1 a1 b1 c1
((s2,b2'),c2') = update w2 a2 b2 c2
in ((s1 s2,(b1',b2')),Product c1' c2')
lookup (a1,a2) (Product c1 c2) = (\(s1,b1) (s2,b2) -> (s1 s2,(b1,b2))) <$> lookup a1 c1 <*> lookup a2 c2
data (&&) c1 c2 a b where
And :: c1 a b1 -> c2 a b2 -> (&&) c1 c2 a (b1,b2)
instance (IsEmpty (c1 a b1), IsEmpty (c2 a b2)) => IsEmpty ((&&) c1 c2 a (b1,b2)) where
empty = And empty empty
-- data Monotone a b where
-- Monotone :: s -> Monotone s ()
-- instance IsEmpty s => IsEmpty (Monotone s ()) where
-- empty = Monotone empty
-- instance (IsEmpty s) => IsCache Monotone s () where
-- type Widening Monotone s () = W.Widening s
-- initialize widen s2 (Monotone s1) = let (_,s3) = widen s1 s2 in (s3,Monotone s3)
-- lookup widen s2 (Monotone s1) = let (stable,_) = widen s1 s2 in Just (stable,())
-- update widen s2 () (Monotone s1) = let (stable,s3) = widen s1 s2
-- in ((stable,()),Monotone s3)
-- data Product c1 c2 a b where
-- Product :: c1 a1 b1 -> c2 a2 b2 -> Product c1 c2 (a1,a2) (b1,b2)
-- instance (IsEmpty (c1 a1 b1), IsEmpty (c2 a2 b2)) => IsEmpty (Product c1 c2 (a1,a2) (b1,b2)) where
-- empty = Product empty empty
-- instance (IsCache c1 a1 b1, IsCache c2 a2 b2) => IsCache (Product c1 c2) (a1,a2) (b1,b2) where
-- type Widening (Product c1 c2) (a1,a2) (b1,b2) = (Widening c1 a1 b1,Widening c2 a2 b2)
-- initialize (w1,w2) (a1,a2) (Product c1 c2) =
-- let (a1',c1') = initialize w1 a1 c1
-- (a2',c2') = initialize w2 a2 c2
-- in ((a1',a2'),Product c1' c2')
-- lookup (w1,w2) (a1,a2) (Product c1 c2) = (\(s1,b1) (s2,b2) -> (s1 ⊔ s2,(b1,b2))) <$> lookup w1 a1 c1 <*> lookup w2 a2 c2
-- update (w1,w2) (a1,a2) (b1,b2) (Product c1 c2) =
-- let ((s1,b1'),c1') = update w1 a1 b1 c1
-- ((s2,b2'),c2') = update w2 a2 b2 c2
-- in ((s1 ⊔ s2,(b1',b2')),Product c1' c2')
-- data First c1 c2 a b where
-- First :: c1 a1 () -> c2 a2 b2 -> First c1 c2 (a1,a2) b2
-- instance (IsEmpty (c1 a1 ()), IsEmpty (c2 a2 b2)) => IsEmpty (First c1 c2 (a1,a2) b2) where
-- empty = First empty empty
-- instance (IsCache c1 a1 (), IsCache c2 a2 b2) => IsCache (First c1 c2) (a1,a2) b2 where
-- type Widening (First c1 c2) (a1,a2) b2 = (Widening c1 a1 (),Widening c2 a2 b2)
-- lookup (w1,w2) (a1,a2) (First c1 c2) = (\(s1,_) (s2,b2) -> (s1 ⊔ s2,b2)) <$> lookup w1 a1 c1 <*> lookup w2 a2 c2
-- lookupInit (w1,w2) (a1,a2) (First c1 c2) =
-- let ((a1',(s1,_)),c1') = lookupInit w1 a1 c1
-- ((a2',(s2,b2)),c2') = lookupInit w2 a2 c2
-- in (((a1',a2'),(s1 ⊔ s2,b2)),First c1' c2')
-- update (w1,w2) (a1,a2) b2 (First c1 c2) =
-- let ((s1,_),c1') = update w1 a1 () c1