Commit 776b719e authored by Sven Keidel's avatar Sven Keidel

fix PCF and While language

parent 59c73e60
Pipeline #52681 failed with stages
in 86 minutes and 49 seconds
......@@ -38,16 +38,17 @@ import Text.Printf
class ArrowFix c where
-- | Computes the fixpoint of an arrow computation.
type Fix c
fix :: FixpointAlgorithm (Fix c) -> (c -> c) -> c
fix :: (?fixpointAlgorithm :: FixpointAlgorithm (Fix c)) => (c -> c) -> c
default fix :: (c ~ c' x y, ArrowTrans c', Underlying c' x y ~ d, Fix (c' x y) ~ Fix d, ArrowFix d)
=> FixpointAlgorithm (Fix c) -> (c -> c) -> c
fix algo f = lift (fix algo (unlift . f . lift))
default fix :: (c ~ c' x y, ArrowTrans c', Underlying c' x y ~ d, Fix (c' x y) ~ Fix d, ArrowFix d,
?fixpointAlgorithm :: FixpointAlgorithm (Fix c))
=> (c -> c) -> c
fix f = lift (fix (unlift . f . lift))
{-# INLINE fix #-}
instance ArrowFix (x -> y) where
type Fix (x -> y) = (x -> y)
fix algo = algo
fix = ?fixpointAlgorithm
{-# INLINE fix #-}
type FixpointAlgorithm c = (c -> c) -> c
......
......@@ -27,17 +27,17 @@ class (Arrow c, Profunctor c) => ArrowContext ctx c | c -> ctx where
class (Arrow c, Profunctor c) => ArrowJoinContext a c | c -> a where
type Widening c
joinByContext :: (?widening :: Widening c) => c a a
joinByContext :: (?contextWidening :: Widening c) => c a a
default joinByContext :: (c ~ t c', ArrowLift t, ArrowJoinContext a c', ?widening :: Widening c') => c a a
default joinByContext :: (c ~ t c', ArrowLift t, ArrowJoinContext a c', ?contextWidening :: Widening c') => c a a
joinByContext = lift' joinByContext
{-# INLINE joinByContext #-}
callsiteSensitive :: forall a lab b c. (?widening :: Widening c, ArrowContext (CallString lab) c, ArrowJoinContext a c) => Int -> (a -> lab) -> FixpointCombinator c a b
callsiteSensitive :: forall a lab b c. (?contextWidening :: Widening c, ArrowContext (CallString lab) c, ArrowJoinContext a c) => Int -> (a -> lab) -> FixpointCombinator c a b
callsiteSensitive k getLabel = callsiteSensitive' k (Just . getLabel)
{-# INLINE callsiteSensitive #-}
callsiteSensitive' :: forall a lab b c. (?widening :: Widening c, ArrowContext (CallString lab) c, ArrowJoinContext a c) => Int -> (a -> Maybe lab) -> FixpointCombinator c a b
callsiteSensitive' :: forall a lab b c. (?contextWidening :: Widening c, ArrowContext (CallString lab) c, ArrowJoinContext a c) => Int -> (a -> Maybe lab) -> FixpointCombinator c a b
callsiteSensitive' k getLabel f = recordCallsite k getLabel $ f . joinByContext
{-# INLINE callsiteSensitive' #-}
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DefaultSignatures #-}
module Control.Arrow.Random where
import Control.Arrow
import Control.Arrow.Trans
import Data.Profunctor
class (Arrow c, Profunctor c) => ArrowRand v c where
random :: c () v
default random :: (c ~ t c', ArrowLift t, ArrowRand v c') => c () v
random = lift' random
......@@ -53,5 +53,5 @@ deriving instance (ArrowChoice c, ArrowComplete (FreeCompletion y) c) => ArrowCo
deriving instance (ArrowChoice c, ArrowLowerBounded y c) => ArrowLowerBounded y (CompletionT c)
instance (ArrowChoice c, ArrowJoin c) => ArrowJoin (CompletionT c) where
joinSecond lub f g = lift $ joinSecond (toJoin widening lub) (return . f) (unlift g)
joinSecond lub f g = lift $ joinSecond (toJoin1 widening lub) (return . f) (unlift g)
{-# INLINE joinSecond #-}
......@@ -53,5 +53,5 @@ instance (ArrowChoice c, ArrowFix (Underlying (FailureT e c) x y)) => ArrowFix (
type Fix (FailureT e c x y) = Fix (Underlying (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)
joinSecond lub f g = lift $ joinSecond (toJoin1 widening lub) (Success . f) (unlift g)
{-# INLINE joinSecond #-}
......@@ -109,6 +109,9 @@ instance ArrowLift (EnvT var addr val) where
instance (Complete y, Arrow c, Profunctor c) => ArrowComplete y (EnvT var addr val c) where
EnvT f <> EnvT g = EnvT (rmap (uncurry ()) (f &&& g))
{-# INLINE (<⊔>) #-}
instance (Profunctor c, Arrow c, ArrowFix (Underlying (EnvT var addr val c) x y)) => ArrowFix (EnvT var addr val c x y) where
type Fix (EnvT var addr val c x y) = Fix (Underlying (EnvT var addr val c) x y)
instance (Profunctor c, Arrow c, ArrowFix (ReaderT (HashMap var addr) (StateT (HashMap addr val) c) x y)) => ArrowFix (EnvT var addr val c x y) where
type Fix (EnvT var addr val c x y) = Fix (ReaderT (HashMap var addr) (StateT (HashMap addr val) c) x y)
fix f = EnvT (fix (coerce f))
{-# INLINE fix #-}
......@@ -22,16 +22,16 @@ import Control.Arrow.Fix.ControlFlow
import Control.Arrow.Fix.Context
import Control.Arrow.Fix.Metrics
import Control.Arrow.Fix.Stack
import Control.Arrow.Order(ArrowComplete,ArrowJoin)
import Control.Arrow.Order(ArrowComplete(..),ArrowJoin(..))
import Control.Arrow.Trans
import Data.Profunctor
import Data.Profunctor.Unsafe((.#))
import Data.Coerce
import Data.Order hiding (lub)
newtype FixT c x y = FixT (c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,
ArrowComplete z,ArrowJoin,
ArrowContext ctx, ArrowJoinContext a, ArrowControlFlow a,
ArrowCache a b, ArrowParallelCache a b, ArrowIterateCache a b,
ArrowStack a,ArrowStackElements a,ArrowStackDepth,
......@@ -50,7 +50,7 @@ instance ArrowTrans (FixT c) where
instance ArrowFix (FixT c a b) where
type Fix (FixT c a b) = FixT c a b
fix algo = algo
fix = ?fixpointAlgorithm
{-# INLINE fix #-}
{-# SCC fix #-}
......@@ -61,3 +61,10 @@ instance (Profunctor c,ArrowApply c) => ArrowApply (FixT c) where
instance ArrowLift FixT where
lift' = FixT
{-# INLINE lift' #-}
instance (Complete y, Profunctor c, Arrow c) => ArrowComplete y (FixT c) where
FixT f <> FixT g = FixT (rmap (uncurry ()) (f &&& g))
{-# INLINE (<⊔>) #-}
instance (Profunctor c, Arrow c) => ArrowJoin (FixT c) where
joinSecond lub f (FixT g) = FixT (dimap (\x -> (x, x)) (\(x,y) -> (lub (f x) y)) (second g))
......@@ -441,7 +441,7 @@ instance (Identifiable ctx, PreOrd a, Profunctor c, ArrowChoice c, ArrowContext
| otherwise ->
-- If there exists the actual input is not smaller than the cached
-- input, widen the input.
let (_,a'') = ?widening a' a
let (_,a'') = ?contextWidening a' a
in (CtxCache (M.insert ctx a'' cache),a'')
Nothing -> (CtxCache (M.insert ctx a cache),a)
{-# INLINE joinByContext #-}
......
......@@ -45,7 +45,7 @@ instance (ArrowChoice c, Profunctor c, ArrowApply c) => ArrowApply (PowT c) wher
instance (Identifiable y, Profunctor c, ArrowFix (Underlying (PowT c) x y)) => ArrowFix (PowT c x y) where
type Fix (PowT c x y) = Fix (Underlying (PowT c) x y)
fix algo f = lift $ rmap A.dedup (fix algo (unlift1 f))
fix f = lift $ rmap A.dedup (fix (unlift1 f))
{-# INLINE fix #-}
instance (ArrowChoice c, Profunctor c) => ArrowLowerBounded y (PowT c) where
......
......@@ -29,7 +29,7 @@ import Control.Arrow.Fix.Context
import Data.Abstract.Terminating
import Data.Abstract.Widening
import Data.Profunctor
import Data.Profunctor.Unsafe
import Data.Coerce
-- | Arrow that propagates non-terminating computations.
......@@ -42,9 +42,9 @@ runTerminatingT :: TerminatingT c x y -> c x (Terminating y)
runTerminatingT = coerce
{-# INLINE runTerminatingT #-}
-- instance (ArrowChoice c, Profunctor c, ArrowApply c) => ArrowApply (TerminatingT c) where
-- app = lift (app .# first coerce)
-- {-# INLINE app #-}
instance (ArrowChoice c, Profunctor c, ArrowApply c) => ArrowApply (TerminatingT c) where
app = lift (app .# first coerce)
{-# INLINE app #-}
instance (ArrowFix (Underlying (TerminatingT c) x y), Profunctor c) => ArrowFix (TerminatingT c x y) where
type Fix (TerminatingT c x y) = Fix (Underlying (TerminatingT c) x y)
......@@ -56,5 +56,5 @@ instance (ArrowChoice c, Profunctor c) => ArrowLowerBounded y (TerminatingT c) w
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)
joinSecond lub f g = lift $ joinSecond (toJoin1 widening lub) (return . f) (unlift g)
{-# INLINE joinSecond #-}
......@@ -83,7 +83,7 @@ instance (Arrow c, Profunctor c) => ArrowConst r (ConstT r c) where
instance (Arrow c, Profunctor c, ArrowFix (c x y)) => ArrowFix (ConstT r c x y) where
type Fix (ConstT r c x y) = Fix (c x y)
fix algo f = lift $ \r -> fix algo (runConstT r . f . lift')
fix f = lift $ \r -> fix (runConstT r . f . lift')
{-# INLINE fix #-}
instance (ArrowApply c, Profunctor c) => ArrowApply (ConstT r c) where
......
......@@ -96,7 +96,7 @@ instance ArrowApply c => ArrowApply (ContT r c) where
instance ArrowFix (c x r) => ArrowFix (ContT r c x y) where
type Fix (ContT r c x y) = Fix (c x r)
fix algo f = lift $ \k -> fix algo $ \g -> unlift1 f (const g) k
fix f = lift $ \k -> fix $ \g -> unlift1 f (const g) k
{-# INLINE fix #-}
-- instance (ArrowApply c, ArrowJoin c, ArrowComplete r c) => ArrowJoin (ContT r c) where
......
......@@ -69,7 +69,7 @@ instance (ArrowStore var (val,f Label) c, IsEmpty (f Label), IsSingleton (f Labe
instance (HasLabel x, Arrow c, ArrowFix (c x y), Profunctor c) => ArrowFix (ReachingDefsT f c x y) where
type Fix (ReachingDefsT f c x y) = Fix (c x y)
fix algo f = ReachingDefsT $ ReaderT $ proc (_,x) -> fix algo (unwrap . f . lift') -< x
fix f = ReachingDefsT $ ReaderT $ proc (_,x) -> fix (unwrap . f . lift') -< x
where
unwrap :: ReachingDefsT f c x y -> c x y
unwrap g = lmap (\x -> (Just (label x),x)) (runReachingDefsT' g)
......
......@@ -2,12 +2,13 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Abstract.Error where
import Control.Arrow hiding (ArrowMonad)
import Control.Arrow hiding (ArrowMonad,(<+>))
import Control.Arrow.Monad
import Control.Monad
import Control.Monad.Except
......@@ -21,6 +22,7 @@ import Data.GaloisConnection
import Data.Concrete.Powerset as C
import Data.Identifiable
import qualified Data.Concrete.Error as C
import Data.Text.Prettyprint.Doc
import Data.Abstract.FreeCompletion (FreeCompletion(..))
import Data.Abstract.Widening
......@@ -36,6 +38,10 @@ instance (Show e,Show a) => Show (Error e a) where
show (Fail e) = "Error " ++ show e
show (Success a) = show a
instance (Pretty e, Pretty a) => Pretty (Error e a) where
pretty (Fail e) = "Error" <+> pretty e
pretty (Success a) = pretty a
instance (Hashable e, Hashable a) => Hashable (Error e a) where
hashWithSalt s (Fail e) = s `hashWithSalt` (0::Int) `hashWithSalt` e
hashWithSalt s (Success a) = s `hashWithSalt` (1::Int) `hashWithSalt` a
......
......@@ -5,13 +5,14 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns -Wno-incomplete-patterns #-}
module Data.Abstract.Except where
import Prelude hiding (id,(.))
import Control.Arrow hiding (ArrowMonad)
import Control.Arrow hiding (ArrowMonad,(<+>))
import Control.Arrow.Monad
import qualified Control.Arrow.Order as O
......@@ -23,6 +24,7 @@ import Data.Bifunctor (Bifunctor(bimap))
import Data.Hashable
import Data.Order hiding (lub)
import Data.Traversable
import Data.Text.Prettyprint.Doc
import Data.Abstract.FreeCompletion (FreeCompletion(..))
import Data.Abstract.Widening
......@@ -45,6 +47,11 @@ instance (Show x, Show e) => Show (Except e x) where
show (Fail e) = "Fail " ++ show e
show (SuccessOrFail e x) = "Success " ++ show x ++ " ⊔ Fail " ++ show e
instance (Pretty e, Pretty a) => Pretty (Except e a) where
pretty (Fail e) = "Fail" <+> pretty e
pretty (Success a) = pretty a
pretty (SuccessOrFail e x) = "Success" <+> pretty x <+> "⊔" <+> "Fail" <+> pretty e
instance (O.ArrowJoin c, ArrowChoice c, Profunctor c) => ArrowFunctor (Except e) c where
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))
......
......@@ -4,6 +4,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Abstract.FreeCompletion where
......@@ -16,6 +17,7 @@ import Control.DeepSeq
import Data.Abstract.Widening
import Data.Abstract.Stable
import Data.Text.Prettyprint.Doc
import Data.Profunctor
import Data.Hashable
import Data.Order
......@@ -30,6 +32,10 @@ instance Show a => Show (FreeCompletion a) where
show Top = "⊤"
show (Lower a) = show a
instance Pretty a => Pretty (FreeCompletion a) where
pretty Top = "⊤"
pretty (Lower a) = pretty a
instance NFData a => NFData (FreeCompletion a)
instance Hashable a => Hashable (FreeCompletion a) where
......
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
module Data.Abstract.Map (
......@@ -12,7 +13,7 @@ module Data.Abstract.Map (
import Prelude hiding (lookup,map,Either(..),(**))
import Control.Arrow
import Control.Arrow hiding ((<+>))
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as H
......@@ -21,6 +22,7 @@ import Data.Order
import Data.Identifiable
import Data.Maybe (fromJust)
import Data.Empty
import Data.Text.Prettyprint.Doc
import qualified Data.Abstract.Maybe as M
import Data.Abstract.There (There(..))
......@@ -41,12 +43,16 @@ instance (Show a,Show b) => Show (Map a b) where
| H.null h = "[]"
| otherwise = "[" ++ init (unwords [ printf "%s%s -> %s," (show k) (show t) (show v) | (k,(t,v)) <- H.toList h]) ++ "]"
instance (Pretty k, Pretty v) => Pretty (Map k v) where
pretty (Map m) = list [ pretty k <> pretty t <+> " -> " <> pretty v | (k, (t,v)) <- H.toList m ]
instance (Identifiable a, PreOrd b) => PreOrd (Map a b) where
m1 Map m2 = all (\(k,(t,v)) -> lookup k m1 (case t of Must -> M.Just v; May -> M.JustNothing v))
(H.toList m2)
instance (Identifiable a, Complete b) => Complete (Map a b) where
() = toJoin widening ()
() = toJoin1 widening ()
widening :: Identifiable a => Widening b -> Widening (Map a b)
widening w (Map m1) (Map m2)
......
......@@ -4,6 +4,7 @@ module Data.Abstract.There where
import Data.Order
import Data.Hashable
import Data.Text.Prettyprint.Doc
import Data.Abstract.Widening
import Data.Abstract.Stable
......@@ -17,6 +18,9 @@ instance Show There where
show Must = ""
show May = "?"
instance Pretty There where
pretty = viaShow
instance PreOrd There where
Must May = True
Must Must = True
......
......@@ -27,10 +27,14 @@ finite :: Complete a => Widening a
finite a b = let x = a b in (if x a then Stable else Unstable,x)
{-# INLINE finite #-}
toJoin :: (Widening a -> Widening b) -> (a -> a -> a) -> (b -> b -> b)
toJoin f g a a' = snd (f (\b b' -> (Unstable,g b b')) a a')
toJoin :: Widening a -> (a -> a -> a)
toJoin w a b = snd (w a b)
{-# INLINE toJoin #-}
toJoin1 :: (Widening a -> Widening b) -> (a -> a -> a) -> (b -> b -> b)
toJoin1 f g a a' = snd (f (\b b' -> (Unstable,g b b')) a a')
{-# INLINE toJoin1 #-}
toJoin2 :: (Widening a -> Widening b -> Widening c) -> (a -> a -> a) -> (b -> b -> b) -> (c -> c -> c)
toJoin2 f g h c c' = snd (f (\a a' -> (Unstable,g a a')) (\b b' -> (Unstable,h b b')) c c')
{-# INLINE toJoin2 #-}
......
{-# LANGUAGE TypeFamilies #-}
module Data.Hashed.Lazy where
import Data.Hashable(Hashable(..))
......@@ -6,6 +7,8 @@ import Data.Empty
import Control.DeepSeq
import GHC.Exts
-- | Lazy version of Data.Hashable.Hashed. This datatype caches the hash of the
-- wrapped type.
data Hashed a = Hashed a Int
......@@ -32,6 +35,11 @@ instance Hashable (Hashed a) where
instance (Hashable a, IsEmpty a) => IsEmpty (Hashed a) where
empty = hashed empty
instance (Hashable a, IsList a) => IsList (Hashed a) where
type Item (Hashed a) = Item a
fromList = hashed . fromList
toList = toList . unhashed
instance PreOrd a => PreOrd (Hashed a) where
a b = unhashed a unhashed b
a b = unhashed a unhashed b
......@@ -42,3 +50,5 @@ instance (Hashable a, Complete a) => Complete (Hashed a) where
instance NFData a => NFData (Hashed a) where
rnf (Hashed a _) = rnf a
instance (Hashable a, Semigroup a) => Semigroup (Hashed a) where
a <> b = hashed (unhashed a <> unhashed b)
......@@ -104,10 +104,21 @@ unsoundExample = fix $ \call -> proc fun -> case fun of
where
c = True
type Arr x y = forall c. (?fixpointAlgorithm :: (Fix (c x y) -> Fix (c x y)) -> Fix (c x y),
ArrowChoice c, Profunctor c, ArrowApply c, ArrowComplete y c, ArrowFix (c x y))
=> c x y
newtype Strat x y = Strat { getStrat :: forall c. (ArrowChoice c, Profunctor c, ArrowApply c, ArrowComplete (Terminating y) c, ArrowStack x c, ArrowStackDepth c, ArrowStackElements x c, ArrowCache x (Terminating y) c) => FixpointCombinator c x (Terminating y)}
type Arr x y = forall c.
(?fixpointAlgorithm :: (Fix (c x y) -> Fix (c x y)) -> Fix (c x y),
ArrowChoice c, Profunctor c, ArrowApply c, ArrowComplete y c, ArrowFix (c x y))
=> c x y
newtype Strat x y =
Strat { getStrat :: forall c.
( ArrowChoice c
, Profunctor c
, ArrowStack x c
, ArrowStackDepth c
, ArrowStackElements x c
, ArrowCache x (Terminating y) c
)
=> FixpointCombinator c x (Terminating y)
}
type IV = Interval (InfiniteNumber Int)
iv :: InfiniteNumber Int -> InfiniteNumber Int -> IV
......
......@@ -25,7 +25,7 @@ import TestPrograms hiding (Fun(..))
import Control.Monad(forM_)
import Control.Arrow
import Control.Arrow.Fix as F
import Control.Arrow.Fix.Context
import Control.Arrow.Fix.Context(ArrowContext,callsiteSensitive)
import Control.Arrow.Fix.Chaotic
import qualified Control.Arrow.Trans as Arrow
import Control.Arrow.Transformer.Abstract.Terminating
......@@ -62,12 +62,16 @@ spec =
describe "Chaotic" $ do
describe "inner component" $
callsiteSpec $ \f a ->
let ?fixpointAlgorithm = fixpointAlgorithm (callsiteSensitive ?sensitivity fst . chaotic innermost)
in snd $ Arrow.run (f :: ChaoticT _ _ _) (?widenA, T.widening ?widenB) a
let ?contextWidening = ?widenA
?cacheWidening = T.widening ?widenB in
let ?fixpointAlgorithm = fixpointAlgorithm (callsiteSensitive ?sensitivity fst . chaotic innermost) in
snd $ Arrow.run (f :: ChaoticT _ _ _) a
describe "outer component" $
callsiteSpec $ \f a ->
let ?fixpointAlgorithm = fixpointAlgorithm (callsiteSensitive ?sensitivity fst . chaotic outermost)
in snd $ Arrow.run (f :: ChaoticT _ _ _) (?widenA, T.widening ?widenB) a
let ?contextWidening = ?widenA
?cacheWidening = T.widening ?widenB in
let ?fixpointAlgorithm = fixpointAlgorithm (callsiteSensitive ?sensitivity fst . chaotic outermost) in
snd $ Arrow.run (f :: ChaoticT _ _ _) a
data Val = Num IV | Unit | Top deriving (Show,Eq,Generic,Hashable)
instance Pretty Val where pretty = viaShow
......@@ -165,14 +169,3 @@ type ChaoticT lab a b =
(CacheT (Context (Cache.Proj2 (CtxCache (CallString lab))) Cache) (lab,a) (Terminating b)
(ContextT (CallString lab)
(->)))))) (lab,a) b
-- toChaotic :: (Identifiable lab, Identifiable a, Complete b)
-- => Arr (lab,a) b -> TerminatingT
-- (FixT (lab,a) (Terminating b)
-- (ComponentT Component (lab,a)
-- (StackT Stack (lab,a)
-- (CacheT (Context (Cache.Proj2 (CtxCache (CallString lab))) Cache) (lab,a) (Terminating b)
-- (ContextT (CallString lab)
-- (->)))))) (lab,a) b
-- toChaotic x = x
-- {-# INLINE toChaotic #-}
......@@ -13,6 +13,7 @@ import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Fix.Stack (ArrowStack,ArrowStackDepth,ArrowStackElements,widenInput,maxDepth,reuseByMetric)
import Control.Arrow.Fix.Cache (ArrowCache,ArrowParallelCache)
import qualified Control.Arrow.Fix.Cache as Cache
import Control.Arrow.Fix.Chaotic (ArrowInComponent,chaotic,innermost,outermost)
import Control.Arrow.Fix.Parallel (parallel,adi)
import qualified Control.Arrow.Trans as Arrow
......@@ -126,32 +127,47 @@ sharedSpec run = do
{-# INLINE shouldBe' #-}
{-# INLINE sharedSpec #-}
type ParallelT a b = TerminatingT (FixT (MetricsT a (StackT Stack a (CacheT (Parallel Cache) a (Terminating b) (->))))) a b
type ParallelT a b =
TerminatingT
(FixT
(MetricsT Metrics a
(StackT Stack a
(CacheT (Parallel Cache) a (Terminating b) (->))))) a b
runParallel :: forall a b.
(forall x y c. (Pretty x, Pretty y, Identifiable x, ArrowChoice c,
ArrowStack x c, ArrowStackDepth c, ArrowStackElements x c,
ArrowParallelCache x y c, ArrowCache x y c) =>
(FixpointCombinator c x y -> FixpointCombinator c x y) -> FixpointAlgorithm c x y)
ArrowParallelCache x y c, ArrowCache x y c,
?cacheWidening :: Cache.Widening c) =>
(FixpointCombinator c x y -> FixpointCombinator c x y) -> FixpointAlgorithm (c x y))
-> ((Pretty a, Pretty b, Identifiable a, Complete b,
?strat :: Strat a b, ?widen :: Widening b) =>
Arr a b -> a -> (Metrics a,Terminating b))
runParallel algorithm f a =
let ?fixpointAlgorithm = algorithm (\update -> getStrat ?strat . update)
in snd $ Arrow.run (f :: ParallelT a b) (T.widening ?widen) a
let ?cacheWidening = T.widening ?widen in
let ?fixpointAlgorithm = algorithm (\update -> getStrat ?strat . update) in
snd $ Arrow.run (f :: ParallelT a b) a
{-# INLINE runParallel #-}
type ChaoticT a b = TerminatingT (FixT (MetricsT a (ComponentT Component a (StackT Stack a (CacheT Cache a (Terminating b) (->)))))) a b
type ChaoticT a b =
TerminatingT
(FixT
(MetricsT Metrics a
(ComponentT Component a
(StackT Stack a
(CacheT Cache a (Terminating b) (->)))))) a b
runChaotic :: forall a b.
(forall x y c. (Pretty x, Pretty y, Identifiable x, ArrowChoice c,
ArrowStack x c, ArrowStackDepth c, ArrowStackElements x c,
ArrowInComponent x c, ArrowCache x y c) =>
ArrowInComponent x c, ArrowCache x y c,
?cacheWidening :: Cache.Widening c) =>
FixpointCombinator c x y)
-> ((Pretty a, Pretty b, Identifiable a, Complete b,
?strat :: Strat a b, ?widen :: Widening b) =>
Arr a b -> a -> (Metrics a,Terminating b))
runChaotic algorithm f a =
let ?fixpointAlgorithm = fixpointAlgorithm (getStrat ?strat . algorithm)
in snd $ Arrow.run (f :: ChaoticT a b) (T.widening ?widen) a
let ?cacheWidening = T.widening ?widen in
let ?fixpointAlgorithm = fixpointAlgorithm (getStrat ?strat . algorithm) in
snd $ Arrow.run (f :: ChaoticT a b) a
{-# INLINE runChaotic #-}
......@@ -13,6 +13,7 @@ dependencies:
- text
- transformers
- unordered-containers
- prettyprinter
library:
source-dirs:
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
-- | Concrete semantics of PCF.
......@@ -10,7 +11,7 @@ module ConcreteInterpreter where
import Prelude hiding (fail,(.))
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Fail as Fail
import Control.Arrow.Closure as Cls
import Control.Arrow.Trans
import Control.Arrow.Transformer.Value
......@@ -25,6 +26,7 @@ import qualified Data.HashMap.Lazy as M
import Data.Text (Text)
import Data.Label
import Data.Profunctor
import qualified Data.Function as Function
import GHC.Generics(Generic)
......@@ -39,8 +41,9 @@ data Val = NumVal Int | ClosureVal Cls deriving (Eq,Generic)
-- implemented by instantiating the shared semantics with the concrete
-- interpreter arrow `Interp`.
evalConcrete :: [(Text,Val)] -> State Label Expr -> Error String Val
evalConcrete env e = run
(eval ::
evalConcrete env e =
let ?fixpointAlgorithm = Function.fix in
run (eval ::
ValueT Val
(EnvT Env
(FailureT String
......@@ -48,8 +51,8 @@ evalConcrete env e = run
(M.fromList env,generate e)
-- | Concrete instance of the interface for value operations.
instance (ArrowClosure Expr Cls c, ArrowChoice c, ArrowFail String c) => IsVal Val (ValueT Val c) where
type Join y (ValueT Val c) = ()
instance (ArrowClosure Expr Cls c, ArrowChoice c, ArrowFail String c, Fail.Join Val c) => IsVal Val (ValueT Val c) where
type Join y (ValueT Val c) = (Fail.Join y c)
succ = proc x -> case x of
NumVal n -> returnA -< NumVal (n + 1)
......@@ -72,7 +75,7 @@ instance (ArrowClosure Expr Cls c, ArrowChoice c, ArrowFail String c) => IsVal V
instance (ArrowChoice c, ArrowFail String c, ArrowClosure Expr Cls c)
=> ArrowClosure Expr Val (ValueT Val c) where
type Join y Val (ValueT Val c) = Cls.Join y Cls c
type Join y Val (ValueT Val c) = (Cls.Join y Cls c, Fail.Join y c)
closure = ValueT $ rmap ClosureVal Cls.closure
apply (ValueT f) = ValueT $ proc (v,x) -> case v of
ClosureVal cls -> Cls.apply f -< (cls,x)
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TypeFamilies #-}
module GenericInterpreter where
......@@ -10,7 +11,8 @@ import Syntax (Expr(..))
import Control.Arrow
import Control.Arrow.Utils
import Control.Arrow.Fix
import Control.Arrow.Fail
import Control.Arrow.Fail (ArrowFail,failString)
import qualified Control.Arrow.Fail as Fail
import Control.Arrow.Closure (ArrowClosure)
import qualified Control.Arrow.Closure as Cls
import Control.Arrow.Environment (ArrowEnv)
......