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

fix and polish PCF analysis

parent d6c8d718
Pipeline #13210 failed with stages
in 20 minutes and 28 seconds
......@@ -69,13 +69,13 @@ instance ArrowLift (EnvT var addr val) where
instance (Identifiable var, Identifiable addr, Complete val, ArrowChoice c, Profunctor c) =>
ArrowEnv var val (Map var addr val) (EnvT var addr val c) where
type Join (EnvT var addr val c) x y = Complete (c (Map var addr val,x) y)
type Join (EnvT var addr val c) x y = (ArrowJoin c, Complete y)
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- ask -< ()
case do M.lookup var env of
Just val -> f -< (val,x)
JustNothing val -> joined f g -< ((val,x),x)
Nothing -> g -< x
Just val -> f -< (val,x)
Nothing -> g -< x
JustNothing val -> (f -< (val,x)) <> (g -< x)
getEnv = EnvT ask
extendEnv = EnvT $ ConstT $ StaticT $ \alloc -> lift' $ M.insertBy alloc
localEnv (EnvT f) = EnvT $ local f
......@@ -90,9 +90,3 @@ instance (ArrowApply c, Profunctor c) => ArrowApply (EnvT var addr val c) where
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 PreOrd (c ((Map var addr val),x) y) => PreOrd (EnvT var addr val c x y)
deriving instance Complete (c ((Map var addr val),x) y) => Complete (EnvT var addr val c x y)
deriving instance CoComplete (c ((Map var addr val),x) y) => CoComplete (EnvT var addr val c x y)
deriving instance LowerBounded (c ((Map var addr val),x) y) => LowerBounded (EnvT var addr val c x y)
deriving instance UpperBounded (c ((Map var addr val),x) y) => UpperBounded (EnvT var addr val c x y)
......@@ -27,7 +27,6 @@ import Control.Category
import Data.Profunctor
import Data.Abstract.FreeCompletion
import Data.Identifiable
import Data.Order hiding (lub)
-- | Allows to describe computations over non-completely ordered types.
-- E.g. allows to join a computation of type 'c x [y]'.
......@@ -43,12 +42,6 @@ type instance Fix x y (CompletionT c) = CompletionT (Fix (Dom (CompletionT) x y)
deriving instance (ArrowChoice c, ArrowFix (Dom (CompletionT) x y) (Cod (CompletionT) x y) c) => ArrowFix x y (CompletionT c)
deriving instance (Identifiable (Cod CompletionT x y), ArrowChoice c, ArrowDeduplicate (Dom CompletionT x y) (Cod CompletionT x y) c) => ArrowDeduplicate x y (CompletionT c)
deriving instance PreOrd (c x (Cod CompletionT x y)) => PreOrd (CompletionT c x y)
deriving instance LowerBounded (c (Dom CompletionT x y) (Cod CompletionT x y)) => LowerBounded (CompletionT c x y)
deriving instance Complete (c (Dom CompletionT x y) (Cod CompletionT x y)) => Complete (CompletionT c x y)
deriving instance CoComplete (c (Dom CompletionT x y) (Cod CompletionT x y)) => CoComplete (CompletionT c x y)
deriving instance UpperBounded (c (Dom CompletionT x y) (Cod CompletionT x y)) => UpperBounded (CompletionT c x y)
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (CompletionT c) where
joinWith lub f g = lift $ joinWith join (unlift f) (unlift g)
where join (Lower x) (Lower y) = Lower (lub x y)
......
......@@ -25,7 +25,6 @@ import Control.Arrow.Transformer.Reader
import Control.Category
import Data.Label
import Data.Order
import Data.CallString
import Data.Profunctor
......@@ -64,9 +63,3 @@ instance (ArrowApply c, Profunctor c) => ArrowApply (ContourT lab c) where
instance ArrowReader r c => ArrowReader r (ContourT lab c) where
ask = lift' ask
local (ContourT (ReaderT f)) = ContourT $ ReaderT $ ((\(c,(r,x)) -> (r,(c,x))) ^>> local f)
deriving instance PreOrd (c (CallString lab,x) y) => PreOrd (ContourT lab c x y)
deriving instance LowerBounded (c (CallString lab,x) y) => LowerBounded (ContourT lab c x y)
deriving instance Complete (c (CallString lab,x) y) => Complete (ContourT lab c x y)
deriving instance CoComplete (c (CallString lab,x) y) => CoComplete (ContourT lab c x y)
deriving instance UpperBounded (c (CallString lab,x) y) => UpperBounded (ContourT lab c x y)
......@@ -43,13 +43,13 @@ runEnvT' :: (Arrow c, Profunctor c, Identifiable var) => EnvT var val c x y -> c
runEnvT' f = first M.fromList ^>> runEnvT f
instance (Identifiable var, UpperBounded val, ArrowChoice c, Profunctor c) => ArrowEnv var val (Map var val) (EnvT var val c) where
type Join (EnvT var val c) x y = (Complete (c (Map var val,x) y))
type Join (EnvT var val c) x y = (ArrowJoin c, Complete y)
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- ask -< ()
case M.lookup' var env of
Just val -> f -< (val,x)
JustNothing val -> joined f g -< ((val,x),x)
Nothing -> g -< x
Just val -> f -< (val,x)
JustNothing val -> (f -< (val,x)) <> (g -< x)
Nothing -> g -< x
getEnv = EnvT ask
extendEnv = arr $ \(x,y,env) -> M.insert x y env
localEnv (EnvT f) = EnvT (local f)
......@@ -63,9 +63,3 @@ instance ArrowReader r c => ArrowReader r (EnvT var val c) where
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 PreOrd (c (Map var val,x) y) => PreOrd (EnvT var val c x y)
deriving instance Complete (c (Map var val,x) y) => Complete (EnvT var val c x y)
deriving instance CoComplete (c (Map var val,x) y) => CoComplete (EnvT var val c x y)
deriving instance LowerBounded (c (Map var val,x) y) => LowerBounded (EnvT var val c x y)
deriving instance UpperBounded (c (Map var val,x) y) => UpperBounded (EnvT var val c x y)
......@@ -46,12 +46,6 @@ type instance Fix x y (ErrorT e c) = ErrorT e (Fix (Dom (ErrorT e) x y) (Cod (Er
deriving instance (ArrowChoice c, ArrowFix (Dom (ErrorT e) x y) (Cod (ErrorT e) x y) c) => ArrowFix x y (ErrorT e c)
deriving instance (Identifiable (Cod (ErrorT e) x y), ArrowChoice c, ArrowDeduplicate (Dom (ErrorT e) x y) (Cod (ErrorT e) x y) c) => ArrowDeduplicate x y (ErrorT e c)
deriving instance PreOrd (c x (Cod (ErrorT e) x y)) => PreOrd (ErrorT e c x y)
deriving instance LowerBounded (c (Dom (ErrorT e) x y) (Cod (ErrorT e) x y)) => LowerBounded (ErrorT e c x y)
deriving instance Complete (c (Dom (ErrorT e) x y) (Cod (ErrorT e) x y)) => Complete (ErrorT e c x y)
deriving instance CoComplete (c (Dom (ErrorT e) x y) (Cod (ErrorT e) x y)) => CoComplete (ErrorT e c x y)
deriving instance UpperBounded (c (Dom (ErrorT e) x y) (Cod (ErrorT e) x y)) => UpperBounded (ErrorT e c x y)
instance (Complete e, ArrowJoin c, ArrowChoice c) => ArrowJoin (ErrorT e c) where
joinWith lub' f g = lift $ joinWith (toJoin2 widening () lub') (unlift f) (unlift g)
......@@ -54,12 +54,6 @@ type instance Fix x y (ExceptT e c) = ExceptT e (Fix (Dom (ExceptT e) x y) (Cod
deriving 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)
deriving instance (Complete e, ArrowJoin c, Identifiable (Cod (ExceptT e) x y), ArrowChoice c, ArrowDeduplicate (Dom (ExceptT e) x y) (Cod (ExceptT e) x y) c) => ArrowDeduplicate x y (ExceptT e c)
deriving instance PreOrd (c x (Cod (ExceptT e) x y)) => PreOrd (ExceptT e c x y)
deriving instance LowerBounded (c (Dom (ExceptT e) x y) (Cod (ExceptT e) x y)) => LowerBounded (ExceptT e c x y)
deriving instance Complete (c (Dom (ExceptT e) x y) (Cod (ExceptT e) x y)) => Complete (ExceptT e c x y)
deriving instance CoComplete (c (Dom (ExceptT e) x y) (Cod (ExceptT e) x y)) => CoComplete (ExceptT e c x y)
deriving instance UpperBounded (c (Dom (ExceptT e) x y) (Cod (ExceptT e) x y)) => UpperBounded (ExceptT e c x y)
instance (Complete e, ArrowJoin c, ArrowChoice c) => ArrowJoin (ExceptT e c) where
joinWith lub' f g = lift $ joinWith (toJoin2 widening () lub') (unlift f) (unlift g)
......@@ -25,7 +25,6 @@ import Control.Arrow.Except as Exc
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Kleisli
import Data.Order
import Data.Identifiable
import Data.Profunctor
import Data.Abstract.Failure
......@@ -47,11 +46,5 @@ type instance Fix x y (FailureT e c) = FailureT e (Fix (Dom (FailureT e) x y) (C
deriving instance (ArrowChoice c, ArrowFix (Dom (FailureT e) x y) (Cod (FailureT e) x y) c) => ArrowFix x y (FailureT e c)
deriving instance (Identifiable (Cod (FailureT e) x y), ArrowChoice c, ArrowDeduplicate (Dom (FailureT e) x y) (Cod (FailureT e) x y) c) => ArrowDeduplicate x y (FailureT e c)
deriving instance PreOrd (c x (Cod (FailureT e) x y)) => PreOrd (FailureT e c x y)
deriving instance LowerBounded (c (Dom (FailureT e) x y) (Cod (FailureT e) x y)) => LowerBounded (FailureT e c x y)
deriving instance Complete (c (Dom (FailureT e) x y) (Cod (FailureT e) x y)) => Complete (FailureT e c x y)
deriving instance CoComplete (c (Dom (FailureT e) x y) (Cod (FailureT e) x y)) => CoComplete (FailureT e c x y)
deriving instance UpperBounded (c (Dom (FailureT e) x y) (Cod (FailureT e) x y)) => UpperBounded (FailureT e c x y)
instance (ArrowJoin c, ArrowChoice c) => ArrowJoin (FailureT e c) where
joinWith lub' f g = lift $ joinWith (toJoin widening lub') (unlift f) (unlift g)
......@@ -40,9 +40,6 @@ instance (Identifiable a, LowerBounded b, Profunctor c,ArrowChoice c,ArrowApply
fix f = iterationStrategy (f (fix f))
instance (Profunctor c,ArrowApply c) => ArrowApply (FixT a b c) where app = FixT (lmap (first coerce) app)
deriving instance PreOrd (c x y) => PreOrd (FixT a b c x y)
deriving instance Complete (c x y) => Complete (FixT a b c x y)
deriving instance LowerBounded (c x y) => LowerBounded (FixT a b c x y)
instance ArrowLift (FixT a b) where
lift' = FixT . lift'
......
......@@ -25,7 +25,6 @@ import Control.Arrow.Transformer.Kleisli
import Control.Category
import qualified Data.Abstract.Powerset as A
import Data.Order
import Data.Identifiable
import Data.Profunctor
......@@ -44,11 +43,5 @@ instance (ArrowChoice c, Profunctor c, ArrowApply c) => ArrowApply (PowT c) wher
type instance Fix x y (PowT c) = PowT (Fix (Dom PowT x y) (Cod PowT x y) c)
deriving instance (ArrowChoice c, ArrowFix x (A.Pow y) c) => ArrowFix x y (PowT c)
deriving instance PreOrd (c x (A.Pow y)) => PreOrd (PowT c x y)
deriving instance LowerBounded (c x (A.Pow y)) => LowerBounded (PowT c x y)
deriving instance Complete (c x (A.Pow y)) => Complete (PowT c x y)
deriving instance CoComplete (c x (A.Pow y)) => CoComplete (PowT c x y)
deriving instance UpperBounded (c x (A.Pow y)) => UpperBounded (PowT c x y)
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (PowT c) where
joinWith _ f g = lift $ joinWith A.union (unlift f) (unlift g)
......@@ -21,7 +21,6 @@ import Prelude hiding ((.),read,id)
import Control.Category
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Conditional
import Control.Arrow.Except
import Control.Arrow.Fix
import Control.Arrow.Trans
......@@ -34,7 +33,6 @@ import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Reader
import Data.Identifiable
import Data.Order
import Data.Label
import Data.Profunctor
import Data.Abstract.DiscretePowerset(Pow)
......@@ -43,7 +41,7 @@ import qualified Data.Abstract.DiscretePowerset as P
newtype ReachingDefsT lab c x y = ReachingDefsT (ReaderT (Maybe lab) c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowLift,
ArrowFail e,ArrowExcept e,ArrowState s,ArrowEnv var val env,
ArrowCond val,ArrowJoin)
ArrowJoin)
reachingDefsT :: (Arrow c,Profunctor c) => c (Maybe lab,x) y -> ReachingDefsT lab c x y
reachingDefsT = lift
......@@ -75,9 +73,3 @@ instance ArrowReader r c => ArrowReader r (ReachingDefsT lab c) where
instance ArrowAlloc x y c => ArrowAlloc x y (ReachingDefsT lab c) where
alloc = lift' alloc
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)
......@@ -47,14 +47,14 @@ evalStoreT f = runStoreT f >>> pi2
execStoreT :: Arrow c => StoreT var val c x y -> c (Map var val, x) (Map var val)
execStoreT f = runStoreT f >>> pi1
instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (StoreT var val c) where
type Join (StoreT var val c) ((val,x),x) y = Complete (c (Map var val, ((val, x), x)) (Map var val, y))
instance (Identifiable var, ArrowChoice c, Profunctor c, Complete val) => ArrowStore var val (StoreT var val c) where
type Join (StoreT var val c) ((val,x),x) y = (ArrowJoin c, Complete y)
read (StoreT f) (StoreT g) = StoreT $ proc (var,x) -> do
s <- get -< ()
case M.lookup var s of
Just val -> f -< (val,x)
JustNothing val -> joined f g -< ((val,x),x)
Nothing -> g -< x
Just val -> f -< (val,x)
JustNothing val -> (f -< (val,x)) <> (g -< x)
Nothing -> g -< x
write = StoreT $ modify $ arr $ \((var,val),st) -> ((),M.insert var val st)
instance ArrowState s c => ArrowState s (StoreT var val c) where
......@@ -66,9 +66,3 @@ instance (ArrowApply c, Profunctor c) => ArrowApply (StoreT var val c) where app
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)
deriving instance CoComplete (c (Map var val,x) (Map var val,y)) => CoComplete (StoreT var val c x y)
deriving instance UpperBounded (c (Map var val,x) (Map var val,y)) => UpperBounded (StoreT var val c x y)
deriving instance LowerBounded (c (Map var val,x) (Map var val,y)) => LowerBounded (StoreT var val c x y)
......@@ -21,7 +21,6 @@ import Control.Arrow.Transformer.Kleisli
import Control.Category
import Data.Identifiable
import Data.Order
import Data.Profunctor
import Data.Abstract.Terminating
import Data.Abstract.Widening (toJoin)
......@@ -41,11 +40,5 @@ type instance Fix x y (TerminatingT c) = TerminatingT (Fix (Dom TerminatingT x y
deriving instance (ArrowChoice c, ArrowFix (Dom TerminatingT x y) (Cod TerminatingT x y) c) => ArrowFix x y (TerminatingT c)
deriving instance (Identifiable (Cod TerminatingT x y), ArrowChoice c, ArrowDeduplicate (Dom TerminatingT x y) (Cod TerminatingT x y) c) => ArrowDeduplicate x y (TerminatingT c)
deriving instance PreOrd (c x (Terminating y)) => PreOrd (TerminatingT c x y)
deriving instance LowerBounded (c x (Terminating y)) => LowerBounded (TerminatingT c x y)
deriving instance Complete (c x (Terminating y)) => Complete (TerminatingT c x y)
deriving instance CoComplete (c x (Terminating y)) => CoComplete (TerminatingT c x y)
deriving instance UpperBounded (c x (Terminating y)) => UpperBounded (TerminatingT c x y)
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (TerminatingT c) where
joinWith lub' f g = lift $ joinWith (toJoin widening lub') (unlift f) (unlift g)
......@@ -10,7 +10,6 @@ module Control.Arrow.Transformer.Concrete.Random where
import Control.Category
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Conditional
import Control.Arrow.Environment
import Control.Arrow.Except
import Control.Arrow.Trans
......@@ -31,7 +30,7 @@ import qualified System.Random as R
newtype RandomT c x y = RandomT (StateT StdGen c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowLift,
ArrowReader r, ArrowFail e, ArrowExcept e,
ArrowEnv var val env, ArrowStore var val, ArrowCond val)
ArrowEnv var val env, ArrowStore var val)
runRandomT :: RandomT c x y -> c (StdGen,x) (StdGen,y)
runRandomT (RandomT (StateT f)) = f
......
......@@ -28,7 +28,6 @@ import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Static
import Data.Order
import Data.Profunctor
-- | Passes along constant data.
......@@ -36,8 +35,7 @@ newtype ConstT r c x y = ConstT (StaticT ((->) r) c x y)
deriving (Category,Profunctor,Arrow,ArrowChoice,ArrowJoin,ArrowLift,
ArrowState s,ArrowReader r',ArrowWriter w,
ArrowEnv var val env, ArrowStore var val,
ArrowFail e, ArrowExcept e,
PreOrd, Complete, CoComplete, UpperBounded, LowerBounded)
ArrowFail e, ArrowExcept e)
runConstT :: r -> ConstT r c x y -> c x y
runConstT r (ConstT (StaticT f)) = f r
......
......@@ -17,7 +17,6 @@ import Control.Arrow.Trans
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Writer
-- import Control.Arrow.Conditional
import Data.Profunctor
newtype ContT c x y = ContT { runContT :: forall r. c y r -> c x r }
......@@ -71,7 +70,3 @@ instance (ArrowApply c, ArrowWriter w c) => ArrowWriter w (ContT c) where
instance (ArrowApply c, ArrowFail e c) => ArrowFail e (ContT c) where
fail = lift' fail
-- instance (ArrowApply c, ArrowCond v c) => ArrowCond v (ContT c) where
-- type Join (ContT c) x y = Cond.Join c (Dom1 ContT x y) (Cod1 ContT x y)
-- if_ (ContT f) (ContT g) = ContT $ \k -> if_ (f k) (g k)
......@@ -25,7 +25,6 @@ import Control.Arrow.Trans
import Control.Category
import Data.Identifiable
import Data.Order
import Data.Monoidal
import Data.Profunctor (Profunctor(..))
import Data.Coerce
......@@ -106,9 +105,3 @@ instance (Identifiable (f y), ArrowMonad f c, Arrow c, ArrowDeduplicate (Dom (Kl
instance (ArrowMonad f c, ArrowConst r c) => ArrowConst r (KleisliT f c) where
askConst f = lift (askConst (unlift . f))
deriving instance PreOrd (c x (f y)) => PreOrd (KleisliT f c x y)
deriving instance LowerBounded (c x (f y)) => LowerBounded (KleisliT f c x y)
deriving instance Complete (c x (f y)) => Complete (KleisliT f c x y)
deriving instance CoComplete (c x (f y)) => CoComplete (KleisliT f c x y)
deriving instance UpperBounded (c x (f y)) => UpperBounded (KleisliT f c x y)
......@@ -13,7 +13,6 @@ import Prelude hiding (id,(.),lookup,read,fail)
import Control.Arrow
import Control.Arrow.Const
import Control.Arrow.Conditional as Cond
import Control.Arrow.Environment as Env
import Control.Arrow.Fail
import Control.Arrow.Fix
......@@ -29,7 +28,6 @@ import Control.Arrow.Abstract.Join
import Control.Category
import Data.Profunctor
import Data.Order hiding (lub)
import Data.Monoidal
import Data.Coerce
......@@ -118,14 +116,3 @@ instance ArrowJoin c => ArrowJoin (ReaderT r c) where
instance ArrowConst x c => ArrowConst x (ReaderT r c) where
askConst f = lift (askConst (unlift . f))
instance ArrowCond v c => ArrowCond v (ReaderT r c) where
type instance Join (ReaderT r c) (x,y) z = Cond.Join c (Dom (ReaderT r) x z,Dom (ReaderT r) y z) (Cod (ReaderT r) (x,y) z)
if_ f g = lift $ lmap (\(r,(v,(x,y))) -> (v,((r,x),(r,y))))
$ if_ (unlift f) (unlift g)
deriving instance PreOrd (c (r,x) y) => PreOrd (ReaderT r c x y)
deriving instance LowerBounded (c (r,x) y) => LowerBounded (ReaderT r c x y)
deriving instance Complete (c (r,x) y) => Complete (ReaderT r c x y)
deriving instance CoComplete (c (r,x) y) => CoComplete (ReaderT r c x y)
deriving instance UpperBounded (c (r,x) y) => UpperBounded (ReaderT r c x y)
......@@ -12,7 +12,6 @@ import Prelude hiding (id,(.),lookup,read,fail)
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Const
import Control.Arrow.Conditional as Cond
import Control.Arrow.Deduplicate
import Control.Arrow.Environment as Env
import Control.Arrow.Fail
......@@ -134,15 +133,5 @@ instance ArrowConst x c => ArrowConst x (StateT s c) where
instance ArrowAlloc x y c => ArrowAlloc x y (StateT s c) where
alloc = lift' alloc
instance (ArrowCond v c) => ArrowCond v (StateT s c) where
type instance Join (StateT s c) (x,y) z = Cond.Join c ((s,x),(s,y)) (s,z)
if_ f g = lift $ lmap (\(s,(v,(x,y))) -> (v,((s,x),(s,y)))) (if_ (unlift f) (unlift g))
instance ArrowRand v c => ArrowRand v (StateT s c) where
random = lift' random
deriving instance PreOrd (c (s,x) (s,y)) => PreOrd (StateT s c x y)
deriving instance LowerBounded (c (s,x) (s,y)) => LowerBounded (StateT s c x y)
deriving instance Complete (c (s,x) (s,y)) => Complete (StateT s c x y)
deriving instance CoComplete (c (s,x) (s,y)) => CoComplete (StateT s c x y)
deriving instance UpperBounded (c (s,x) (s,y)) => UpperBounded (StateT s c x y)
......@@ -26,11 +26,9 @@ import Control.Arrow.Writer
import Control.Arrow.Abstract.Join
import Data.Profunctor
import Data.Order hiding (lub)
-- Due to https://hackage.haskell.org/package/arrows/docs/Control-Arrow-Transformer-StaticT.html
newtype StaticT f c x y = StaticT { runStaticT :: f (c x y) }
deriving (PreOrd,Complete,CoComplete,UpperBounded,LowerBounded)
instance (Applicative f, Profunctor c) => Profunctor (StaticT f c) where
dimap f g (StaticT h) = StaticT $ dimap f g <$> h
......
......@@ -140,6 +140,7 @@ newtype ChaoticT s a b c x y = ChaoticT (WriterT (Component a) (StateT (HashMap
instance (Identifiable a,Profunctor c,ArrowApply c) => ArrowApply (ChaoticT s a b c) where app = ChaoticT (lmap (first coerce) app)
instance (Identifiable a,Profunctor c,Arrow c) => ArrowJoin (ChaoticT s a b c) where
joinWith _lub (ChaoticT f) (ChaoticT g) = ChaoticT $ rmap (uncurry _lub) (f &&& g)
-- deriving instance PreOrd (ChaoticT s a b c)
instance (IsEmpty (s a)) => ArrowRun (ChaoticT s a b) where
run (ChaoticT f) = dimap (\a -> (empty,(M.empty,a))) (snd . snd) (runReaderT (runStateT (runWriterT f)))
......
......@@ -16,7 +16,6 @@ import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Environment
import Control.Arrow.Fix
import Control.Arrow.Conditional
import Control.Arrow.Transformer.Concrete.Environment
import Control.Arrow.Transformer.Concrete.Failure
import Control.Monad.State hiding (fail)
......@@ -55,6 +54,7 @@ deriving instance ArrowEnv var Val env c => ArrowEnv var Val env (ConcreteT c)
-- | Concrete instance of the interface for value operations.
instance (ArrowChoice c, ArrowFail String c) => IsVal Val (ConcreteT c) where
type Join (ConcreteT c) x y = ()
succ = proc x -> case x of
NumVal n -> returnA -< NumVal (n + 1)
_ -> fail -< "Expected a number as argument for 'succ'"
......@@ -63,6 +63,11 @@ instance (ArrowChoice c, ArrowFail String c) => IsVal Val (ConcreteT c) where
_ -> fail -< "Expected a number as argument for 'pred'"
zero = arr $ const (NumVal 0)
if_ f g = proc (v1, (x, y)) -> case v1 of
NumVal 0 -> f -< x
NumVal _ -> g -< y
_ -> fail -< "Expected a number as condition for 'ifZero'"
-- | Concrete instance of the interface for closure operations.
instance (ArrowChoice c, ArrowFail String c) => IsClosure Val (HashMap Text Val) (ConcreteT c) where
closure = arr $ \(e, env) -> ClosureVal $ Closure e env
......@@ -70,13 +75,6 @@ instance (ArrowChoice c, ArrowFail String c) => IsClosure Val (HashMap Text Val)
ClosureVal (Closure e env) -> f -< ((e,env),arg)
NumVal _ -> fail -< "Expected a closure"
instance (ArrowChoice c, ArrowFail String c) => ArrowCond Val (ConcreteT c) where
type Join (ConcreteT c) x y = ()
if_ f g = proc (v1, (x, y)) -> case v1 of
NumVal 0 -> f -< x
NumVal _ -> g -< y
_ -> fail -< "Expected a number as condition for 'ifZero'"
instance Hashable Closure
instance Hashable Val
instance Show Closure where
......
......@@ -2,24 +2,25 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
module GenericInterpreter where
import Prelude hiding (succ, pred, fail)
import Syntax (Expr(..))
import Prelude hiding (succ, pred, fail)
import Syntax (Expr(..))
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Fail
import Control.Arrow.Environment as Env
import Control.Arrow.Conditional as Cond
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Fail
import Control.Arrow.Environment(ArrowEnv,lookup',getEnv,extendEnv,localEnv)
import qualified Control.Arrow.Environment as Env
import Data.Text (Text)
import Data.Text (Text)
import GHC.Exts(IsString(..))
import GHC.Exts (IsString(..),Constraint)
-- | Shared interpreter for PCF.
eval :: (ArrowChoice c, ArrowFix Expr v c, ArrowEnv Text v env c, ArrowFail e c, IsString e,
ArrowCond v c, IsVal v c, IsClosure v env c, Env.Join c ((v,Text),Text) v, Cond.Join c (Expr,Expr) v)
IsVal v c, IsClosure v env c, Env.Join c ((v,Text),Text) v, Join c (Expr,Expr) v)
=> c Expr v
eval = fix $ \ev -> proc e0 -> case e0 of
Var x _ -> lookup' -< x
......@@ -59,6 +60,8 @@ eval = fix $ \ev -> proc e0 -> case e0 of
-- | Interface for numeric operations
class Arrow c => IsVal v c | c -> v where
type family Join (c :: * -> * -> *) x y :: Constraint
-- | increments the given number value.
succ :: c v v
......@@ -68,6 +71,9 @@ class Arrow c => IsVal v c | c -> v where
-- | creates the numeric value zero.
zero :: c () v
if_ :: Join c (x,y) z => c x z -> c y z -> c (v, (x, y)) z
-- | Interface for closures
class Arrow c => IsClosure v env c | c -> env, c -> v where
-- | creates a closure from an expression and an environment.
......
......@@ -27,7 +27,6 @@ import Control.Arrow.Alloc
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Trans
import Control.Arrow.Conditional as Cond
import Control.Arrow.Environment
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Abstract.Contour
......@@ -94,10 +93,10 @@ evalInterval k env0 e =
(ContourT Label
(ErrorT (Pow String)
(TerminatingT
(FixT _ _ () () (->))))))) Expr Val))))))
(FixT () () _)))))) Expr Val))))))
(env0,generate e)
where
iterationStrategy :: IterationStrategy _ _ (Env,Expr) _
iterationStrategy :: IterationStrategy _ (Env,Expr) _
iterationStrategy = S.filter apply
$ S.chaotic stackWiden (T.widening (E.widening W.finite widenVal))
......@@ -122,18 +121,20 @@ instance ArrowTrans IntervalT where
unlift = runIntervalT
instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowJoin c) => IsVal Val (IntervalT c) where
type Join (IntervalT c) x y = Complete y
succ = proc x -> case x of
Top -> (returnA -< NumVal top) <> (fail -< "Expected a number as argument for 'succ'")
NumVal n -> returnA -< NumVal $ n + 1 -- uses the `Num` instance of intervals
ClosureVal _ -> fail -< "Expected a number as argument for 'succ'"
pred = proc x -> case x of
Top -> (returnA -< NumVal top) <> (fail -< "Expected a number as argument for 'pred'")
NumVal n -> returnA -< NumVal $ n - 1
ClosureVal _ -> fail -< "Expected a number as argument for 'pred'"
zero = proc _ -> returnA -< (NumVal 0)
instance (IsString e, ArrowChoice c, ArrowJoin c, ArrowFail e c) => ArrowCond Val (IntervalT c) where
type Join (IntervalT c) x y = Complete y
if_ f g = proc v -> case v of
(Top, (x,y)) -> (f -< x) <> (g -< y) <> (fail -< "Expected a number as condition for 'ifZero'")
(NumVal (I.Interval i1 i2), (x, y))
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment