Merge pull request #1696 from github/symbol-resolution

Symbol resolution
2024-11-28 10:15:55 +03:00 · 2018-04-02 17:12:39 -04:00 · 2018-04-02 17:12:39 -04:00 · 851de212cb
commit 851de212cb
parent d732d8caf5 d1d70bf31f
23 changed files with 464 additions and 404 deletions
--- a/semantic.cabal
+++ b/semantic.cabal
@ -54,9 +54,11 @@ library
                     , Data.Abstract.FreeVariables
                     , Data.Abstract.Heap
                     , Data.Abstract.Live
+                     , Data.Abstract.Located
                     , Data.Abstract.Module
                     , Data.Abstract.ModuleTable
                     , Data.Abstract.Number
+                     , Data.Abstract.Origin
                     , Data.Abstract.Path
                     , Data.Abstract.Type
                     , Data.Abstract.Value
--- a/src/Analysis/Abstract/BadVariables.hs
+++ b/src/Analysis/Abstract/BadVariables.hs
@ -12,19 +12,19 @@ newtype BadVariables m (effects :: [* -> *]) a = BadVariables (m effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

 deriving instance MonadControl term (m effects)                    => MonadControl term (BadVariables m effects)
-deriving instance MonadEnvironment value (m effects)      => MonadEnvironment value (BadVariables m effects)
-deriving instance MonadHeap value (m effects)             => MonadHeap value (BadVariables m effects)
-deriving instance MonadModuleTable term value (m effects) => MonadModuleTable term value (BadVariables m effects)
-deriving instance MonadEvaluator term value (m effects)   => MonadEvaluator term value (BadVariables m effects)
+deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (BadVariables m effects)
+deriving instance MonadHeap location value (m effects)             => MonadHeap location value (BadVariables m effects)
+deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadVariables m effects)
+deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (BadVariables m effects)

 instance ( Effectful m
         , Member (Resumable (EvalError value)) effects
         , Member (State [Name]) effects
-         , MonadAnalysis term value (m effects)
-         , MonadValue value (BadVariables m effects)
+         , MonadAnalysis location term value (m effects)
+         , MonadValue location value (BadVariables m effects)
         )
-      => MonadAnalysis term value (BadVariables m effects) where
-  type Effects term value (BadVariables m effects) = State [Name] ': Effects term value (m effects)
+      => MonadAnalysis location term value (BadVariables m effects) where
+  type Effects location term value (BadVariables m effects) = State [Name] ': Effects location term value (m effects)

  analyzeTerm eval term = resumeException @(EvalError value) (liftAnalyze analyzeTerm eval term) (
        \yield (FreeVariableError name) ->
--- a/src/Analysis/Abstract/Caching.hs
+++ b/src/Analysis/Abstract/Caching.hs
@ -4,6 +4,7 @@ module Analysis.Abstract.Caching
 ) where

 import Control.Abstract.Analysis
+import Data.Abstract.Address
 import Data.Abstract.Cache
 import Data.Abstract.Configuration
 import Data.Abstract.Heap
@ -11,50 +12,46 @@ import Data.Abstract.Module
 import Prologue

 -- | The effects necessary for caching analyses.
-type CachingEffects term value effects
-  = Fresh                        -- For 'MonadFresh'.
- ': NonDet                       -- For 'Alternative' and 'MonadNonDet'.
- ': Reader (CacheFor term value) -- The in-cache used as an oracle while converging on a result.
- ': State  (CacheFor term value) -- The out-cache used to record results in each iteration of convergence.
+type CachingEffects location term value effects
+  = NonDet                             -- For 'Alternative' and 'MonadNonDet'.
+ ': Reader (Cache location term value) -- The in-cache used as an oracle while converging on a result.
+ ': State  (Cache location term value) -- The out-cache used to record results in each iteration of convergence.
 ': effects

-- | The cache for term and abstract value types.
-type CacheFor term value = Cache (LocationFor value) term value
-
 -- | A (coinductively-)cached analysis suitable for guaranteeing termination of (suitably finitized) analyses over recursive programs.
 newtype Caching m (effects :: [* -> *]) a = Caching (m effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

 deriving instance MonadControl term (m effects)                    => MonadControl term (Caching m effects)
-deriving instance MonadEnvironment value (m effects)      => MonadEnvironment value (Caching m effects)
-deriving instance MonadHeap value (m effects)             => MonadHeap value (Caching m effects)
-deriving instance MonadModuleTable term value (m effects) => MonadModuleTable term value (Caching m effects)
-deriving instance MonadEvaluator term value (m effects)   => MonadEvaluator term value (Caching m effects)
+deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (Caching m effects)
+deriving instance MonadHeap location value (m effects)             => MonadHeap location value (Caching m effects)
+deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Caching m effects)
+deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (Caching m effects)

 -- | Functionality used to perform caching analysis. This is not exported, and exists primarily for organizational reasons.
-class MonadEvaluator term value m => MonadCaching term value m where
+class MonadEvaluator location term value m => MonadCaching location term value m where
  -- | Look up the set of values for a given configuration in the in-cache.
-  consultOracle :: ConfigurationFor term value -> m (Set (value, HeapFor value))
+  consultOracle :: Configuration location term value -> m (Set (value, Heap location value))
  -- | Run an action with the given in-cache.
-  withOracle :: CacheFor term value -> m a -> m a
+  withOracle :: Cache location term value -> m a -> m a

  -- | Look up the set of values for a given configuration in the out-cache.
-  lookupCache :: ConfigurationFor term value -> m (Maybe (Set (value, HeapFor value)))
+  lookupCache :: Configuration location term value -> m (Maybe (Set (value, Heap location value)))
  -- | Run an action, caching its result and 'Heap' under the given configuration.
-  caching :: ConfigurationFor term value -> Set (value, HeapFor value) -> m value -> m value
+  caching :: Configuration location term value -> Set (value, Heap location value) -> m value -> m value

  -- | Run an action starting from an empty out-cache, and return the out-cache afterwards.
