Commit 3d33d95b authored by Sven Keidel's avatar Sven Keidel

widening returns stable indicator

parent 25de95c1
{ pkgs ? import <nixpkgs> {} }:
let
hsEnv = pkgs.haskell.packages.ghc844.ghcWithPackages(p: with p; [
hsEnv = pkgs.haskellPackages.ghcWithPackages (p: with p; [
stack
]);
......@@ -10,6 +10,6 @@ in pkgs.stdenv.mkDerivation {
version = "0.0.1";
src = ./.;
buildInputs = [
hsEnv pkgs.pandoc
hsEnv pkgs.jdk
];
}
......@@ -4,7 +4,6 @@ module Control.Arrow.Abstract.Join where
import Prelude hiding ((.))
import Control.Arrow
import Control.Arrow.Utils
import Data.Order(Complete(..))
import Data.Profunctor
......@@ -17,8 +16,8 @@ class (Arrow c, Profunctor c) => ArrowJoin c where
-- @
joinWith :: (y -> y -> y) -> c x y -> c x y -> c x y
joinWith' :: ArrowJoin c => (y -> y -> y) -> c x y -> c x' y -> c (x,x') y
joinWith' lub f g = joinWith lub (f <<< pi1) (g <<< pi2)
joinWith' :: (ArrowJoin c) => (y -> y -> y) -> c x y -> c x' y -> c (x,x') y
joinWith' lub f g = joinWith lub (lmap fst f) (lmap snd g)
(<>) :: (ArrowJoin c, Complete y) => c x y -> c x y -> c x y
(<>) = joinWith ()
......@@ -30,8 +29,8 @@ joinWith' lub f g = joinWith lub (f <<< pi1) (g <<< pi2)
-- @
joinList :: (ArrowChoice c, ArrowJoin c, Complete y) => c (e,s) y -> c (e,(x,s)) y -> c (e,([x],s)) y
joinList empty f = proc (e,(l,s)) -> case l of
[] -> empty -< (e,s)
[x] -> f -< (e,(x,s))
[] -> empty -< (e,s)
[x] -> f -< (e,(x,s))
(x:xs) -> (f -< (e,(x,s))) <> (joinList empty f -< (e,(xs,s)))
instance ArrowJoin (->) where
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE GADTs #-}
module Control.Arrow.Transformer.Abstract.Error(ErrorT(..)) where
import Prelude hiding (id,lookup,(.),read,fail)
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Deduplicate
import Control.Arrow.Environment as Env
import Control.Arrow.Fail
import Control.Arrow.Trans
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Store as Store
import Control.Arrow.Except as Exc
import Control.Arrow.Fix
import Control.Arrow.Utils (duplicate)
import Control.Arrow.Abstract.Join
import Control.Category
import Data.Monoidal
import Data.Order
import Data.Profunctor
import Data.Abstract.Error
import Data.Abstract.Widening (toJoin2)
newtype ErrorT e c x y = ErrorT { runErrorT :: c x (Error e y)}
instance (ArrowChoice c, Profunctor c) => ArrowFail e (ErrorT e c) where
fail = lift $ arr Fail
instance (ArrowChoice c, Profunctor c) => Category (ErrorT e c) where
id = lift' id
f . g = lift $ rmap toEither (unlift g) >>> (arr Fail ||| unlift f)
instance (Profunctor c, Arrow c) => Profunctor (ErrorT e c) where
dimap f g h = lift $ dimap f (fmap g) (unlift h)
lmap f h = lift $ lmap f (unlift h)
rmap g h = lift $ rmap (fmap g) (unlift h)
instance ArrowLift (ErrorT e) where
lift' f = ErrorT (rmap Success f)
instance ArrowTrans (ErrorT e) where
type Dom (ErrorT e) x y = x
type Cod (ErrorT e) x y = Error e y
lift = ErrorT
unlift = runErrorT
instance (ArrowChoice c, Profunctor c) => Arrow (ErrorT e c) where
arr f = lift' (arr f)
first f = lift $ rmap strength1 (first (unlift f))
second f = lift $ rmap strength2 (second (unlift f))
f &&& g = lmap duplicate (f *** g)
f *** g = first f >>> second g
instance (ArrowChoice c, Profunctor c) => ArrowChoice (ErrorT e c) where
left f = lift $ rmap strength1 (left (unlift f))
right f = lift $ rmap strength2 (right (unlift f))
f ||| g = lift $ unlift f ||| unlift g
f +++ g = left f >>> right g
instance (ArrowApply c, ArrowChoice c, Profunctor c) => ArrowApply (ErrorT e c) where
app = lift $ lmap (first unlift) app
instance (ArrowState s c, ArrowChoice c, Profunctor c) => ArrowState s (ErrorT e c) where
get = lift' get
put = lift' put
instance (ArrowStore var val c, ArrowChoice c, Profunctor c) => ArrowStore var val (ErrorT e c) where
type Join (ErrorT e c) x y = Store.Join c (Dom (ErrorT e) x y) (Cod (ErrorT e) x y)
read f g = lift $ read (unlift f) (unlift g)
write = lift' write
instance (ArrowReader r c, ArrowChoice c, Profunctor c) => ArrowReader r (ErrorT e c) where
ask = lift' ask
local f = lift (local (unlift f))
instance (ArrowEnv x y env c, ArrowChoice c, Profunctor c) => ArrowEnv x y env (ErrorT e c) where
type Join (ErrorT e c) x y = Env.Join c (Dom (ErrorT e) x y) (Cod (ErrorT e) x y)
lookup f g = lift $ lookup (unlift f) (unlift g)
getEnv = lift' getEnv
extendEnv = lift' extendEnv
localEnv f = lift (localEnv (unlift f))
instance (ArrowChoice c, ArrowExcept e c) => ArrowExcept e (ErrorT e' c) where
type Join (ErrorT e' c) x y = Exc.Join c (Dom (ErrorT e') x y) (Cod (ErrorT e') x y)
throw = lift $ throw
catch f g = lift $ catch (unlift f) (unlift g)
finally f g = lift $ finally (unlift f) (unlift g)
type instance Fix x y (ErrorT e c) = ErrorT e (Fix (Dom (ErrorT e) x y) (Cod (ErrorT e) x y) c)
instance (ArrowFix (Dom (ErrorT e) x y) (Cod (ErrorT e) x y) c, ArrowChoice c, Profunctor c) => ArrowFix x y (ErrorT e c) where
fix = liftFix
instance (ArrowDeduplicate (Dom (ErrorT e) x y) (Cod (ErrorT e) x y) c, ArrowChoice c, Profunctor c) => ArrowDeduplicate x y (ErrorT e c) where
dedup f = lift $ dedup (unlift f)
instance (ArrowConst r c, ArrowChoice c) => ArrowConst r (ErrorT e c) where
askConst = lift' askConst
instance (Complete e, ArrowJoin c, ArrowChoice c) => ArrowJoin (ErrorT e c) where
joinWith lub' f g = ErrorT $ joinWith (toJoin2 widening () lub') (unlift f) (unlift g)
deriving instance PreOrd (c x (Error e y)) => PreOrd (ErrorT e c x y)
deriving instance LowerBounded (c x (Error e y)) => LowerBounded (ErrorT e c x y)
deriving instance Complete (c x (Error e y)) => Complete (ErrorT e c x y)
deriving instance CoComplete (c x (Error e y)) => CoComplete (ErrorT e c x y)
deriving instance UpperBounded (c x (Error e y)) => UpperBounded (ErrorT e c x y)
......@@ -25,15 +25,16 @@ import Control.Arrow.Utils (duplicate)
import Control.Arrow.Abstract.Join
import Control.Category
import Data.Abstract.Error
import Data.Monoidal
import Data.Order
import Data.Profunctor
import Data.Abstract.Except
import Data.Abstract.Widening (toJoin2)
newtype ExceptT e c x y = ExceptT { runExceptT :: c x (Error e y)}
newtype ExceptT e c x y = ExceptT { runExceptT :: c x (Except e y)}
instance (ArrowChoice c, Complete e, ArrowJoin c) => ArrowExcept e (ExceptT e c) where
type Join (ExceptT e c) (x,(x,e)) y = Complete (c (y,(x,e)) (Error e y))
type Join (ExceptT e c) (x,(x,e)) y = Complete (c (y,(x,e)) (Except e y))
throw = lift $ arr Fail
catch f g = lift $ proc x -> do
e <- unlift f -< x
......@@ -56,11 +57,12 @@ instance (ArrowChoice c, ArrowJoin c, Complete e) => Category (ExceptT e c) wher
SuccessOrFail e y' -> do
-- Ideally we would like to write '(returnA -< Fail e) ⊔ (f -< y)',
-- however this is not possible, because the result type of
-- 'f', 'Error e z', is not 'Complete' because 'z' is not
-- 'f', 'Except e z', is not 'Complete' because 'z' is not
-- 'Complete'. However, in '(returnA -< Fail e) ⊔ (f -< y)' we
-- actually never join to values of type 'z'.
joinWith' (\(Fail e) er -> case er of
Success z -> SuccessOrFail e z
Fail e' -> Fail (e e')
SuccessOrFail e' z -> SuccessOrFail (e e') z)
id (unlift f) -< (Fail e,y')
......@@ -75,7 +77,7 @@ instance ArrowLift (ExceptT e) where
instance ArrowTrans (ExceptT e) where
type Dom (ExceptT e) x y = x
type Cod (ExceptT e) x y = Error e y
type Cod (ExceptT e) x y = Except e y
lift = ExceptT
unlift = runExceptT
......@@ -129,10 +131,10 @@ instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowConst r c) => ArrowConst
askConst = lift' askConst
instance (Complete e, ArrowJoin c, ArrowChoice c) => ArrowJoin (ExceptT e c) where
joinWith lub' f g = ExceptT $ joinWith (widening () lub') (unlift f) (unlift g)
joinWith lub' f g = ExceptT $ joinWith (toJoin2 widening () lub') (unlift f) (unlift g)
deriving instance PreOrd (c x (Error e y)) => PreOrd (ExceptT e c x y)
deriving instance LowerBounded (c x (Error e y)) => LowerBounded (ExceptT e c x y)
deriving instance Complete (c x (Error e y)) => Complete (ExceptT e c x y)
deriving instance CoComplete (c x (Error e y)) => CoComplete (ExceptT e c x y)
deriving instance UpperBounded (c x (Error e y)) => UpperBounded (ExceptT e c x y)
deriving instance PreOrd (c x (Except e y)) => PreOrd (ExceptT e c x y)
deriving instance LowerBounded (c x (Except e y)) => LowerBounded (ExceptT e c x y)
deriving instance Complete (c x (Except e y)) => Complete (ExceptT e c x y)
deriving instance CoComplete (c x (Except e y)) => CoComplete (ExceptT e c x y)
deriving instance UpperBounded (c x (Except e y)) => UpperBounded (ExceptT e c x y)
......@@ -10,7 +10,6 @@ module Control.Arrow.Transformer.Abstract.Failure(FailureT(..)) where
import Prelude hiding (id,(.),lookup,read)
import Control.Applicative
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Deduplicate
......@@ -26,11 +25,12 @@ import Control.Arrow.Utils(duplicate)
import Control.Arrow.Abstract.Join
import Control.Category
import Data.Abstract.Failure
import Data.Order
import Data.Monoidal
import Data.Identifiable
import Data.Profunctor
import Data.Abstract.Failure
import Data.Abstract.Widening (toJoin)
-- | Describes computations that can fail.
newtype FailureT e c x y = FailureT { runFailureT :: c x (Failure e y) }
......@@ -110,7 +110,7 @@ instance (ArrowChoice c, ArrowConst r c) => ArrowConst r (FailureT e c) where
askConst = lift' askConst
instance (ArrowJoin c, ArrowChoice c) => ArrowJoin (FailureT e c) where
joinWith lub' (FailureT f) (FailureT g) = FailureT $ joinWith (widening lub') f g
joinWith lub' (FailureT f) (FailureT g) = FailureT $ joinWith (toJoin widening lub') f g
deriving instance PreOrd (c x (Failure e y)) => PreOrd (FailureT e c x y)
deriving instance LowerBounded (c x (Failure e y)) => LowerBounded (FailureT e c x y)
......
......@@ -9,22 +9,24 @@
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Abstract.Fix(FixT,runFixT) where
import Prelude hiding (id,(.),const,head,iterate)
import Control.Category
import Control.Arrow hiding (loop)
import Control.Arrow.Const
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Trans
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Const
import Control.Arrow.Transformer.Static
import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.State
import Control.Category
import qualified Control.Monad.State as S
import Control.Arrow.Utils (const,(&&>))
import Data.Identifiable
import Data.Order
import Data.Abstract.Widening (Widening)
import Data.Abstract.Widening (Widening,Stable(..))
import Data.Abstract.StackWidening (StackWidening,Loop(..))
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
......@@ -48,73 +50,46 @@ runFixT sw w f = dimap (\x -> ((M.empty,H.empty),(mempty,x))) snd $ runStateT $
#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
fix f = FixT $ stackWiden'
(let iterate = proc (x,x') -> do
-- If we are not in a loop, continue recursing.
(y,(member,head)) <- unFixT (f (fix f)) &&& inComponent -< x'
if member
then do
(stable,yNew) <- updateCache -< (x',y)
-- If we did not reach a fixpoint of f(x'), keep iterating.
if head && not stable
then iterate -< (x,x')
else returnA -< yNew
else returnA -< y
in iterate)
-- 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)
(addToComponent &&> initializeCache)
#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
fix f = FixT $ stackWiden'
(let iterate = proc (x,x') -> do
-- If we are not in a loop, continue recursing.
(y,(member,head)) <- unFixT (f (fix f)) &&& inComponent -< trace (printf "call [%s -> %s]" (show x) (show x')) x'
if member
then do
(stable,yNew) <- updateCache -< (x',y)
-- If we did not reach a fixpoint of f(x'), keep iterating.
if head && not stable
then iterate -< trace (printf "iterate [%s -> %s] = %s" (show x) (show x') (show yNew)) (x,x')
else returnA -< if head then trace (printf "fixed [%s -> %s] = %s" (show x) (show x') (show yNew)) yNew else yNew
else returnA -< trace (printf "return [%s -> %s] = %s" (show x) (show x') (show y)) y
in iterate)
-- 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)
(addToComponent &&> initializeCache)
#endif
instance (ArrowJoin c, ArrowChoice c) => ArrowJoin (FixT s a b c) where
......@@ -131,31 +106,43 @@ instance (ArrowJoin (FixT s a b c), Profunctor c, Complete y, PreOrd (c x y)) =>
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 (Arrow c, Profunctor c, LowerBounded (c x y)) => LowerBounded (FixT s a b c x y) where
bottom = lift' bottom
instance ArrowLift (FixT s a b) where
lift' = FixT . lift' . lift' . lift'
instance (ArrowApply c, Profunctor c) => ArrowApply (FixT s a b c) where
app = FixT (lmap (first unFixT) app)
----- Helper functions -----
stackWiden' :: (ArrowReader (s a) c,ArrowChoice c) => ConstT (StackWidening s a,r) c (a,a) b -> ConstT (StackWidening s a,r) c a b -> ConstT (StackWidening s a,r) c a b
stackWiden' (ConstT (StaticT f)) (ConstT (StaticT g)) = constT $ \(sw,w) -> (local (f (sw,w)) ||| g (sw,w))
<<< rmap (\(s,x) -> let ~(s',(l,x')) = sw s x
in case l of
NoLoop -> Left (s',(x,x'))
Loop -> Right x'
) (const ask &&& id)
getStackWidening :: (ArrowConst (StackWidening s a,r) c, ArrowReader (s a) c) => c () (StackWidening s a,s a)
getStackWidening = rmap (first fst) (askConst &&& ask)
initializeCache :: (Identifiable a, LowerBounded b, ArrowState (Cache a b,Component a) c) => c a b
initializeCache = modifyCache (\x -> insertWithLookup (\_ old -> old) x bottom)
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)
updateCache :: (Identifiable a, LowerBounded b, ArrowState (Cache a b,Component a) c) => ConstT (r,Widening b) c (a,b) (Bool,b)
updateCache = constT $ \(_,widen) -> modifyCache $ \(x,y) cache -> case M.lookup x cache of
Just yOld -> let (s,yNew) = widen yOld y in ((s == Stable,yNew),M.insert x yNew cache)
Nothing -> ((False,y),M.insert x y cache)
getComponent :: ArrowState (Cache a b,Component a) c => c () (Component a)
getComponent = rmap snd get
inComponent :: (Identifiable a, Arrow c, Profunctor c, ArrowState (Cache a b,Component a) c) => c a (Bool,Bool)
inComponent = modifyComp $ \x comp -> ((not (H.null comp) && H.member x comp, H.singleton x == comp), H.delete x comp)
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
addToComponent = modifyComp (\x comp -> ((),H.insert 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))))
modifyCache :: ArrowState (Cache a b,Component a) c => (x -> Cache a b -> (y,Cache a b)) -> c x y
modifyCache f = modify (arr $ \(x,(cache,comp)) -> let (y,cache') = f x cache in (y,(cache',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)))
modifyComp :: ArrowState (Cache a b,Component a) c => (x -> Component a -> (y,Component a)) -> c x y
modifyComp f = modify (arr $ \(x,(cache,comp)) -> let (y,comp') = f x comp in (y,(cache,comp')))
insertWithLookup :: Identifiable a => (b -> b -> b) -> a -> b -> HashMap a b -> (b,HashMap a b)
insertWithLookup w a b m =
......
......@@ -19,10 +19,11 @@ import Control.Arrow.Utils(duplicate)
import Control.Arrow.Abstract.Join
import Control.Category
import Data.Abstract.Terminating
import Data.Order
import Data.Monoidal
import Data.Profunctor
import Data.Abstract.Terminating
import Data.Abstract.Widening (toJoin)
-- | Arrow that propagates non-terminating computations.
newtype TerminatingT c x y = TerminatingT { runTerminatingT :: c x (Terminating y) }
......@@ -77,7 +78,7 @@ instance (ArrowChoice c, ArrowFix (Dom TerminatingT x y) (Cod TerminatingT x y)
fix = liftFix
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (TerminatingT c) where
joinWith lub' f g = lift $ joinWith (widening lub') (unlift f) (unlift g)
joinWith lub' f g = lift $ joinWith (toJoin 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)
......
......@@ -24,12 +24,12 @@ import Control.Arrow.Utils
import Control.Category
import Data.Profunctor
import Data.Concrete.Failure
import Data.Concrete.Error
import Data.Monoidal
import Data.Identifiable
-- | Arrow transformer that adds failure to the result of a computation
newtype FailureT e c x y = FailureT { runFailureT :: c x (Failure e y) }
newtype FailureT e c x y = FailureT { runFailureT :: c x (Error e y) }
instance (ArrowChoice c, Profunctor c) => ArrowFail e (FailureT e c) where
fail = lift $ arr Fail
......@@ -41,7 +41,7 @@ instance (Profunctor c, Arrow c) => Profunctor (FailureT e c) where
instance ArrowTrans (FailureT e) where
type Dom (FailureT e) x y = x
type Cod (FailureT e) x y = Failure e y
type Cod (FailureT e) x y = Error e y
lift = FailureT
unlift = runFailureT
......
......@@ -4,6 +4,7 @@ module Control.Arrow.Utils where
import Prelude hiding (map,zipWith)
import Control.Arrow
import Data.Profunctor
-- | Applies a computation to all elements of the input list and
-- collects the results in an list.
......@@ -16,14 +17,12 @@ map f = proc l -> case l of
returnA -< (b:bs)
-- | Throws away the result of a computation.
void :: Arrow c => c x y -> c x ()
void f = proc x -> do
_ <- f -< x
returnA -< ()
void :: Profunctor c => c x y -> c x ()
void f = rmap (\_ -> ()) f
infixr 1 &&>
(&&>) :: Arrow c => c a () -> c a b -> c a b
f &&> g = f &&& g >>> arr snd
(&&>) :: (Arrow c, Profunctor c) => c a () -> c a b -> c a b
f &&> g = rmap snd (f &&& g)
-- | Projects the first component of a product.
pi1 :: Arrow c => c (x,y) x
......@@ -34,11 +33,11 @@ pi2 :: Arrow c => c (x,y) y
pi2 = arr snd
-- | Zips two lists together.
zipWith :: ArrowChoice c => c (x,y) z -> c ([x],[y]) [z]
zipWith :: (ArrowChoice c,Profunctor c) => c (x,y) z -> c ([x],[y]) [z]
zipWith f = proc (l1,l2) -> case (l1,l2) of
([],_) -> returnA -< []
(_,[]) -> returnA -< []
(a:as,b:bs) -> uncurry (:) ^<< f *** zipWith f -< ((a,b),(as,bs))
(a:as,b:bs) -> rmap (uncurry (:)) (f *** zipWith f) -< ((a,b),(as,bs))
-- | Folds a computation over a list from left to right.
fold :: ArrowChoice c => c (a,x) a -> c ([x],a) a
......@@ -53,5 +52,5 @@ duplicate :: Arrow c => c x (x,x)
duplicate = arr (\x -> (x,x))
-- | creates a computation that always returns the same value.
const :: Arrow c => c () x -> c y x
const f = arr (\_ -> ()) >>> f
const :: Profunctor c => c () x -> c y x
const f = lmap (\_ -> ()) f
......@@ -57,4 +57,7 @@ instance UpperBounded Bool where
instance Hashable Bool
widening :: Widening Bool
widening = finite
widening True True = (Stable,True)
widening False False = (Stable,False)
widening Top Top = (Stable,Top)
widening _ _ = (Instable,Top)
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
module Data.Abstract.DiscretePowerset where
import Data.Order
......@@ -8,6 +9,9 @@ import qualified Data.HashSet as H
import Data.Hashable
import Data.Identifiable
import Data.List (intercalate)
import Data.Abstract.Widening
import Data.Abstract.FreeCompletion (FreeCompletion)
import qualified Data.Abstract.FreeCompletion as F
import GHC.Generics
import GHC.Exts
......@@ -57,6 +61,17 @@ instance Identifiable x => PreOrd (Pow x) where
instance Identifiable x => Complete (Pow x) where
() = union
widening :: Identifiable x => Widening (Pow x)
widening (Pow xs) (Pow ys) = let zs = H.union xs ys in (if H.size zs == H.size xs then Stable else Instable,Pow zs)
widening Top (Pow _) = (Instable,Top)
widening (Pow _) Top = (Instable,Top)
widening Top Top = (Stable,Top)
instance Identifiable x => Complete (FreeCompletion (Pow x)) where
F.Top _ = F.Top
_ F.Top = F.Top
F.Lower xs F.Lower ys = F.Lower (xs ys)
instance Hashable x => Hashable (Pow x)
instance Identifiable x => UpperBounded (Pow x) where
......@@ -70,3 +85,6 @@ instance Identifiable x => IsList (Pow x) where
fromList ls = Pow (H.fromList ls)
toList (Pow xs) = H.toList xs
toList Top = error "toList ⊤"
instance (IsString x, Identifiable x) => IsString (Pow x) where
fromString s = Pow (H.singleton (fromString s))
......@@ -46,15 +46,17 @@ instance (Complete a, Complete b) => Complete (Either a b) where