Commit aec853da authored by Sven Keidel's avatar Sven Keidel

fix wrong join operator of Kleisli arrows

parent b258f02c
Pipeline #16128 passed with stages
in 32 minutes and 49 seconds
......@@ -27,9 +27,9 @@ import Text.Printf
class (Arrow c, Profunctor c) => ArrowReuse a b c where
-- | Reuse cached results at the cost of precision.
reuse :: (Show m, Monoid m) => (a -> a -> Stable -> b -> m) -> c (a,Stable) m
reuse :: (Monoid m) => (a -> a -> Stable -> b -> m) -> c (a,Stable) m
reuseFirst :: (ArrowChoice c, ArrowReuse a b c, Show a, Show b) => Stable -> IterationStrategy c a b
reuseFirst :: (ArrowChoice c, ArrowReuse a b c) => Stable -> IterationStrategy c a b
reuseFirst st f = proc a -> do
m <- reuse (\_ a' s' b' -> First (Just (a',b',s'))) -< (a,st)
case getFirst m of
......@@ -46,15 +46,15 @@ reuseExact f = proc a -> do
_ -> f -< a
{-# INLINE reuseExact #-}
reuseByMetric :: (Show a, Show b, Show n, Ord n, ArrowChoice c, ArrowReuse a b c) => Metric a n -> IterationStrategy c a b
reuseByMetric :: (Ord n, ArrowChoice c, ArrowReuse a b c) => Metric a n -> IterationStrategy c a b
reuseByMetric metric = reuseByMetric_ (\s a a' -> Product s (metric a a')) Unstable
{-# INLINE reuseByMetric #-}
reuseStableByMetric :: (Show a, Show b, Show n, Ord n, ArrowChoice c, ArrowReuse a b c) => Metric a n -> IterationStrategy c a b
reuseStableByMetric :: (Ord n, ArrowChoice c, ArrowReuse a b c) => Metric a n -> IterationStrategy c a b
reuseStableByMetric metric = reuseByMetric_ (const metric) Stable
{-# INLINE reuseStableByMetric #-}
reuseByMetric_ :: (Show a, Show b, Show n, Ord n, ArrowChoice c, ArrowReuse a b c) => (Stable -> Metric a n) -> Stable -> IterationStrategy c a b
reuseByMetric_ :: (Ord n, ArrowChoice c, ArrowReuse a b c) => (Stable -> Metric a n) -> Stable -> IterationStrategy c a b
reuseByMetric_ metric st f = proc a -> do
m <- reuse (\a a' s' b' -> Just (Measured { input = a', output = b', stable = s', measured = metric s' a a' })) -< (a,st)
case m of
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Control.Arrow.Order where
......@@ -18,7 +17,7 @@ class (Arrow c, Profunctor c) => ArrowComplete y c where
(<>) :: c x y -> c x y -> c x y
instance Complete y => ArrowComplete y (->) where
(<>) f g = \x -> f x g x
(<>) f g x = f x g x
{-# INLINE (<⊔>) #-}
-- | An arrow computation @c@ is effect commutative iff for all @f, g :: c x y@,
......@@ -26,8 +25,8 @@ instance Complete y => ArrowComplete y (->) where
-- > (f ⊔ g) ⊑ (proc x -> do y1 <- f -< x
-- > y2 <- g -< x
-- > returnA -< y1 ⊔ y2)
--
-- and
--
-- and
--
-- > (f ⊔ g) ⊑ (proc x -> do y1 <- g -< x
-- > y2 <- f -< x
......@@ -37,10 +36,10 @@ class (Arrow c, Profunctor c) => ArrowEffectCommutative c
instance ArrowEffectCommutative (->)
class (Arrow c, Profunctor c) => ArrowJoin c where
joinSecond :: c x y -> c (z,x) (z,y)
joinSecond :: (y -> y -> y) -> (x -> y) -> c x y -> c x y
instance ArrowJoin (->) where
joinSecond g = \(z,x) -> (z,g x)
joinSecond lub f g x = f x `lub` g x
{-# INLINE joinSecond #-}
-- | Joins a list of arguments. Use it with idiom brackets:
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Abstract.Completion(CompletionT,runCompletionT) where
......@@ -24,6 +23,7 @@ import Control.Arrow.Transformer.Kleisli
import Control.Category
import Data.Abstract.FreeCompletion
import Data.Abstract.Widening
import Data.Profunctor
import Data.Profunctor.Unsafe((.#))
......@@ -32,7 +32,7 @@ import Data.Coerce
-- | Allows to describe computations over non-completely ordered types.
-- E.g. allows to join a computation of type 'c x [y]'.
newtype CompletionT c x y = CompletionT (KleisliT FreeCompletion c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun, ArrowJoin,
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun,
ArrowConst r, ArrowState s, ArrowReader r,
ArrowEnv var val, ArrowClosure var val env, ArrowStore a b,
ArrowFail e, ArrowExcept e)
......@@ -48,3 +48,7 @@ deriving instance (ArrowFix (Underlying (CompletionT c) x y)) => ArrowFix (Compl
deriving instance (ArrowChoice c, ArrowComplete (FreeCompletion y) c) => ArrowComplete y (CompletionT c)
deriving instance (ArrowChoice c, ArrowLowerBounded c) => ArrowLowerBounded (CompletionT c)
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (CompletionT c) where
joinSecond lub f g = lift $ joinSecond (toJoin widening lub) (return . f) (unlift g)
{-# INLINE joinSecond #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Abstract.Error(ErrorT,runErrorT) where
import Prelude hiding (id,lookup,(.),read,fail)
......@@ -24,14 +23,16 @@ import Control.Arrow.Order
import Control.Arrow.Transformer.Kleisli
import Control.Category
import qualified Data.Order as O
import Data.Abstract.Error
import Data.Abstract.Widening
import Data.Profunctor
import Data.Profunctor.Unsafe((.#))
import Data.Coerce
newtype ErrorT e c x y = ErrorT (KleisliT (Error e) c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun, ArrowJoin,
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun,
ArrowConst r, ArrowState s, ArrowReader r,
ArrowEnv var val, ArrowClosure var val env, ArrowStore a b,
ArrowExcept e')
......@@ -42,15 +43,21 @@ runErrorT = coerce
instance (ArrowChoice c, Profunctor c) => ArrowFail e (ErrorT e c) where
fail = lift $ arr Fail
{-# INLINE fail #-}
instance (ArrowChoice c, ArrowApply c, Profunctor c) => ArrowApply (ErrorT e c) where
app = lift (app .# first coerce)
{-# INLINE app #-}
type instance Fix (ErrorT e c) x y = ErrorT e (Fix c x (Error e y))
deriving instance (ArrowFix (Underlying (ErrorT e c) x y)) => ArrowFix (ErrorT e c x y)
instance (ArrowChoice c, ArrowLowerBounded c) => ArrowLowerBounded (ErrorT e c) where
bottom = lift bottom
{-# INLINE bottom #-}
deriving instance (ArrowChoice c, ArrowComplete (Error e y) c) => ArrowComplete y (ErrorT e c)
instance (O.Complete e, ArrowChoice c, ArrowJoin c) => ArrowJoin (ErrorT e c) where
joinSecond lub f g = lift $ joinSecond (toJoin2 widening (O.) lub) (Success . f) (unlift g)
{-# INLINE joinSecond #-}
......@@ -25,14 +25,15 @@ import Control.Arrow.Trans
import Control.Arrow.Transformer.Kleisli
import Data.Abstract.Except
import Data.Abstract.Widening
import Data.Order(Complete(..))
import qualified Data.Order as O
import Data.Profunctor
import Data.Profunctor.Unsafe((.#))
import Data.Coerce
newtype ExceptT e c x y = ExceptT (KleisliT (Except e) c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun, ArrowJoin, ArrowLowerBounded,
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun, ArrowLowerBounded,
ArrowConst r, ArrowState s, ArrowReader r,
ArrowEnv var val, ArrowClosure var val env, ArrowStore a b,
ArrowFail e')
......@@ -41,7 +42,7 @@ runExceptT :: ExceptT e c x y -> c x (Except e y)
runExceptT = coerce
{-# INLINE runExceptT #-}
instance (Complete e, ArrowChoice c, ArrowJoin c) => ArrowExcept e (ExceptT e c) where
instance (O.Complete e, ArrowChoice c, ArrowJoin c) => ArrowExcept e (ExceptT e c) where
type Join y (ExceptT e c) = ArrowComplete (Except e y) c
throw = lift $ arr Fail
try f g h = lift $ proc x -> do
......@@ -53,10 +54,14 @@ instance (Complete e, ArrowChoice c, ArrowJoin c) => ArrowExcept e (ExceptT e c)
{-# INLINE throw #-}
{-# INLINE try #-}
instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowApply c, Profunctor c) => ArrowApply (ExceptT e c) where
instance (O.Complete e, ArrowJoin c, ArrowChoice c, ArrowApply c, Profunctor c) => ArrowApply (ExceptT e c) where
app = lift (app .# first coerce)
{-# INLINE app #-}
type instance Fix (ExceptT e c) x y = ExceptT e (Fix c x (Except e y))
instance ArrowFix (Underlying (ExceptT e c) x y) => ArrowFix (ExceptT e c x y)
deriving instance (Complete e, ArrowChoice c, ArrowJoin c, ArrowComplete (Except e y) c) => ArrowComplete y (ExceptT e c)
deriving instance (O.Complete e, ArrowChoice c, ArrowJoin c, ArrowComplete (Except e y) c) => ArrowComplete y (ExceptT e c)
instance (O.Complete e, ArrowChoice c, ArrowJoin c) => ArrowJoin (ExceptT e c) where
joinSecond lub f g = lift $ joinSecond (toJoin2 widening (O.) lub) (Success . f) (unlift g)
{-# INLINE joinSecond #-}
......@@ -2,8 +2,6 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
module Control.Arrow.Transformer.Abstract.Failure(FailureT,runFailureT) where
......@@ -25,6 +23,7 @@ import Control.Arrow.Order
import Control.Arrow.Transformer.Kleisli
import Data.Abstract.Failure
import Data.Abstract.Widening
import Data.Profunctor
import Data.Profunctor.Unsafe((.#))
......@@ -32,7 +31,7 @@ import Data.Coerce
-- | Describes computations that can fail.
newtype FailureT e c x y = FailureT (KleisliT (Failure e) c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun, ArrowJoin,
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun,
ArrowConst r, ArrowState s, ArrowReader r,
ArrowEnv var val, ArrowClosure var val env, ArrowStore a b,
ArrowExcept e')
......@@ -49,3 +48,7 @@ instance (ArrowChoice c, ArrowApply c, Profunctor c) => ArrowApply (FailureT e c
type instance Fix (FailureT e c) x y = FailureT e (Fix c x y)
instance (ArrowChoice c, ArrowFix (Underlying (FailureT e c) x y)) => ArrowFix (FailureT e c x y)
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (FailureT e c) where
joinSecond lub f g = lift $ joinSecond (toJoin widening lub) (Success . f) (unlift g)
{-# INLINE joinSecond #-}
......@@ -10,7 +10,7 @@
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Control.Arrow.Transformer.Abstract.Fix.Cache where
import Prelude hiding (pred,lookup,map,head,iterate,(.),truncate,elem)
import Prelude hiding (pred,lookup,map,head,iterate,(.),id,truncate,elem)
import Control.Category
import Control.Arrow
......@@ -27,7 +27,7 @@ import Control.Arrow.Transformer.State
import Data.Profunctor.Unsafe
import Data.Empty
import Data.Order
import Data.Order hiding (lub)
import Data.Coerce
import Data.Identifiable
import Data.HashMap.Lazy(HashMap)
......@@ -65,7 +65,7 @@ instance (Complete y, ArrowEffectCommutative c) => ArrowComplete y (CacheT cache
{-# INLINE (<⊔>) #-}
instance (Arrow c, Profunctor c) => ArrowJoin (CacheT cache a b c) where
joinSecond (CacheT f) = CacheT (second f)
joinSecond lub f (CacheT g) = CacheT (rmap (\(x,y) -> f x `lub` y) (id &&& g))
{-# INLINE joinSecond #-}
instance (Profunctor c,ArrowApply c) => ArrowApply (CacheT cache a b c) where
......@@ -75,7 +75,9 @@ instance (Profunctor c,ArrowApply c) => ArrowApply (CacheT cache a b c) where
instance ArrowEffectCommutative c => ArrowEffectCommutative (CacheT cache a b c)
----- Basic Cache -----
newtype Cache a b = Cache { getMap :: HashMap a (Stable,b)}
instance (Show a, Show b) => Show (Cache a b) where
show (Cache m) = show (M.toList m)
......@@ -119,6 +121,10 @@ instance (PreOrd a, Arrow c, Profunctor c) => ArrowReuse a b (CacheT Cache a b c
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 #-}
instance Identifiable a => IsList (Cache a b) where
type Item (Cache a b) = (a,b,Stable)
toList (Cache m) = [ (a,b,s) | (a,(s,b)) <- M.toList m]
fromList l = Cache $ M.fromList [ (a,(s,b)) | (a,b,s) <- l]
------ Group Cache ------
data Group cache a b where
......
......@@ -8,7 +8,7 @@
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Abstract.Fix.Context where
import Prelude hiding (lookup,truncate,(.))
import Prelude hiding (lookup,truncate,(.),id)
import Control.Category
import Control.Arrow
......@@ -31,7 +31,7 @@ import qualified Data.HashMap.Lazy as M
import Data.Profunctor.Unsafe
import Data.Coerce
import Data.Empty
import Data.Order
import Data.Order hiding (lub)
import Data.Identifiable
callsiteSensitive :: forall a lab b c. ArrowContext (CallString lab) a c => Int -> (a -> lab) -> Widening c a -> IterationStrategy c a b
......@@ -97,7 +97,7 @@ instance (Complete y, ArrowEffectCommutative c) => ArrowComplete y (ContextT ctx
{-# INLINE (<⊔>) #-}
instance (Arrow c, Profunctor c) => ArrowJoin (ContextT ctx a c) where
joinSecond (ContextT f) = ContextT (second f)
joinSecond lub f (ContextT g) = ContextT (rmap (\(x,y) -> f x `lub` y) (id &&& g))
{-# INLINE joinSecond #-}
instance ArrowEffectCommutative c => ArrowEffectCommutative (ContextT ctx a c)
......
......@@ -34,7 +34,7 @@ trace showA showB f = proc x -> do
returnA -< Debug.trace (printf "RETURN\n%s\n%s\n\n" (showA x) (showB y)) y
{-# INLINE trace #-}
traceCtx :: (ArrowContext ctx a c,ArrowState cache c) => (a -> String) -> (b -> String) -> (ctx -> String) -> (cache -> String) -> IterationStrategy c a b
traceCtx :: (ArrowContext ctx a' c,ArrowState cache c) => (a -> String) -> (b -> String) -> (ctx -> String) -> (cache -> String) -> IterationStrategy c a b
traceCtx showA showB showCtx showCache f = proc x -> do
ctx <- askContext -< ()
cache <- get -< ()
......@@ -47,19 +47,20 @@ traceShow = trace show show
{-# INLINE traceShow #-}
newtype TraceT c x y = TraceT (c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowComplete z,ArrowJoin,ArrowEffectCommutative,ArrowComponent a,ArrowStack a,ArrowContext ctx a,ArrowState s)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowComplete z,ArrowJoin,
ArrowEffectCommutative,ArrowComponent a,ArrowStack a,ArrowContext ctx a,ArrowState s, ArrowReuse a b)
instance (Show a, ArrowReuse a b c) => ArrowReuse a b (TraceT c) where
-- | Reuse cached results at the cost of precision.
reuse f = TraceT $ proc (a,s) -> do
m <- Reuse.reuse f -< (a,s)
returnA -< Debug.trace (printf "REUSE\nx: %s\n%s\n\n" (show a) (show m)) m
-- instance (Show a, ArrowReuse a b c) => ArrowReuse a b (TraceT c) where
-- -- | Reuse cached results at the cost of precision.
-- reuse f = TraceT $ proc (a,s) -> do
-- m <- Reuse.reuse f -< (a,s)
-- returnA -< Debug.trace (printf "REUSE\nx: %s\n%s\n\n" (show a) (show m)) m
instance (Show a, ArrowIterate a c) => ArrowIterate a (TraceT c) where
iterate = TraceT $ proc (a,b) ->
iterate -< Debug.trace (printf "ITERATE\n\tx: %s\n\n" (show a)) (a,b)
instance (Show a, Show b, Show cache, ArrowState cache c, ArrowCache a b c) => ArrowCache a b (TraceT c) where
instance (Show a, Show b, ArrowCache a b c) => ArrowCache a b (TraceT c) where
lookup = TraceT $ proc a -> do
b <- lookup -< a
returnA -< Debug.trace (printf "LOOKUP\n\tx: %s\n\ty: %s\n\n" (show a) (show b)) b
......@@ -68,10 +69,9 @@ instance (Show a, Show b, Show cache, ArrowState cache c, ArrowCache a b c) => A
(s,b') <- update -< (a,b)
returnA -< Debug.trace (printf "UPDATE\n\tx: %s\n\ty: %s -> %s, %s\n\n" (show a) (show bOld) (show b') (show s)) (s,b')
write = TraceT $ proc (a,b,s) -> do
cache <- get -< ()
write -< Debug.trace (printf "WRITE\n\tx: %s\n\ty: %s\n\t%s\n\tcache: %s\n\n" (show a) (show b) (show s) (show cache)) (a,b,s)
write -< Debug.trace (printf "WRITE\n\tx: %s\n\ty: %s\n\t%s\n\t\n\n" (show a) (show b) (show s)) (a,b,s)
setStable = TraceT $ proc (s,a) ->
setStable -< Debug.trace (printf "STABLE: %s\n\n" (show s)) (s,a)
setStable -< Debug.trace (printf "STABLE\n\tx: %s\n\t%s\n\n" (show a) (show s)) (s,a)
{-# INLINE lookup #-}
{-# INLINE update #-}
{-# INLINE write #-}
......
......@@ -3,8 +3,6 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Arrows #-}
module Control.Arrow.Transformer.Abstract.Powerset(PowT,runPowT) where
import Prelude hiding (id,(.),lookup,fail)
......@@ -31,7 +29,7 @@ import Data.Coerce
-- | Computation that produces a set of results.
newtype PowT c x y = PowT (KleisliT A.Pow c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun, ArrowJoin,
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun,
ArrowConst r, ArrowState s, ArrowReader r,
ArrowEnv var val, ArrowClosure var val env, ArrowStore a b,
ArrowFail e', ArrowExcept e')
......@@ -48,4 +46,8 @@ instance (Identifiable y, Profunctor c, ArrowFix (Underlying (PowT c) x y)) => A
fix f = lift $ rmap A.dedup (fix (coerce f))
instance (ArrowChoice c, Profunctor c) => ArrowLowerBounded (PowT c) where
bottom = lift $ arr (\_ -> A.empty)
bottom = lift $ arr (const A.empty)
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (PowT c) where
joinSecond _ f g = lift $ joinSecond A.union (return . f) (unlift g)
{-# INLINE joinSecond #-}
......@@ -22,14 +22,15 @@ import Control.Arrow.Transformer.Kleisli
import Control.Category
import Data.Abstract.Terminating
import Data.Abstract.Widening
import Data.Profunctor
import Data.Profunctor.Unsafe((.#))
import Data.Coerce
-- | Arrow that propagates non-terminating computations.
newtype TerminatingT c x y = TerminatingT (KleisliT Terminating c x y)
deriving (Profunctor, Category, Arrow, ArrowChoice, ArrowTrans, ArrowLift, ArrowRun, ArrowJoin,
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, ArrowStore addr val)
......@@ -45,7 +46,11 @@ type instance Fix (TerminatingT c) x y = TerminatingT (Fix c x (Terminating y))
deriving instance (ArrowFix (Underlying (TerminatingT c) x y)) => ArrowFix (TerminatingT c x y)
instance (ArrowChoice c, Profunctor c) => ArrowLowerBounded (TerminatingT c) where
bottom = lift $ arr (\_ -> NonTerminating)
bottom = lift $ arr (const NonTerminating)
{-# INLINE bottom #-}
deriving instance (ArrowChoice c, ArrowComplete (Terminating y) c) => ArrowComplete y (TerminatingT c)
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (TerminatingT c) where
joinSecond lub f g = lift $ joinSecond (toJoin widening lub) (return . f)(unlift g)
{-# INLINE joinSecond #-}
......@@ -3,9 +3,6 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
module Control.Arrow.Transformer.Cokleisli where
import Prelude hiding (id,(.),lookup,read,fail)
......@@ -136,6 +133,6 @@ instance (ArrowComonad f c, ArrowComplete y c) => ArrowComplete y (CokleisliT f
{-# INLINE (<⊔>) #-}
instance (ArrowComonad f c, ArrowJoin c) => ArrowJoin (CokleisliT f c) where
joinSecond g = lift $ lmap costrength2 (joinSecond (unlift g))
{-# INLINE joinSecond#-}
joinSecond lub f g = lift $ joinSecond lub (f . extract) (unlift g)
{-# INLINE joinSecond #-}
......@@ -140,7 +140,3 @@ instance (ArrowMonad f c, ArrowComplete (f y) c) => ArrowComplete y (KleisliT f
instance (ArrowMonad f c, ArrowLowerBounded c) => ArrowLowerBounded (KleisliT f c) where
bottom = lift bottom
instance (ArrowMonad f c, ArrowJoin c) => ArrowJoin (KleisliT f c) where
joinSecond g = lift $ rmap strength2 (joinSecond (unlift g))
{-# INLINE joinSecond#-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
......@@ -146,7 +143,7 @@ instance ArrowLowerBounded c => ArrowLowerBounded (ReaderT r c) where
{-# INLINE bottom #-}
instance ArrowJoin c => ArrowJoin (ReaderT r c) where
joinSecond g = lift $ lmap shuffle1 (joinSecond (unlift g))
joinSecond lub f g = lift $ joinSecond lub (f . snd) (unlift g)
{-# INLINE joinSecond #-}
instance ArrowComplete y c => ArrowComplete y (ReaderT r c) where
......
......@@ -163,7 +163,7 @@ instance (ArrowLowerBounded c) => ArrowLowerBounded (StateT s c) where
{-# INLINE bottom #-}
instance (ArrowJoin c, O.Complete s) => ArrowJoin (StateT s c) where
joinSecond g = lift $ dimap (\(s,(z,x)) -> ((s,z),(s,x))) (\((s,z),(s',x)) -> (s O. s',(z,x))) (joinSecond (unlift g))
joinSecond lub f g = lift $ joinSecond (\(s1,y1) (s2,y2) -> (s1 O. s2, lub y1 y2)) (second f) (unlift g)
{-# INLINE joinSecond #-}
instance (ArrowComplete (s,y) c) => ArrowComplete y (StateT s c) where
......
......@@ -149,7 +149,7 @@ instance (Applicative f, ArrowLowerBounded c) => ArrowLowerBounded (StaticT f c)
{-# SPECIALIZE instance ArrowLowerBounded c => ArrowLowerBounded (StaticT ((->) r) c) #-}
instance (Applicative f, ArrowJoin c) => ArrowJoin (StaticT f c) where
joinSecond (StaticT g) = StaticT $ joinSecond <$> g
joinSecond lub f (StaticT g) = StaticT $ joinSecond lub f <$> g
{-# INLINE joinSecond #-}
{-# SPECIALIZE instance ArrowJoin c => ArrowJoin (StaticT ((->) r) c) #-}
......
......@@ -29,6 +29,7 @@ import Control.Arrow.Store as Store
import Control.Arrow.Trans
import Control.Arrow.Writer
import qualified Data.Order as O
import Data.Monoidal
import Data.Profunctor
import Data.Profunctor.Unsafe
......@@ -154,8 +155,8 @@ instance (Monoid w, ArrowLowerBounded c) => ArrowLowerBounded (WriterT w c) wher
bottom = lift bottom
{-# INLINE bottom #-}
instance (Monoid w, ArrowJoin c) => ArrowJoin (WriterT w c) where
joinSecond g = lift $ rmap shuffle1 (joinSecond (unlift g))
instance (Monoid w, O.Complete w, ArrowJoin c) => ArrowJoin (WriterT w c) where
joinSecond lub f g = lift $ joinSecond (\(w1,y1) (w2,y2) -> (w1 O. w2, lub y1 y2) ) (\x -> (mempty,f x)) (unlift g)
{-# INLINE joinSecond #-}
instance (Monoid w, ArrowComplete (w,y) c) => ArrowComplete y (WriterT w c) where
......
......@@ -6,6 +6,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns -Wno-incomplete-patterns #-}
module Data.Abstract.Except where
import Prelude hiding (id,(.))
......@@ -45,13 +46,13 @@ instance (Show x, Show e) => Show (Except e x) where
show (SuccessOrFail e x) = "Success " ++ show x ++ " ⊔ Fail " ++ show e
instance (O.ArrowJoin c, ArrowChoice c, Profunctor c) => ArrowFunctor (Except e) c where
mapA f = lmap toEither (arr Fail ||| rmap Success f ||| rmap (\(e,y) -> SuccessOrFail e y) (O.joinSecond f))
mapA f = lmap toEither (arr Fail ||| rmap Success f ||| O.joinSecond (\(Fail e) (Success y) -> SuccessOrFail e y) (\(e,_) -> Fail e) (proc (_,x) -> rmap Success f -< x))
{-# INLINABLE mapA #-}
instance (Complete e, O.ArrowJoin c, ArrowChoice c, Profunctor c) => ArrowMonad (Except e) c where
mapJoinA f = lmap toEither (arr Fail ||| f ||| rmap lub (O.joinSecond f))
where
lub (e,m) = case m of
mapJoinA f = lmap toEither (arr Fail ||| f ||| O.joinSecond lub (\(e,_) -> Fail e) (proc (_,x) -> f -< x))
where
lub (Fail e) m = case m of
Fail e' -> Fail (e e')
Success y -> SuccessOrFail e y
SuccessOrFail e' y -> SuccessOrFail (e e') y
......@@ -94,7 +95,7 @@ widening we wa m1 m2 = case (m1,m2) of
{-# INLINE widening #-}
instance (PreOrd e, PreOrd a, Complete (FreeCompletion e), Complete (FreeCompletion a)) => Complete (FreeCompletion (Except e a)) where
Lower m1 Lower m2 = case (bimap Lower Lower m1 bimap Lower Lower m2) of
Lower m1 Lower m2 = case bimap Lower Lower m1 bimap Lower Lower m2 of
Fail (Lower e) -> Lower (Fail e)
Success (Lower a) -> Lower (Success a)
SuccessOrFail (Lower e) (Lower a) -> Lower (SuccessOrFail e a)
......
......@@ -228,3 +228,8 @@ instance LowerBounded a => LowerBounded (Identity a) where
instance Complete a => Complete (Identity a) where
Identity x Identity y = Identity $ x y
newtype Discrete a = Discrete a deriving (Eq)
instance Eq a => PreOrd (Discrete a) where
() = (==)
() = (==)
......@@ -18,6 +18,7 @@ import Abstract.TermEnvironment
import Control.Category
import Control.Arrow.Fix as Fix
import Control.Arrow.Fix.Reuse
import Control.Arrow.Fix.Context as Context
import Control.Arrow.Trans
import Control.Arrow.Transformer.Value
......@@ -34,6 +35,7 @@ import Control.Arrow.Transformer.Abstract.Fix.Stack
import Control.Arrow.Transformer.Abstract.Fix.Cache
import Control.Arrow.Transformer.Abstract.Fix.Trace
import Data.Hashable
import Data.Abstract.FreeCompletion hiding (Top)
import qualified Data.Abstract.FreeCompletion as Free
import Data.Abstract.Except as E
......@@ -51,6 +53,7 @@ import Data.Identifiable
import Data.Label
import Text.Printf
import GHC.Exts
type TypeError = Pow String
......@@ -67,7 +70,7 @@ type Interp t x y =
(CompletionT
(TerminatingT
(FixT () ()
(--TraceT
(-- TraceT
(ChaoticT (Dom t)
(StackT Stack (Dom t)
(CacheT (Group Cache) (Dom t) (Cod t)
......@@ -75,19 +78,21 @@ type Interp t x y =
(->)))))))))))))))
(Strat,t) t x y
runInterp :: forall t x y. (Show t, Complete t, Complete (FreeCompletion t), Identifiable t, ?sensitivity :: Int) =>
runInterp :: forall t x y. (Show t, Complete t, Identifiable t, ?sensitivity :: Int) =>
Interp t x y -> W.Widening t -> StratEnv -> Context -> TermEnv t -> x -> Terminating (FreeCompletion (Error (Pow String) (Except () (TermEnv t,y))))
runInterp f termWidening senv0 ctx tenv0 a =
snd (run f ctx iterationStrategy resultWidening (tenv0, (senv0, a)))
runInterp f termWidening senv0 ctx0 tenv0 a0 =
snd (run f ctx0 iterationStrategy resultWidening (tenv0, (senv0, a0)))
where
iterationStrategy
= trace (\(tenv,(_senv,(strat,term))) -> printf "STRAT %s\nTERM %s\nENV %s" (show strat) (show term) (show tenv))
= traceCtx
(\(tenv,(senv,(strat,term))) -> printf "STRAT %s\nTERM %s\nENV %s\nSENV %s\n" (show strat) (show term) (show tenv) (show (hash senv)))
(printf "RET %s" . show . fmap (fmap (fmap (fmap snd))))
-- (\cx -> printf "CTX %s" (show cx))
-- (\cache -> printf "CACHE %s" (show [ (strat,ctx,a,b,s) | ((strat,_),cache') <- toList cache, (ctx,(a,_),b,s) <- toList cache']))
(\cx -> printf "CTX %s" (show cx))
(\cache -> printf "CACHE %s" (show [ (strat,a,tenv,b,s,senv) | ((strat,senv),cache') <- toList cache, ((a,tenv),b,s) <- toList cache']))
. Fix.filter stratCall (recordCallsite ?sensitivity (\((strat,_),_) -> Just (label strat)))
. Fix.filter stratApply
( joinByContext' (termWidening W.** S.widening termWidening)
-- . reuseFirst Unstable
. iterateInner
)
......
......@@ -56,10 +56,11 @@ eval = fix' $ \ev s0 -> case s0 of
Call f ss ts _ -> proc t -> do
senv <- readStratEnv -< ()
case M.lookup f senv of
Just (Closure strat@(Strategy _ params _ _) senv') -> do
Just (Closure strat senv') -> do
let senv'' = if M.null senv' then senv else senv'
args <- map lookupTermVarOrFail -< ts
scope params (invoke ev) -<< (strat, senv'', ss, args, t)
scope (strategyTermArguments strat)
(invoke ev) -<< (strat, senv'', ss, args, t)
Nothing -> failString -< printf "strategy %s not in scope" (show f)
Apply body _ -> ev body
......@@ -122,7 +123,12 @@ let_ ss body interp = proc a -> do
-- | Strategy calls bind strategy variables and term variables.
invoke :: (ArrowChoice c, ArrowFail e c, ArrowApply c, IsString e, IsTermEnv env t c, HasStratEnv c, Env.Join t c)
=> (Strat -> c t t) -> c (Strategy, StratEnv, [Strat], [t], t) t
invoke ev = proc (Strategy formalStratArgs formalTermArgs body l, senv, actualStratArgs, actualTermArgs, t) -> do
invoke ev = proc (Strategy { strategyStratArguments = formalStratArgs
, strategyTermArguments = formalTermArgs
, strategyBody = body
, strategyLabel = l
},
senv, actualStratArgs, actualTermArgs, t) -> do
bindings -< zip formalTermArgs actualTermArgs
let senv' = bindStratArgs (zip formalStratArgs actualStratArgs) senv
case body of
......@@ -136,7 +142,7 @@ invoke ev = proc (Strategy formalStratArgs formalTermArgs body l, senv, actualSt
Just s -> M.insert v s (bindStratArgs ss senv)
_ -> error $ "unknown strategy: " ++ show v'
bindStratArgs ((v,s) : ss) senv =
M.insert v (Closure (Strategy [] [] s (label s)) senv) (bindStratArgs ss senv)
M.insert v (Closure (Strategy [] [] s (label s) (S.freeStratVars s)) senv) (bindStratArgs ss senv)
{-# INLINE invoke #-}
-- | Matches a pattern against the current term. Pattern variables are
......
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}