From 87145308cd0a029b7eb729572caad61592122384 Mon Sep 17 00:00:00 2001 From: Timothy Clem Date: Wed, 22 Nov 2017 08:04:13 -0800 Subject: [PATCH] Bring in some of the other interpreters --- semantic-diff.cabal | 8 +- src/Abstract/Configuration.hs | 46 ++++++ src/Abstract/Interpreter/Caching.hs | 206 +++++++++++++++++++++++++ src/Abstract/Interpreter/Collecting.hs | 61 ++++++++ src/Abstract/Interpreter/Dead.hs | 69 +++++++++ src/Abstract/Interpreter/Symbolic.hs | 133 ++++++++++++++++ src/Abstract/Interpreter/Tracing.hs | 89 +++++++++++ 7 files changed, 611 insertions(+), 1 deletion(-) create mode 100644 src/Abstract/Configuration.hs create mode 100644 src/Abstract/Interpreter/Caching.hs create mode 100644 src/Abstract/Interpreter/Collecting.hs create mode 100644 src/Abstract/Interpreter/Dead.hs create mode 100644 src/Abstract/Interpreter/Symbolic.hs create mode 100644 src/Abstract/Interpreter/Tracing.hs diff --git a/semantic-diff.cabal b/semantic-diff.cabal index 25d8184c3..8440f1ed9 100644 --- a/semantic-diff.cabal +++ b/semantic-diff.cabal @@ -15,10 +15,16 @@ library hs-source-dirs: src exposed-modules: Algorithm , Alignment + , Abstract.Configuration , Abstract.Environment - , Abstract.Interpreter , Abstract.Eval , Abstract.FreeVariables + , Abstract.Interpreter + , Abstract.Interpreter.Caching + , Abstract.Interpreter.Collecting + , Abstract.Interpreter.Dead + -- , Abstract.Interpreter.Symbolic + , Abstract.Interpreter.Tracing , Abstract.Primitive , Abstract.Set , Abstract.Store diff --git a/src/Abstract/Configuration.hs b/src/Abstract/Configuration.hs new file mode 100644 index 000000000..4f2dd91e5 --- /dev/null +++ b/src/Abstract/Configuration.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE DeriveFoldable, FlexibleContexts, StandaloneDeriving, UndecidableInstances #-} +module Abstract.Configuration where + +import Abstract.Set +import Abstract.Store +import Abstract.Environment + +import Data.List (intersperse) +import Data.Functor.Classes +import Data.Monoid + +data Configuration l t v + = Configuration + { configurationTerm :: t + , configurationRoots :: Set (Address l v) + , configurationEnvironment :: Environment l v + , configurationStore :: Store l v + } + +deriving instance (Eq l, Eq t, Eq v, Eq1 (Cell l)) => Eq (Configuration l t v) +deriving instance (Ord l, Ord t, Ord v, Ord1 (Cell l)) => Ord (Configuration l t v) +deriving instance (Show l, Show t, Show v, Show1 (Cell l)) => Show (Configuration l t v) +deriving instance (Ord l, Foldable (Cell l)) => Foldable (Configuration l t) + + +instance (Eq l, Eq1 (Cell l)) => Eq2 (Configuration l) where + liftEq2 eqT eqV (Configuration t1 r1 e1 s1) (Configuration t2 r2 e2 s2) = eqT t1 t2 && liftEq (liftEq eqV) r1 r2 && liftEq eqV e1 e2 && liftEq eqV s1 s2 + +instance (Eq l, Eq t, Eq1 (Cell l)) => Eq1 (Configuration l t) where + liftEq = liftEq2 (==) + +instance (Ord l, Ord1 (Cell l)) => Ord2 (Configuration l) where + liftCompare2 compareT compareV (Configuration t1 r1 e1 s1) (Configuration t2 r2 e2 s2) = compareT t1 t2 <> liftCompare (liftCompare compareV) r1 r2 <> liftCompare compareV e1 e2 <> liftCompare compareV s1 s2 + +instance (Ord l, Ord t, Ord1 (Cell l)) => Ord1 (Configuration l t) where + liftCompare = liftCompare2 compare + +showsConstructor :: String -> Int -> [Int -> ShowS] -> ShowS +showsConstructor name d fields = showParen (d > 10) $ showString name . showChar ' ' . foldr (.) id (intersperse (showChar ' ') ([($ 11)] <*> fields)) + + +instance (Show l, Show1 (Cell l)) => Show2 (Configuration l) where + liftShowsPrec2 spT _ spV slV d (Configuration t r e s) = showsConstructor "Configuration" d [ flip spT t, flip (liftShowsPrec (liftShowsPrec spV slV) (liftShowList spV slV)) r, flip (liftShowsPrec spV slV) e, flip (liftShowsPrec spV slV) s ] + +instance (Show l, Show t, Show1 (Cell l)) => Show1 (Configuration l t) where + liftShowsPrec = liftShowsPrec2 showsPrec showList diff --git a/src/Abstract/Interpreter/Caching.hs b/src/Abstract/Interpreter/Caching.hs new file mode 100644 index 000000000..d2c24d9e6 --- /dev/null +++ b/src/Abstract/Interpreter/Caching.hs @@ -0,0 +1,206 @@ +{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-} +module Abstract.Interpreter.Caching where + +import Abstract.Configuration +import Abstract.Environment +import Abstract.Eval +import Abstract.Interpreter +import Abstract.Interpreter.Collecting +import Abstract.Primitive +import Abstract.Set +import Abstract.Store +import Abstract.Type +import Abstract.Value +import Data.Term + +import Control.Applicative +import Control.Effect +import Control.Monad.Effect.Fail +import Control.Monad.Effect.Internal hiding (run) +import Control.Monad.Effect.NonDetEff +import Control.Monad.Effect.Reader +import Control.Monad.Effect.State +import Data.Foldable +import Data.Function (fix) +import Data.Functor.Classes +import Data.Maybe +import Data.Pointed +import Data.Semigroup +import qualified Data.Map as Map + +newtype Cache l t v = Cache { unCache :: Map.Map (Configuration l t v) (Set (v, Store l v)) } + +deriving instance (Ord l, Ord t, Ord v, Ord1 (Cell l)) => Monoid (Cache l t v) + +cacheLookup :: (Ord l, Ord t, Ord v, Ord1 (Cell l)) => Configuration l t v -> Cache l t v -> Maybe (Set (v, Store l v)) +cacheLookup key = Map.lookup key . unCache + +cacheSet :: (Ord l, Ord t, Ord v, Ord1 (Cell l)) => Configuration l t v -> Set (v, Store l v) -> Cache l t v -> Cache l t v +cacheSet = (((Cache .) . (. unCache)) .) . Map.insert + +cacheInsert :: (Ord l, Ord t, Ord v, Ord1 (Cell l)) => Configuration l t v -> (v, Store l v) -> Cache l t v -> Cache l t v +cacheInsert = (((Cache .) . (. unCache)) .) . (. point) . Map.insertWith (<>) + + +type CachingInterpreter l t v = '[Fresh, Reader (Set (Address l v)), Reader (Environment l v), Fail, NonDetEff, State (Store l v), Reader (Cache l t v), State (Cache l t v)] + +type CachingResult l t v = Final (CachingInterpreter l t v) v + +type MonadCachingInterpreter l t v m = (MonadEnv l v m, MonadStore l v m, MonadCacheIn l t v m, MonadCacheOut l t v m, MonadGC l v m, Alternative m) + + + +class Monad m => MonadCacheIn l t v m where + askCache :: m (Cache l t v) + localCache :: (Cache l t v -> Cache l t v) -> m a -> m a + +instance (Reader (Cache l t v) :< fs) => MonadCacheIn l t v (Eff fs) where + askCache = ask + localCache = local + + +class Monad m => MonadCacheOut l t v m where + getCache :: m (Cache l t v) + putCache :: Cache l t v -> m () + +instance (State (Cache l t v) :< fs) => MonadCacheOut l t v (Eff fs) where + getCache = get + putCache = put + +modifyCache :: MonadCacheOut l t v m => (Cache l t v -> Cache l t v) -> m () +modifyCache f = fmap f getCache >>= putCache + + +class (Alternative m, Monad m) => MonadNonDet m where + collect :: Monoid b => (a -> b) -> m a -> m b + +instance (NonDetEff :< fs) => MonadNonDet (Eff fs) where + collect f = interpose (pure . f) (\ m k -> case m of + MZero -> pure mempty + MPlus -> mappend <$> k True <*> k False) + + +-- Coinductively-cached evaluation +-- +-- Examples: +-- evalCache @Monovariant @Type @Syntax (makeLam "x" (var "x") # true) +-- evalCache @Precise @(Value Syntax Precise) @Syntax (makeLam "x" (var "x") # true) + +evalCache :: forall l v syntax ann + . ( Ord v + , Ord l + , Ord ann + , Ord1 (Cell l) + , Ord1 syntax + , Foldable (Cell l) + , MonadAddress l (Eff (CachingInterpreter l (Term syntax ann) v)) + , MonadPrim v (Eff (CachingInterpreter l (Term syntax ann) v)) + , Semigroup (Cell l v) + , AbstractValue l v + , EvalCollect l v (Eff (CachingInterpreter l (Term syntax ann) v)) syntax ann (TermF syntax ann) + ) + => Term syntax ann + -> CachingResult l (Term syntax ann) v +evalCache e = run @(CachingInterpreter l (Term syntax ann) v) (fixCache @l (fix (evCache @l (evCollect @l (evRoots @l)))) e) + + +evCache :: forall l t v m + . ( Ord l + , Ord t + , Ord v + , Ord1 (Cell l) + , MonadCachingInterpreter l t v m + ) + => (Eval' t (m v) -> Eval' t (m v)) + -> Eval' t (m v) + -> Eval' t (m v) +evCache ev0 ev e = do + env <- askEnv + store <- getStore + roots <- askRoots + let c = Configuration e roots env store :: Configuration l t v + out <- getCache + case cacheLookup c out of + Just pairs -> asum . flip map (toList pairs) $ \ (value, store') -> do + putStore store' + return value + Nothing -> do + in' <- askCache + let pairs = fromMaybe mempty (cacheLookup c in') + putCache (cacheSet c pairs out) + v <- ev0 ev e + store' <- getStore + modifyCache (cacheInsert c (v, store')) + return v + +fixCache :: forall l t v m + . ( Ord l + , Ord t + , Ord v + , Ord1 (Cell l) + , MonadCachingInterpreter l t v m + , MonadNonDet m + , MonadFresh m + ) + => Eval' t (m v) + -> Eval' t (m v) +fixCache eval e = do + env <- askEnv + store <- getStore + roots <- askRoots + let c = Configuration e roots env store :: Configuration l t v + pairs <- mlfp mempty (\ dollar -> do + putCache (mempty :: Cache l t v) + putStore store + reset 0 + _ <- localCache (const dollar) (collect point (eval e) :: m (Set v)) + getCache) + asum . flip map (maybe [] toList (cacheLookup c pairs)) $ \ (value, store') -> do + putStore store' + return value + + +mlfp :: (Eq a, Monad m) => a -> (a -> m a) -> m a +mlfp a f = loop a + where loop x = do + x' <- f x + if x' == x then + return x + else + loop x' + + +instance (Eq l, Eq1 (Cell l)) => Eq2 (Cache l) where + liftEq2 eqT eqV (Cache a) (Cache b) = liftEq2 (liftEq2 eqT eqV) (liftEq (liftEq2 eqV (liftEq eqV))) a b + +instance (Eq l, Eq t, Eq1 (Cell l)) => Eq1 (Cache l t) where + liftEq = liftEq2 (==) + +instance (Eq l, Eq t, Eq v, Eq1 (Cell l)) => Eq (Cache l t v) where + (==) = eq1 + + +instance (Ord l, Ord1 (Cell l)) => Ord2 (Cache l) where + liftCompare2 compareT compareV (Cache a) (Cache b) = liftCompare2 (liftCompare2 compareT compareV) (liftCompare (liftCompare2 compareV (liftCompare compareV))) a b + +instance (Ord l, Ord t, Ord1 (Cell l)) => Ord1 (Cache l t) where + liftCompare = liftCompare2 compare + +instance (Ord l, Ord t, Ord v, Ord1 (Cell l)) => Ord (Cache l t v) where + compare = compare1 + + +instance (Show l, Show1 (Cell l)) => Show2 (Cache l) where + liftShowsPrec2 spT slT spV slV d = showsUnaryWith (liftShowsPrec2 spKey slKey (liftShowsPrec spPair slPair) (liftShowList spPair slPair)) "Cache" d . unCache + where spKey = liftShowsPrec2 spT slT spV slV + slKey = liftShowList2 spT slT spV slV + spPair = liftShowsPrec2 spV slV spStore slStore + slPair = liftShowList2 spV slV spStore slStore + spStore = liftShowsPrec spV slV + slStore = liftShowList spV slV + +instance (Show l, Show t, Show1 (Cell l)) => Show1 (Cache l t) where + liftShowsPrec = liftShowsPrec2 showsPrec showList + +instance (Show l, Show t, Show v, Show1 (Cell l)) => Show (Cache l t v) where + showsPrec = showsPrec1 diff --git a/src/Abstract/Interpreter/Collecting.hs b/src/Abstract/Interpreter/Collecting.hs new file mode 100644 index 000000000..3004489f7 --- /dev/null +++ b/src/Abstract/Interpreter/Collecting.hs @@ -0,0 +1,61 @@ +{-# LANGUAGE AllowAmbiguousTypes, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeApplications, TypeOperators, UndecidableInstances #-} +module Abstract.Interpreter.Collecting where + +import Abstract.Environment +import Abstract.Interpreter +import Abstract.Primitive +import Abstract.Set +import Abstract.Store +import Data.Term +import Abstract.Value +import Abstract.Eval + +import Control.Monad.Effect +import Control.Monad.Effect.Reader +import Data.Semigroup + + +instance (Ord l, Reader (Set (Address l a)) :< fs) => MonadGC l a (Eff fs) where + askRoots = ask :: Eff fs (Set (Address l a)) + + extraRoots roots' = local (<> roots') + +gc :: (Ord l, Foldable (Cell l), AbstractValue l a) => Set (Address l a) -> Store l a -> Store l a +gc roots store = storeRestrict store (reachable roots store) + +reachable :: (Ord l, Foldable (Cell l), AbstractValue l a) => Set (Address l a) -> Store l a -> Set (Address l a) +reachable roots store = go roots mempty + where go set seen = case split set of + Nothing -> seen + Just (a, as) + | Just values <- storeLookupAll a store -> go (difference (foldr ((<>) . valueRoots) mempty values <> as) seen) (insert a seen) + | otherwise -> go seen (insert a seen) + + +evCollect :: forall l t v m + . ( Ord l + , Foldable (Cell l) + , MonadStore l v m + , MonadGC l v m + , AbstractValue l v + ) + => (Eval' t (m v) -> Eval' t (m v)) + -> Eval' t (m v) + -> Eval' t (m v) +evCollect ev0 ev e = do + roots <- askRoots :: m (Set (Address l v)) + v <- ev0 ev e + modifyStore (gc (roots <> valueRoots v)) + return v + +evRoots :: forall l v m syntax ann + . ( Ord l + , MonadEnv l v m + , MonadGC l v m + , MonadPrim v m + , AbstractValue l v + , EvalCollect l v m syntax ann (TermF syntax ann) + ) + => Eval' (Term syntax ann) (m v) + -> Eval' (Term syntax ann) (m v) +evRoots ev = evalCollect @l ev . unTerm diff --git a/src/Abstract/Interpreter/Dead.hs b/src/Abstract/Interpreter/Dead.hs new file mode 100644 index 000000000..390892dc3 --- /dev/null +++ b/src/Abstract/Interpreter/Dead.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE AllowAmbiguousTypes, DataKinds, DeriveFoldable, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-} +module Abstract.Interpreter.Dead where + +import Abstract.Eval +import Abstract.Interpreter +import Abstract.Primitive +import Abstract.Set +import Abstract.Store +import Data.Term + +import Control.Effect +import Control.Monad.Effect hiding (run) +import Control.Monad.Effect.State +import Data.Function (fix) +import Data.Functor.Foldable +import Data.Functor.Classes +import Data.Pointed +import Data.Semigroup + + +type DeadCodeInterpreter l t v = State (Dead t) ': Interpreter l v + +type DeadCodeResult l t v = Final (DeadCodeInterpreter l t v) v + + +newtype Dead a = Dead { unDead :: Set a } + deriving (Eq, Foldable, Semigroup, Monoid, Ord, Show) + + +class Monad m => MonadDead t m where + killAll :: Dead t -> m () + revive :: Ord t => t -> m () + +instance (State (Dead t) :< fs) => MonadDead t (Eff fs) where + killAll = put + revive = modify . (Dead .) . (. unDead) . delete + + +subterms :: (Ord a, Recursive a, Foldable (Base a)) => a -> Set a +subterms term = para (foldMap (uncurry ((<>) . point))) term <> point term + + +-- Dead code analysis +-- Example: +-- evalDead @Precise @(Value Syntax Precise) @Syntax (if' true (Abstract.Syntax.int 1) (Abstract.Syntax.int 2)) +evalDead :: forall l v syntax ann + . ( Ord v + , Ord ann + , Ord1 syntax + , Recursive (Term syntax ann) + , Foldable (Base (Term syntax ann)) + , Eval v (Eff (DeadCodeInterpreter l (Term syntax ann) v)) syntax ann syntax + , MonadAddress l (Eff (DeadCodeInterpreter l (Term syntax ann) v)) + , MonadPrim v (Eff (DeadCodeInterpreter l (Term syntax ann) v)) + , Semigroup (Cell l v) + ) + => Term syntax ann + -> DeadCodeResult l (Term syntax ann) v +evalDead e0 = run @(DeadCodeInterpreter l (Term syntax ann) v) $ do + killAll (Dead (subterms e0)) + fix (evDead ev) e0 + +evDead :: (Ord t, MonadDead t m) + => (Eval' t (m v) -> Eval' t (m v)) + -> Eval' t (m v) + -> Eval' t (m v) +evDead ev0 ev e = do + revive e + ev0 ev e diff --git a/src/Abstract/Interpreter/Symbolic.hs b/src/Abstract/Interpreter/Symbolic.hs new file mode 100644 index 000000000..3049085de --- /dev/null +++ b/src/Abstract/Interpreter/Symbolic.hs @@ -0,0 +1,133 @@ +{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RankNTypes, TypeOperators, UndecidableInstances #-} +module Abstract.Interpreter.Symbolic where + +import Abstract.Environment +import Abstract.Interpreter +import Abstract.Primitive +import Abstract.Set +import Abstract.Store +import Data.Term + +import Control.Applicative +import Control.Monad +import Control.Monad.Effect +import Control.Monad.Effect.State +import Control.Monad.Fail +import Data.Functor.Classes +import qualified Data.Set as Set +import Data.Union + +data Sym t a = Sym t | V a + deriving (Eq, Ord, Show) + +sym :: (Num a, Num t) => (forall n . Num n => n -> n) -> Sym t a -> Sym t a +sym f (Sym t) = Sym (f t) +sym f (V a) = V (f a) + +sym2 :: Applicative f => (a -> a -> f a) -> (a -> t) -> (t -> t -> t) -> Sym t a -> Sym t a -> f (Sym t a) +sym2 f _ _ (V a) (V b) = V <$> f a b +sym2 _ _ g (Sym a) (Sym b) = pure (Sym (g a b)) +sym2 f num g a (V b) = sym2 f num g a (Sym (num b)) +sym2 f num g (V a) b = sym2 f num g (Sym (num a)) b + + +evSymbolic :: (Eval' t (Eff fs (v (Sym t a))) -> Eval' t (Eff fs (v (Sym t a)))) + -> Eval' t (Eff fs (v (Sym t a))) + -> Eval' t (Eff fs (v (Sym t a))) +evSymbolic ev0 ev e = ev0 ev e + + +data PathExpression t = E t | NotE t + deriving (Eq, Ord, Show) + +newtype PathCondition t = PathCondition { unPathCondition :: Set.Set (PathExpression t) } + deriving (Eq, Ord, Show) + + +refine :: (Ord t, MonadPathCondition t m) => PathExpression t -> m () +refine = modifyPathCondition . pathConditionInsert + +pathConditionMember :: Ord t => PathExpression t -> PathCondition t -> Bool +pathConditionMember = (. unPathCondition) . Set.member + +pathConditionInsert :: Ord t => PathExpression t -> PathCondition t -> PathCondition t +pathConditionInsert = ((PathCondition .) . (. unPathCondition)) . Set.insert + + +class Monad m => MonadPathCondition t m where + getPathCondition :: m (PathCondition t) + putPathCondition :: PathCondition t -> m () + +instance (State (PathCondition t) :< fs) => MonadPathCondition t (Eff fs) where + getPathCondition = get + putPathCondition = put + +modifyPathCondition :: MonadPathCondition t m => (PathCondition t -> PathCondition t) -> m () +modifyPathCondition f = getPathCondition >>= putPathCondition . f + +instance ( Alternative m + , MonadFail m + , MonadPrim Prim m + , MonadPathCondition (Term (Union fs)) m + , Apply Eq1 fs + , Apply Ord1 fs + , Binary :< fs + , Unary :< fs + , Primitive :< fs + ) => MonadPrim (Sym (Term (Union fs)) Prim) m where + delta1 o a = case o of + Negate -> pure (negate a) + Abs -> pure (abs a) + Signum -> pure (signum a) + Not -> case a of + Sym t -> pure (Sym (not' t)) + V a -> V <$> delta1 Not a + + delta2 o a b = case o of + Plus -> pure (a + b) + Minus -> pure (a - b) + Times -> pure (a * b) + DividedBy -> isZero b >>= flip when divisionByZero >> sym2 (delta2 DividedBy) prim div' a b + Quotient -> isZero b >>= flip when divisionByZero >> sym2 (delta2 Quotient) prim quot' a b + Remainder -> isZero b >>= flip when divisionByZero >> sym2 (delta2 Remainder) prim rem' a b + Modulus -> isZero b >>= flip when divisionByZero >> sym2 (delta2 Modulus) prim mod' a b + And -> sym2 (delta2 And) prim and' a b + Or -> sym2 (delta2 Or) prim or' a b + Eq -> sym2 (delta2 Eq) prim eq a b + Lt -> sym2 (delta2 Lt) prim lt a b + LtE -> sym2 (delta2 LtE) prim lte a b + Gt -> sym2 (delta2 Gt) prim gt a b + GtE -> sym2 (delta2 GtE) prim gte a b + + truthy (V a) = truthy a + truthy (Sym e) = do + phi <- getPathCondition + if E e `pathConditionMember` phi then + return True + else if NotE e `pathConditionMember` phi then + return False + else + (refine (E e) >> return True) + <|> (refine (NotE e) >> return False) + +instance (Binary :< fs, Unary :< fs, Primitive :< fs) => Num (Sym (Term (Union fs)) Prim) where + fromInteger = V . fromInteger + + signum (V a) = V (signum a) + signum (Sym t) = Sym (signum t) + abs (V a) = V (abs a) + abs (Sym t) = Sym (abs t) + negate (V a) = V (negate a) + negate (Sym t) = Sym (negate t) + V a + V b = V ( a + b) + Sym a + V b = Sym ( a + prim b) + V a + Sym b = Sym (prim a + b) + Sym a + Sym b = Sym ( a + b) + V a - V b = V ( a - b) + Sym a - V b = Sym ( a - prim b) + V a - Sym b = Sym (prim a - b) + Sym a - Sym b = Sym ( a - b) + V a * V b = V ( a * b) + Sym a * V b = Sym ( a * prim b) + V a * Sym b = Sym (prim a * b) + Sym a * Sym b = Sym ( a * b) diff --git a/src/Abstract/Interpreter/Tracing.hs b/src/Abstract/Interpreter/Tracing.hs new file mode 100644 index 000000000..d0992badb --- /dev/null +++ b/src/Abstract/Interpreter/Tracing.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-} +module Abstract.Interpreter.Tracing where + +import Abstract.Configuration +import Abstract.Environment +import Abstract.Eval +import Abstract.Interpreter +import Abstract.Interpreter.Collecting() +import Abstract.Primitive +import Abstract.Set +import Abstract.Store +import Data.Term + +import Control.Effect +import Control.Monad.Effect hiding (run) +import Control.Monad.Effect.Reader +import Control.Monad.Effect.Writer +import Data.Function (fix) +import Data.Functor.Classes (Ord1) +import Data.Semigroup +import GHC.Exts (IsList(..)) +import qualified Data.Set as Set + +type TracingInterpreter l t v g = Reader (Set (Address l v)) ': Writer (g (Configuration l t v)) ': Interpreter l v + +type TraceInterpreter l t v = TracingInterpreter l t v [] +type ReachableStateInterpreter l t v = TracingInterpreter l t v Set.Set + +type TraceResult l t v f = Final (TracingInterpreter l t v f) v + + +class Monad m => MonadTrace l t v g m where + trace :: g (Configuration l t v) -> m () + +instance (Writer (g (Configuration l t v)) :< fs) => MonadTrace l t v g (Eff fs) where + trace = tell + +-- instance (Ord l, Reader (Set (Address l a)) :< fs) => MonadGC l a (Eff fs) where +-- askRoots = ask :: Eff fs (Set (Address l a)) +-- +-- extraRoots roots' = local (<> roots') + +-- Tracing and reachable state analyses +-- +-- Examples +-- evalTrace @Precise @(Value Syntax Precise) @Syntax (makeLam "x" (var "x") # true) +-- evalReach @Precise @(Value Syntax Precise) @Syntax (makeLam "x" (var "x") # true) + +evalTrace :: forall l v syntax ann + . ( Ord v, Ord ann, Ord1 syntax, Ord1 (Cell l) + , MonadAddress l (Eff (TraceInterpreter l (Term syntax ann) v)) + , MonadPrim v (Eff (TraceInterpreter l (Term syntax ann) v)) + , MonadGC l v (Eff (TraceInterpreter l (Term syntax ann) v)) + , Semigroup (Cell l v) + , Eval v (Eff (TraceInterpreter l (Term syntax ann) v)) syntax ann syntax + ) + => Eval' (Term syntax ann) (TraceResult l (Term syntax ann) v []) +evalTrace = run @(TraceInterpreter l (Term syntax ann) v) . fix (evTell @l @(Term syntax ann) @v @[] ev) + +evalReach :: forall l v syntax ann + . ( Ord v, Ord ann, Ord l, Ord1 (Cell l), Ord1 syntax + , MonadAddress l (Eff (ReachableStateInterpreter l (Term syntax ann) v)) + , MonadPrim v (Eff (ReachableStateInterpreter l (Term syntax ann) v)) + , MonadGC l v (Eff (ReachableStateInterpreter l (Term syntax ann) v)) + , Semigroup (Cell l v) + , Eval v (Eff (ReachableStateInterpreter l (Term syntax ann) v)) syntax ann syntax + ) + => Eval' (Term syntax ann) (TraceResult l (Term syntax ann) v Set.Set) +evalReach = run @(ReachableStateInterpreter l (Term syntax ann) v) . fix (evTell @l @(Term syntax ann) @v @Set.Set ev) + + +evTell :: forall l t v g m + . ( Ord l + , IsList (g (Configuration l t v)) + , Item (g (Configuration l t v)) ~ Configuration l t v + , MonadTrace l t v g m + , MonadEnv l v m + , MonadStore l v m + , MonadGC l v m + ) + => (Eval' t (m v) -> Eval' t (m v)) + -> Eval' t (m v) + -> Eval' t (m v) +evTell ev0 ev e = do + env <- askEnv + store <- getStore + roots <- askRoots + trace (fromList [Configuration e roots env store] :: g (Configuration l t v)) + ev0 ev e