-  isolateCache :: m a -> m (CacheFor term value)
+  isolateCache :: m a -> m (Cache location term value)

 instance ( Effectful m
-         , Members (CachingEffects term value '[]) effects
-         , MonadEvaluator term value (m effects)
-         , Ord (CellFor value)
-         , Ord (LocationFor value)
+         , Members (CachingEffects location term value '[]) effects
+         , MonadEvaluator location term value (m effects)
+         , Ord (Cell location value)
+         , Ord location
         , Ord term
         , Ord value
         )
-         => MonadCaching term value (Caching m effects) where
+         => MonadCaching location term value (Caching m effects) where
  consultOracle configuration = raise (fromMaybe mempty . cacheLookup configuration <$> ask)
  withOracle cache = raise . local (const cache) . lower

@ -65,23 +62,23 @@ instance ( Effectful m
    raise (modify (cacheInsert configuration result))
    pure (fst result)

-  isolateCache action = raise (put (mempty :: CacheFor term value)) *> action *> raise get
+  isolateCache action = raise (put (mempty :: Cache location term value)) *> action *> raise get

 -- | This instance coinductively iterates the analysis of a term until the results converge.
 instance ( Corecursive term
         , Effectful m
-         , Members (CachingEffects term value '[]) effects
-         , MonadAnalysis term value (m effects)
+         , Members (CachingEffects location term value '[]) effects
+         , MonadAnalysis location term value (m effects)
         , MonadFresh (m effects)
         , MonadNonDet (m effects)
-         , Ord (CellFor value)
-         , Ord (LocationFor value)
+         , Ord (Cell location value)
+         , Ord location
         , Ord term
         , Ord value
         )
-         => MonadAnalysis term value (Caching m effects) where
+      => MonadAnalysis location term value (Caching m effects) where
  -- We require the 'CachingEffects' in addition to the underlying analysis’ 'Effects'.
-  type Effects term value (Caching m effects) = CachingEffects term value (Effects term value (m effects))
+  type Effects location term value (Caching m effects) = CachingEffects location term value (Effects location term value (m effects))

  -- Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache.
  analyzeTerm recur e = do
@ -124,5 +121,5 @@ converge f = loop
            loop x'

 -- | Nondeterministically write each of a collection of stores & return their associated results.
-scatter :: (Alternative m, Foldable t, MonadEvaluator term value m) => t (a, Heap (LocationFor value) value) -> m a
+scatter :: (Alternative m, Foldable t, MonadEvaluator location term value m) => t (a, Heap location value) -> m a
 scatter = foldMapA (\ (value, heap') -> putHeap heap' $> value)
--- a/src/Analysis/Abstract/Collecting.hs
+++ b/src/Analysis/Abstract/Collecting.hs
@ -14,31 +14,31 @@ newtype Collecting m (effects :: [* -> *]) a = Collecting (m effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

 deriving instance MonadControl term (m effects)                    => MonadControl term (Collecting m effects)
-deriving instance MonadEnvironment value (m effects)      => MonadEnvironment value (Collecting m effects)
-deriving instance MonadHeap value (m effects)             => MonadHeap value (Collecting m effects)
-deriving instance MonadModuleTable term value (m effects) => MonadModuleTable term value (Collecting m effects)
+deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (Collecting m effects)
+deriving instance MonadHeap location value (m effects)             => MonadHeap location value (Collecting m effects)
+deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Collecting m effects)

 instance ( Effectful m
-         , Member (Reader (Live (LocationFor value) value)) effects
-         , MonadEvaluator term value (m effects)
+         , Member (Reader (Live location value)) effects
+         , MonadEvaluator location term value (m effects)
         )
-      => MonadEvaluator term value (Collecting m effects) where
+      => MonadEvaluator location term value (Collecting m effects) where
  getConfiguration term = Configuration term <$> askRoots <*> getEnv <*> getHeap

  askModuleStack = Collecting askModuleStack


 instance ( Effectful m
-         , Foldable (Cell (LocationFor value))
-         , Member (Reader (Live (LocationFor value) value)) effects
-         , MonadAnalysis term value (m effects)
-         , Ord (LocationFor value)
-         , ValueRoots value
+         , Foldable (Cell location)
+         , Member (Reader (Live location value)) effects
+         , MonadAnalysis location term value (m effects)
+         , Ord location
+         , ValueRoots location value
         )
-      => MonadAnalysis term value (Collecting m effects) where
-  type Effects term value (Collecting m effects)
-    = Reader (Live (LocationFor value) value)
-   ': Effects term value (m effects)
+      => MonadAnalysis location term value (Collecting m effects) where
+  type Effects location term value (Collecting m effects)
+    = Reader (Live location value)
+   ': Effects location term value (m effects)

  -- Small-step evaluation which garbage-collects any non-rooted addresses after evaluating each term.
  analyzeTerm recur term = do
@ -51,32 +51,32 @@ instance ( Effectful m


 -- | Retrieve the local 'Live' set.
-askRoots :: (Effectful m, Member (Reader (Live (LocationFor value) value)) effects) => m effects (Live (LocationFor value) value)
+askRoots :: (Effectful m, Member (Reader (Live location value)) effects) => m effects (Live location value)
 askRoots = raise ask

 -- | Run a computation with the given 'Live' set added to the local root set.
-- extraRoots :: (Effectful m, Member (Reader (Live (LocationFor value) value)) effects, Ord (LocationFor value)) => Live (LocationFor value) value -> m effects a -> m effects a
+-- extraRoots :: (Effectful m, Member (Reader (Live location value)) effects, Ord location) => Live location value -> m effects a -> m effects a
 -- extraRoots roots = raise . local (<> roots) . lower


 -- | Collect any addresses in the heap not rooted in or reachable from the given 'Live' set.
-gc :: ( Ord (LocationFor value)
-      , Foldable (Cell (LocationFor value))
-      , ValueRoots value
+gc :: ( Ord location
+      , Foldable (Cell location)
+      , ValueRoots location value
      )
-   => LiveFor value -- ^ The set of addresses to consider rooted.
-   -> HeapFor value -- ^ A heap to collect unreachable addresses within.
-   -> HeapFor value -- ^ A garbage-collected heap.
+   => Live location value -- ^ The set of addresses to consider rooted.
+   -> Heap location value -- ^ A heap to collect unreachable addresses within.
+   -> Heap location value -- ^ A garbage-collected heap.
 gc roots heap = heapRestrict heap (reachable roots heap)

 -- | Compute the set of addresses reachable from a given root set in a given heap.
-reachable :: ( Ord (LocationFor value)
-             , Foldable (Cell (LocationFor value))
-             , ValueRoots value
+reachable :: ( Ord location
+             , Foldable (Cell location)
+             , ValueRoots location value
             )
-          => LiveFor value -- ^ The set of root addresses.
-          -> HeapFor value -- ^ The heap to trace addresses through.
-          -> LiveFor value -- ^ The set of addresses reachable from the root set.
+          => Live location value -- ^ The set of root addresses.
+          -> Heap location value -- ^ The heap to trace addresses through.
+          -> Live location value -- ^ The set of addresses reachable from the root set.
 reachable roots heap = go mempty roots
  where go seen set = case liveSplit set of
          Nothing -> seen
--- a/src/Analysis/Abstract/Dead.hs
+++ b/src/Analysis/Abstract/Dead.hs
@ -14,10 +14,10 @@ newtype DeadCode m (effects :: [* -> *]) a = DeadCode (m effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

 deriving instance MonadControl term (m effects)                    => MonadControl term (DeadCode m effects)
-deriving instance MonadEnvironment value (m effects)      => MonadEnvironment value (DeadCode m effects)
-deriving instance MonadHeap value (m effects)             => MonadHeap value (DeadCode m effects)
-deriving instance MonadModuleTable term value (m effects) => MonadModuleTable term value (DeadCode m effects)
-deriving instance MonadEvaluator term value (m effects)   => MonadEvaluator term value (DeadCode m effects)
+deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (DeadCode m effects)
+deriving instance MonadHeap location value (m effects)             => MonadHeap location value (DeadCode m effects)
+deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (DeadCode m effects)
+deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (DeadCode m effects)

 -- | A set of “dead” (unreachable) terms.
 newtype Dead term = Dead { unDead :: Set term }
@ -42,12 +42,12 @@ instance ( Corecursive term
         , Effectful m
         , Foldable (Base term)
         , Member (State (Dead term)) effects
-         , MonadAnalysis term value (m effects)
+         , MonadAnalysis location term value (m effects)
         , Ord term
         , Recursive term
         )
-         => MonadAnalysis term value (DeadCode m effects) where
-  type Effects term value (DeadCode m effects) = State (Dead term) ': Effects term value (m effects)
+      => MonadAnalysis location term value (DeadCode m effects) where
+  type Effects location term value (DeadCode m effects) = State (Dead term) ': Effects location term value (m effects)

  analyzeTerm recur term = do
    revive (embedSubterm term)
--- a/src/Analysis/Abstract/Evaluating.hs
+++ b/src/Analysis/Abstract/Evaluating.hs
@ -6,80 +6,86 @@ module Analysis.Abstract.Evaluating

 import           Control.Abstract.Analysis
 import           Control.Monad.Effect
+import           Data.Abstract.Address
 import           Data.Abstract.Configuration
-import qualified Data.Abstract.Environment as Env
+import           Data.Abstract.Environment as Env
 import           Data.Abstract.Evaluatable
+import           Data.Abstract.Exports
+import           Data.Abstract.Heap
 import           Data.Abstract.Module
 import           Data.Abstract.ModuleTable
+import           Data.Abstract.Origin
 import qualified Data.IntMap as IntMap
 import           Lens.Micro
 import           Prelude hiding (fail)
 import           Prologue

 -- | An analysis evaluating @term@s to @value@s with a list of @effects@ using 'Evaluatable', and producing incremental results of type @a@.
-newtype Evaluating term value effects a = Evaluating (Eff effects a)
+newtype Evaluating location term value effects a = Evaluating (Eff effects a)
  deriving (Applicative, Functor, Effectful, Monad)

-deriving instance Member Fail   effects => MonadFail   (Evaluating term value effects)
-deriving instance Member Fresh  effects => MonadFresh  (Evaluating term value effects)
-deriving instance Member NonDet effects => Alternative (Evaluating term value effects)
-deriving instance Member NonDet effects => MonadNonDet (Evaluating term value effects)
+deriving instance Member Fail   effects => MonadFail   (Evaluating location term value effects)
+deriving instance Member Fresh  effects => MonadFresh  (Evaluating location term value effects)
+deriving instance Member NonDet effects => Alternative (Evaluating location term value effects)
+deriving instance Member NonDet effects => MonadNonDet (Evaluating location term value effects)

 -- | Effects necessary for evaluating (whether concrete or abstract).
-type EvaluatingEffects term value
+type EvaluatingEffects location term value
  = '[ Resumable (EvalError value)
     , Resumable (LoadError term value)
-     , Resumable (ValueExc value)
+     , Resumable (ValueExc location value)
     , Resumable (Unspecialized value)
     , Fail                                         -- Failure with an error message
+     , Fresh                                        -- For allocating new addresses and/or type variables.
     , Reader [Module term]                         -- The stack of currently-evaluating modules.
+     , Reader Origin                                -- The current term’s origin.
     , Reader (ModuleTable [Module term])           -- Cache of unevaluated modules
-     , Reader (EnvironmentFor value)       -- Default environment used as a fallback in lookupEnv
-     , State  (EvaluatingState term value) -- Environment, heap, modules, exports, and jumps.
+     , Reader (Environment location value)          -- Default environment used as a fallback in lookupEnv
+     , State  (EvaluatingState location term value) -- Environment, heap, modules, exports, and jumps.
     ]

-data EvaluatingState term value = EvaluatingState
-  { environment :: EnvironmentFor value
-  , heap        :: HeapFor value
-  , modules     :: ModuleTable (EnvironmentFor value, value)
-  , exports     :: ExportsFor value
+data EvaluatingState location term value = EvaluatingState
+  { environment :: Environment location value
+  , heap        :: Heap location value
+  , modules     :: ModuleTable (Environment location value, value)
+  , exports     :: Exports location value
  , jumps       :: IntMap.IntMap term
  }

-deriving instance (Eq (CellFor value), Eq (LocationFor value), Eq term, Eq value) => Eq (EvaluatingState term value)
-deriving instance (Ord (CellFor value), Ord (LocationFor value), Ord term, Ord value) => Ord (EvaluatingState term value)
-deriving instance (Show (CellFor value), Show (LocationFor value), Show term, Show value) => Show (EvaluatingState term value)
+deriving instance (Eq (Cell location value), Eq location, Eq term, Eq value) => Eq (EvaluatingState location term value)
+deriving instance (Ord (Cell location value), Ord location, Ord term, Ord value) => Ord (EvaluatingState location term value)
+deriving instance (Show (Cell location value), Show location, Show term, Show value) => Show (EvaluatingState location term value)

-instance (Ord (LocationFor value), Semigroup (CellFor value)) => Semigroup (EvaluatingState term value) where
+instance (Ord location, Semigroup (Cell location value)) => Semigroup (EvaluatingState location term value) where
  EvaluatingState e1 h1 m1 x1 j1 <> EvaluatingState e2 h2 m2 x2 j2 = EvaluatingState (e1 <> e2) (h1 <> h2) (m1 <> m2) (x1 <> x2) (j1 <> j2)

-instance (Ord (LocationFor value), Semigroup (CellFor value)) => Monoid (EvaluatingState term value) where
+instance (Ord location, Semigroup (Cell location value)) => Monoid (EvaluatingState location term value) where
  mempty = EvaluatingState mempty mempty mempty mempty mempty
  mappend = (<>)

-_environment :: Lens' (EvaluatingState term value) (EnvironmentFor value)
+_environment :: Lens' (EvaluatingState location term value) (Environment location value)
 _environment = lens environment (\ s e -> s {environment = e})

-_heap :: Lens' (EvaluatingState term value) (HeapFor value)
+_heap :: Lens' (EvaluatingState location term value) (Heap location value)
 _heap = lens heap (\ s h -> s {heap = h})

-_modules :: Lens' (EvaluatingState term value) (ModuleTable (EnvironmentFor value, value))
+_modules :: Lens' (EvaluatingState location term value) (ModuleTable (Environment location value, value))
 _modules = lens modules (\ s m -> s {modules = m})

-_exports :: Lens' (EvaluatingState term value) (ExportsFor value)
+_exports :: Lens' (EvaluatingState location term value) (Exports location value)
 _exports = lens exports (\ s e -> s {exports = e})

-_jumps :: Lens' (EvaluatingState term value) (IntMap.IntMap term)
+_jumps :: Lens' (EvaluatingState location term value) (IntMap.IntMap term)
 _jumps = lens jumps (\ s j -> s {jumps = j})


-(.=) :: Member (State (EvaluatingState term value)) effects => ASetter (EvaluatingState term value) (EvaluatingState term value) a b -> b -> Evaluating term value effects ()
+(.=) :: Member (State (EvaluatingState location term value)) effects => ASetter (EvaluatingState location term value) (EvaluatingState location term value) a b -> b -> Evaluating location term value effects ()
 lens .= val = raise (modify' (lens .~ val))

-view :: Member (State (EvaluatingState term value)) effects => Getting a (EvaluatingState term value) a -> Evaluating term value effects a
+view :: Member (State (EvaluatingState location term value)) effects => Getting a (EvaluatingState location term value) a -> Evaluating location term value effects a
 view lens = raise (gets (^. lens))

-localEvaluatingState :: Member (State (EvaluatingState term value)) effects => Lens' (EvaluatingState term value) prj -> (prj -> prj) -> Evaluating term value effects a -> Evaluating term value effects a
+localEvaluatingState :: Member (State (EvaluatingState location term value)) effects => Lens' (EvaluatingState location term value) prj -> (prj -> prj) -> Evaluating location term value effects a -> Evaluating location term value effects a
 localEvaluatingState lens f action = do
  original <- view lens
  lens .= f original
@ -87,7 +93,7 @@ localEvaluatingState lens f action = do
  v <$ lens .= original


-instance Members '[Fail, State (EvaluatingState term value)] effects => MonadControl term (Evaluating term value effects) where
+instance Members '[Fail, State (EvaluatingState location term value)] effects => MonadControl term (Evaluating location term value effects) where
  label term = do
    m <- view _jumps
    let i = IntMap.size m
@ -96,10 +102,10 @@ instance Members '[Fail, State (EvaluatingState term value)] effects => MonadCon

  goto label = IntMap.lookup label <$> view _jumps >>= maybe (fail ("unknown label: " <> show label)) pure

-instance Members '[ State (EvaluatingState term value)
-                  , Reader (EnvironmentFor value)
+instance Members '[ State (EvaluatingState location term value)
+                  , Reader (Environment location value)
                  ] effects
-      => MonadEnvironment value (Evaluating term value effects) where
+      => MonadEnvironment location value (Evaluating location term value effects) where
  getEnv = view _environment
  putEnv = (_environment .=)
  withEnv s = localEvaluatingState _environment (const s)
@ -116,31 +122,40 @@ instance Members '[ State (EvaluatingState term value)
    result <- a
    result <$ modifyEnv Env.pop

-instance Member (State (EvaluatingState term value)) effects => MonadHeap value (Evaluating term value effects) where
+instance Member (State (EvaluatingState location term value)) effects
+      => MonadHeap location value (Evaluating location term value effects) where
  getHeap = view _heap
  putHeap = (_heap .=)

-instance Members '[Reader (ModuleTable [Module term]), State (EvaluatingState term value)] effects => MonadModuleTable term value (Evaluating term value effects) where
+instance Members '[Reader (ModuleTable [Module term]), State (EvaluatingState location term value)] effects
+      => MonadModuleTable location term value (Evaluating location term value effects) where
  getModuleTable = view _modules
  putModuleTable = (_modules .=)

  askModuleTable = raise ask
  localModuleTable f a = raise (local f (lower a))

-instance Members (EvaluatingEffects term value) effects => MonadEvaluator term value (Evaluating term value effects) where
+instance Members (EvaluatingEffects location term value) effects
+      => MonadEvaluator location term value (Evaluating location term value effects) where
  getConfiguration term = Configuration term mempty <$> getEnv <*> getHeap

  askModuleStack = raise ask

-instance ( Members (EvaluatingEffects term value) effects
-         , MonadValue value (Evaluating term value effects)
+instance ( Members (EvaluatingEffects location term value) effects
+         , MonadValue location value (Evaluating location term value effects)
+         , HasOrigin (Base term)
         )
-         => MonadAnalysis term value (Evaluating term value effects) where
-  type Effects term value (Evaluating term value effects) = EvaluatingEffects term value
+      => MonadAnalysis location term value (Evaluating location term value effects) where
+  type Effects location term value (Evaluating location term value effects) = EvaluatingEffects location term value

-  analyzeTerm = id
+  analyzeTerm eval term = do
+    ms <- askModuleStack
+    pushOrigin (originFor ms term) (eval term)

  analyzeModule eval m = pushModule (subterm <$> m) (eval m)

-pushModule :: Member (Reader [Module term]) effects => Module term -> Evaluating term value effects a -> Evaluating term value effects a
+pushModule :: Member (Reader [Module term]) effects => Module term -> Evaluating location term value effects a -> Evaluating location term value effects a
 pushModule m = raise . local (m :) . lower
+
+pushOrigin :: Member (Reader Origin) effects => Origin -> Evaluating location term value effects a -> Evaluating location term value effects a
+pushOrigin o = raise . local (const o) . lower
--- a/src/Analysis/Abstract/ImportGraph.hs
+++ b/src/Analysis/Abstract/ImportGraph.hs
@ -27,19 +27,19 @@ newtype ImportGraphing m (effects :: [* -> *]) a = ImportGraphing (m effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

 deriving instance MonadControl term (m effects)                    => MonadControl term (ImportGraphing m effects)
-deriving instance MonadEnvironment value (m effects)      => MonadEnvironment value (ImportGraphing m effects)
-deriving instance MonadHeap value (m effects)             => MonadHeap value (ImportGraphing m effects)
-deriving instance MonadModuleTable term value (m effects) => MonadModuleTable term value (ImportGraphing m effects)
-deriving instance MonadEvaluator term value (m effects)   => MonadEvaluator term value (ImportGraphing m effects)
+deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (ImportGraphing m effects)
+deriving instance MonadHeap location value (m effects)             => MonadHeap location value (ImportGraphing m effects)
+deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (ImportGraphing m effects)
+deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (ImportGraphing m effects)


 instance ( Effectful m
         , Member (State ImportGraph) effects
-         , MonadAnalysis term value (m effects)
+         , MonadAnalysis location term value (m effects)
         , Member (Resumable (LoadError term value)) effects
         )
-         => MonadAnalysis term value (ImportGraphing m effects) where
-  type Effects term value (ImportGraphing m effects) = State ImportGraph ': Effects term value (m effects)
+      => MonadAnalysis location term value (ImportGraphing m effects) where
+  type Effects location term value (ImportGraphing m effects) = State ImportGraph ': Effects location term value (m effects)

  analyzeTerm eval term = resumeException
                            @(LoadError term value)
@ -52,7 +52,7 @@ instance ( Effectful m

 insertVertexName :: (Effectful m
                   , Member (State ImportGraph) effects
-                   , MonadEvaluator term value (m effects))
+                   , MonadEvaluator location term value (m effects))
                 => NonEmpty ByteString
                 -> ImportGraphing m effects ()
 insertVertexName name = do
--- a/src/Analysis/Abstract/Quiet.hs
+++ b/src/Analysis/Abstract/Quiet.hs
@ -18,18 +18,18 @@ newtype Quietly m (effects :: [* -> *]) a = Quietly (m effects a)
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

 deriving instance MonadControl term (m effects)                    => MonadControl term (Quietly m effects)
-deriving instance MonadEnvironment value (m effects)      => MonadEnvironment value (Quietly m effects)
-deriving instance MonadHeap value (m effects)             => MonadHeap value (Quietly m effects)
-deriving instance MonadModuleTable term value (m effects) => MonadModuleTable term value (Quietly m effects)
-deriving instance MonadEvaluator term value (m effects)   => MonadEvaluator term value (Quietly m effects)
+deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (Quietly m effects)
+deriving instance MonadHeap location value (m effects)             => MonadHeap location value (Quietly m effects)
+deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Quietly m effects)
+deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (Quietly m effects)

 instance ( Effectful m
         , Member (Resumable (Unspecialized value)) effects
-         , MonadAnalysis term value (m effects)
-         , MonadValue value (Quietly m effects)
+         , MonadAnalysis location term value (m effects)
+         , MonadValue location value (Quietly m effects)
         )
-      => MonadAnalysis term value (Quietly m effects) where
-  type Effects term value (Quietly m effects) = Effects term value (m effects)
+      => MonadAnalysis location term value (Quietly m effects) where
+  type Effects location term value (Quietly m effects) = Effects location term value (m effects)

  analyzeTerm eval term = resumeException @(Unspecialized value) (liftAnalyze analyzeTerm eval term) (\yield (Unspecialized _) -> unit >>= yield)

--- a/src/Analysis/Abstract/Tracing.hs
+++ b/src/Analysis/Abstract/Tracing.hs
@ -5,6 +5,7 @@ module Analysis.Abstract.Tracing

 import Control.Abstract.Analysis
 import Control.Monad.Effect.Writer
+import Data.Abstract.Configuration
 import Data.Semigroup.Reducer as Reducer
 import Data.Union
 import Prologue
@ -16,24 +17,24 @@ newtype Tracing (trace :: * -> *) m (effects :: [* -> *]) a = Tracing (m effects
  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

 deriving instance MonadControl term (m effects)                    => MonadControl term (Tracing trace m effects)
-deriving instance MonadEnvironment value (m effects)      => MonadEnvironment value (Tracing trace m effects)
-deriving instance MonadHeap value (m effects)             => MonadHeap value (Tracing trace m effects)
-deriving instance MonadModuleTable term value (m effects) => MonadModuleTable term value (Tracing trace m effects)
-deriving instance MonadEvaluator term value (m effects)   => MonadEvaluator term value (Tracing trace m effects)
+deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (Tracing trace m effects)
+deriving instance MonadHeap location value (m effects)             => MonadHeap location value (Tracing trace m effects)
+deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Tracing trace m effects)
+deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (Tracing trace m effects)

 instance ( Corecursive term
         , Effectful m
-         , Member (Writer (trace (ConfigurationFor term value))) effects
-         , MonadAnalysis term value (m effects)
-         , Ord (LocationFor value)
-         , Reducer (ConfigurationFor term value) (trace (ConfigurationFor term value))
+         , Member (Writer (trace (Configuration location term value))) effects
+         , MonadAnalysis location term value (m effects)
+         , Ord location
+         , Reducer (Configuration location term value) (trace (Configuration location term value))
         )
-         => MonadAnalysis term value (Tracing trace m effects) where
-  type Effects term value (Tracing trace m effects) = Writer (trace (ConfigurationFor term value)) ': Effects term value (m effects)
+      => MonadAnalysis location term value (Tracing trace m effects) where
+  type Effects location term value (Tracing trace m effects) = Writer (trace (Configuration location term value)) ': Effects location term value (m effects)

  analyzeTerm recur term = do
    config <- getConfiguration (embedSubterm term)
-    raise (tell @(trace (ConfigurationFor term value)) (Reducer.unit config))
+    raise (tell @(trace (Configuration location term value)) (Reducer.unit config))
    liftAnalyze analyzeTerm recur term

  analyzeModule = liftAnalyze analyzeModule
--- a/src/Control/Abstract/Addressable.hs
+++ b/src/Control/Abstract/Addressable.hs
@ -1,39 +1,39 @@
-{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
 module Control.Abstract.Addressable where

 import Control.Abstract.Evaluator
 import Control.Applicative
-import Control.Monad ((<=<))
+import Control.Effect.Fresh
 import Data.Abstract.Address
 import Data.Abstract.Environment (insert)
 import Data.Abstract.FreeVariables
-import Data.Abstract.Heap
 import Data.Semigroup.Reducer
 import Prelude hiding (fail)
 import Prologue

 -- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Heap.
-class (Monad m, Ord l, l ~ LocationFor value, Reducer value (Cell l value)) => MonadAddressable l value m where
-  deref :: Address l value -> m value
+class (MonadFresh m, Ord location) => MonadAddressable location m where
+  derefCell :: Address location value -> Cell location value -> m value

-  alloc :: Name -> m (Address l value)
+  allocLoc :: Name -> m location

 -- | Look up or allocate an address for a 'Name'.
-lookupOrAlloc :: ( MonadAddressable (LocationFor value) value m
-                 , MonadEnvironment value m
+lookupOrAlloc :: ( MonadAddressable location m
+                 , MonadEnvironment location value m
                 )
              => Name
-                 -> m (Address (LocationFor value) value)
+              -> m (Address location value)
 lookupOrAlloc name = lookupEnv name >>= maybe (alloc name) pure


-letrec :: ( MonadAddressable (LocationFor value) value m
-          , MonadEnvironment value m
-          , MonadHeap value m
+letrec :: ( MonadAddressable location m
+          , MonadEnvironment location value m
+          , MonadHeap location value m
+          , Reducer value (Cell location value)
          )
       => Name
       -> m value
-       -> m (value, Address (LocationFor value) value)
+       -> m (value, Address location value)
 letrec name body = do
  addr <- lookupOrAlloc name
  v <- localEnv (insert name addr) body
@ -41,11 +41,11 @@ letrec name body = do
  pure (v, addr)

 -- Lookup/alloc a name passing the address to a body evaluated in a new local environment.
-letrec' :: ( MonadAddressable (LocationFor value) value m
-           , MonadEnvironment value m
+letrec' :: ( MonadAddressable location m
+           , MonadEnvironment location value m
           )
        => Name
-        -> (Address (LocationFor value) value -> m value)
+        -> (Address location value -> m value)
        -> m value
 letrec' name body = do
  addr <- lookupOrAlloc name
@ -55,22 +55,22 @@ letrec' name body = do
 -- Instances

 -- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
-instance (MonadFail m, LocationFor value ~ Precise, MonadHeap value m) => MonadAddressable Precise value m where
-  deref = derefWith (maybeM uninitializedAddress . unLatest)
-  alloc _ = do
-    -- Compute the next available address in the heap, then write an empty value into it.
-    addr <- fmap (Address . Precise . heapSize) getHeap
-    addr <$ modifyHeap (heapInit addr mempty)
+instance (MonadFail m, MonadFresh m) => MonadAddressable Precise m where
+  derefCell addr = maybeM (uninitializedAddress addr) . unLatest
+  allocLoc _ = Precise <$> fresh

 -- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
-instance (Alternative m, LocationFor value ~ Monovariant, MonadFail m, MonadHeap value m, Ord value) => MonadAddressable Monovariant value m where
-  deref = derefWith (foldMapA pure)
-  alloc = pure . Address . Monovariant
+instance (Alternative m, MonadFresh m) => MonadAddressable Monovariant m where
+  derefCell _ = foldMapA pure
+  allocLoc = pure . Monovariant

-- | Dereference the given 'Address' in the heap, using the supplied function to act on the cell, or failing if the address is uninitialized.
-derefWith :: (MonadFail m, MonadHeap value m, Ord (LocationFor value)) => (CellFor value -> m a) -> Address (LocationFor value) value -> m a
-derefWith with = maybe uninitializedAddress with <=< lookupHeap
+-- | Dereference the given 'Address'in the heap, or fail if the address is uninitialized.
+deref :: (MonadFail m, MonadAddressable location m, MonadHeap location value m, Show location) => Address location value -> m value
+deref addr = lookupHeap addr >>= maybe (uninitializedAddress addr) (derefCell addr)
+
+alloc :: MonadAddressable location m => Name -> m (Address location value)
+alloc = fmap Address . allocLoc

 -- | Fail with a message denoting an uninitialized address (i.e. one which was 'alloc'ated, but never 'assign'ed a value before being 'deref'erenced).
-uninitializedAddress :: MonadFail m => m a
-uninitializedAddress = fail "uninitialized address"
+uninitializedAddress :: (MonadFail m, Show location) => Address location value -> m a
+uninitializedAddress addr = fail $ "uninitialized address: " <> show addr
--- a/src/Control/Abstract/Analysis.hs
+++ b/src/Control/Abstract/Analysis.hs
@ -28,9 +28,9 @@ import Prologue
 -- | A 'Monad' in which one can evaluate some specific term type to some specific value type.
 --
 --   This typeclass is left intentionally unconstrained to avoid circular dependencies between it and other typeclasses.
-class MonadEvaluator term value m => MonadAnalysis term value m where
+class MonadEvaluator location term value m => MonadAnalysis location term value m where
  -- | The effects necessary to run the analysis. Analyses which are composed on top of (wrap) other analyses should include the inner analyses 'Effects' in their own list.
-  type family Effects term value m :: [* -> *]
+  type family Effects location term value m :: [* -> *]

  -- | Analyze a term using the semantics of the current analysis.
  analyzeTerm :: (Base term (Subterm term (outer value)) -> m value)
@ -56,8 +56,8 @@ liftAnalyze analyze recur term = coerce (analyze (coerceWith (sym Coercion) . r
 --
 --   This enables us to refer to the analysis type as e.g. @Analysis1 (Analysis2 Evaluating) Term Value@ without explicitly mentioning its effects (which are inferred to be simply its 'Effects').
 runAnalysis :: ( Effectful m
-               , Effects term value (m effects) ~ effects
-               , MonadAnalysis term value (m effects)
+               , Effects location term value (m effects) ~ effects
+               , MonadAnalysis location term value (m effects)
               , RunEffects effects a
               )
            => m effects a
--- a/src/Control/Abstract/Evaluator.hs
+++ b/src/Control/Abstract/Evaluator.hs
@ -15,25 +15,16 @@ module Control.Abstract.Evaluator
  , modifyModuleTable
  , MonadControl(..)
  , MonadThrow(..)
-  -- Type synonyms specialized for location types
-  , CellFor
-  , ConfigurationFor
-  , EnvironmentFor
-  , ExportsFor
-  , HeapFor
-  , LiveFor
-  , LocationFor
  ) where

 import Control.Effect
 import Control.Monad.Effect.Resumable
 import Data.Abstract.Address
 import Data.Abstract.Configuration
-import qualified Data.Abstract.Environment as Env
-import qualified Data.Abstract.Exports as Export
+import Data.Abstract.Environment as Env
+import Data.Abstract.Exports as Export
 import Data.Abstract.FreeVariables
 import Data.Abstract.Heap
-import Data.Abstract.Live
 import Data.Abstract.Module
 import Data.Abstract.ModuleTable
 import Data.Semigroup.Reducer
@ -46,14 +37,14 @@ import Prologue hiding (throwError)
 --   - a heap mapping addresses to (possibly sets of) values
 --   - tables of modules available for import
 class ( MonadControl term m
-      , MonadEnvironment value m
+      , MonadEnvironment location value m
      , MonadFail m
-      , MonadModuleTable term value m
-      , MonadHeap value m
+      , MonadModuleTable location term value m
+      , MonadHeap location value m
      )
-      => MonadEvaluator term value m | m -> term, m -> value where
+      => MonadEvaluator location term value m | m -> location, m -> term, m -> value where
  -- | Get the current 'Configuration' with a passed-in term.
-  getConfiguration :: Ord (LocationFor value) => term -> m (ConfigurationFor term value)
+  getConfiguration :: Ord location => term -> m (Configuration location term value)

  -- | Retrieve the stack of modules currently being evaluated.
  --
@ -62,100 +53,100 @@ class ( MonadControl term m


 -- | A 'Monad' abstracting local and global environments.
-class Monad m => MonadEnvironment value m | m -> value where
+class Monad m => MonadEnvironment location value m | m -> value, m -> location where
  -- | Retrieve the environment.
-  getEnv :: m (EnvironmentFor value)
+  getEnv :: m (Environment location value)
  -- | Set the environment.
-  putEnv :: EnvironmentFor value -> m ()
+  putEnv :: Environment location value -> m ()
  -- | Sets the environment for the lifetime of the given action.
-  withEnv :: EnvironmentFor value -> m a -> m a
+  withEnv :: Environment location value -> m a -> m a

  -- | Retrieve the default environment.
-  defaultEnvironment :: m (EnvironmentFor value)
+  defaultEnvironment :: m (Environment location value)

  -- | Set the default environment for the lifetime of an action.
  --   Usually only invoked in a top-level evaluation function.
-  withDefaultEnvironment :: EnvironmentFor value -> m a -> m a
+  withDefaultEnvironment :: Environment location value -> m a -> m a

  -- | Get the global export state.
-  getExports :: m (ExportsFor value)
+  getExports :: m (Exports location value)
  -- | Set the global export state.
-  putExports :: ExportsFor value -> m ()
+  putExports :: Exports location value -> m ()
  -- | Sets the global export state for the lifetime of the given action.
-  withExports :: ExportsFor value -> m a -> m a
+  withExports :: Exports location value -> m a -> m a

  -- | Run an action with a locally-modified environment.
-  localEnv :: (EnvironmentFor value -> EnvironmentFor value) -> m a -> m a
+  localEnv :: (Environment location value -> Environment location value) -> m a -> m a

  -- | Look a 'Name' up in the current environment, trying the default environment if no value is found.
-  lookupEnv :: Name -> m (Maybe (Address (LocationFor value) value))
+  lookupEnv :: Name -> m (Maybe (Address location value))
  lookupEnv name = (<|>) <$> (Env.lookup name <$> getEnv) <*> (Env.lookup name <$> defaultEnvironment)

  -- | Look up a 'Name' in the environment, running an action with the resolved address (if any).
-  lookupWith :: (Address (LocationFor value) value -> m value) -> Name -> m (Maybe value)
+  lookupWith :: (Address location value -> m value) -> Name -> m (Maybe value)
  lookupWith with name = do
    addr <- lookupEnv name
    maybe (pure Nothing) (fmap Just . with) addr

 -- | Run a computation in a new local environment.
-localize :: MonadEnvironment value m => m a -> m a
+localize :: MonadEnvironment location value m => m a -> m a
 localize = localEnv id

 -- | Update the global environment.
-modifyEnv :: MonadEnvironment value m => (EnvironmentFor value -> EnvironmentFor value) -> m ()
+modifyEnv :: MonadEnvironment location value m => (Environment location value -> Environment location value) -> m ()
 modifyEnv f = do
  env <- getEnv
  putEnv $! f env

 -- | Update the global export state.
-modifyExports :: MonadEnvironment value m => (ExportsFor value -> ExportsFor value) -> m ()
+modifyExports :: MonadEnvironment location value m => (Exports location value -> Exports location value) -> m ()
 modifyExports f = do
  exports <- getExports
  putExports $! f exports

 -- | Add an export to the global export state.
-addExport :: MonadEnvironment value m => Name -> Name -> Maybe (Address (LocationFor value) value) -> m ()
+addExport :: MonadEnvironment location value m => Name -> Name -> Maybe (Address location value) -> m ()
 addExport name alias = modifyExports . Export.insert name alias

 -- | Obtain an environment that is the composition of the current and default environments.
 --   Useful for debugging.
-fullEnvironment :: MonadEnvironment value m => m (EnvironmentFor value)
+fullEnvironment :: MonadEnvironment location value m => m (Environment location value)
 fullEnvironment = mappend <$> getEnv <*> defaultEnvironment

 -- | A 'Monad' abstracting a heap of values.
-class Monad m => MonadHeap value m | m -> value where
+class Monad m => MonadHeap location value m | m -> value, m -> location where
  -- | Retrieve the heap.
-  getHeap :: m (HeapFor value)
+  getHeap :: m (Heap location value)
  -- | Set the heap.
-  putHeap :: HeapFor value -> m ()
+  putHeap :: Heap location value -> m ()

 -- | Update the heap.
-modifyHeap :: MonadHeap value m => (HeapFor value -> HeapFor value) -> m ()
+modifyHeap :: MonadHeap location value m => (Heap location value -> Heap location value) -> m ()
 modifyHeap f = do
  s <- getHeap
  putHeap $! f s

 -- | Look up the cell for the given 'Address' in the 'Heap'.
-lookupHeap :: (MonadHeap value m, Ord (LocationFor value)) => Address (LocationFor value) value -> m (Maybe (CellFor value))
+lookupHeap :: (MonadHeap location value m, Ord location) => Address location value -> m (Maybe (Cell location value))
 lookupHeap = flip fmap getHeap . heapLookup

 -- | Write a value to the given 'Address' in the 'Store'.
-assign :: ( Ord (LocationFor value)
-          , MonadHeap value m
-          , Reducer value (CellFor value)
+assign :: ( Ord location
+          , MonadHeap location value m
+          , Reducer value (Cell location value)
          )
-       => Address (LocationFor value) value
+       => Address location value
       -> value
       -> m ()
 assign address = modifyHeap . heapInsert address


 -- | A 'Monad' abstracting tables of modules available for import.
-class Monad m => MonadModuleTable term value m | m -> term, m -> value where
+class Monad m => MonadModuleTable location term value m | m -> location, m -> term, m -> value where
  -- | Retrieve the table of evaluated modules.
-  getModuleTable :: m (ModuleTable (EnvironmentFor value, value))
+  getModuleTable :: m (ModuleTable (Environment location value, value))
  -- | Set the table of evaluated modules.
-  putModuleTable :: ModuleTable (EnvironmentFor value, value) -> m ()
+  putModuleTable :: ModuleTable (Environment location value, value) -> m ()

  -- | Retrieve the table of unevaluated modules.
  askModuleTable :: m (ModuleTable [Module term])
@ -163,7 +154,7 @@ class Monad m => MonadModuleTable term value m | m -> term, m -> value where
  localModuleTable :: (ModuleTable [Module term] -> ModuleTable [Module term]) -> m a -> m a

 -- | Update the evaluated module table.
-modifyModuleTable :: MonadModuleTable term value m => (ModuleTable (EnvironmentFor value, value) -> ModuleTable (EnvironmentFor value, value)) -> m ()
+modifyModuleTable :: MonadModuleTable location term value m => (ModuleTable (Environment location value, value) -> ModuleTable (Environment location value, value)) -> m ()
 modifyModuleTable f = do
  table <- getModuleTable
  putModuleTable $! f table
@ -185,25 +176,3 @@ class Monad m => MonadThrow exc m where

 instance (Effectful m, Members '[Resumable exc] effects, Monad (m effects)) => MonadThrow exc (m effects) where
  throwException = raise . throwError
-
-
-- | The cell for an abstract value type.
-type CellFor value = Cell (LocationFor value) value
-
-- | The configuration for term and abstract value types.
-type ConfigurationFor term value = Configuration (LocationFor value) term value
-
-- | The environment for an abstract value type.
-type EnvironmentFor value = Env.Environment (LocationFor value) value
-
-- | The exports for an abstract value type.
-type ExportsFor value = Export.Exports (LocationFor value) value
-
-- | The 'Heap' for an abstract value type.
-type HeapFor value = Heap (LocationFor value) value
-
-- | The address set type for an abstract value type.
-type LiveFor value = Live (LocationFor value) value
-
-- | The location type (the body of 'Address'es) which should be used for an abstract value type.
-type family LocationFor value :: *
--- a/src/Control/Abstract/Value.hs
+++ b/src/Control/Abstract/Value.hs
@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, MultiParamTypeClasses, Rank2Types, TypeFamilies, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE FunctionalDependencies, GADTs, Rank2Types, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Control.Abstract.Value
 ( MonadValue(..)
 , Comparator(..)
@ -9,20 +9,14 @@ module Control.Abstract.Value
 , makeNamespace
 , ValueRoots(..)
 , ValueExc(..)
-, EnvironmentFor
-, ExportsFor
-, HeapFor
-, CellFor
-, LiveFor
-, LocationFor
-, ConfigurationFor
 ) where

 import Control.Abstract.Evaluator
 import Data.Abstract.FreeVariables
 import Data.Abstract.Environment as Env
-import Data.Abstract.Address (Address)
+import Data.Abstract.Address (Address, Cell)
 import Data.Abstract.Number as Number
+import Data.Abstract.Live (Live)
 import Data.Scientific (Scientific)
 import Data.Semigroup.Reducer hiding (unit)
 import Prelude
@ -41,7 +35,7 @@ data Comparator
 -- | A 'Monad' abstracting the evaluation of (and under) binding constructs (functions, methods, etc).
 --
 --   This allows us to abstract the choice of whether to evaluate under binders for different value types.
-class (Monad m, Show value) => MonadValue value m where
+class (Monad m, Show value) => MonadValue location value m | m value -> location where
  -- | Construct an abstract unit value.
  --   TODO: This might be the same as the empty tuple for some value types
  unit :: m value
@ -116,18 +110,18 @@ class (Monad m, Show value) => MonadValue value m where
  -- | Build a class value from a name and environment.
  klass :: Name                       -- ^ The new class's identifier
        -> [value]                    -- ^ A list of superclasses
-        -> EnvironmentFor value -- ^ The environment to capture
+        -> Environment location value -- ^ The environment to capture
        -> m value

  -- | Build a namespace value from a name and environment stack
  --
  -- Namespaces model closures with monoidal environments.
  namespace :: Name                       -- ^ The namespace's identifier
-            -> EnvironmentFor value -- ^ The environment to mappend
+            -> Environment location value -- ^ The environment to mappend
            -> m value

  -- | Extract the environment from any scoped object (e.g. classes, namespaces, etc).
-  scopedEnvironment :: value -> m (EnvironmentFor value)
+  scopedEnvironment :: value -> m (Environment location value)

  -- | Evaluate an abstraction (a binder like a lambda or method definition).
  abstract :: (FreeVariables term, MonadControl term m) => [Name] -> Subterm term (m value) -> m value
@ -141,10 +135,10 @@ class (Monad m, Show value) => MonadValue value m where


 -- | Attempt to extract a 'Prelude.Bool' from a given value.
-toBool :: MonadValue value m => value -> m Bool
+toBool :: MonadValue location value m => value -> m Bool
 toBool v = ifthenelse v (pure True) (pure False)

-forLoop :: (MonadEnvironment value m, MonadValue value m)
+forLoop :: (MonadEnvironment location value m, MonadValue location value m)
        => m value -- ^ Initial statement
        -> m value -- ^ Condition
        -> m value -- ^ Increment/stepper
@ -154,7 +148,7 @@ forLoop initial cond step body =
  localize (initial *> while cond (body *> step))

 -- | The fundamental looping primitive, built on top of ifthenelse.
-while :: MonadValue value m
+while :: MonadValue location value m
      => m value
      -> m value
      -> m value
@ -163,7 +157,7 @@ while cond body = loop $ \ continue -> do
  ifthenelse this (body *> continue) unit

 -- | Do-while loop, built on top of while.
-doWhile :: MonadValue value m
+doWhile :: MonadValue location value m
        => m value
        -> m value
        -> m value
@ -171,14 +165,14 @@ doWhile body cond = loop $ \ continue -> body *> do
  this <- cond
  ifthenelse this continue unit

-makeNamespace :: ( MonadValue value m
-                 , MonadEnvironment value m
-                 , MonadHeap value m
-                 , Reducer value (CellFor value)
-                 , Ord (LocationFor value)
+makeNamespace :: ( MonadValue location value m
+                 , MonadEnvironment location value m
+                 , MonadHeap location value m
+                 , Ord location
+                 , Reducer value (Cell location value)
                 )
              => Name
-              -> Address (LocationFor value) value
+              -> Address location value
              -> [value]
              -> m value
 makeNamespace name addr supers = do
@ -189,25 +183,25 @@ makeNamespace name addr supers = do


 -- | Value types, e.g. closures, which can root a set of addresses.
-class ValueRoots value where
+class ValueRoots location value where
  -- | Compute the set of addresses rooted by a given value.
-  valueRoots :: value -> LiveFor value
+  valueRoots :: value -> Live location value


 -- The type of exceptions that can be thrown when constructing values in `MonadValue`.
-data ValueExc value resume where
-  TypeError              :: Prelude.String -> ValueExc value value
-  StringError            :: Prelude.String -> ValueExc value ByteString
-  NamespaceError         :: Prelude.String -> ValueExc value (EnvironmentFor value)
-  ScopedEnvironmentError :: Prelude.String -> ValueExc value (EnvironmentFor value)
+data ValueExc location value resume where
+  TypeError              :: Prelude.String -> ValueExc location value value
+  StringError            :: Prelude.String -> ValueExc location value ByteString
+  NamespaceError         :: Prelude.String -> ValueExc location value (Environment location value)
+  ScopedEnvironmentError :: Prelude.String -> ValueExc location value (Environment location value)

-instance Eq1 (ValueExc value) where
+instance Eq1 (ValueExc location value) where
  liftEq _ (TypeError a)  (TypeError b)                          = a == b
  liftEq _ (StringError a) (StringError b)                       = a == b
  liftEq _ (NamespaceError a) (NamespaceError b)                 = a == b
  liftEq _ (ScopedEnvironmentError a) (ScopedEnvironmentError b) = a == b
  liftEq _ _             _                                       = False

-deriving instance Show (ValueExc value resume)
-instance Show1 (ValueExc value) where
+deriving instance Show (ValueExc location value resume)
+instance Show1 (ValueExc location value) where
  liftShowsPrec _ _ = showsPrec
--- a/src/Control/Effect/Fresh.hs
+++ b/src/Control/Effect/Fresh.hs
@ -4,22 +4,20 @@ module Control.Effect.Fresh where
 import Control.Effect
 import Control.Monad.Effect.Internal

-type TName = Int
-
 -- | An effect offering a (resettable) sequence of always-incrementing, and therefore “fresh,” type variables.
 data Fresh a where
  -- | Request a reset of the sequence of variable names.
-  Reset :: TName -> Fresh ()
+  Reset :: Int -> Fresh ()
  -- | Request a fresh variable name.
-  Fresh :: Fresh TName
+  Fresh :: Fresh Int

 -- | 'Monad's offering a (resettable) sequence of guaranteed-fresh type variables.
 class Monad m => MonadFresh m where
  -- | Get a fresh variable name, guaranteed unused (since the last 'reset').
-  fresh :: m TName
+  fresh :: m Int

  -- | Reset the sequence of variable names. Useful to avoid complicated alpha-equivalence comparisons when iteratively recomputing the results of an analysis til convergence.
-  reset :: TName -> m ()
+  reset :: Int -> m ()

 instance (Fresh :< fs) => MonadFresh (Eff fs) where
  fresh = send Fresh
@ -28,6 +26,6 @@ instance (Fresh :< fs) => MonadFresh (Eff fs) where

 -- | 'Fresh' effects are interpreted starting from 0, incrementing the current name with each request for a fresh name, and overwriting the counter on reset.
 instance RunEffect Fresh a where
-  runEffect = relayState (0 :: TName) (const pure) (\ s action k -> case action of
+  runEffect = relayState (0 :: Int) (const pure) (\ s action k -> case action of
    Fresh -> k (succ s) s
    Reset s' -> k s' ())
--- a/src/Data/Abstract/Address.hs
+++ b/src/Data/Abstract/Address.hs
@ -1,4 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, TypeFamilyDependencies #-}
+{-# LANGUAGE TypeFamilies #-}
 module Data.Abstract.Address where

 import Data.Abstract.FreeVariables
@ -14,19 +14,25 @@ instance Ord l => Ord1 (Address l) where liftCompare = genericLiftCompare
 instance Show l => Show1 (Address l) where liftShowsPrec = genericLiftShowsPrec


+class Ord loc => Location loc where
+  -- | The type into which stored values will be written for a given location type.
+  type family Cell loc :: * -> *
+
+
 -- | 'Precise' models precise store semantics where only the 'Latest' value is taken. Everything gets it's own address (always makes a new allocation) which makes for a larger store.
 newtype Precise = Precise { unPrecise :: Int }
  deriving (Eq, Ord, Show)

+instance Location Precise where
+  type Cell Precise = Latest
+
+
 -- | 'Monovariant' models using one address for a particular name. It trackes the set of values that a particular address takes and uses it's name to lookup in the store and only allocation if new.
 newtype Monovariant = Monovariant { unMonovariant :: Name }
  deriving (Eq, Ord, Show)

-
-- | The type into which stored values will be written for a given location type.
-type family Cell l = res | res -> l where
-  Cell Precise = Latest
-  Cell Monovariant = Set
+instance Location Monovariant where
+  type Cell Monovariant = Set


 -- | A cell holding a single value. Writes will replace any prior value.
--- a/src/Data/Abstract/Evaluatable.hs
+++ b/src/Data/Abstract/Evaluatable.hs
@ -17,29 +17,32 @@ module Data.Abstract.Evaluatable

 import           Control.Abstract.Addressable as X
 import           Control.Abstract.Analysis as X
-import qualified Data.Abstract.Environment as Env
+import           Data.Abstract.Address
+import           Data.Abstract.Environment as X
 import qualified Data.Abstract.Exports as Exports
 import           Data.Abstract.FreeVariables as X
 import           Data.Abstract.Module
 import           Data.Abstract.ModuleTable as ModuleTable
 import           Data.Semigroup.App
 import           Data.Semigroup.Foldable
+import           Data.Semigroup.Reducer hiding (unit)
 import           Data.Term
 import           Prelude hiding (fail)
 import           Prologue

-type MonadEvaluatable term value m =
+type MonadEvaluatable location term value m =
  ( Evaluatable (Base term)
  , FreeVariables term
-  , MonadAddressable (LocationFor value) value m
-  , MonadAnalysis term value m
+  , MonadAddressable location m
+  , MonadAnalysis location term value m
  , MonadThrow (Unspecialized value) m
-  , MonadThrow (ValueExc value) m
+  , MonadThrow (ValueExc location value) m
  , MonadThrow (LoadError term value) m
  , MonadThrow (EvalError value) m
-  , MonadValue value m
+  , MonadValue location value m
  , Recursive term
-  , Show (LocationFor value)
+  , Reducer value (Cell location value)
+  , Show location
  )


@ -66,7 +69,7 @@ instance Show1 (EvalError value) where
 instance Eq1 (EvalError term) where
  liftEq _ (FreeVariableError a) (FreeVariableError b) = a == b

-throwLoadError :: MonadEvaluatable term value m => LoadError term value resume -> m resume
+throwLoadError :: MonadEvaluatable location term value m => LoadError term value resume -> m resume
 throwLoadError = throwException

 data Unspecialized a b where
@ -82,7 +85,7 @@ instance Show1 (Unspecialized a) where

 -- | The 'Evaluatable' class defines the necessary interface for a term to be evaluated. While a default definition of 'eval' is given, instances with computational content must implement 'eval' to perform their small-step operational semantics.
 class Evaluatable constr where
-  eval :: MonadEvaluatable term value m
+  eval :: MonadEvaluatable location term value m
       => SubtermAlgebra constr term (m value)
  default eval :: (MonadThrow (Unspecialized value) m, Show1 constr) => SubtermAlgebra constr term (m value)
  eval expr = throwException (Unspecialized ("Eval unspecialized for " ++ liftShowsPrec (const (const id)) (const id) 0 expr ""))
@ -110,17 +113,17 @@ instance Evaluatable [] where
 -- | Require/import another module by name and return it's environment and value.
 --
 -- Looks up the term's name in the cache of evaluated modules first, returns if found, otherwise loads/evaluates the module.
-require :: MonadEvaluatable term value m
+require :: MonadEvaluatable location term value m
        => ModuleName
-        -> m (EnvironmentFor value, value)
+        -> m (Environment location value, value)
 require name = getModuleTable >>= maybe (load name) pure . moduleTableLookup name

 -- | Load another module by name and return it's environment and value.
 --
 -- Always loads/evaluates.
-load :: MonadEvaluatable term value m
+load :: MonadEvaluatable location term value m
     => ModuleName
-     -> m (EnvironmentFor value, value)
+     -> m (Environment location value, value)
 load name = askModuleTable >>= maybe notFound pure . moduleTableLookup name >>= evalAndCache
  where
    notFound = throwLoadError (LoadError name)
@ -141,36 +144,36 @@ load name = askModuleTable >>= maybe notFound pure . moduleTableLookup name >>=
    -- TODO: If the set of exports is empty because no exports have been
    -- defined, do we export all terms, or no terms? This behavior varies across
    -- languages. We need better semantics rather than doing it ad-hoc.
-    filterEnv :: Exports.Exports l a -> Env.Environment l a -> Env.Environment l a
+    filterEnv :: Exports.Exports l a -> Environment l a -> Environment l a
    filterEnv ports env
      | Exports.null ports = env
-      | otherwise = Exports.toEnvironment ports <> Env.overwrite (Exports.aliases ports) env
+      | otherwise = Exports.toEnvironment ports <> overwrite (Exports.aliases ports) env


 -- | Evaluate a term to a value using the semantics of the current analysis.
 --
 --   This should always be called when e.g. evaluating the bodies of closures instead of explicitly folding either 'eval' or 'analyzeTerm' over subterms, except in 'MonadAnalysis' instances themselves. On the other hand, top-level evaluation should be performed using 'evaluateModule'.
-evaluateTerm :: MonadEvaluatable term value m
+evaluateTerm :: MonadEvaluatable location term value m
             => term
             -> m value
 evaluateTerm = foldSubterms (analyzeTerm eval)

 -- | Evaluate a (root-level) term to a value using the semantics of the current analysis. This should be used to evaluate single-term programs, or (via 'evaluateModules') the entry point of multi-term programs.
-evaluateModule :: MonadEvaluatable term value m
+evaluateModule :: MonadEvaluatable location term value m
               => Module term
               -> m value
 evaluateModule m = analyzeModule (subtermValue . moduleBody) (fmap (Subterm <*> evaluateTerm) m)


 -- | Run an action with the a list of 'Module's available for imports.
-withModules :: MonadEvaluatable term value m
+withModules :: MonadEvaluatable location term value m
            => [Module term]
            -> m a
            -> m a
 withModules = localModuleTable . const . ModuleTable.fromList

 -- | Evaluate with a list of modules in scope, taking the head module as the entry point.
-evaluateModules :: MonadEvaluatable term value m
+evaluateModules :: MonadEvaluatable location term value m
                => [Module term]
                -> m value
 evaluateModules []     = fail "evaluateModules: empty list"
--- a/src/Data/Abstract/Located.hs
+++ b/src/Data/Abstract/Located.hs
@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+module Data.Abstract.Located where
+
+import Control.Abstract.Addressable
+import Data.Abstract.Address
+import Data.Abstract.Origin
+
+data Located location = Located { location :: location, origin :: !Origin }
+  deriving (Eq, Ord, Show)
+
+instance Location location => Location (Located location) where
+  type Cell (Located location) = Cell location
+
+instance (MonadAddressable location m, MonadOrigin m) => MonadAddressable (Located location) m where
+  derefCell (Address (Located loc _)) = derefCell (Address loc)
+
+  allocLoc name = Located <$> allocLoc name <*> askOrigin
--- a/src/Data/Abstract/Origin.hs
+++ b/src/Data/Abstract/Origin.hs
@ -0,0 +1,45 @@
+{-# LANGUAGE UndecidableInstances #-}
+module Data.Abstract.Origin where
+
+import Control.Effect
+import Control.Monad.Effect.Reader
+import Data.Abstract.Module
+import Data.Range
+import Data.Record
+import Data.Span
+import Data.Term
+import Prologue
+
+-- TODO: Upstream dependencies
+data Origin
+  = Unknown
+  | Local !ModuleName !FilePath !Range !Span
+  deriving (Eq, Ord, Show)
+
+
+class HasOrigin f where
+  originFor :: [Module a] -> f b -> Origin
+
+instance (HasField fields Range, HasField fields Span) => HasOrigin (TermF syntax (Record fields)) where
+  originFor []    _          = Unknown
+  originFor (m:_) (In ann _) = Local (moduleName m) (modulePath m) (getField ann) (getField ann)
+
+
+class Monad m => MonadOrigin m where
+  askOrigin :: m Origin
+
+instance ( Effectful m
+         , Member (Reader Origin) effects
+         , Monad (m effects)
+         )
+      => MonadOrigin (m effects) where
+  askOrigin = raise ask
+
+
+instance Semigroup Origin where
+  a       <> Unknown = a
+  _       <> b       = b
+
+instance Monoid Origin where
+  mempty = Unknown
+  mappend = (<>)
--- a/src/Data/Abstract/Type.hs
+++ b/src/Data/Abstract/Type.hs
@ -5,9 +5,12 @@ import Control.Abstract.Analysis
 import Data.Abstract.Address
 import Data.Abstract.Environment as Env
 import Data.Align (alignWith)
+import Data.Semigroup.Reducer (Reducer)
 import Prelude hiding (fail)
 import Prologue

+type TName = Int
+
 -- | A datatype representing primitive types and combinations thereof.
 data Type
  = Int                 -- ^ Primitive int type.
@ -43,14 +46,20 @@ unify t1 t2
  | otherwise = fail ("cannot unify " ++ show t1 ++ " with " ++ show t2)


-type instance LocationFor Type = Monovariant
-
-instance ValueRoots Type where
+instance Ord location => ValueRoots location Type where
  valueRoots _ = mempty


 -- | Discard the value arguments (if any), constructing a 'Type' instead.
-instance (Alternative m, MonadEnvironment Type m, MonadFail m, MonadFresh m, MonadHeap Type m) => MonadValue Type m where
+instance ( Alternative m
+         , MonadAddressable location m
+         , MonadEnvironment location Type m
+         , MonadFail m
+         , MonadFresh m
+         , MonadHeap location Type m
+         , Reducer Type (Cell location Type)
+         )
+      => MonadValue location Type m where
  abstract names (Subterm _ body) = do
    (env, tvars) <- foldr (\ name rest -> do
      a <- alloc name
--- a/src/Data/Abstract/Value.hs
+++ b/src/Data/Abstract/Value.hs
@ -2,7 +2,6 @@
 module Data.Abstract.Value where

 import Control.Abstract.Analysis
-import Data.Abstract.Address
 import Data.Abstract.Environment (Environment)
 import qualified Data.Abstract.Environment as Env
 import Data.Abstract.Evaluatable
@ -13,16 +12,16 @@ import Prologue hiding (TypeError)
 import Prelude hiding (Float, Integer, String, Rational, fail)
 import qualified Prelude

-type ValueConstructors
+type ValueConstructors location
  = '[Array
    , Boolean
-    , Class
-    , Closure
+    , Class location
+    , Closure location
    , Float
    , Hash
    , Integer
    , KVPair
-    , Namespace
+    , Namespace location
    , Null
    , Rational
    , String
@ -33,32 +32,32 @@ type ValueConstructors

 -- | Open union of primitive values that terms can be evaluated to.
 --   Fix by another name.
-newtype Value = Value { deValue :: Union ValueConstructors Value }
+newtype Value location = Value { deValue :: Union (ValueConstructors location) (Value location) }
  deriving (Eq, Show, Ord)

 -- | Identical to 'inj', but wraps the resulting sub-entity in a 'Value'.
-injValue :: (f :< ValueConstructors) => f Value -> Value
+injValue :: (f :< ValueConstructors location) => f (Value location) -> Value location
 injValue = Value . inj

 -- | Identical to 'prj', but unwraps the argument out of its 'Value' wrapper.
-prjValue :: (f :< ValueConstructors) => Value -> Maybe (f Value)
+prjValue :: (f :< ValueConstructors location) => Value location -> Maybe (f (Value location))
 prjValue = prj . deValue

 -- | Convenience function for projecting two values.
-prjPair :: (f :< ValueConstructors , g :< ValueConstructors)
-        => (Value, Value)
-        -> Maybe (f Value, g Value)
+prjPair :: (f :< ValueConstructors location , g :< ValueConstructors location)
+        => (Value location, Value location)
+        -> Maybe (f (Value location), g (Value location))
 prjPair = bitraverse prjValue prjValue

 -- TODO: Parameterize Value by the set of constructors s.t. each language can have a distinct value union.

 -- | A function value consisting of a list of parameter 'Name's, a 'Label' to jump to the body of the function, and an 'Environment' of bindings captured by the body.
-data Closure value = Closure [Name] Label (Environment Precise value)
+data Closure location value = Closure [Name] Label (Environment location value)
  deriving (Eq, Generic1, Ord, Show)

-instance Eq1 Closure where liftEq = genericLiftEq
-instance Ord1 Closure where liftCompare = genericLiftCompare
-instance Show1 Closure where liftShowsPrec = genericLiftShowsPrec
+instance Eq location => Eq1 (Closure location) where liftEq = genericLiftEq
+instance Ord location => Ord1 (Closure location) where liftCompare = genericLiftCompare
+instance Show location => Show1 (Closure location) where liftShowsPrec = genericLiftShowsPrec

 -- | The unit value. Typically used to represent the result of imperative statements.
 data Unit value = Unit
@ -138,23 +137,23 @@ instance Show1 Array where liftShowsPrec = genericLiftShowsPrec

 -- | Class values. There will someday be a difference between classes and objects,
 --   but for the time being we're pretending all languages have prototypical inheritance.
-data Class value = Class
+data Class location value = Class
  { _className  :: Name
-  , _classScope :: Environment Precise value
+  , _classScope :: Environment location value
  } deriving (Eq, Generic1, Ord, Show)

-instance Eq1 Class where liftEq = genericLiftEq
-instance Ord1 Class where liftCompare = genericLiftCompare
-instance Show1 Class where liftShowsPrec = genericLiftShowsPrec
+instance Eq location => Eq1 (Class location) where liftEq = genericLiftEq
+instance Ord location => Ord1 (Class location) where liftCompare = genericLiftCompare
+instance Show location => Show1 (Class location) where liftShowsPrec = genericLiftShowsPrec

-data Namespace value = Namespace
+data Namespace location value = Namespace
  { namespaceName  :: Name
-  , namespaceScope :: Environment Precise value
+  , namespaceScope :: Environment location value
  } deriving (Eq, Generic1, Ord, Show)

-instance Eq1 Namespace where liftEq = genericLiftEq
-instance Ord1 Namespace where liftCompare = genericLiftCompare
-instance Show1 Namespace where liftShowsPrec = genericLiftShowsPrec
+instance Eq location => Eq1 (Namespace location) where liftEq = genericLiftEq
+instance Ord location => Ord1 (Namespace location) where liftCompare = genericLiftCompare
+instance Show location => Show1 (Namespace location) where liftShowsPrec = genericLiftShowsPrec

 data KVPair value = KVPair value value
  deriving (Eq, Generic1, Ord, Show)
@ -184,15 +183,14 @@ instance Ord1 Null where liftCompare = genericLiftCompare
 instance Show1 Null where liftShowsPrec = genericLiftShowsPrec


-type instance LocationFor Value = Precise
-
-instance ValueRoots Value where
+instance Ord location => ValueRoots location (Value location) where
  valueRoots v
    | Just (Closure _ _ env) <- prjValue v = Env.addresses env
    | otherwise                            = mempty

+
 -- | Construct a 'Value' wrapping the value arguments (if any).
-instance (Monad m, MonadEvaluatable term Value m) => MonadValue Value m where
+instance (Monad m, MonadEvaluatable location term (Value location) m) => MonadValue location (Value location) m where
  unit     = pure . injValue $ Unit
  integer  = pure . injValue . Integer . Number.Integer
  boolean  = pure . injValue . Boolean
@ -259,7 +257,7 @@ instance (Monad m, MonadEvaluatable term Value m) => MonadValue Value m where
    | otherwise = fail ("Invalid operands to liftNumeric2: " <> show pair)
      where
        -- Dispatch whatever's contained inside a 'Number.SomeNumber' to its appropriate 'MonadValue' ctor
-        specialize :: MonadValue value m => Number.SomeNumber -> m value
+        specialize :: MonadValue location value m => Number.SomeNumber -> m value
        specialize (Number.SomeNumber (Number.Integer i)) = integer i
        specialize (Number.SomeNumber (Number.Ratio r))          = rational r
        specialize (Number.SomeNumber (Number.Decimal d))        = float d
@ -277,7 +275,7 @@ instance (Monad m, MonadEvaluatable term Value m) => MonadValue Value m where
      where
        -- Explicit type signature is necessary here because we're passing all sorts of things
        -- to these comparison functions.
-        go :: (Ord a, MonadValue value m) => a -> a -> m value
+        go :: (Ord a, MonadValue location value m) => a -> a -> m value
        go l r = case comparator of
          Concrete f  -> boolean (f l r)
          Generalized -> integer (orderingToInt (compare l r))
--- a/src/Language/PHP/Syntax.hs
+++ b/src/Language/PHP/Syntax.hs
@ -33,14 +33,14 @@ instance Evaluatable VariableName
 -- file, the complete contents of the included file are treated as though it
 -- were defined inside that function.

-doInclude :: MonadEvaluatable term value m => Subterm t (m value) -> m value
+doInclude :: MonadEvaluatable location term value m => Subterm t (m value) -> m value
 doInclude path = do
  name <- toQualifiedName <$> (subtermValue path >>= asString)
  (importedEnv, v) <- isolate (load name)
  modifyEnv (mappend importedEnv)
  pure v

-doIncludeOnce :: MonadEvaluatable term value m => Subterm t (m value) -> m value
+doIncludeOnce :: MonadEvaluatable location term value m => Subterm t (m value) -> m value
 doIncludeOnce path = do
  name <- toQualifiedName <$> (subtermValue path >>= asString)
  (importedEnv, v) <- isolate (require name)
--- a/src/Language/Ruby/Syntax.hs
+++ b/src/Language/Ruby/Syntax.hs
@ -25,9 +25,9 @@ instance Evaluatable Require where
    where
      toName = qualifiedName . splitOnPathSeparator . dropRelativePrefix . stripQuotes

-doRequire :: MonadEvaluatable term value m
+doRequire :: MonadEvaluatable location term value m
          => ModuleName
-          -> m (EnvironmentFor value, value)
+          -> m (Environment location value, value)
 doRequire name = do
  moduleTable <- getModuleTable
  case moduleTableLookup name moduleTable of
@ -52,7 +52,7 @@ instance Evaluatable Load where
    doLoad path shouldWrap
  eval (Load _) = fail "invalid argument supplied to load, path is required"

-doLoad :: MonadEvaluatable term value m => ByteString -> Bool -> m value
+doLoad :: MonadEvaluatable location term value m => ByteString -> Bool -> m value
 doLoad path shouldWrap = do
  (importedEnv, _) <- isolate (load (toName path))
  unless shouldWrap $ modifyEnv (mappend importedEnv)
--- a/src/Semantic/Util.hs
+++ b/src/Semantic/Util.hs
@ -12,15 +12,17 @@ import Analysis.Abstract.Tracing
 import Analysis.Declaration
 import Control.Abstract.Analysis
 import Control.Monad.IO.Class
-import Data.Abstract.Evaluatable
+import Data.Abstract.Evaluatable hiding (head)
 import Data.Abstract.Address
 import Data.Abstract.Module
+import Data.Abstract.Origin
 import Data.Abstract.Type
 import Data.Abstract.Value
 import Data.Blob
 import Data.Diff
 import Data.Range
 import Data.Record
+import Data.Semigroup.Reducer
 import Data.Span
 import Data.Term
 import Diffing.Algorithm
@ -42,27 +44,27 @@ import qualified Language.TypeScript.Assignment as TypeScript
 -- Ruby
 evaluateRubyFile = evaluateWithPrelude rubyParser
 evaluateRubyFiles = evaluateFilesWithPrelude rubyParser
-evaluateRubyImportGraph paths = runAnalysis @(ImportGraphing (Evaluating Ruby.Term Value)) . evaluateModules <$> parseFiles rubyParser paths
-evaluateRubyBadVariables paths = runAnalysis @(BadVariables (Evaluating Ruby.Term Value)) . evaluateModules <$> parseFiles rubyParser paths
+evaluateRubyImportGraph paths = runAnalysis @(ImportGraphing (Evaluating Precise Ruby.Term (Value Precise))) . evaluateModules <$> parseFiles rubyParser paths
+evaluateRubyBadVariables paths = runAnalysis @(BadVariables (Evaluating Precise Ruby.Term (Value Precise))) . evaluateModules <$> parseFiles rubyParser paths

 -- Go
 evaluateGoFile = evaluateFile goParser
 evaluateGoFiles = evaluateFiles goParser
-typecheckGoFile path = runAnalysis @(Caching (Evaluating Go.Term Type)) . evaluateModule <$> parseFile goParser Nothing path
+typecheckGoFile path = runAnalysis @(Caching (Evaluating Monovariant Go.Term Type)) . evaluateModule <$> parseFile goParser Nothing path

 -- Python
 evaluatePythonFile = evaluateWithPrelude pythonParser
 evaluatePythonFiles = evaluateFilesWithPrelude pythonParser
-typecheckPythonFile path = runAnalysis @(Caching (Evaluating Python.Term Type)) . evaluateModule <$> parseFile pythonParser Nothing path
-tracePythonFile path = runAnalysis @(Tracing [] (Evaluating Python.Term Value)) . evaluateModule <$> parseFile pythonParser Nothing path
-evaluateDeadTracePythonFile path = runAnalysis @(DeadCode (Tracing [] (Evaluating Python.Term Value))) . evaluateModule <$> parseFile pythonParser Nothing path
+typecheckPythonFile path = runAnalysis @(Caching (Evaluating Monovariant Python.Term Type)) . evaluateModule <$> parseFile pythonParser Nothing path
+tracePythonFile path = runAnalysis @(Tracing [] (Evaluating Precise Python.Term (Value Precise))) . evaluateModule <$> parseFile pythonParser Nothing path
+evaluateDeadTracePythonFile path = runAnalysis @(DeadCode (Tracing [] (Evaluating Precise Python.Term (Value Precise)))) . evaluateModule <$> parseFile pythonParser Nothing path

 -- PHP
 evaluatePHPFile = evaluateFile phpParser
 evaluatePHPFiles = evaluateFiles phpParser

 -- TypeScript
-typecheckTypeScriptFile path = runAnalysis @(Caching (Evaluating TypeScript.Term Type)) . evaluateModule <$> parseFile typescriptParser Nothing path
+typecheckTypeScriptFile path = runAnalysis @(Caching (Evaluating Monovariant TypeScript.Term Type)) . evaluateModule <$> parseFile typescriptParser Nothing path
 evaluateTypeScriptFile = evaluateFile typescriptParser
 evaluateTypeScriptFiles = evaluateFiles typescriptParser

@ -70,29 +72,31 @@ evaluateTypeScriptFiles = evaluateFiles typescriptParser
 evaluateFile :: forall term effects
             .  ( Evaluatable (Base term)
                , FreeVariables term
-                , effects ~ Effects term Value (Evaluating term Value effects)
-                , MonadAddressable Precise Value (Evaluating term Value effects)
-                , MonadValue Value (Evaluating term Value effects)
+                , effects ~ Effects Precise term (Value Precise) (Evaluating Precise term (Value Precise) effects)
+                , HasOrigin (Base term)
+                , MonadAddressable Precise (Evaluating Precise term (Value Precise) effects)
                , Recursive term
                )
             => Parser term
             -> FilePath
-             -> IO (Final effects Value)
-evaluateFile parser path = runAnalysis @(Evaluating term Value) . evaluateModule <$> parseFile parser Nothing path
+             -> IO (Final effects (Value Precise))
+evaluateFile parser path = runAnalysis @(Evaluating Precise term (Value Precise)) . evaluateModule <$> parseFile parser Nothing path

-evaluateWith :: forall value term effects
-             .  ( effects ~ Effects term value (Evaluating term value effects)
+evaluateWith :: forall location value term effects
+             .  ( effects ~ Effects location term value (Evaluating location term value effects)
                , Evaluatable (Base term)
                , FreeVariables term
-                , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-                , MonadValue value (Evaluating term value effects)
+                , HasOrigin (Base term)
+                , MonadAddressable location (Evaluating location term value effects)
+                , MonadValue location value (Evaluating location term value effects)
                , Recursive term
-                , Show (LocationFor value)
+                , Reducer value (Cell location value)
+                , Show location
                )
         => Module term
         -> Module term
         -> Final effects value
-evaluateWith prelude m = runAnalysis @(Evaluating term value) $ do
+evaluateWith prelude m = runAnalysis @(Evaluating location term value) $ do
  -- TODO: we could add evaluatePrelude to MonadAnalysis as an alias for evaluateModule,
  -- overridden in Evaluating to not reset the environment. In the future we'll want the
  -- result of evaluating the Prelude to be a build artifact, rather than something that's
@ -104,71 +108,73 @@ evaluateWith prelude m = runAnalysis @(Evaluating term value) $ do
 evaluateWithPrelude :: forall term effects
                    .  ( Evaluatable (Base term)
                       , FreeVariables term
-                       , effects ~ Effects term Value (Evaluating term Value effects)
-                       , MonadAddressable Precise Value (Evaluating term Value effects)
-                       , MonadValue Value (Evaluating term Value effects)
+                       , effects ~ Effects Precise term (Value Precise) (Evaluating Precise term (Value Precise) effects)
+                       , HasOrigin (Base term)
+                       , MonadAddressable Precise (Evaluating Precise term (Value Precise) effects)
                       , Recursive term
                       , TypeLevel.KnownSymbol (PreludePath term)
                       )
                    => Parser term
                    -> FilePath
-                    -> IO (Final effects Value)
+                    -> IO (Final effects (Value Precise))
 evaluateWithPrelude parser path = do
  let preludePath = TypeLevel.symbolVal (Proxy :: Proxy (PreludePath term))
  prelude <- parseFile parser Nothing preludePath
  m <- parseFile parser Nothing path
-  pure $ evaluateWith prelude m
+  pure $ evaluateWith @Precise prelude m


 -- Evaluate a list of files (head of file list is considered the entry point).
 evaluateFiles :: forall term effects
              .  ( Evaluatable (Base term)
                 , FreeVariables term
-                 , effects ~ Effects term Value (Evaluating term Value effects)
-                 , MonadAddressable Precise Value (Evaluating term Value effects)
-                 , MonadValue Value (Evaluating term Value effects)
+                 , effects ~ Effects Precise term (Value Precise) (Evaluating Precise term (Value Precise) effects)
+                 , HasOrigin (Base term)
+                 , MonadAddressable Precise (Evaluating Precise term (Value Precise) effects)
                 , Recursive term
                 )
              => Parser term
              -> [FilePath]
-              -> IO (Final effects Value)
-evaluateFiles parser paths = runAnalysis @(Evaluating term Value) . evaluateModules <$> parseFiles parser paths
+              -> IO (Final effects (Value Precise))
+evaluateFiles parser paths = runAnalysis @(Evaluating Precise term (Value Precise)) . evaluateModules <$> parseFiles parser paths

 -- | Evaluate terms and an entry point to a value with a given prelude.
-evaluatesWith :: forall value term effects
-              .  ( effects ~ Effects term value (Evaluating term value effects)
+evaluatesWith :: forall location value term effects
+              .  ( effects ~ Effects location term value (Evaluating location term value effects)
                 , Evaluatable (Base term)
                 , FreeVariables term
-                 , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-                 , MonadValue value (Evaluating term value effects)
+                 , HasOrigin (Base term)
+                 , MonadAddressable location (Evaluating location term value effects)
+                 , MonadValue location value (Evaluating location term value effects)
                 , Recursive term
-                 , Show (LocationFor value)
+                 , Reducer value (Cell location value)
+                 , Show location
                 )
              => Module term   -- ^ Prelude to evaluate once
              -> [Module term] -- ^ List of (blob, term) pairs that make up the program to be evaluated
              -> Module term   -- ^ Entrypoint
              -> Final effects value
-evaluatesWith prelude modules m = runAnalysis @(Evaluating term value) $ do
+evaluatesWith prelude modules m = runAnalysis @(Evaluating location term value) $ do
  preludeEnv <- evaluateModule prelude *> getEnv
  withDefaultEnvironment preludeEnv (withModules modules (evaluateModule m))

 evaluateFilesWithPrelude :: forall term effects
                         .  ( Evaluatable (Base term)
                            , FreeVariables term
-                            , effects ~ Effects term Value (Evaluating term Value effects)
-                            , MonadAddressable Precise Value (Evaluating term Value effects)
-                            , MonadValue Value (Evaluating term Value effects)
+                            , effects ~ Effects Precise term (Value Precise) (Evaluating Precise term (Value Precise) effects)
+                            , HasOrigin (Base term)
+                            , MonadAddressable Precise (Evaluating Precise term (Value Precise) effects)
                            , Recursive term
                            , TypeLevel.KnownSymbol (PreludePath term)
                            )
                         => Parser term
                         -> [FilePath]
-                         -> IO (Final effects Value)
+                         -> IO (Final effects (Value Precise))
 evaluateFilesWithPrelude parser paths = do
  let preludePath = TypeLevel.symbolVal (Proxy :: Proxy (PreludePath term))
  prelude <- parseFile parser Nothing preludePath
  entry:xs <- traverse (parseFile parser Nothing) paths
-  pure $ evaluatesWith @Value prelude xs entry
+  pure $ evaluatesWith @Precise @(Value Precise) prelude xs entry


 -- Read and parse a file.