Commit 2a2f6246 authored by Sven Keidel's avatar Sven Keidel

fix while tests

parent 0676b3ec
Pipeline #15792 passed with stages
in 23 minutes and 24 seconds
......@@ -8,15 +8,15 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Control.Arrow.Fix(Fix,Fix',ArrowFix(..),IterationStrategy,filter) where
module Control.Arrow.Fix(Fix,Fix',ArrowFix(..),IterationStrategy,transform,filter) where
import Prelude hiding (filter,pred)
import Prelude hiding (filter,pred)
import Control.Arrow
import Control.Arrow.Trans
import Control.Arrow
import Control.Arrow.Trans
import Data.Profunctor
import Data.Lens(Prism',getMaybe,set)
import Data.Profunctor
import Data.Lens(Iso',from,Prism',getMaybe,get,set)
-- | Type family that computes the type of the fixpoint.
type family Fix (c :: * -> * -> *) x y :: * -> * -> *
......@@ -37,7 +37,13 @@ instance ArrowFix (x -> y) where
type IterationStrategy c a b = c a b -> c a b
transform :: Profunctor c => Iso' a a' -> IterationStrategy c a' b -> IterationStrategy c a b
transform iso strat f = lmap (get iso) (strat (lmap (get (from iso)) f))
{-# INLINE transform #-}
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
Just a' -> strat (lmap (\x -> set pred x a) f) -<< a'
Nothing -> f -< a
{-# INLINE filter #-}
......@@ -3,7 +3,7 @@ module Control.Arrow.Fix.Cache where
import Control.Arrow
import Data.Profunctor
import Data.Abstract.Widening
import Data.Abstract.Stable
class (Arrow c, Profunctor c) => ArrowCache a b c | c -> a, c -> b where
-- | Looks up if there is an entry in the cache.
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
module Control.Arrow.Fix.Reuse where
import Control.Arrow
import Control.Arrow.Fix
import Data.Measure
import Data.Abstract.Stable
import Data.Metric
import Data.Profunctor
import Data.Monoid
import Text.Printf
class (Arrow c, Profunctor c) => ArrowReuse a b c where
type Dom c :: *
class ArrowReuse a b c where
-- | Reuse cached results at the cost of precision.
reuseStable :: (Show m, Monoid m) => (a -> a -> b -> m) -> c a m
reuse :: (Monoid m) => (Dom c -> Dom c -> Stable -> b -> m) -> c (a,Stable) m
reuseFirst :: (ArrowChoice c, ArrowReuse a b c) => IterationStrategy c a b
reuseFirst f = proc a -> do
m <- reuse (\_ _ _ b -> First (Just b)) -< (a,Stable)
case getFirst m of
Just b -> returnA -< b
Nothing -> f -< a
{-# INLINE reuseFirst #-}
reuseStableByMetric :: (Show b, Show n, Ord n, ArrowChoice c, ArrowReuse a b c) => Metric a n -> IterationStrategy c a b
reuseStableByMetric metric f = proc a -> do
m <- reuseStable (\a a' b -> Just (Measured { measured = metric a a', argument = b })) -< a
reuseExact :: (Eq (Dom c), ArrowChoice c, ArrowReuse a b c) => IterationStrategy c a b
reuseExact = reuseByMetric discrete
{-# INLINE reuseExact #-}
reuseByMetric :: (Ord n, ArrowChoice c, ArrowReuse a b c) => Metric (Dom c) n -> IterationStrategy c a b
reuseByMetric metric f = proc a -> do
m <- reuse (\a a' _ b -> Just (Measured { measured = metric a a', argument = b })) -< (a,Stable)
case m of
Just n -> returnA -< argument n
Nothing -> f -< a
{-# INLINE reuseStableByMetric #-}
{-# INLINE reuseByMetric #-}
data Measured a n = Measured { argument :: a, measured :: n }
instance (Show a, Show n) => Show (Measured a n) where
show m = printf "%s@%s" (show (argument m)) (show (measured m))
instance Ord n => Semigroup (Measured a n) where
m1 <> m2
| measured m1 <= measured m2 = m1
| otherwise = m2
{-# INLINE (<>) #-}
......@@ -5,7 +5,8 @@ module Control.Arrow.Fix.Widening where
import Control.Arrow
import Data.Profunctor
import Data.Order
import Data.Abstract.Widening (Stable,finite)
import Data.Abstract.Stable
import Data.Abstract.Widening (finite)
class (Arrow c, Profunctor c) => ArrowWidening a c where
widening :: c (a,a) (Stable,a)
......
......@@ -2,8 +2,6 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Abstract.Fix.Cache.Basic where
......@@ -25,7 +23,7 @@ import Data.Empty
import Data.HashMap.Lazy(HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Abstract.Widening(Stable(..))
import Data.Abstract.Stable
newtype Cache a b = Cache { getMap :: HashMap a (Stable,b)}
instance (Show a, Show b) => Show (Cache a b) where
......@@ -47,8 +45,8 @@ instance (Identifiable a, ArrowChoice c, Profunctor c) => ArrowCache a b (CacheT
put -< Cache (M.insert a b'' cache)
returnA -< b''
Nothing -> do
put -< Cache (M.insert a (Instable,b) cache)
returnA -< (Instable,b)
put -< Cache (M.insert a (Unstable,b) cache)
returnA -< (Unstable,b)
write = CacheT $ modify' (\((a,b,s),Cache cache) -> ((),Cache (M.insert a (s,b) cache)))
setStable = CacheT $ modify' $ \((s,a),Cache cache) -> ((),Cache (M.adjust (first (const s)) a cache))
{-# INLINE lookup #-}
......@@ -57,7 +55,8 @@ instance (Identifiable a, ArrowChoice c, Profunctor c) => ArrowCache a b (CacheT
{-# INLINE setStable #-}
instance (PreOrd a, Arrow c, Profunctor c) => ArrowReuse a b (CacheT Cache a b c) where
reuseStable f = CacheT $ proc a -> do
type Dom (CacheT Cache a b c) = a
reuse f = CacheT $ proc (a,s) -> do
Cache cache <- get -< ()
returnA -< M.foldlWithKey' (\m a' (s,b) -> if s == Stable && a a' then m <> f a a' b else m) mempty cache
{-# INLINE reuseStable #-}
returnA -< M.foldlWithKey' (\m a' (s',b') -> if s' s && a a' then m <> f a a' s' b' else m) mempty cache
{-# INLINE reuse #-}
......@@ -7,7 +7,7 @@
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Abstract.Fix.Cache.ContextSensitive
( module Control.Arrow.Transformer.Abstract.Fix.Cache
, Cache
, Cache(..)
) where
import Prelude hiding (pred,lookup,map,head,iterate,(.),truncate,elem)
......@@ -27,7 +27,7 @@ import Data.Empty
import Data.Order
import Data.Abstract.Widening as W
import Data.Abstract.Widening (Stable(..))
import Data.Abstract.Stable
import Data.HashMap.Lazy(HashMap)
import qualified Data.HashMap.Lazy as M
......@@ -48,13 +48,13 @@ instance (Identifiable ctx, PreOrd a, LowerBounded b, ArrowChoice c, ArrowContex
Just (a',b,s)
| a a' -> case s of
Stable -> Right b
Instable -> Left (Cache cache,a')
Unstable -> Left (Cache cache,a')
| otherwise ->
-- If there exists the actual input is not smaller than the cached
-- input, widen the input and recompute.
let (_,a'') = widen a' a
in Left (Cache (M.insert ctx (a'',b,Instable) cache), a'')
Nothing -> Left (Cache (M.insert ctx (a,bottom,Instable) cache), a)
in Left (Cache (M.insert ctx (a'',b,Unstable) cache), a'')
Nothing -> Left (Cache (M.insert ctx (a,bottom,Unstable) cache), a)
{-# INLINE joinContexts' #-}
instance (Identifiable ctx, PreOrd a, Eq a, Complete b, ArrowChoice c, Profunctor c, ArrowContext ctx c)
......@@ -65,7 +65,7 @@ instance (Identifiable ctx, PreOrd a, Eq a, Complete b, ArrowChoice c, Profuncto
case M.lookup ctx cache of
Just (a',b,s)
| a a' -> returnA -< Just (s,b)
| otherwise -> returnA -< Just (Instable,b)
| otherwise -> returnA -< Just (Unstable,b)
Nothing -> returnA -< Nothing
update = CacheT $ askConst $ \widening -> proc (a,b) -> do
ctx <- askContext -< ()
......@@ -73,11 +73,11 @@ instance (Identifiable ctx, PreOrd a, Eq a, Complete b, ArrowChoice c, Profuncto
case M.lookup ctx cache of
Just (a',b',_) -> do
let (s,b'') = widening b' b
put -< Cache (M.insert ctx (a',b'',if a == a' then s else Instable) cache)
put -< Cache (M.insert ctx (a',b'',if a == a' then s else Unstable) cache)
returnA -< (s,b'')
Nothing -> do
put -< Cache (M.insert ctx (a,b,Instable) cache)
returnA -< (Instable,b)
put -< Cache (M.insert ctx (a,b,Unstable) cache)
returnA -< (Unstable,b)
write = CacheT $ proc (a,b,s) -> do
ctx <- askContext -< ()
Cache cache <- get -< ()
......@@ -97,7 +97,8 @@ instance (Identifiable ctx, PreOrd a, Eq a, Complete b, ArrowChoice c, Profuncto
{-# INLINE setStable #-}
instance (PreOrd a, Arrow c, Profunctor c) => ArrowReuse a b (CacheT (Cache ctx) a b c) where
reuseStable f = CacheT $ proc a -> do
type Dom (CacheT (Cache ctx) a b c) = a
reuse f = CacheT $ proc (a,s) -> do
Cache cache <- get -< ()
returnA -< M.foldl' (\m (a',b,s) -> if s == Stable && a a' then m <> f a a' b else m) mempty cache
{-# INLINE reuseStable #-}
returnA -< M.foldl' (\m (a',b',s') -> if s' s && a a' then m <> f a a' s' b' else m) mempty cache
{-# INLINE reuse #-}
......@@ -13,7 +13,7 @@ module Control.Arrow.Transformer.Abstract.Fix.Cache.Group where
import Prelude hiding (pred,lookup,map,head,iterate,(.))
import Control.Arrow
-- import Control.Arrow.Fix.Reuse
import Control.Arrow.Fix.Reuse
import Control.Arrow.Fix.Context
import Control.Arrow.Fix.Cache as Cache
import Control.Arrow.State
......@@ -60,11 +60,10 @@ instance (Identifiable k, Arrow c, Profunctor c, ArrowCache a b (CacheT cache a
{-# INLINE write #-}
{-# INLINE setStable #-}
-- instance (PreOrd a, Arrow c, Profunctor c) => ArrowReuse a b (CacheT Cache a b c) where
-- reuseStable f = CacheT $ proc a -> do
-- Cache cache <- get -< ()
-- returnA -< M.foldlWithKey' (\m a' (s,b) -> if s == Stable && a ⊑ a' then m <> f a a' b else m) mempty cache
-- {-# INLINE reuseStable #-}
instance (Identifiable k, IsEmpty (cache a b), Arrow c, Profunctor c, ArrowReuse a b (CacheT cache a b c)) => ArrowReuse (k,a) b (CacheT (Group cache) (k,a) b c) where
type Dom (CacheT (Group cache) (k,a) b c) = Dom (CacheT cache a b c)
reuse f = lmap (\((k,a),s) -> (k,(a,s))) (withCache (reuse f))
{-# INLINE reuse #-}
withCache :: (Identifiable k, IsEmpty (cache a b), Arrow c, Profunctor c) => CacheT cache a b c x y -> CacheT (Group cache) (k,a) b c (k,x) y
withCache f = CacheT $ modify $ proc ((k,x),g) -> do
......
......@@ -17,6 +17,7 @@ import Control.Category
import Control.Arrow hiding (loop)
import Control.Arrow.Fix
import Control.Arrow.Fix.Chaotic
import Control.Arrow.Fix.Reuse
import Control.Arrow.Fix.Cache as Cache
import Control.Arrow.Fix.Stack as Stack
import Control.Arrow.Fix.Context as Context
......@@ -27,14 +28,13 @@ import Control.Arrow.Utils
import Control.Arrow.Transformer.Writer
import Data.Abstract.Stable
import Data.Order
import Data.Profunctor
import qualified Data.HashSet as H
import Data.Identifiable
import Data.Coerce
import Data.Maybe(fromMaybe)
import Data.Abstract.Widening(Stable(..))
-- | Iterate on the innermost fixpoint component.
iterateInner :: (Identifiable a, LowerBounded b, ArrowStack a c, ArrowIterate a c, ArrowComponent a c, ArrowCache a b c, ArrowChoice c) => IterationStrategy c a b
......@@ -52,7 +52,7 @@ iterateInner = detectLoop . go
(stable,bNew) <- Cache.update -< (a,b)
case stable of
Stable -> setComponent -< (component { head = H.delete a (head component) },bNew)
Instable -> go f -< a
Unstable -> go f -< a
-- | Iterate on the outermost fixpoint component.
iterateOuter :: (Identifiable a, LowerBounded b, ArrowStack a c, ArrowIterate a c, ArrowComponent a c, ArrowCache a b c, ArrowChoice c) => IterationStrategy c a b
......@@ -80,29 +80,30 @@ iterateOuter = detectLoop . go
setComponent -< (mempty, bNew)
-- If the head of a fixpoint component is not stable, keep iterating.
Instable ->
Unstable ->
go f -< a
-- We are inside an fixpoint component, but its head has not stabilized.
| otherwise -> do
Cache.write -< (a,b,Instable)
Cache.write -< (a,b,Unstable)
setComponent -< (Component { head = H.delete a (head component),
body = H.insert a (body component) }, b)
detectLoop :: (LowerBounded b, ArrowStack a c, ArrowCache a b c, ArrowIterate a c, ArrowChoice c) => IterationStrategy c a b
detectLoop f = proc a -> do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
_ -> do
loop <- Stack.elem -< a
if loop
then iterate -< (a, snd (fromMaybe bottom m))
else Stack.push f -< a
loop <- Stack.elem -< a
if loop
then do
m <- Cache.lookup -< a
case m of
Just (Stable,b) -> returnA -< b
Just (Unstable,b) -> iterate -< (a, b)
Nothing -> iterate -< (a, bottom)
else Stack.push f -< a
{-# INLINE detectLoop #-}
newtype ChaoticT a c x y = ChaoticT (WriterT (Component a) c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowStack a,ArrowCache a b,ArrowState s,ArrowContext ctx)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowStack a,ArrowCache a b,ArrowReuse a b,ArrowState s,ArrowContext ctx)
instance (Identifiable a, Arrow c, Profunctor c) => ArrowIterate a (ChaoticT a c) where
iterate = lift (arr (first singleton))
......
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
......@@ -12,6 +13,7 @@ import Prelude hiding (pred,lookup,map,head,iterate,(.))
import Control.Category
import Control.Arrow hiding (loop)
import Control.Arrow.Fix
import Control.Arrow.Fix.Reuse as Reuse
import Control.Arrow.Fix.Cache as Cache
import Control.Arrow.Fix.Stack(ArrowStack)
import Control.Arrow.Fix.Context(ArrowContext)
......@@ -59,7 +61,7 @@ instance IsEmpty (Stack a) where
{-# INLINE empty #-}
newtype StackT stack a c x y = StackT (ReaderT (stack a) c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowJoin,ArrowComplete z,ArrowCache a b,ArrowState s,ArrowTrans,ArrowContext ctx)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowJoin,ArrowComplete z,ArrowCache a b,ArrowReuse a b,ArrowState s,ArrowTrans,ArrowContext ctx)
instance (Identifiable a, Arrow c, Profunctor c) => ArrowStack a (StackT Stack a c) where
peek = lift $ proc (stack,()) -> returnA -< top stack
......
......@@ -18,6 +18,7 @@ import Control.Arrow.Environment as Env
import Control.Arrow.Except as Exc
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Fix.Reuse as Reuse
import Control.Arrow.Fix.Cache as Cache
import Control.Arrow.Fix.Context as Context
import Control.Arrow.Order
......@@ -158,6 +159,11 @@ instance ArrowConst x c => ArrowConst x (ReaderT r c) where
instance ArrowEffectCommutative c => ArrowEffectCommutative (ReaderT r c)
instance ArrowReuse a b c => ArrowReuse a b (ReaderT r c) where
type Dom (ReaderT r c) = Dom c
reuse f = lift' $ reuse f
{-# INLINE reuse #-}
instance ArrowContext ctx c => ArrowContext ctx (ReaderT r c) where
askContext = lift' Context.askContext
localContext f = lift $ lmap shuffle1 (localContext (unlift f))
......
......@@ -12,6 +12,7 @@ import Prelude hiding (id,(.),lookup,read,fail)
import Control.Category
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Fix.Reuse as Reuse
import Control.Arrow.Fix.Cache as Cache
import Control.Arrow.Fix.Stack as Stack
import Control.Arrow.Fix.Context as Context
......@@ -180,6 +181,11 @@ instance (Monoid w, ArrowStack a c) => ArrowStack a (WriterT w c) where
{-# INLINE elems #-}
{-# INLINE size #-}
instance (Monoid w, ArrowReuse a b c) => ArrowReuse a b (WriterT w c) where
type Dom (WriterT w c) = Dom c
reuse f = lift' (Reuse.reuse f)
{-# INLINE reuse #-}
instance (Monoid w, ArrowContext ctx c) => ArrowContext ctx (WriterT w c) where
askContext = lift' Context.askContext
localContext f = lift (Context.localContext (unlift f))
......
......@@ -6,11 +6,13 @@ module Data.Abstract.Boolean where
import Prelude hiding (Bool(..))
import qualified Prelude as P
import Data.Abstract.Widening
import Data.Boolean
import Data.Hashable
import Data.Order
import Data.Abstract.Stable
import Data.Abstract.Widening
import GHC.Generics
data Bool = True | False | Top deriving (Eq,Generic)
......@@ -37,12 +39,18 @@ instance Logic Bool where
True -> False
False -> True
Top -> Top
{-# INLINE true #-}
{-# INLINE false #-}
{-# INLINE and #-}
{-# INLINE or #-}
{-# INLINE not #-}
instance PreOrd Bool where
_ Top = P.True
True True = P.True
False False = P.True
_ _ = P.False
{-# INLINE (⊑) #-}
instance Complete Bool where
Top _ = Top
......@@ -50,14 +58,21 @@ instance Complete Bool where
True True = True
False False = False
_ _ = Top
{-# INLINE (⊔) #-}
instance UpperBounded Bool where
top = Top
{-# INLINE top #-}
instance Hashable Bool
instance Hashable Bool where
hashWithSalt s True = s `hashWithSalt` (1::Int)
hashWithSalt s False = s `hashWithSalt` (2::Int)
hashWithSalt s Top = s `hashWithSalt` (3::Int)
{-# INLINE hashWithSalt #-}
widening :: Widening Bool
widening True True = (Stable,True)
widening False False = (Stable,False)
widening Top Top = (Stable,Top)
widening _ _ = (Instable,Top)
widening _ _ = (Unstable,Top)
{-# INLINE widening #-}
......@@ -12,14 +12,16 @@ 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 Data.GaloisConnection
import qualified Data.Concrete.Powerset as C
import qualified Data.Empty as E
import qualified Data.Singleton as S
import Data.Abstract.Widening
import Data.Abstract.Stable
import Data.Abstract.FreeCompletion (FreeCompletion)
import qualified Data.Abstract.FreeCompletion as F
import GHC.Generics
import GHC.Exts
......@@ -44,7 +46,7 @@ unions Top = Top
insert :: Identifiable x => x -> Pow x -> Pow x
insert x (Pow xs) = Pow (H.insert x xs)
insert _ Top = Top
delete :: Identifiable x => x -> Pow x -> Pow x
delete x (Pow xs) = Pow (H.delete x xs)
delete _ Top = Top -- Less precise than it could be.
......@@ -81,9 +83,9 @@ instance Identifiable x => S.IsSingleton (Pow x) where
singleton = singleton
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 (Pow xs) (Pow ys) = let zs = H.union xs ys in (if H.size zs == H.size xs then Stable else Unstable,Pow zs)
widening Top (Pow _) = (Unstable,Top)
widening (Pow _) Top = (Unstable,Top)
widening Top Top = (Stable,Top)
instance Identifiable x => Complete (FreeCompletion (Pow x)) where
......@@ -111,4 +113,4 @@ instance (IsString x, Identifiable x) => IsString (Pow x) where
instance Identifiable a => Galois (C.Pow a) (Pow a) where
alpha xs = Pow (C.toHashSet xs)
gamma = fromList . toList
......@@ -8,6 +8,7 @@ import Prelude hiding (Either(..))
import Control.Monad(ap)
import Data.Abstract.Stable
import Data.Abstract.Widening
import Data.Bifunctor
import Data.Hashable
......@@ -22,6 +23,7 @@ instance (Hashable a, Hashable b) => Hashable (Either a b) where
hashWithSalt s (Left a) = s `hashWithSalt` (1::Int) `hashWithSalt` a
hashWithSalt s (Right b) = s `hashWithSalt` (2::Int) `hashWithSalt` b
hashWithSalt s (LeftRight a b) = s `hashWithSalt` (3 ::Int) `hashWithSalt` a `hashWithSalt` b
{-# INLINE hashWithSalt #-}
instance (PreOrd a, PreOrd b) => PreOrd (Either a b) where
m1 m2 = case (m1,m2) of
......@@ -31,6 +33,7 @@ instance (PreOrd a, PreOrd b) => PreOrd (Either a b) where
(Right b, LeftRight _ b') -> b b'
(Left a, LeftRight a' _) -> a a'
(_, _) -> False
{-# INLINE (⊑) #-}
instance (Complete a, Complete b) => Complete (Either a b) where
m1 m2 = case (m1,m2) of
......@@ -43,21 +46,23 @@ instance (Complete a, Complete b) => Complete (Either a b) where
(LeftRight a b, Left a') -> LeftRight (a a') b
(Left a, LeftRight a' b') -> LeftRight (a a') b'
(LeftRight a b, LeftRight a' b') -> LeftRight (a a') (b b')
{-# INLINE (⊔) #-}
widening :: Widening a -> Widening b -> Widening (Either a b)
widening wa wb m1 m2 = case (m1,m2) of
(Right b, Right b') -> second Right (b `wb` b')
(Right b, Left a') -> (Instable,LeftRight a' b)
(Left a, Right b') -> (Instable,LeftRight a b')
(Right b, Left a') -> (Unstable,LeftRight a' b)
(Left a, Right b') -> (Unstable,LeftRight a b')
(Left a, Left a') -> second Left (a `wa` a')
(LeftRight a b, Right b') -> let (_,b'') = b `wb` b' in (Instable,LeftRight a b'')
(Right b, LeftRight a' b') -> let (_,b'') = b `wb` b' in (Instable,LeftRight a' b'')
(LeftRight a b, Left a') -> let (_,a'') = a `wa` a' in (Instable,LeftRight a'' b)
(Left a, LeftRight a' b') -> let (_,a'') = a `wa` a' in (Instable,LeftRight a'' b')
(LeftRight a b, Right b') -> let (_,b'') = b `wb` b' in (Unstable,LeftRight a b'')
(Right b, LeftRight a' b') -> let (_,b'') = b `wb` b' in (Unstable,LeftRight a' b'')
(LeftRight a b, Left a') -> let (_,a'') = a `wa` a' in (Unstable,LeftRight a'' b)
(Left a, LeftRight a' b') -> let (_,a'') = a `wa` a' in (Unstable,LeftRight a'' b')
(LeftRight a b, LeftRight a' b') -> let (sa,a'') = a `wa` a'
(sb,b'') = b `wb` b'
in (sa sb,LeftRight a'' b'')
instance Bifunctor Either where
bimap f g x = case x of
Left a -> Left (f a)
......@@ -91,23 +96,3 @@ instance Traversable (Either a) where
traverse _ (Left a) = pure (Left a)
traverse f (Right b) = Right <$> f b
traverse f (LeftRight a b) = LeftRight a <$> f b
-- instance PreOrd b => LowerBounded (Either () b) where
-- bottom = Left ()
-- instance (PreOrd a, PreOrd b, Complete (FreeCompletion a), Complete (FreeCompletion b)) => Complete (FreeCompletion (Either a b)) where
-- Lower m1 ⊔ Lower m2 = case (bimap Lower Lower m1 ⊔ bimap Lower Lower m2) of
-- Left (Lower a) -> Lower (Left a)
-- Right (Lower b) -> Lower (Right b)
-- LeftRight (Lower a) (Lower b) -> Lower (LeftRight a b)
-- _ -> Top
-- _ ⊔ _ = Top
-- instance (UpperBounded e, UpperBounded a) => UpperBounded (Either e a) where
-- top = LeftRight top top
-- instance (PreOrd a, PreOrd b, UpperBounded (FreeCompletion a), UpperBounded (FreeCompletion b))
-- => UpperBounded (FreeCompletion (Either a b)) where
-- top = case (top,top) of
-- (Lower a,Lower b) -> Lower (LeftRight a b)
-- (_,_) -> Top
......@@ -17,13 +17,15 @@ import Data.Profunctor
import Data.Bifunctor hiding (second)
import Data.Hashable
import Data.Order
import Data.Abstract.FreeCompletion (FreeCompletion(..))
import Data.Abstract.Widening
import Data.GaloisConnection
import Data.Concrete.Powerset as C
import Data.Identifiable
import qualified Data.Concrete.Error as C
import Data.Abstract.FreeCompletion (FreeCompletion(..))
import Data.Abstract.Widening
import Data.Abstract.Stable
import GHC.Generics (Generic, Generic1)
-- | Error is an Either-like type with the ordering Success ⊑ Failure.
......@@ -84,8 +86,8 @@ instance (PreOrd a, UpperBounded e) => UpperBounded (Error e a) where
widening :: Widening e -> Widening a -> Widening (Error e a)
widening we _ (Fail a) (Fail b) = second Fail (a `we` b)
widening _ wa (Success a) (Success b) = second Success (a `wa` b)
widening _ _ (Fail a) (Success _) = (Instable ,Fail a)
widening _ _ (Success _) (Fail b) = (Instable ,Fail b)
widening _ _ (Fail a) (Success _) = (Unstable ,Fail a)
widening _ _ (Success _) (Fail b) = (Unstable ,Fail b)
instance (PreOrd e, PreOrd a, Complete (FreeCompletion e), Complete (FreeCompletion a)) => Complete (FreeCompletion (Error e a)) where
Lower m1 Lower m2 = case (bimap Lower Lower m1 bimap Lower Lower m2) of
......
......@@ -22,8 +22,10 @@ import Data.Bifunctor (Bifunctor(bimap))
import Data.Hashable
import Data.Order hiding (lub)
import Data.Traversable
import Data.Abstract.FreeCompletion (FreeCompletion(..))
import Data.Abstract.Widening
import Data.Abstract.Stable
import GHC.Generics (Generic, Generic1)
import GHC.TypeLits
......@@ -64,6 +66,7 @@ instance (PreOrd e, PreOrd a) => PreOrd (Except e a) where
(SuccessOrFail e a, SuccessOrFail e' b) -> e e' && a b
(Fail e, SuccessOrFail e' _) -> e e'
(_, _) -> False
{-# INLINE (⊑) #-}
instance (Complete e, Complete a) => Complete (Except e a) where
() = toJoin2 widening () ()
......@@ -72,13 +75,13 @@ instance (Complete e, Complete a) => Complete (Except e a) where
widening :: Widening e -> Widening a -> Widening (Except e a)
widening we wa m1 m2 = case (m1,m2) of
(Success x, Success y) -> second Success (x `wa` y)
(Success x, Fail e) -> (Instable,SuccessOrFail e x)
(Fail e, Success y) -> (Instable,SuccessOrFail e y)
(Success x, Fail e) -> (Unstable,SuccessOrFail e x)
(Fail e, Success y) -> (Unstable,SuccessOrFail e y)
(Fail e, Fail e') -> second Fail (e `we` e')
(SuccessOrFail e x, Success y) -> (Instable,SuccessOrFail e (snd (x `wa` y)))
(Success x, SuccessOrFail e y) -> (Instable,SuccessOrFail e (snd (x `wa` y)))
(SuccessOrFail e x, Fail e') -> (Instable,SuccessOrFail (snd (e `we` e')) x)
(Fail e, SuccessOrFail e' y) -> (Instable,SuccessOrFail (snd (e `we` e')) y)
(SuccessOrFail e x, Success y) -> (Unstable,SuccessOrFail e (snd (x `wa` y)))
(Success x, SuccessOrFail e y) -> (Unstable,SuccessOrFail e (snd (x `wa` y)))
(SuccessOrFail e x, Fail e') -> (Unstable,SuccessOrFail (snd (e `we` e')) x)
(Fail e, SuccessOrFail e' y) -> (Unstable,SuccessOrFail (snd (e `we` e')) y)
(SuccessOrFail e x, SuccessOrFail e' y) ->
let (s,e'') = e `we` e'
(s',z) = x `wa` y
......@@ -92,9 +95,11 @@ instance (PreOrd e, PreOrd a, Complete (FreeCompletion e), Complete (FreeComplet
SuccessOrFail (Lower e) (Lower a) -> Lower (SuccessOrFail e a)
_ -> Top
_ _ = Top
{-# INLINE (⊔) #-}
instance (UpperBounded e, UpperBounded a) => UpperBounded (Except e a) where
top = SuccessOrFail top top
{-# INLINE top #-}
instance (TypeError ('Text "Except does not have a lower bound. You probably want to use bottom of Data.Abstract.Terminating"), PreOrd a, PreOrd e) => LowerBounded (Except e a) where
bottom = error "do not implement"
......
......@@ -13,12 +13,14 @@ import Control.Monad
import Control.Monad.Except
import Control.DeepSeq
import Data.Abstract.FreeCompletion(FreeCompletion(..))
import Data.Abstract.Widening
import Data.Abstract.Stable
import Data.Bifunctor (Bifunctor(bimap))
import Data.Profunctor
import Data.Hashable
import Data.Order
import Data.Abstract.FreeCompletion(FreeCompletion(..))
import Data.Abstract.Widening
import GHC.Generics (Generic, Generic1)