Bring in some of the other interpreters

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

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

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

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

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

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)

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