Commit e46df256 authored by Sven Keidel's avatar Sven Keidel

Merge remote-tracking branch 'origin/wip-update-stratego' into develop

parents 797ab08d 80ee1151
......@@ -5,7 +5,7 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DefaultSignatures #-}
module Control.Arrow.Fix(ArrowFix(..),liftFix) where
module Control.Arrow.Fix(ArrowFix(..),Fix,liftFix) where
import Control.Arrow
import Control.Arrow.Trans
......@@ -16,5 +16,11 @@ class Arrow c => ArrowFix x y c where
-- | Computes the fixpoint of an arrow computation.
fix :: (c x y -> c x y) -> c x y
liftFix :: (ArrowFix (Dom1 t x y) (Cod1 t x y) c,ArrowTrans t) => (t c x y -> t c x y) -> t c x y
type family Fix x y (c :: * -> * -> *) :: * -> * -> *
type instance Fix x y (->) = (->)
instance ArrowFix x y (->) where
fix f = f (fix f)
liftFix :: (ArrowFix (Dom t x y) (Cod t x y) c,ArrowTrans t) => (t c x y -> t c x y) -> t c x y
liftFix f = lift $ fix (unlift . f . lift)
......@@ -3,19 +3,15 @@ module Control.Arrow.Trans where
import Control.Arrow
type family Dom (c :: * -> * -> *) x y :: *
type family Cod (c :: * -> * -> *) x y :: *
type instance Dom (->) x y = x
type instance Cod (->) x y = y
class ArrowLift t where
lift' :: Arrow c => c x y -> t c x y
-- | Lifts an inner computation into an arrow transformer and vice versa.
class ArrowTrans t where
type Dom1 t x y :: *
type Cod1 t x y :: *
type Dom t x y :: *
type Cod t x y :: *
lift :: Arrow c => c (Dom t x y) (Cod t x y) -> t c x y
unlift :: Arrow c => t c x y -> c (Dom t x y) (Cod t x y)
lift :: Arrow c => c (Dom1 t x y) (Cod1 t x y) -> t c x y
unlift :: Arrow c => t c x y -> c (Dom1 t x y) (Cod1 t x y)
type family Rep c x y
......@@ -51,6 +51,12 @@ runEnvT alloc f =
localEnv f -< (env',x)
in (const (M.empty) &&& id) ^>> runReaderT (runConstT alloc f')
instance ArrowTrans (EnvT var addr val) where
type Dom (EnvT var addr val) x y = Dom (ReaderT (Map var addr val)) x y
type Cod (EnvT var addr val) x y = Cod (ReaderT (Map var addr val)) x y
lift = undefined
unlift = undefined
instance ArrowLift (EnvT var addr val) where
lift' f = EnvT (lift' (lift' f))
......@@ -75,7 +81,8 @@ instance ArrowReader r c => ArrowReader r (EnvT var addr val c) where
instance ArrowApply c => ArrowApply (EnvT var addr val c) where
app = EnvT $ (\(EnvT f,x) -> (f,x)) ^>> app
deriving instance ArrowFix ((Map var addr val),x) y c => ArrowFix x y (EnvT var addr val c)
type instance Fix x y (EnvT var addr val c) = EnvT var addr val (Fix (Dom (EnvT var addr val) x y) (Cod (EnvT var addr val) x y) c)
deriving instance ArrowFix (Dom (EnvT var addr val) x y) (Cod (EnvT var addr val) x y) c => ArrowFix x y (EnvT var addr val c)
deriving instance Arrow c => Category (EnvT var addr val c)
deriving instance Arrow c => Arrow (EnvT var addr val c)
deriving instance ArrowChoice c => ArrowChoice (EnvT var addr val c)
......
......@@ -30,8 +30,8 @@ import Data.Order hiding (lub)
newtype CompletionT c x y = CompletionT { runCompletionT :: c x (FreeCompletion y) }
instance ArrowTrans CompletionT where
type Dom1 CompletionT x y = x
type Cod1 CompletionT x y = FreeCompletion y
type Dom CompletionT x y = x
type Cod CompletionT x y = FreeCompletion y
lift = CompletionT
unlift = runCompletionT
......@@ -70,14 +70,14 @@ instance (ArrowChoice c, ArrowReader r c) => ArrowReader r (CompletionT c) where
local f = lift (local (unlift f))
instance (ArrowChoice c, ArrowEnv var val env c) => ArrowEnv var val env (CompletionT c) where
type Join (CompletionT c) x y = Env.Join c (Dom1 CompletionT x y) (Cod1 CompletionT x y)
type Join (CompletionT c) x y = Env.Join c (Dom CompletionT x y) (Cod CompletionT 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 (CompletionT c) where
type Join (CompletionT c) x y = Exc.Join c (Dom1 CompletionT x y) (Cod1 CompletionT x y)
type Join (CompletionT c) x y = Exc.Join c (Dom CompletionT x y) (Cod CompletionT x y)
throw = lift' throw
catch f g = lift $ catch (unlift f) (unlift g)
finally f g = lift $ finally (unlift f) (unlift g)
......@@ -85,7 +85,8 @@ instance (ArrowChoice c, ArrowExcept e c) => ArrowExcept e (CompletionT c) where
instance ArrowChoice c => ArrowDeduplicate x y (CompletionT c) where
dedup = returnA
instance (ArrowChoice c, ArrowFix x (FreeCompletion y) c) => ArrowFix x y (CompletionT c) where
type instance Fix x y (CompletionT c) = CompletionT (Fix (Dom CompletionT x y) (Cod CompletionT x y) c)
instance (ArrowChoice c, ArrowFix (Dom CompletionT x y) (Cod CompletionT x y) c) => ArrowFix x y (CompletionT c) where
fix = liftFix
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (CompletionT c) where
......
......@@ -37,6 +37,7 @@ newtype ContourT lab c a b = ContourT (ReaderT (CallString lab) c a b)
runContourT :: Arrow c => Int -> ContourT lab c a b -> c a b
runContourT k (ContourT (ReaderT f)) = (\a -> (empty k,a)) ^>> f
type instance Fix x y (ContourT lab c) = ContourT lab (Fix x y c)
instance (ArrowFix x y c, ArrowApply c, HasLabel x lab) => ArrowFix x y (ContourT lab c) where
-- Pushes the label of the last argument on the call string and truncate the call string in case it reached the maximum length
fix f = ContourT $ ReaderT $ proc (c,x) -> fix (unwrap c . f . wrap) -<< x
......@@ -58,9 +59,8 @@ instance ArrowApply c => ArrowApply (ContourT lab c) where
instance ArrowReader r c => ArrowReader r (ContourT lab c) where
ask = lift' ask
local f = lift ((\(c,(r,x)) -> (r,(c,x))) ^>> local (unlift f))
deriving instance ArrowTrans (ContourT lab)
local (ContourT (ReaderT f)) = ContourT $ ReaderT $ ((\(c,(r,x)) -> (r,(c,x))) ^>> local f)
deriving instance Arrow c => Category (ContourT lab c)
deriving instance Arrow c => Arrow (ContourT lab c)
deriving instance ArrowLift (ContourT lab)
......
......@@ -58,8 +58,9 @@ instance ArrowReader r c => ArrowReader r (EnvT var val c) where
ask = lift' ask
local f = lift $ (\(env,(r,x)) -> (r,(env,x))) ^>> local (unlift f)
deriving instance ArrowJoin c => ArrowJoin (EnvT var val c)
type instance Fix x y (EnvT var val c) = EnvT var val (Fix (Dom (EnvT var val) x y) (Cod (EnvT var val) x y) c)
deriving instance ArrowFix (Map var val,x) y c => ArrowFix x y (EnvT var val c)
deriving instance ArrowJoin c => ArrowJoin (EnvT var val c)
deriving instance Arrow c => Category (EnvT var val c)
deriving instance Arrow c => Arrow (EnvT var val c)
deriving instance ArrowTrans (EnvT var val)
......
......@@ -31,8 +31,8 @@ import Data.Order
newtype ExceptT e c x y = ExceptT { runExceptT :: c x (Error e y)}
instance ArrowTrans (ExceptT e) where
type Dom1 (ExceptT e) x y = x
type Cod1 (ExceptT e) x y = Error e y
type Dom (ExceptT e) x y = x
type Cod (ExceptT e) x y = Error e y
lift = ExceptT
unlift = runExceptT
......@@ -75,7 +75,7 @@ instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowState s c) => ArrowState
put = lift' put
instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowStore var val c) => ArrowStore var val (ExceptT e c) where
type Join (ExceptT e c) x y = Store.Join c (Dom1 (ExceptT e) x y) (Cod1 (ExceptT e) x y)
type Join (ExceptT e c) x y = Store.Join c (Dom (ExceptT e) x y) (Cod (ExceptT e) x y)
read (ExceptT f) (ExceptT g) = ExceptT $ read f g
write = lift' write
......@@ -88,7 +88,7 @@ instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowReader r c) => ArrowReade
local f = lift (local (unlift f))
instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowEnv x y env c) => ArrowEnv x y env (ExceptT e c) where
type Join (ExceptT e c) x y = Env.Join c (Dom1 (ExceptT e) x y) (Cod1 (ExceptT e) x y)
type Join (ExceptT e c) x y = Env.Join c (Dom (ExceptT e) x y) (Cod (ExceptT e) x y)
lookup f g = lift $ lookup (unlift f) (unlift g)
getEnv = lift' getEnv
extendEnv = lift' extendEnv
......@@ -108,7 +108,8 @@ instance (ArrowChoice c, Complete e, ArrowJoin c) => ArrowExcept e (ExceptT e c)
unlift g -< x
returnA -< e
instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowFix (Dom1 (ExceptT e) x y) (Cod1 (ExceptT e) x y) c) => ArrowFix x y (ExceptT e c) where
type instance Fix x y (ExceptT e c) = ExceptT e (Fix (Dom (ExceptT e) x y) (Cod (ExceptT e) x y) c)
instance (Complete e, ArrowJoin c, ArrowChoice c, ArrowFix (Dom (ExceptT e) x y) (Cod (ExceptT e) x y) c) => ArrowFix x y (ExceptT e c) where
fix = liftFix
instance (Complete e, ArrowJoin c, ArrowChoice c) => ArrowDeduplicate x y (ExceptT e c) where
......
......@@ -36,8 +36,8 @@ instance ArrowChoice c => ArrowFail e (FailureT e c) where
fail = lift $ arr Fail
instance ArrowTrans (FailureT e) where
type Dom1 (FailureT e) x y = x
type Cod1 (FailureT e) x y = Failure e y
type Dom (FailureT e) x y = x
type Cod (FailureT e) x y = Failure e y
lift = FailureT
unlift = runFailureT
......@@ -71,27 +71,28 @@ instance (ArrowChoice c, ArrowReader r c) => ArrowReader r (FailureT e c) where
local f = lift (local (unlift f))
instance (ArrowChoice c, ArrowEnv x y env c) => ArrowEnv x y env (FailureT e c) where
type Join (FailureT e c) x y = Env.Join c (Dom1 (FailureT e) x y) (Cod1 (FailureT e) x y)
type Join (FailureT e c) x y = Env.Join c (Dom (FailureT e) x y) (Cod (FailureT 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, ArrowStore var val c) => ArrowStore var val (FailureT e c) where
type Join (FailureT e c) x y = Store.Join c (Dom1 (FailureT e) x y) (Cod1 (FailureT e) x y)
type Join (FailureT e c) x y = Store.Join c (Dom (FailureT e) x y) (Cod (FailureT e) x y)
read f g = lift $ read (unlift f) (unlift g)
write = lift' $ write
instance (ArrowChoice c, ArrowFix (Dom1 (FailureT e) x y) (Cod1 (FailureT e) x y) c) => ArrowFix x y (FailureT e c) where
type instance Fix x y (FailureT e c) = FailureT e (Fix (Dom (FailureT e) x y) (Cod (FailureT e) x y) c)
instance (ArrowChoice c, ArrowFix (Dom (FailureT e) x y) (Cod (FailureT e) x y) c) => ArrowFix x y (FailureT e c) where
fix = liftFix
instance (ArrowChoice c, ArrowExcept e c) => ArrowExcept e (FailureT e' c) where
type Join (FailureT e' c) x y = Exc.Join c (Dom1 (FailureT e') x y) (Cod1 (FailureT e') x y)
type Join (FailureT e' c) x y = Exc.Join c (Dom (FailureT e') x y) (Cod (FailureT e') x y)
throw = lift' throw
catch f g = lift $ catch (unlift f) (unlift g)
finally f g = lift $ finally (unlift f) (unlift g)
instance (Identifiable e, ArrowChoice c, ArrowDeduplicate (Dom1 (FailureT e) x y) (Cod1 (FailureT e) x y) c) => ArrowDeduplicate x y (FailureT e c) where
instance (Identifiable e, ArrowChoice c, ArrowDeduplicate (Dom (FailureT e) x y) (Cod (FailureT e) x y) c) => ArrowDeduplicate x y (FailureT e c) where
dedup f = lift (dedup (unlift f))
instance (ArrowChoice c, ArrowConst r c) => ArrowConst r (FailureT e c) where
......
......@@ -17,7 +17,6 @@ import qualified Data.Function as F
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Abstract.Join
import Control.Category
import Control.Monad.State hiding (fix)
......@@ -59,10 +58,10 @@ import qualified Data.Abstract.StackWidening as SW
-- 'Fix Expr Val (Reader Env (State Store (LeastFix Stack () ())))'
-- evaluates to
-- 'Reader Env (State Store (LeastFix Stack (Store,(Env,Expr)) (Store)))'
newtype FixT s a b c x y = FixT (Underlying s a b c x y)
type Underlying s a b c x y = (StackWidening s a, Widening b) -> c (((s a,Map a (Terminating b)), Map a (Terminating b)),x) (Map a (Terminating b), Terminating y)
newtype FixT s a b c x y = FixT (Underlying s a b c x y)
type Fix stack a b t c = t (FixT stack (Dom1 t a b) (Cod1 t a b) c)
type instance Fix x y (FixT s () () c) = FixT s x y c
runFixT :: (Arrow c, Complete b) => FixT SW.Unit a b c x y -> c x (Terminating y)
runFixT f = runFixT' SW.finite W.finite f
......
......@@ -31,8 +31,8 @@ import Data.Sequence hiding (lookup)
newtype PowT c x y = PowT { runPowT :: c x (A.Pow y)}
instance ArrowTrans PowT where
type Dom1 PowT x y = x
type Cod1 PowT x y = A.Pow y
type Dom PowT x y = x
type Cod PowT x y = A.Pow y
lift = PowT
unlift = runPowT
......@@ -87,6 +87,7 @@ instance (ArrowChoice c, ArrowDeduplicate x y c, Identifiable y) => ArrowDedupli
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (PowT c) where
joinWith _ (PowT f) (PowT g) = PowT $ joinWith A.union f g
type instance Fix x y (PowT c) = PowT (Fix (Dom PowT x y) (Cod PowT x y) c)
instance (ArrowChoice c, ArrowFix x (A.Pow y) c) => ArrowFix x y (PowT c) where
fix f = PowT (fix (runPowT . f . PowT))
......
......@@ -51,11 +51,12 @@ runReachingDefsT' :: Arrow c => ReachingDefsT lab c x y -> c x y
runReachingDefsT' f = (\x -> (Nothing,x)) ^>> runReachingDefsT f
instance (Identifiable var, Identifiable lab, ArrowStore var (val,Pow lab) c) => ArrowStore var val (ReachingDefsT lab c) where
type Join (ReachingDefsT lab c) ((val,x),x) y = Store.Join c (((val,Pow lab),Dom1 (ReachingDefsT lab) x y), Dom1 (ReachingDefsT lab) x y) (Cod1 (ReachingDefsT lab) x y)
type Join (ReachingDefsT lab c) ((val,x),x) y = Store.Join c (((val,Pow lab),Dom (ReachingDefsT lab) x y), Dom (ReachingDefsT lab) x y) (Cod (ReachingDefsT lab) x y)
read (ReachingDefsT f) (ReachingDefsT g) = ReachingDefsT $ read ((\((v,_::Pow lab),x) -> (v,x)) ^>> f) g
write = reachingDefsT $ proc (lab,(var,val)) ->
write -< (var,(val,P.fromMaybe lab))
type instance Fix x y (ReachingDefsT lab c) = ReachingDefsT lab (Fix x y c)
instance (HasLabel x lab, Arrow c, ArrowFix x y c) => ArrowFix x y (ReachingDefsT lab c) where
fix f = ReachingDefsT $ ReaderT $ proc (_,x) -> fix (unwrap . f . lift') -< x
where
......@@ -88,8 +89,8 @@ deriving instance ArrowState s c => ArrowState s (ReachingDefsT lab c)
deriving instance ArrowEnv x y env c => ArrowEnv x y env (ReachingDefsT lab c)
deriving instance ArrowCond val c => ArrowCond val (ReachingDefsT lab c)
deriving instance PreOrd (c (Maybe lab,x) y) => PreOrd (ReachingDefsT lab c x y)
deriving instance LowerBounded (c (Maybe lab,x) y) => LowerBounded (ReachingDefsT lab c x y)
deriving instance Complete (c (Maybe lab,x) y) => Complete (ReachingDefsT lab c x y)
deriving instance CoComplete (c (Maybe lab,x) y) => CoComplete (ReachingDefsT lab c x y)
deriving instance UpperBounded (c (Maybe lab,x) y) => UpperBounded (ReachingDefsT lab c x y)
deriving instance PreOrd (c (Dom (ReachingDefsT lab) x y) (Cod (ReachingDefsT lab) x y)) => PreOrd (ReachingDefsT lab c x y)
deriving instance LowerBounded (c (Dom (ReachingDefsT lab) x y) (Cod (ReachingDefsT lab) x y)) => LowerBounded (ReachingDefsT lab c x y)
deriving instance Complete (c (Dom (ReachingDefsT lab) x y) (Cod (ReachingDefsT lab) x y)) => Complete (ReachingDefsT lab c x y)
deriving instance CoComplete (c (Dom (ReachingDefsT lab) x y) (Cod (ReachingDefsT lab) x y)) => CoComplete (ReachingDefsT lab c x y)
deriving instance UpperBounded (c (Dom (ReachingDefsT lab) x y) (Cod (ReachingDefsT lab) x y)) => UpperBounded (ReachingDefsT lab c x y)
......@@ -61,6 +61,7 @@ deriving instance (Eq var,Hashable var,Complete val,ArrowJoin c) => ArrowJoin (S
deriving instance Arrow c => Category (StoreT var val c)
deriving instance Arrow c => Arrow (StoreT var val c)
deriving instance ArrowChoice c => ArrowChoice (StoreT var val c)
deriving instance ArrowTrans (StoreT var val)
deriving instance ArrowLift (StoreT var val)
deriving instance ArrowReader r c => ArrowReader r (StoreT var val c)
deriving instance ArrowFail e c => ArrowFail e (StoreT var val c)
......@@ -68,7 +69,9 @@ deriving instance ArrowExcept e c => ArrowExcept e (StoreT var val c)
deriving instance ArrowEnv x y env c => ArrowEnv x y env (StoreT var val c)
deriving instance ArrowConst x c => ArrowConst x (StoreT var val c)
instance ArrowApply c => ArrowApply (StoreT var val c) where app = StoreT $ (\(StoreT f,x) -> (f,x)) ^>> app
deriving instance ArrowFix (Map var val, x) (Map var val, y) c => ArrowFix x y (StoreT var val c)
type instance Fix x y (StoreT var val c) = StoreT var val (Fix (Dom (StoreT var val) x y) (Cod (StoreT var val) x y) c)
deriving instance ArrowFix (Dom (StoreT var val) x y) (Cod (StoreT var val) x y) c => ArrowFix x y (StoreT var val c)
deriving instance PreOrd (c (Map var val,x) (Map var val,y)) => PreOrd (StoreT var val c x y)
deriving instance Complete (c (Map var val,x) (Map var val,y)) => Complete (StoreT var val c x y)
......
......@@ -5,6 +5,9 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Compose where
import Control.Category
......@@ -28,11 +31,19 @@ instance ArrowApply c => ArrowApply (IdentityT c) where
instance ArrowFix x y c => ArrowFix x y (IdentityT c) where
fix = liftFix
type Compose (s :: (* -> * -> *) -> (* -> * -> *))
(t :: (* -> * -> *) -> (* -> * -> *))
(c :: * -> * -> *)
(x :: *)
(y :: *)
= s (t c) x y
newtype ComposeT
(s :: (* -> * -> *) -> (* -> * -> *))
(t :: (* -> * -> *) -> (* -> * -> *))
(c :: * -> * -> *) (x :: *) (y :: *)
= ComposeT { runComposeT :: (s (t c)) x y }
type (:*:) s t c x y = Compose s t c x y
type (:*:) = ComposeT
instance (ArrowTrans s,ArrowTrans t) => ArrowTrans (ComposeT s t) where
type Dom1 (ComposeT s t) x y = Dom1 t (Dom1 s x y) (Cod1 s x y)
type Cod1 (ComposeT s t) x y = Cod1 t (Dom1 s x y) (Cod1 s x y)
lift = undefined
unlift = undefined
(*:) :: ComposeT s t c x y -> s (t c) x y
(*:) = runComposeT
......@@ -46,8 +46,8 @@ instance ArrowChoice c => ArrowExcept e (ExceptT e c) where
returnA -< e
instance ArrowTrans (ExceptT e) where
type Dom1 (ExceptT e) x y = x
type Cod1 (ExceptT e) x y = Error e y
type Dom (ExceptT e) x y = x
type Cod (ExceptT e) x y = Error e y
lift = ExceptT
unlift = runExceptT
......@@ -84,18 +84,19 @@ instance (ArrowChoice c, ArrowReader r c) => ArrowReader r (ExceptT e c) where
local f = lift (local (unlift f))
instance (ArrowChoice c, ArrowEnv x y env c) => ArrowEnv x y env (ExceptT e c) where
type Join (ExceptT e c) x y = Env.Join c (Dom1 (ExceptT e) x y) (Cod1 (ExceptT e) x y)
type Join (ExceptT e c) x y = Env.Join c (Dom (ExceptT e) x y) (Cod (ExceptT 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, ArrowStore var val c) => ArrowStore var val (ExceptT e c) where
type Join (ExceptT e c) x y = Store.Join c (Dom1 (ExceptT e) x y) (Cod1 (ExceptT e) x y)
type Join (ExceptT e c) x y = Store.Join c (Dom (ExceptT e) x y) (Cod (ExceptT e) x y)
read f g = lift $ read (unlift f) (unlift g)
write = lift' write
instance (ArrowChoice c, ArrowFix (Dom1 (ExceptT e) x y) (Cod1 (ExceptT e) x y) c) => ArrowFix x y (ExceptT e c) where
type instance Fix x y (ExceptT e c) = ExceptT e (Fix (Dom (ExceptT e) x y) (Cod (ExceptT e) x y) c)
instance (ArrowChoice c, ArrowFix (Dom (ExceptT e) x y) (Cod (ExceptT e) x y) c) => ArrowFix x y (ExceptT e c) where
fix = liftFix
instance (Identifiable e, ArrowChoice c, ArrowDeduplicate x (Error e y) c) => ArrowDeduplicate x y (ExceptT e c) where
......
......@@ -33,8 +33,8 @@ instance ArrowChoice c => ArrowFail e (FailureT e c) where
fail = lift $ arr Fail
instance ArrowTrans (FailureT e) where
type Dom1 (FailureT e) x y = x
type Cod1 (FailureT e) x y = Failure e y
type Dom (FailureT e) x y = x
type Cod (FailureT e) x y = Failure e y
lift = FailureT
unlift = runFailureT
......@@ -68,27 +68,28 @@ instance (ArrowChoice c, ArrowReader r c) => ArrowReader r (FailureT e c) where
local f = lift (local (unlift f))
instance (ArrowChoice c, ArrowEnv x y env c) => ArrowEnv x y env (FailureT e c) where
type Join (FailureT e c) x y = Env.Join c (Dom1 (FailureT e) x y) (Cod1 (FailureT e) x y)
type Join (FailureT e c) x y = Env.Join c (Dom (FailureT e) x y) (Cod (FailureT 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, ArrowStore var val c) => ArrowStore var val (FailureT e c) where
type Join (FailureT e c) x y = Store.Join c (Dom1 (FailureT e) x y) (Cod1 (FailureT e) x y)
type Join (FailureT e c) x y = Store.Join c (Dom (FailureT e) x y) (Cod (FailureT e) x y)
read f g = lift $ read (unlift f) (unlift g)
write = lift' $ write
instance (ArrowChoice c, ArrowFix (Dom1 (FailureT e) x y) (Cod1 (FailureT e) x y) c) => ArrowFix x y (FailureT e c) where
type instance Fix x y (FailureT e c) = FailureT e (Fix (Dom (FailureT e) x y) (Cod (FailureT e) x y) c)
instance (ArrowChoice c, ArrowFix (Dom (FailureT e) x y) (Cod (FailureT e) x y) c) => ArrowFix x y (FailureT e c) where
fix = liftFix
instance (ArrowChoice c, ArrowExcept e c) => ArrowExcept e (FailureT e' c) where
type Join (FailureT e' c) x y = Exc.Join c (Dom1 (FailureT e') x y) (Cod1 (FailureT e') x y)
type Join (FailureT e' c) x y = Exc.Join c (Dom (FailureT e') x y) (Cod (FailureT e') x y)
throw = lift' throw
catch f g = lift $ catch (unlift f) (unlift g)
finally f g = lift $ finally (unlift f) (unlift g)
instance (Identifiable e, ArrowChoice c, ArrowDeduplicate (Dom1 (FailureT e) x y) (Cod1 (FailureT e) x y) c) => ArrowDeduplicate x y (FailureT e c) where
instance (Identifiable e, ArrowChoice c, ArrowDeduplicate (Dom (FailureT e) x y) (Cod (FailureT e) x y) c) => ArrowDeduplicate x y (FailureT e c) where
dedup f = lift (dedup (unlift f))
instance (ArrowChoice c, ArrowConst r c) => ArrowConst r (FailureT e c) where
......
......@@ -14,5 +14,7 @@ import Control.Arrow
-- | Arrow transformer that computes the fixpoint in the concrete interpreter.
newtype FixT a b c x y = FixT {runFixT :: c x y} deriving (Category,Arrow,ArrowChoice)
type instance Fix x y (FixT () () c) = FixT x y c
instance Arrow c => ArrowFix x y (FixT x y c) where
fix f = FixT $ runFixT (f (fix f))
......@@ -50,7 +50,9 @@ deriving instance ArrowEnv var val env c => ArrowEnv var val env (RandomT c)
deriving instance ArrowAlloc x y c => ArrowAlloc x y (RandomT c)
deriving instance ArrowCond val c => ArrowCond val (RandomT c)
deriving instance ArrowStore var val c => ArrowStore var val (RandomT c)
deriving instance (Arrow c, ArrowFix (StdGen,x) (StdGen,y) c) => ArrowFix x y (RandomT c)
type instance Fix x y (RandomT c) = RandomT (Fix (Dom RandomT x y) (Cod RandomT x y) c)
deriving instance (Arrow c, ArrowFix (Dom RandomT x y) (Cod RandomT x y) c) => ArrowFix x y (RandomT c)
instance ArrowState s c => ArrowState s (RandomT c) where
get = lift' get
......
......@@ -65,4 +65,6 @@ deriving instance ArrowConst r c => ArrowConst r (StoreT var val c)
deriving instance ArrowReader r c => ArrowReader r (StoreT var val c)
deriving instance ArrowFail e c => ArrowFail e (StoreT var val c)
deriving instance ArrowExcept e c => ArrowExcept e (StoreT var val c)
deriving instance ArrowFix (HashMap var val, x) (HashMap var val, y) c => ArrowFix x y (StoreT var val c)
type instance Fix x y (StoreT var val c) = StoreT var val (Fix (Dom (StoreT var val) x y) (Cod (StoreT var val) x y) c)
deriving instance ArrowFix (Dom (StoreT var val) x y) (Cod (StoreT var val) x y) c => ArrowFix x y (StoreT var val c)
......@@ -35,7 +35,8 @@ deriving instance ArrowChoice c => ArrowChoice (TraceT a b c)
instance ArrowApply c => ArrowApply (TraceT a b c) where
app = TraceT $ (\(TraceT f,x) -> (f,x)) ^>> app
instance ArrowFix x (Log x y,y) c => ArrowFix x y (TraceT x y c) where
type instance Fix x y (TraceT x y c) = TraceT x y (Fix (Dom (TraceT x y) x y) (Cod (TraceT x y) x y) c)
instance ArrowFix (Dom (TraceT x y) x y) (Cod (TraceT x y) x y) c => ArrowFix x y (TraceT x y c) where
fix f = TraceT $ fix (unwrap . f . TraceT)
where
unwrap :: Arrow c => TraceT x y c x y -> WriterT (Log x y) c x y
......
......@@ -35,6 +35,7 @@ newtype ConstT r c x y = ConstT (StaticT ((->) r) c x y)
runConstT :: r -> ConstT r c x y -> c x y
runConstT r (ConstT (StaticT f)) = f r
type instance Fix x y (ConstT r c) = ConstT r (Fix x y c)
instance ArrowFix x y c => ArrowFix x y (ConstT r c) where
fix f = ConstT $ StaticT $ \r -> fix (runConstT r . f . lift')
......
......@@ -37,13 +37,14 @@ instance (ArrowApply c, ArrowChoice c) => ArrowChoice (ContT c) where
ContT f ||| ContT g = ContT $ \k -> f k ||| g k
ContT f +++ ContT g = ContT $ \k -> f (k . arr Left) ||| g (k . arr Right)
type instance Fix x y (ContT c) = ContT (Fix (Dom ContT x y) (Cod ContT x y) c)
instance (ArrowApply c, ArrowFix x y c) => ArrowFix x y (ContT c) where
fix = liftFix
-- | Lift and unlift proof the yoneda lemma.
instance ArrowTrans ContT where
type Dom1 ContT x y = x
type Cod1 ContT x y = y
type Dom ContT x y = x
type Cod ContT x y = y
lift f = ContT $ \k -> k . f
unlift (ContT f) = f id
......
......@@ -29,19 +29,13 @@ import Control.Category
import Data.Order hiding (lub)
import Data.Monoidal
import Data.Soundness
-- Due to "Generalising Monads to Arrows", by John Hughes, in Science of Computer Programming 37.
newtype ReaderT r c x y = ReaderT { runReaderT :: c (r,x) y }
type instance Dom (ReaderT r c) x y = Dom c (r,x) y
type instance Cod (ReaderT r c) x y = Cod c (r,x) y
instance Sound c c' => Sound (ReaderT r c) (ReaderT r' c') where
sound (ReaderT f) (ReaderT g) = sound f g
instance ArrowTrans (ReaderT r) where
type Dom1 (ReaderT r) x y = (r,x)
type Cod1 (ReaderT r) x y = y
type Dom (ReaderT r) x y = (r,x)
type Cod (ReaderT r) x y = y
lift = ReaderT
unlift = runReaderT
......@@ -83,18 +77,19 @@ instance ArrowFail e c => ArrowFail e (ReaderT r c) where
fail = lift' fail
instance ArrowEnv var val env c => ArrowEnv var val env (ReaderT r c) where
type instance Join (ReaderT r c) ((val,x),x) y = Env.Join c ((val,Dom1 (ReaderT r) x y),Dom1 (ReaderT r) x y) (Cod1 (ReaderT r) x y)
type instance Join (ReaderT r c) ((val,x),x) y = Env.Join c ((val,Dom (ReaderT r) x y),Dom (ReaderT r) x y) (Cod (ReaderT r) x y)
lookup f g = lift $ (\(r,(v,a)) -> (v,(r,a))) ^>> lookup ((\(v,(r,a)) -> (r,(v,a))) ^>> unlift f) (unlift g)
getEnv = lift' getEnv
extendEnv = lift' extendEnv
localEnv f = lift ((\(r,(env,a)) -> (env,(r,a))) ^>> localEnv (unlift f))
instance ArrowStore var val c => ArrowStore var val (ReaderT r c) where
type instance Join (ReaderT r c) ((val,x),x) y = Store.Join c ((val,Dom1 (ReaderT r) x y),Dom1 (ReaderT r) x y) (Cod1 (ReaderT r) x y)
type instance Join (ReaderT r c) ((val,x),x) y = Store.Join c ((val,Dom (ReaderT r) x y),Dom (ReaderT r) x y) (Cod (ReaderT r) x y)
read f g = lift $ (\(r,(v,a)) -> (v,(r,a))) ^>> read ((\(v,(r,a)) -> (r,(v,a))) ^>> unlift f) (unlift g)
write = lift' write
instance ArrowFix (Dom1 (ReaderT r) x y) (Cod1 (ReaderT r) x y) c => ArrowFix x y (ReaderT r c) where
type instance Fix x y (ReaderT r c) = ReaderT r (Fix (Dom (ReaderT r) x y) (Cod (ReaderT r) x y) c)
instance ArrowFix (Dom (ReaderT r) x y) (Cod (ReaderT r) x y) c => ArrowFix x y (ReaderT r c) where
fix = liftFix
instance ArrowExcept e c => ArrowExcept e (ReaderT r c) where
......
......@@ -44,8 +44,8 @@ execStateT :: Arrow c => StateT s c x y -> c (s,x) s
execStateT f = runStateT f >>> pi1
instance ArrowTrans (StateT s) where
type Dom1 (StateT s) x y = (s,x)
type Cod1 (StateT s) x y = (s,y)
type Dom (StateT s) x y = (s,x)
type Cod (StateT s) x y = (s,y)
lift = StateT
unlift = runStateT
......@@ -87,14 +87,14 @@ instance ArrowWriter w c => ArrowWriter w (StateT s c) where
tell = lift' tell
instance (ArrowEnv var val env c) => ArrowEnv var val env (StateT s c) where
type instance Join (StateT s c) ((val,x),x) y = Env.Join c ((val,Dom1 (StateT s) x y),Dom1 (StateT s) x y) (Cod1 (StateT s) x y)
type instance Join (StateT s c) ((val,x),x) y = Env.Join c ((val,Dom (StateT s) x y),Dom (StateT s) x y) (Cod (StateT s) x y)
lookup f g = lift $ (\(s,(v,a)) -> (v,(s,a))) ^>> lookup ((\(v,(s,a)) -> (s,(v,a))) ^>> unlift f) (unlift g)
getEnv = lift' getEnv
extendEnv = lift' extendEnv
localEnv f = lift ((\(r,(env,a)) -> (env,(r,a))) ^>> localEnv (unlift f))
instance (ArrowStore var val c) => ArrowStore var val (StateT s c) where
type instance Join (StateT s c) ((val,x),x) y =