mirror of
https://github.com/github/semantic.git
synced 2025-01-04 13:34:31 +03:00
Merge remote-tracking branch 'origin/master' into tuples-and-variable-declarations
This commit is contained in:
commit
ce1a3d1e78
@ -19,7 +19,7 @@ library
|
||||
-- , Analysis.Abstract.Collecting
|
||||
, Analysis.Abstract.Dead
|
||||
, Analysis.Abstract.Evaluating
|
||||
-- , Analysis.Abstract.Tracing
|
||||
, Analysis.Abstract.Tracing
|
||||
, Analysis.ConstructorName
|
||||
, Analysis.CyclomaticComplexity
|
||||
, Analysis.Decorator
|
||||
@ -40,7 +40,6 @@ library
|
||||
, Control.Monad.Effect.Fresh
|
||||
-- , Control.Monad.Effect.GC
|
||||
, Control.Monad.Effect.NonDet
|
||||
-- , Control.Monad.Effect.Trace
|
||||
-- Datatypes for abstract interpretation
|
||||
, Data.Abstract.Address
|
||||
, Data.Abstract.Cache
|
||||
@ -64,6 +63,7 @@ library
|
||||
, Data.Functor.Classes.Generic
|
||||
, Data.JSON.Fields
|
||||
, Data.Language
|
||||
, Data.Map.Monoidal
|
||||
, Data.Mergeable
|
||||
, Data.Output
|
||||
, Data.Patch
|
||||
@ -158,8 +158,8 @@ library
|
||||
, optparse-applicative
|
||||
, parallel
|
||||
, parsers
|
||||
, pointed
|
||||
, recursion-schemes
|
||||
, reducers
|
||||
, scientific
|
||||
, split
|
||||
, stm-chans
|
||||
|
@ -1,123 +1,110 @@
|
||||
{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, UndecidableInstances #-}
|
||||
{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
|
||||
module Analysis.Abstract.Caching
|
||||
( evaluateCache )
|
||||
where
|
||||
( type Caching
|
||||
) where
|
||||
|
||||
import Prologue
|
||||
import Data.Monoid (Alt(..))
|
||||
import Control.Abstract.Evaluator
|
||||
import Control.Effect
|
||||
import Control.Monad.Effect.Fail
|
||||
import Control.Monad.Effect.Fresh
|
||||
import Control.Monad.Effect.NonDet
|
||||
import Control.Monad.Effect.Reader
|
||||
import Control.Monad.Effect.State
|
||||
import Data.Abstract.Address
|
||||
import Control.Abstract.Analysis
|
||||
import Data.Abstract.Cache
|
||||
import Data.Abstract.Configuration
|
||||
import Data.Abstract.Environment
|
||||
import Data.Abstract.Evaluatable
|
||||
import Data.Abstract.ModuleTable
|
||||
import Data.Abstract.Live
|
||||
import Data.Abstract.Store
|
||||
import Data.Abstract.Value
|
||||
import qualified Data.Set as Set
|
||||
import Data.Monoid (Alt (..))
|
||||
import Prologue
|
||||
|
||||
-- | The effects necessary for caching analyses.
|
||||
type CachingEffects t v
|
||||
= '[ Fresh -- For 'MonadFresh'.
|
||||
, Reader (Live (LocationFor v) v) -- For 'MonadGC'.
|
||||
, Reader (Environment (LocationFor v) v) -- For 'MonadEnv'.
|
||||
, State (Environment (LocationFor v) v) -- For 'MonadEvaluator'.
|
||||
, Fail -- For 'MonadFail'.
|
||||
, NonDetEff -- For 'Alternative' & 'MonadNonDet'.
|
||||
, State (Store (LocationFor v) v) -- For 'MonadStore'.
|
||||
, Reader (Cache (LocationFor v) t v) -- For reading memoized values.
|
||||
, State (Cache (LocationFor v) t v) -- For writing said values.
|
||||
, Reader (ModuleTable t) -- Cache of unevaluated modules
|
||||
, State (ModuleTable (EnvironmentFor v)) -- Cache of evaluated modules
|
||||
]
|
||||
type CachingEffects term value effects
|
||||
= Fresh -- For 'MonadFresh'.
|
||||
': NonDetEff -- 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.
|
||||
': effects
|
||||
|
||||
newtype CachingAnalysis term value a = CachingAnalysis { runCachingAnalysis :: Evaluator (CachingEffects term value) term value a }
|
||||
deriving (Alternative, Applicative, Functor, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
-- | The cache for term and abstract value types.
|
||||
type CacheFor term value = Cache (LocationFor value) term value
|
||||
|
||||
deriving instance MonadEvaluator term value (CachingAnalysis term value)
|
||||
-- | A (coinductively-)cached analysis suitable for guaranteeing termination of (suitably finitized) analyses over recursive programs.
|
||||
newtype Caching m term value (effects :: [* -> *]) a = Caching (m term value effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
|
||||
-- TODO: reabstract these later on
|
||||
deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (Caching m term value effects)
|
||||
|
||||
askCache :: CachingAnalysis t v (Cache (LocationFor v) t v)
|
||||
askCache = CachingAnalysis (Evaluator ask)
|
||||
-- | 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
|
||||
-- | Look up the set of values for a given configuration in the in-cache.
|
||||
consultOracle :: ConfigurationFor term value -> m (Set (value, StoreFor value))
|
||||
-- | Run an action with the given in-cache.
|
||||
withOracle :: CacheFor term value -> m a -> m a
|
||||
|
||||
localCache :: (Cache (LocationFor v) t v -> Cache (LocationFor v) t v) -> CachingAnalysis t v a -> CachingAnalysis t v a
|
||||
localCache f (CachingAnalysis (Evaluator a)) = CachingAnalysis (Evaluator (local f a))
|
||||
-- | Look up the set of values for a given configuration in the out-cache.
|
||||
lookupCache :: ConfigurationFor term value -> m (Maybe (Set (value, StoreFor value)))
|
||||
-- | Run an action, caching its result and 'Store' under the given configuration.
|
||||
caching :: ConfigurationFor term value -> Set (value, StoreFor value) -> m value -> m value
|
||||
|
||||
asksCache :: (Cache (LocationFor v) t v -> a) -> CachingAnalysis t v a
|
||||
asksCache f = f <$> askCache
|
||||
-- | Run an action starting from an empty out-cache, and return the out-cache afterwards.
|
||||
isolateCache :: m a -> m (CacheFor term value)
|
||||
|
||||
getsCache :: (Cache (LocationFor v) t v -> a) -> CachingAnalysis t v a
|
||||
getsCache f = f <$> getCache
|
||||
instance ( Effectful (m term value)
|
||||
, Members (CachingEffects term value '[]) effects
|
||||
, MonadEvaluator term value (m term value effects)
|
||||
, Ord (CellFor value)
|
||||
, Ord (LocationFor value)
|
||||
, Ord term
|
||||
, Ord value
|
||||
)
|
||||
=> MonadCaching term value (Caching m term value effects) where
|
||||
consultOracle configuration = raise (fromMaybe mempty . cacheLookup configuration <$> ask)
|
||||
withOracle cache = raise . local (const cache) . lower
|
||||
|
||||
getCache :: CachingAnalysis t v (Cache (LocationFor v) t v)
|
||||
getCache = CachingAnalysis (Evaluator get)
|
||||
lookupCache configuration = raise (cacheLookup configuration <$> get)
|
||||
caching configuration values action = do
|
||||
raise (modify (cacheSet configuration values))
|
||||
result <- (,) <$> action <*> getStore
|
||||
raise (modify (cacheInsert configuration result))
|
||||
pure (fst result)
|
||||
|
||||
putCache :: Cache (LocationFor v) t v -> CachingAnalysis t v ()
|
||||
putCache v = CachingAnalysis (Evaluator (put v))
|
||||
|
||||
modifyCache :: (Cache (LocationFor v) t v -> Cache (LocationFor v) t v) -> CachingAnalysis t v ()
|
||||
modifyCache f = fmap f getCache >>= putCache
|
||||
isolateCache action = raise (put (mempty :: CacheFor term value)) *> action *> raise get
|
||||
|
||||
-- | This instance coinductively iterates the analysis of a term until the results converge.
|
||||
instance ( Corecursive t
|
||||
, Ord t
|
||||
, Ord v
|
||||
, Ord (Cell (LocationFor v) v)
|
||||
, Evaluatable (Base t)
|
||||
, Foldable (Cell (LocationFor v))
|
||||
, FreeVariables t
|
||||
, MonadAddressable (LocationFor v) v (CachingAnalysis t v)
|
||||
, MonadValue t v (CachingAnalysis t v)
|
||||
, Recursive t
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
instance ( Corecursive term
|
||||
, Effectful (m term value)
|
||||
, MonadAnalysis term value (m term value effects)
|
||||
, MonadFresh (m term value effects)
|
||||
, MonadNonDet (m term value effects)
|
||||
, Members (CachingEffects term value '[]) effects
|
||||
, Ord (CellFor value)
|
||||
, Ord (LocationFor value)
|
||||
, Ord term
|
||||
, Ord value
|
||||
)
|
||||
=> MonadAnalysis t v (CachingAnalysis t v) where
|
||||
=> MonadAnalysis term value (Caching m term value effects) where
|
||||
-- We require the 'CachingEffects' in addition to the underlying analysis’ 'RequiredEffects'.
|
||||
type RequiredEffects term value (Caching m term value effects) = CachingEffects term value (RequiredEffects term value (m term value effects))
|
||||
|
||||
-- Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache.
|
||||
analyzeTerm e = do
|
||||
c <- getConfiguration (embedSubterm e)
|
||||
cached <- lookupCache c
|
||||
case cached of
|
||||
Just pairs -> scatter pairs
|
||||
Nothing -> do
|
||||
pairs <- consultOracle c
|
||||
caching c pairs (liftAnalyze analyzeTerm e)
|
||||
|
||||
evaluateModule e = do
|
||||
c <- getConfiguration e
|
||||
-- Convergence here is predicated upon an Eq instance, not α-equivalence
|
||||
cache <- converge (\ prevCache -> do
|
||||
putCache (mempty :: Cache (LocationFor v) t v)
|
||||
cache <- converge (\ prevCache -> isolateCache $ do
|
||||
putStore (configurationStore c)
|
||||
-- We need to reset fresh generation so that this invocation converges.
|
||||
reset 0
|
||||
-- This is subtle: though the calling context supports nondeterminism, we want
|
||||
-- to corral all the nondeterminism that happens in this @eval@ invocation, so
|
||||
-- that it doesn't "leak" to the calling context and diverge
|
||||
-- (otherwise this would never complete).
|
||||
_ <- localCache (const prevCache) (gather Set.singleton (memoizeEval e))
|
||||
getCache) mempty
|
||||
-- that it doesn't "leak" to the calling context and diverge (otherwise this
|
||||
-- would never complete). We don’t need to use the values, so we 'gather' the
|
||||
-- nondeterministic values into @()@.
|
||||
withOracle prevCache (gather (const ()) (Caching (evaluateModule e)))) mempty
|
||||
maybe empty scatter (cacheLookup c cache)
|
||||
|
||||
|
||||
-- | Coinductively-cached evaluation.
|
||||
evaluateCache :: forall v term
|
||||
. ( Ord v
|
||||
, Ord term
|
||||
, Ord (LocationFor v)
|
||||
, Ord (Cell (LocationFor v) v)
|
||||
, Corecursive term
|
||||
, Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, Foldable (Cell (LocationFor v))
|
||||
, Functor (Base term)
|
||||
, Recursive term
|
||||
, MonadAddressable (LocationFor v) v (CachingAnalysis term v)
|
||||
, MonadValue term v (CachingAnalysis term v)
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
, ValueRoots (LocationFor v) v
|
||||
)
|
||||
=> term
|
||||
-> Final (CachingEffects term v) v
|
||||
evaluateCache = run @(CachingEffects term v) . runEvaluator . runCachingAnalysis . evaluateTerm
|
||||
|
||||
-- | Iterate a monadic action starting from some initial seed until the results converge.
|
||||
--
|
||||
-- This applies the Kleene fixed-point theorem to finitize a monotone action. cf https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem
|
||||
@ -133,40 +120,6 @@ converge f = loop
|
||||
else
|
||||
loop x'
|
||||
|
||||
-- | Get the current 'Configuration' with a passed-in term.
|
||||
getConfiguration :: Ord (LocationFor v) => t -> CachingAnalysis t v (Configuration (LocationFor v) t v)
|
||||
getConfiguration term = Configuration term mempty <$> askLocalEnv <*> getStore
|
||||
|
||||
-- | Nondeterministically write each of a collection of stores & return their associated results.
|
||||
scatter :: (Alternative m, Foldable t, MonadEvaluator term v m) => t (a, Store (LocationFor v) v) -> m a
|
||||
scatter :: (Alternative m, Foldable t, MonadEvaluator term value m) => t (a, Store (LocationFor value) value) -> m a
|
||||
scatter = getAlt . foldMap (\ (value, store') -> Alt (putStore store' *> pure value))
|
||||
|
||||
-- | Evaluation of a single iteration of an analysis, given a 'MonadCacheIn' instance as an oracle for results and a 'MonadCacheOut' instance to record computed results in.
|
||||
memoizeEval :: forall v term
|
||||
. ( Ord v
|
||||
, Ord term
|
||||
, Ord (LocationFor v)
|
||||
, Ord (Cell (LocationFor v) v)
|
||||
, Corecursive term
|
||||
, Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, Foldable (Cell (LocationFor v))
|
||||
, Functor (Base term)
|
||||
, Recursive term
|
||||
, MonadAddressable (LocationFor v) v (CachingAnalysis term v)
|
||||
, MonadValue term v (CachingAnalysis term v)
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
)
|
||||
=> SubtermAlgebra (Base term) term (CachingAnalysis term v v)
|
||||
memoizeEval e = do
|
||||
c <- getConfiguration (embedSubterm e)
|
||||
cached <- getsCache (cacheLookup c)
|
||||
case cached of
|
||||
Just pairs -> scatter pairs
|
||||
Nothing -> do
|
||||
pairs <- asksCache (fromMaybe mempty . cacheLookup c)
|
||||
modifyCache (cacheSet c pairs)
|
||||
v <- eval e
|
||||
store' <- getStore
|
||||
modifyCache (cacheInsert c (v, store'))
|
||||
pure v
|
||||
|
@ -1,84 +1,52 @@
|
||||
{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, UndecidableInstances #-}
|
||||
module Analysis.Abstract.Dead where
|
||||
{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, TypeFamilies, TypeOperators #-}
|
||||
module Analysis.Abstract.Dead
|
||||
( type DeadCode
|
||||
) where
|
||||
|
||||
import Control.Abstract.Addressable
|
||||
import Control.Abstract.Evaluator
|
||||
import Control.Effect
|
||||
import Control.Monad.Effect.Fail
|
||||
import Control.Monad.Effect.Reader
|
||||
import Control.Monad.Effect.State
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Evaluatable
|
||||
import Data.Abstract.ModuleTable
|
||||
import Data.Abstract.Store
|
||||
import Data.Abstract.Value
|
||||
import Control.Abstract.Analysis
|
||||
import Data.Semigroup.Reducer as Reducer
|
||||
import Data.Set (delete)
|
||||
import Prologue
|
||||
|
||||
-- | The effects necessary for dead code analysis.
|
||||
type DeadCodeEffects t v
|
||||
= '[ State (Dead t) -- The set of dead terms
|
||||
, Fail -- Failure with an error message
|
||||
, State (Store (LocationFor v) v) -- The heap
|
||||
, State (EnvironmentFor v) -- Global (imperative) environment
|
||||
, Reader (EnvironmentFor v) -- Local environment (e.g. binding over a closure)
|
||||
, Reader (ModuleTable t) -- Cache of unevaluated modules
|
||||
, State (ModuleTable (EnvironmentFor v)) -- Cache of evaluated modules
|
||||
]
|
||||
|
||||
|
||||
-- | Run a dead code analysis of the given program.
|
||||
evaluateDead :: forall term value
|
||||
. ( Corecursive term
|
||||
, Evaluatable (Base term)
|
||||
, Foldable (Base term)
|
||||
, FreeVariables term
|
||||
, MonadAddressable (LocationFor value) value (DeadCodeAnalysis term value)
|
||||
, MonadValue term value (DeadCodeAnalysis term value)
|
||||
, Ord (LocationFor value)
|
||||
, Ord term
|
||||
, Recursive term
|
||||
, Semigroup (Cell (LocationFor value) value)
|
||||
)
|
||||
=> term
|
||||
-> Final (DeadCodeEffects term value) value
|
||||
evaluateDead term = run @(DeadCodeEffects term value) . runEvaluator . runDeadCodeAnalysis $ do
|
||||
killAll (subterms term)
|
||||
evaluateTerm term
|
||||
where subterms :: (Ord a, Recursive a, Foldable (Base a)) => a -> Dead a
|
||||
subterms term = para (foldMap (uncurry ((<>) . point))) term <> point term
|
||||
|
||||
|
||||
-- | A newtype wrapping 'Evaluator' which performs a dead code analysis on evaluation.
|
||||
newtype DeadCodeAnalysis term value a = DeadCodeAnalysis { runDeadCodeAnalysis :: Evaluator (DeadCodeEffects term value) term value a }
|
||||
deriving (Applicative, Functor, Monad, MonadFail)
|
||||
|
||||
deriving instance MonadEvaluator term value (DeadCodeAnalysis term value)
|
||||
-- | An analysis tracking dead (unreachable) code.
|
||||
newtype DeadCode m term value (effects :: [* -> *]) a = DeadCode (m term value effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
|
||||
deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (DeadCode m term value effects)
|
||||
|
||||
-- | A set of “dead” (unreachable) terms.
|
||||
newtype Dead a = Dead { unDead :: Set a }
|
||||
deriving (Eq, Foldable, Semigroup, Monoid, Ord, Pointed, Show)
|
||||
newtype Dead term = Dead { unDead :: Set term }
|
||||
deriving (Eq, Foldable, Semigroup, Monoid, Ord, Show)
|
||||
|
||||
deriving instance Ord term => Reducer term (Dead term)
|
||||
|
||||
-- | Update the current 'Dead' set.
|
||||
killAll :: Dead t -> DeadCodeAnalysis t v ()
|
||||
killAll = DeadCodeAnalysis . Evaluator . put
|
||||
killAll :: (Effectful (m term value), Member (State (Dead term)) effects) => Dead term -> DeadCode m term value effects ()
|
||||
killAll = raise . put
|
||||
|
||||
-- | Revive a single term, removing it from the current 'Dead' set.
|
||||
revive :: Ord t => t -> DeadCodeAnalysis t v ()
|
||||
revive t = DeadCodeAnalysis (Evaluator (modify (Dead . delete t . unDead)))
|
||||
revive :: (Effectful (m term value), Member (State (Dead term)) effects) => Ord term => term -> DeadCode m term value effects ()
|
||||
revive t = raise (modify (Dead . delete t . unDead))
|
||||
|
||||
-- | Compute the set of all subterms recursively.
|
||||
subterms :: (Ord term, Recursive term, Foldable (Base term)) => term -> Dead term
|
||||
subterms term = term `cons` para (foldMap (uncurry cons)) term
|
||||
|
||||
|
||||
instance ( Corecursive t
|
||||
, Evaluatable (Base t)
|
||||
, FreeVariables t
|
||||
, MonadAddressable (LocationFor v) v (DeadCodeAnalysis t v)
|
||||
, MonadValue t v (DeadCodeAnalysis t v)
|
||||
, Ord t
|
||||
, Recursive t
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
instance ( Corecursive term
|
||||
, Effectful (m term value)
|
||||
, Foldable (Base term)
|
||||
, Member (State (Dead term)) effects
|
||||
, MonadAnalysis term value (m term value effects)
|
||||
, Ord term
|
||||
)
|
||||
=> MonadAnalysis t v (DeadCodeAnalysis t v) where
|
||||
=> MonadAnalysis term value (DeadCode m term value effects) where
|
||||
type RequiredEffects term value (DeadCode m term value effects) = State (Dead term) ': RequiredEffects term value (m term value effects)
|
||||
|
||||
analyzeTerm term = do
|
||||
revive (embedSubterm term)
|
||||
eval term
|
||||
liftAnalyze analyzeTerm term
|
||||
|
||||
evaluateModule term = do
|
||||
killAll (subterms term)
|
||||
DeadCode (evaluateModule term)
|
||||
|
@ -1,65 +1,55 @@
|
||||
{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableInstances #-}
|
||||
module Analysis.Abstract.Evaluating where
|
||||
{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
|
||||
module Analysis.Abstract.Evaluating
|
||||
( type Evaluating
|
||||
, evaluate
|
||||
, evaluates
|
||||
) where
|
||||
|
||||
import Control.Abstract.Evaluator
|
||||
import Control.Effect
|
||||
import Control.Monad.Effect hiding (run)
|
||||
import Control.Monad.Effect.Fail
|
||||
import Control.Monad.Effect.Fresh
|
||||
import Control.Monad.Effect.NonDet
|
||||
import Control.Monad.Effect.Reader
|
||||
import Control.Monad.Effect.State
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Evaluatable
|
||||
import Data.Abstract.ModuleTable
|
||||
import Data.Abstract.Store
|
||||
import Data.Abstract.Value
|
||||
import Data.Blob
|
||||
import Data.List.Split (splitWhen)
|
||||
import Prologue
|
||||
import qualified Data.ByteString.Char8 as BC
|
||||
import Data.List.Split (splitWhen)
|
||||
import qualified Data.Map as Map
|
||||
import Prelude hiding (fail)
|
||||
import Prologue
|
||||
import System.FilePath.Posix
|
||||
|
||||
|
||||
-- | The effects necessary for concrete interpretation.
|
||||
type EvaluationEffects t v
|
||||
= '[ Fail -- Failure with an error message
|
||||
, State (Store (LocationFor v) v) -- The heap
|
||||
, State (EnvironmentFor v) -- Global (imperative) environment
|
||||
, Reader (EnvironmentFor v) -- Local environment (e.g. binding over a closure)
|
||||
, Reader (ModuleTable t) -- Cache of unevaluated modules
|
||||
, State (ModuleTable (EnvironmentFor v)) -- Cache of evaluated modules
|
||||
]
|
||||
|
||||
-- | Evaluate a term to a value.
|
||||
evaluate :: forall v term
|
||||
evaluate :: forall value term
|
||||
. ( Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, MonadAddressable (LocationFor v) v (Evaluation term v)
|
||||
, MonadValue term v (Evaluation term v)
|
||||
, Ord (LocationFor v)
|
||||
, MonadAddressable (LocationFor value) value (Evaluating term value (EvaluatingEffects term value))
|
||||
, MonadValue term value (Evaluating term value (EvaluatingEffects term value))
|
||||
, Recursive term
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
)
|
||||
=> term
|
||||
-> Final (EvaluationEffects term v) v
|
||||
evaluate = run @(EvaluationEffects term v) . runEvaluator . runEvaluation . evaluateTerm
|
||||
-> Final (EvaluatingEffects term value) value
|
||||
evaluate = runAnalysis @(Evaluating term value) . evaluateModule
|
||||
|
||||
-- | Evaluate terms and an entry point to a value.
|
||||
evaluates :: forall v term
|
||||
evaluates :: forall value term
|
||||
. ( Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, MonadAddressable (LocationFor v) v (Evaluation term v)
|
||||
, MonadValue term v (Evaluation term v)
|
||||
, Ord (LocationFor v)
|
||||
, MonadAddressable (LocationFor value) value (Evaluating term value (EvaluatingEffects term value))
|
||||
, MonadValue term value (Evaluating term value (EvaluatingEffects term value))
|
||||
, Recursive term
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
)
|
||||
=> [(Blob, term)] -- List of (blob, term) pairs that make up the program to be evaluated
|
||||
-> (Blob, term) -- Entrypoint
|
||||
-> Final (EvaluationEffects term v) v
|
||||
evaluates pairs (b, t) = run @(EvaluationEffects term v) (runEvaluator (runEvaluation (withModules b pairs (evaluateTerm t))))
|
||||
-> Final (EvaluatingEffects term value) value
|
||||
evaluates pairs (b, t) = runAnalysis @(Evaluating term value) (withModules b pairs (evaluateModule t))
|
||||
|
||||
-- | Run an action with the passed ('Blob', @term@) pairs available for imports.
|
||||
withModules :: (MonadAnalysis term value m, MonadEvaluator term value m) => Blob -> [(Blob, term)] -> m a -> m a
|
||||
withModules :: MonadAnalysis term value m => Blob -> [(Blob, term)] -> m a -> m a
|
||||
withModules Blob{..} pairs = localModuleTable (const moduleTable)
|
||||
where
|
||||
moduleTable = ModuleTable (Map.fromList (map (first moduleName) pairs))
|
||||
@ -67,18 +57,50 @@ withModules Blob{..} pairs = localModuleTable (const moduleTable)
|
||||
moduleName Blob{..} = toName (dropExtensions (makeRelative rootDir blobPath))
|
||||
toName str = qualifiedName (fmap BC.pack (splitWhen (== pathSeparator) str))
|
||||
|
||||
-- | An analysis performing concrete evaluation of @term@s to @value@s.
|
||||
newtype Evaluation term value a = Evaluation { runEvaluation :: Evaluator (EvaluationEffects term value) term value a }
|
||||
deriving (Applicative, Functor, Monad, MonadFail)
|
||||
-- | 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)
|
||||
deriving (Applicative, Functor, Effectful, Monad)
|
||||
|
||||
deriving instance MonadEvaluator term value (Evaluation term value)
|
||||
|
||||
instance ( Evaluatable (Base t)
|
||||
, FreeVariables t
|
||||
, MonadAddressable (LocationFor v) v (Evaluation t v)
|
||||
, MonadValue t v (Evaluation t v)
|
||||
, Recursive t
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
deriving instance Member Fail effects => MonadFail (Evaluating term value effects)
|
||||
deriving instance Member Fresh effects => MonadFresh (Evaluating term value effects)
|
||||
deriving instance Member NonDetEff effects => Alternative (Evaluating term value effects)
|
||||
deriving instance Member NonDetEff effects => MonadNonDet (Evaluating term value effects)
|
||||
|
||||
-- | Effects necessary for evaluating (whether concrete or abstract).
|
||||
type EvaluatingEffects term value
|
||||
= '[ Fail -- Failure with an error message
|
||||
, Reader (EnvironmentFor value) -- Local environment (e.g. binding over a closure)
|
||||
, State (EnvironmentFor value) -- Global (imperative) environment
|
||||
, State (StoreFor value) -- The heap
|
||||
, Reader (ModuleTable term) -- Cache of unevaluated modules
|
||||
, State (ModuleTable (EnvironmentFor value)) -- Cache of evaluated modules
|
||||
]
|
||||
|
||||
instance Members (EvaluatingEffects term value) effects => MonadEvaluator term value (Evaluating term value effects) where
|
||||
getGlobalEnv = raise get
|
||||
putGlobalEnv = raise . put
|
||||
|
||||
askLocalEnv = raise ask
|
||||
localEnv f a = raise (local f (lower a))
|
||||
|
||||
getStore = raise get
|
||||
putStore = raise . put
|
||||
|
||||
getModuleTable = raise get
|
||||
modifyModuleTable f = raise (modify f)
|
||||
|
||||
askModuleTable = raise ask
|
||||
localModuleTable f a = raise (local f (lower a))
|
||||
|
||||
instance ( Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, Members (EvaluatingEffects term value) effects
|
||||
, MonadAddressable (LocationFor value) value (Evaluating term value effects)
|
||||
, MonadValue term value (Evaluating term value effects)
|
||||
, Recursive term
|
||||
)
|
||||
=> MonadAnalysis t v (Evaluation t v) where
|
||||
=> MonadAnalysis term value (Evaluating term value effects) where
|
||||
type RequiredEffects term value (Evaluating term value effects) = EvaluatingEffects term value
|
||||
|
||||
analyzeTerm = eval
|
||||
|
@ -1,73 +1,42 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes, DataKinds, ScopedTypeVariables, TypeApplications, TypeFamilies #-}
|
||||
module Analysis.Abstract.Tracing where
|
||||
{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
|
||||
module Analysis.Abstract.Tracing
|
||||
( type Tracing
|
||||
) where
|
||||
|
||||
import Prologue
|
||||
import Control.Effect
|
||||
import Control.Monad.Effect hiding (run)
|
||||
import Control.Monad.Effect.Addressable
|
||||
import Control.Monad.Effect.Env
|
||||
import Control.Monad.Effect.Fail
|
||||
import Control.Monad.Effect.Reader
|
||||
import Control.Monad.Effect.State
|
||||
import Control.Monad.Effect.Trace
|
||||
import Control.Abstract.Analysis
|
||||
import Control.Monad.Effect.Writer
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Configuration
|
||||
import Data.Abstract.Environment
|
||||
import Data.Abstract.Eval
|
||||
import Data.Abstract.Store
|
||||
import Data.Abstract.Value
|
||||
import Data.Semigroup.Reducer as Reducer
|
||||
import Prologue
|
||||
|
||||
-- | The effects necessary for tracing analyses.
|
||||
type Tracing g t v
|
||||
= '[ Writer (g (Configuration (LocationFor v) t v)) -- For 'MonadTrace'.
|
||||
, Fail -- For 'MonadFail'.
|
||||
, State (Store (LocationFor v) v) -- For 'MonadStore'.
|
||||
, Reader (Environment (LocationFor v) v) -- For 'MonadEnv'.
|
||||
]
|
||||
-- | Trace analysis.
|
||||
--
|
||||
-- Instantiating @trace@ to @[]@ yields a linear trace analysis, while @Set@ yields a reachable state analysis.
|
||||
newtype Tracing (trace :: * -> *) m term value (effects :: [* -> *]) a = Tracing (m term value effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
|
||||
-- | Linear trace analysis.
|
||||
evalTrace :: forall v term
|
||||
. ( Ord v, Ord term, Ord (Cell (LocationFor v) v)
|
||||
, Functor (Base term)
|
||||
, Recursive term
|
||||
, Addressable (LocationFor v) (Eff (Tracing [] term v))
|
||||
, MonadGC v (Eff (Tracing [] term v))
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
, Eval term v (Eff (Tracing [] term v)) (Base term)
|
||||
)
|
||||
=> term -> Final (Tracing [] term v) v
|
||||
evalTrace = run @(Tracing [] term v) . fix (evTell @[] (\ recur yield -> eval recur yield . project)) pure
|
||||
deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (Tracing trace m term value effects)
|
||||
|
||||
-- | Reachable configuration analysis.
|
||||
evalReach :: forall v term
|
||||
. ( Ord v, Ord term, Ord (LocationFor v), Ord (Cell (LocationFor v) v)
|
||||
, Functor (Base term)
|
||||
, Recursive term
|
||||
, Addressable (LocationFor v) (Eff (Tracing Set term v))
|
||||
, MonadGC v (Eff (Tracing Set term v))
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
, Eval term v (Eff (Tracing Set term v)) (Base term)
|
||||
)
|
||||
=> term -> Final (Tracing Set term v) v
|
||||
evalReach = run @(Tracing Set term v) . fix (evTell @Set (\ recur yield -> eval recur yield . project)) pure
|
||||
|
||||
|
||||
-- | Small-step evaluation which records every visited configuration.
|
||||
evTell :: forall g t m v
|
||||
. ( Monoid (g (Configuration (LocationFor v) t v))
|
||||
, Pointed g
|
||||
, MonadTrace t v g m
|
||||
, MonadEnv v m
|
||||
, MonadStore v m
|
||||
, MonadGC v m
|
||||
instance ( Corecursive term
|
||||
, Effectful (m term value)
|
||||
, Member (Writer (trace (ConfigurationFor term value))) effects
|
||||
, MonadAnalysis term value (m term value effects)
|
||||
, Ord (LocationFor value)
|
||||
, Reducer (ConfigurationFor term value) (trace (ConfigurationFor term value))
|
||||
)
|
||||
=> (((v -> m v) -> t -> m v) -> (v -> m v) -> t -> m v)
|
||||
-> ((v -> m v) -> t -> m v)
|
||||
-> (v -> m v) -> t -> m v
|
||||
evTell ev0 ev' yield e = do
|
||||
env <- askEnv
|
||||
store <- getStore
|
||||
roots <- askRoots
|
||||
trace (point (Configuration e roots env store) :: g (Configuration (LocationFor v) t v))
|
||||
ev0 ev' yield e
|
||||
=> MonadAnalysis term value (Tracing trace m term value effects) where
|
||||
type RequiredEffects term value (Tracing trace m term value effects) = Writer (trace (ConfigurationFor term value)) ': RequiredEffects term value (m term value effects)
|
||||
|
||||
analyzeTerm term = do
|
||||
config <- getConfiguration (embedSubterm term)
|
||||
trace (Reducer.unit config)
|
||||
liftAnalyze analyzeTerm term
|
||||
|
||||
-- | Log the given trace of configurations.
|
||||
trace :: ( Effectful (m term value)
|
||||
, Member (Writer (trace (ConfigurationFor term value))) effects
|
||||
)
|
||||
=> trace (ConfigurationFor term value)
|
||||
-> Tracing trace m term value effects ()
|
||||
trace = raise . tell
|
||||
|
@ -1,65 +1,61 @@
|
||||
{-# LANGUAGE FunctionalDependencies, TypeFamilies, UndecidableInstances #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}
|
||||
module Control.Abstract.Addressable where
|
||||
|
||||
import Control.Abstract.Evaluator
|
||||
import Control.Abstract.Analysis
|
||||
import Control.Applicative
|
||||
import Control.Monad ((<=<))
|
||||
import Control.Monad.Effect.Fail
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Environment
|
||||
import Data.Abstract.FreeVariables
|
||||
import Data.Abstract.Store
|
||||
import Data.Abstract.Value
|
||||
import Data.Foldable (asum, toList)
|
||||
import Data.Pointed
|
||||
import Data.Semigroup
|
||||
import Data.Semigroup.Reducer
|
||||
import Prelude hiding (fail)
|
||||
|
||||
-- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Store.
|
||||
class (Monad m, Ord l, Pointed (Cell l), l ~ LocationFor a) => MonadAddressable l a m | m -> a where
|
||||
deref :: Address l a
|
||||
-> m a
|
||||
class (Monad m, Ord l, l ~ LocationFor value, Reducer value (Cell l value)) => MonadAddressable l value m where
|
||||
deref :: Address l value -> m value
|
||||
|
||||
alloc :: Name
|
||||
-> m (Address l a)
|
||||
alloc :: Name -> m (Address l value)
|
||||
|
||||
-- | Look up or allocate an address for a 'Name' free in a given term & assign it a given value, returning the 'Name' paired with the address.
|
||||
--
|
||||
-- The term is expected to contain one and only one free 'Name', meaning that care should be taken to apply this only to e.g. identifiers.
|
||||
lookupOrAlloc :: ( FreeVariables t
|
||||
, MonadAddressable (LocationFor a) a m
|
||||
, MonadEvaluator t a m
|
||||
, Semigroup (Cell (LocationFor a) a)
|
||||
lookupOrAlloc :: ( FreeVariables term
|
||||
, MonadAddressable (LocationFor value) value m
|
||||
, MonadEvaluator term value m
|
||||
, Semigroup (CellFor value)
|
||||
)
|
||||
=> t
|
||||
-> a
|
||||
-> Environment (LocationFor a) a
|
||||
-> m (Name, Address (LocationFor a) a)
|
||||
=> term
|
||||
-> value
|
||||
-> Environment (LocationFor value) value
|
||||
-> m (Name, Address (LocationFor value) value)
|
||||
lookupOrAlloc term = let [name] = toList (freeVariables term) in
|
||||
lookupOrAlloc' name
|
||||
|
||||
-- | Look up or allocate an address for a 'Name' & assign it a given value, returning the 'Name' paired with the address.
|
||||
lookupOrAlloc' :: ( Semigroup (Cell (LocationFor a) a)
|
||||
, MonadAddressable (LocationFor a) a m
|
||||
, MonadEvaluator t a m
|
||||
lookupOrAlloc' :: ( Semigroup (CellFor value)
|
||||
, MonadAddressable (LocationFor value) value m
|
||||
, MonadEvaluator term value m
|
||||
)
|
||||
=> Name
|
||||
-> a
|
||||
-> Environment (LocationFor a) a
|
||||
-> m (Name, Address (LocationFor a) a)
|
||||
-> value
|
||||
-> Environment (LocationFor value) value
|
||||
-> m (Name, Address (LocationFor value) value)
|
||||
lookupOrAlloc' name v env = do
|
||||
a <- maybe (alloc name) pure (envLookup name env)
|
||||
assign a v
|
||||
pure (name, a)
|
||||
|
||||
-- | Write a value to the given 'Address' in the 'Store'.
|
||||
assign :: ( Ord (LocationFor a)
|
||||
, MonadEvaluator t a m
|
||||
, Pointed (Cell (LocationFor a))
|
||||
, Semigroup (Cell (LocationFor a) a)
|
||||
assign :: ( Ord (LocationFor value)
|
||||
, MonadEvaluator term value m
|
||||
, Reducer value (CellFor value)
|
||||
)
|
||||
=> Address (LocationFor a) a
|
||||
-> a
|
||||
=> Address (LocationFor value) value
|
||||
-> value
|
||||
-> m ()
|
||||
assign address = modifyStore . storeInsert address
|
||||
|
||||
@ -67,7 +63,7 @@ assign address = modifyStore . storeInsert address
|
||||
-- Instances
|
||||
|
||||
-- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
|
||||
instance (Monad m, MonadEvaluator t v m, LocationFor v ~ Precise) => MonadAddressable Precise v m where
|
||||
instance (Monad m, LocationFor value ~ Precise, MonadEvaluator term value m) => MonadAddressable Precise value m where
|
||||
deref = maybe uninitializedAddress (pure . unLatest) <=< flip fmap getStore . storeLookup
|
||||
where
|
||||
-- | 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).
|
||||
@ -78,7 +74,7 @@ instance (Monad m, MonadEvaluator t v m, LocationFor v ~ Precise) => MonadAddres
|
||||
|
||||
|
||||
-- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
|
||||
instance (Alternative m, LocationFor v ~ Monovariant, Monad m, MonadEvaluator t v m) => MonadAddressable Monovariant v m where
|
||||
instance (Alternative m, Monad m, LocationFor value ~ Monovariant, MonadEvaluator term value m, Ord value) => MonadAddressable Monovariant value m where
|
||||
deref = asum . maybe [] (map pure . toList) <=< flip fmap getStore . storeLookup
|
||||
|
||||
alloc = pure . Address . Monovariant
|
||||
|
@ -1,18 +1,64 @@
|
||||
{-# LANGUAGE DefaultSignatures, FunctionalDependencies #-}
|
||||
module Control.Abstract.Analysis where
|
||||
{-# LANGUAGE DataKinds, MultiParamTypeClasses, TypeFamilies #-}
|
||||
module Control.Abstract.Analysis
|
||||
( MonadAnalysis(..)
|
||||
, evaluateTerm
|
||||
, liftAnalyze
|
||||
, runAnalysis
|
||||
, module X
|
||||
, Subterm(..)
|
||||
, SubtermAlgebra
|
||||
) where
|
||||
|
||||
import Control.Abstract.Evaluator as X
|
||||
import Control.Effect as X
|
||||
import qualified Control.Monad.Effect as Effect
|
||||
import Control.Monad.Effect.Fail as X
|
||||
import Control.Monad.Effect.Fresh as X
|
||||
import Control.Monad.Effect.NonDet as X
|
||||
import Control.Monad.Effect.Reader as X
|
||||
import Control.Monad.Effect.State as X
|
||||
import Data.Coerce
|
||||
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 Monad m => MonadAnalysis term value m | m -> term, m -> value where
|
||||
class (MonadEvaluator term value m, Recursive term) => MonadAnalysis 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 'RequiredEffects' in their own list.
|
||||
type family RequiredEffects term value m :: [* -> *]
|
||||
|
||||
-- | Analyze a term using the semantics of the current analysis. This should generally only be called by definitions of 'evaluateTerm' and 'analyzeTerm' in this or other instances.
|
||||
analyzeTerm :: SubtermAlgebra (Base term) term (m value)
|
||||
|
||||
-- | Evaluate a term to a value using the semantics of the current analysis.
|
||||
--
|
||||
-- This should always be called instead of explicitly folding either 'eval' or 'analyzeTerm' over subterms, except in 'MonadAnalysis' instances themselves.
|
||||
evaluateTerm :: MonadAnalysis term value m => term -> m value
|
||||
default evaluateTerm :: (MonadAnalysis term value m, Recursive term) => term -> m value
|
||||
evaluateTerm = foldSubterms analyzeTerm
|
||||
-- | Evaluate a (root-level) term to a value using the semantics of the current analysis. This should be used to evaluate single-term programs as well as each module in multi-term programs.
|
||||
evaluateModule :: term -> m value
|
||||
evaluateModule = evaluateTerm
|
||||
|
||||
-- | 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 :: MonadAnalysis term value m => term -> m value
|
||||
evaluateTerm = foldSubterms analyzeTerm
|
||||
|
||||
|
||||
-- | Lift a 'SubtermAlgebra' for an underlying analysis into a containing analysis. Use this when defining an analysis which can be composed onto other analyses to ensure that a call to 'analyzeTerm' occurs in the inner analysis and not the outer one.
|
||||
liftAnalyze :: ( Coercible ( m term value (effects :: [* -> *]) value) (t m term value effects value)
|
||||
, Coercible (t m term value effects value) ( m term value effects value)
|
||||
, Functor (Base term)
|
||||
)
|
||||
=> SubtermAlgebra (Base term) term ( m term value effects value)
|
||||
-> SubtermAlgebra (Base term) term (t m term value effects value)
|
||||
liftAnalyze analyze term = coerce (analyze (second coerce <$> term))
|
||||
|
||||
|
||||
-- | Run an analysis, performing its effects and returning the result alongside any state.
|
||||
--
|
||||
-- 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 'RequiredEffects').
|
||||
runAnalysis :: ( Effectful m
|
||||
, RunEffects effects a
|
||||
, RequiredEffects term value (m effects) ~ effects
|
||||
, MonadAnalysis term value (m effects)
|
||||
)
|
||||
=> m effects a
|
||||
-> Final effects a
|
||||
runAnalysis = Effect.run . runEffects . lower
|
||||
|
@ -1,16 +1,12 @@
|
||||
{-# LANGUAGE DataKinds, FunctionalDependencies, GeneralizedNewtypeDeriving, RankNTypes, StandaloneDeriving, UndecidableInstances #-}
|
||||
{-# LANGUAGE ConstrainedClassMethods, FunctionalDependencies #-}
|
||||
module Control.Abstract.Evaluator where
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad.Effect
|
||||
import Control.Monad.Effect.Fail
|
||||
import Control.Monad.Effect.Fresh
|
||||
import Control.Monad.Effect.NonDet
|
||||
import Control.Monad.Effect.Reader
|
||||
import Control.Monad.Effect.State
|
||||
import Data.Abstract.Configuration
|
||||
import Data.Abstract.Live
|
||||
import Data.Abstract.ModuleTable
|
||||
import Data.Abstract.Value
|
||||
import Prelude hiding (fail)
|
||||
import Prologue
|
||||
|
||||
-- | A 'Monad' providing the basic essentials for evaluation.
|
||||
--
|
||||
@ -23,8 +19,6 @@ class MonadFail m => MonadEvaluator term value m | m -> term, m -> value where
|
||||
getGlobalEnv :: m (EnvironmentFor value)
|
||||
-- | Set the global environment
|
||||
putGlobalEnv :: EnvironmentFor value -> m ()
|
||||
-- | Update the global environment.
|
||||
modifyGlobalEnv :: (EnvironmentFor value -> EnvironmentFor value) -> m ()
|
||||
|
||||
-- | Retrieve the local environment.
|
||||
askLocalEnv :: m (EnvironmentFor value)
|
||||
@ -33,8 +27,8 @@ class MonadFail m => MonadEvaluator term value m | m -> term, m -> value where
|
||||
|
||||
-- | Retrieve the heap.
|
||||
getStore :: m (StoreFor value)
|
||||
-- | Update the heap.
|
||||
modifyStore :: (StoreFor value -> StoreFor value) -> m ()
|
||||
-- | Set the heap.
|
||||
putStore :: StoreFor value -> m ()
|
||||
|
||||
-- | Retrieve the table of evaluated modules.
|
||||
getModuleTable :: m (ModuleTable (EnvironmentFor value))
|
||||
@ -46,38 +40,18 @@ class MonadFail m => MonadEvaluator term value m | m -> term, m -> value where
|
||||
-- | Run an action with a locally-modified table of unevaluated modules.
|
||||
localModuleTable :: (ModuleTable term -> ModuleTable term) -> m a -> m a
|
||||
|
||||
instance Members '[ Fail
|
||||
, Reader (EnvironmentFor value)
|
||||
, State (EnvironmentFor value)
|
||||
, State (StoreFor value)
|
||||
, Reader (ModuleTable term)
|
||||
, State (ModuleTable (EnvironmentFor value))
|
||||
] effects
|
||||
=> MonadEvaluator term value (Evaluator effects term value) where
|
||||
getGlobalEnv = Evaluator get
|
||||
putGlobalEnv = Evaluator . put
|
||||
modifyGlobalEnv f = Evaluator (modify f)
|
||||
-- | Retrieve the current root set.
|
||||
askRoots :: Ord (LocationFor value) => m (Live (LocationFor value) value)
|
||||
askRoots = pure mempty
|
||||
|
||||
askLocalEnv = Evaluator ask
|
||||
localEnv f a = Evaluator (local f (runEvaluator a))
|
||||
-- | Get the current 'Configuration' with a passed-in term.
|
||||
getConfiguration :: Ord (LocationFor value) => term -> m (Configuration (LocationFor value) term value)
|
||||
getConfiguration term = Configuration term <$> askRoots <*> askLocalEnv <*> getStore
|
||||
|
||||
getStore = Evaluator get
|
||||
modifyStore f = Evaluator (modify f)
|
||||
-- | Update the global environment.
|
||||
modifyGlobalEnv :: MonadEvaluator term value m => (EnvironmentFor value -> EnvironmentFor value) -> m ()
|
||||
modifyGlobalEnv f = getGlobalEnv >>= putGlobalEnv . f
|
||||
|
||||
getModuleTable = Evaluator get
|
||||
modifyModuleTable f = Evaluator (modify f)
|
||||
|
||||
askModuleTable = Evaluator ask
|
||||
localModuleTable f a = Evaluator (local f (runEvaluator a))
|
||||
|
||||
putStore :: MonadEvaluator t value m => StoreFor value -> m ()
|
||||
putStore = modifyStore . const
|
||||
|
||||
-- | An evaluator of @term@s to @value@s, producing incremental results of type @a@ using a list of @effects@.
|
||||
newtype Evaluator effects term value a = Evaluator { runEvaluator :: Eff effects a }
|
||||
deriving (Applicative, Functor, Monad)
|
||||
|
||||
deriving instance Member Fail effects => MonadFail (Evaluator effects term value)
|
||||
deriving instance Member NonDetEff effects => Alternative (Evaluator effects term value)
|
||||
deriving instance Member NonDetEff effects => MonadNonDet (Evaluator effects term value)
|
||||
deriving instance Member Fresh effects => MonadFresh (Evaluator effects term value)
|
||||
-- | Update the heap.
|
||||
modifyStore :: MonadEvaluator term value m => (StoreFor value -> StoreFor value) -> m ()
|
||||
modifyStore f = getStore >>= putStore . f
|
||||
|
@ -1,65 +1,60 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}
|
||||
module Control.Abstract.Value where
|
||||
|
||||
import Control.Abstract.Addressable
|
||||
import Control.Abstract.Analysis
|
||||
import Control.Abstract.Evaluator
|
||||
import Control.Monad.Effect.Fresh
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Environment
|
||||
import Data.Abstract.FreeVariables
|
||||
import Data.Abstract.Value as Value
|
||||
import Data.Abstract.Type as Type
|
||||
import Data.Abstract.Value as Value
|
||||
import Data.Scientific (Scientific)
|
||||
import Prologue
|
||||
import Prelude hiding (fail)
|
||||
import Prologue
|
||||
|
||||
-- | 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 (MonadEvaluator t v m) => MonadValue t v m where
|
||||
class (MonadAnalysis term value m, Show value) => MonadValue term value m where
|
||||
-- | Construct an abstract unit value.
|
||||
-- TODO: This might be the same as the empty tuple for some value types
|
||||
unit :: m v
|
||||
unit :: m value
|
||||
|
||||
-- | Construct an abstract integral value.
|
||||
integer :: Prelude.Integer -> m v
|
||||
integer :: Prelude.Integer -> m value
|
||||
|
||||
-- | Construct an abstract boolean value.
|
||||
boolean :: Bool -> m v
|
||||
boolean :: Bool -> m value
|
||||
|
||||
-- | Construct an abstract string value.
|
||||
string :: ByteString -> m v
|
||||
string :: ByteString -> m value
|
||||
|
||||
-- | Construct a floating-point value.
|
||||
float :: Scientific -> m v
|
||||
float :: Scientific -> m value
|
||||
|
||||
-- | Construct an N-ary tuple of multiple (possibly-disjoint) values
|
||||
multiple :: [v] -> m v
|
||||
multiple :: [value] -> m value
|
||||
|
||||
-- | Construct an abstract interface value.
|
||||
interface :: v -> m v
|
||||
interface :: value -> m value
|
||||
|
||||
-- | Eliminate boolean values. TODO: s/boolean/truthy
|
||||
ifthenelse :: v -> m v -> m v -> m v
|
||||
ifthenelse :: value -> m value -> m value -> m value
|
||||
|
||||
-- | Evaluate an abstraction (a binder like a lambda or method definition).
|
||||
abstract :: [Name] -> Subterm t (m v) -> m v
|
||||
abstract :: [Name] -> Subterm term (m value) -> m value
|
||||
-- | Evaluate an application (like a function call).
|
||||
apply :: v -> [Subterm t (m v)] -> m v
|
||||
apply :: value -> [Subterm term (m value)] -> m value
|
||||
|
||||
-- | Extract the environment from an interface value.
|
||||
environment :: v -> m (EnvironmentFor v)
|
||||
environment :: value -> m (EnvironmentFor value)
|
||||
|
||||
-- | Construct a 'Value' wrapping the value arguments (if any).
|
||||
instance ( FreeVariables t
|
||||
, MonadAddressable location (Value location t) m
|
||||
, MonadAnalysis t (Value location t) m
|
||||
, MonadEvaluator t (Value location t) m
|
||||
, Recursive t
|
||||
, Semigroup (Cell location (Value location t))
|
||||
instance ( MonadAddressable location (Value location term) m
|
||||
, MonadAnalysis term (Value location term) m
|
||||
, Show location
|
||||
, Show term
|
||||
)
|
||||
=> MonadValue t (Value location t) m where
|
||||
=> MonadValue term (Value location term) m where
|
||||
|
||||
unit = pure . injValue $ Value.Unit
|
||||
integer = pure . injValue . Integer
|
||||
@ -73,12 +68,12 @@ instance ( FreeVariables t
|
||||
|
||||
ifthenelse cond if' else'
|
||||
| Just (Boolean b) <- prjValue cond = if b then if' else else'
|
||||
| otherwise = fail "not defined for non-boolean conditions"
|
||||
| otherwise = fail ("not defined for non-boolean conditions: " <> show cond)
|
||||
|
||||
abstract names (Subterm body _) = injValue . Closure names body <$> askLocalEnv
|
||||
|
||||
apply op params = do
|
||||
Closure names body env <- maybe (fail "expected a closure") pure (prjValue op)
|
||||
Closure names body env <- maybe (fail ("expected a closure, got: " <> show op)) pure (prjValue op)
|
||||
bindings <- foldr (\ (name, param) rest -> do
|
||||
v <- subtermValue param
|
||||
a <- alloc name
|
||||
@ -91,7 +86,7 @@ instance ( FreeVariables t
|
||||
| otherwise = pure mempty
|
||||
|
||||
-- | Discard the value arguments (if any), constructing a 'Type.Type' instead.
|
||||
instance (Alternative m, MonadEvaluator t Type m, MonadFresh m) => MonadValue t Type m where
|
||||
instance (Alternative m, MonadAnalysis term Type m, MonadFresh m) => MonadValue term Type m where
|
||||
abstract names (Subterm _ body) = do
|
||||
(env, tvars) <- foldr (\ name rest -> do
|
||||
a <- alloc name
|
||||
|
@ -1,7 +1,6 @@
|
||||
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeFamilies, TypeOperators, UndecidableInstances #-}
|
||||
{-# LANGUAGE DataKinds, MultiParamTypeClasses, TypeFamilies, TypeOperators, UndecidableInstances #-}
|
||||
module Control.Effect where
|
||||
|
||||
import Prologue
|
||||
import qualified Control.Monad.Effect as Effect
|
||||
import Control.Monad.Effect.Fail
|
||||
import Control.Monad.Effect.Internal hiding (run)
|
||||
@ -9,10 +8,12 @@ import Control.Monad.Effect.NonDetEff
|
||||
import Control.Monad.Effect.Reader
|
||||
import Control.Monad.Effect.State
|
||||
import Control.Monad.Effect.Writer
|
||||
import Data.Semigroup.Reducer
|
||||
import Prologue
|
||||
|
||||
-- | Run a computation in 'Eff' to completion, interpreting each effect with some sensible defaults, and return the 'Final' result.
|
||||
run :: RunEffects fs a => Eff fs a -> Final fs a
|
||||
run = Effect.run . runEffects
|
||||
-- | Run an 'Effectful' computation to completion, interpreting each effect with some sensible defaults, and return the 'Final' result.
|
||||
run :: (Effectful m, RunEffects effects a) => m effects a -> Final effects a
|
||||
run = Effect.run . runEffects . lower
|
||||
|
||||
-- | A typeclass to run a computation to completion, interpreting each effect with some sensible defaults.
|
||||
class RunEffects fs a where
|
||||
@ -60,6 +61,20 @@ instance Monoid w => RunEffect (Writer w) a where
|
||||
-- | 'NonDetEff' effects are interpreted into a nondeterministic set of result values.
|
||||
instance Ord a => RunEffect NonDetEff a where
|
||||
type Result NonDetEff a = Set a
|
||||
runEffect = relay (pure . point) (\ m k -> case m of
|
||||
runEffect = relay (pure . unit) (\ m k -> case m of
|
||||
MZero -> pure mempty
|
||||
MPlus -> mappend <$> k True <*> k False)
|
||||
|
||||
|
||||
-- | Types wrapping 'Eff' actions.
|
||||
--
|
||||
-- Most instances of 'Effectful' will be derived using @-XGeneralizedNewtypeDeriving@, with these ultimately bottoming out on the instance for 'Eff' (for which 'raise' and 'lower' are simply the identity). Because of this, types can be nested arbitrarily deeply and still call 'raise'/'lower' just once to get at the (ultimately) underlying 'Eff'.
|
||||
class Effectful (m :: [* -> *] -> * -> *) where
|
||||
-- | Raise an action in 'Eff' into an action in @m@.
|
||||
raise :: Eff effects a -> m effects a
|
||||
-- | Lower an action in @m@ into an action in 'Eff'.
|
||||
lower :: m effects a -> Eff effects a
|
||||
|
||||
instance Effectful Eff where
|
||||
raise = id
|
||||
lower = id
|
||||
|
@ -4,15 +4,15 @@ module Control.Monad.Effect.NonDet
|
||||
, NonDetEff
|
||||
) where
|
||||
|
||||
import Prologue
|
||||
import Control.Monad.Effect.Internal
|
||||
import Control.Monad.Effect.NonDetEff
|
||||
import Prologue
|
||||
|
||||
-- | 'Monad's offering local isolation of nondeterminism effects.
|
||||
class (Alternative m, Monad m) => MonadNonDet m where
|
||||
-- | Run a computation, gathering any nondeterministically produced results into a single 'Monoid'al value.
|
||||
gather :: Monoid b
|
||||
=> (a -> b) -- ^ A function constructing a 'Monoid'al value from a single computed result. This might typically be @point@ (for @Pointed@ functors), 'pure' (for 'Applicative's), or some similar singleton constructor.
|
||||
=> (a -> b) -- ^ A function constructing a 'Monoid'al value from a single computed result. This might typically be @unit@ (for @Reducer@s), 'pure' (for 'Applicative's), or some similar singleton constructor.
|
||||
-> m a -- ^ The computation to run locally-nondeterministically.
|
||||
-> m b -- ^ A _deterministic_ computation producing the 'Monoid'al accumulation of the _locally-nondeterministic_ result values.
|
||||
|
||||
|
@ -1,17 +0,0 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, UndecidableInstances #-}
|
||||
module Control.Monad.Effect.Trace where
|
||||
|
||||
import Control.Monad.Effect
|
||||
import Control.Monad.Effect.Writer
|
||||
import Data.Abstract.Configuration
|
||||
import Data.Abstract.Value
|
||||
|
||||
-- | 'Monad's offering a writable trace of configurations.
|
||||
--
|
||||
-- @t@ is the type of terms, @v@ the type of values, @g@ the type of the collection represented by the log (e.g. '[]' for regular traces, or @Set@ for the trace of reachable states).
|
||||
class Monad m => MonadTrace t v g m where
|
||||
-- | Log the given collection of configurations.
|
||||
trace :: g (Configuration (LocationFor v) t v) -> m ()
|
||||
|
||||
instance (Writer (g (Configuration (LocationFor v) t v)) :< fs) => MonadTrace t v g (Eff fs) where
|
||||
trace = tell
|
@ -1,8 +1,9 @@
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, TypeFamilyDependencies #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeFamilies, TypeFamilyDependencies #-}
|
||||
module Data.Abstract.Address where
|
||||
|
||||
import Prologue
|
||||
import Data.Abstract.FreeVariables
|
||||
import Data.Semigroup.Reducer
|
||||
import Prologue
|
||||
|
||||
-- | An abstract address with a location of @l@ pointing to a variable of type @a@.
|
||||
newtype Address l a = Address { unAddress :: l }
|
||||
@ -33,10 +34,12 @@ newtype Latest a = Latest { unLatest :: a }
|
||||
deriving (Eq, Foldable, Functor, Generic1, Ord, Show, Traversable)
|
||||
|
||||
instance Semigroup (Latest a) where
|
||||
(<>) = flip const
|
||||
_ <> a = a
|
||||
|
||||
instance Pointed Latest where
|
||||
point = Latest
|
||||
instance Reducer a (Latest a) where
|
||||
unit = Latest
|
||||
cons _ = id
|
||||
snoc _ = unit
|
||||
|
||||
instance Eq1 Latest where liftEq = genericLiftEq
|
||||
instance Ord1 Latest where liftCompare = genericLiftCompare
|
||||
|
@ -1,32 +1,33 @@
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving, UndecidableInstances #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, UndecidableInstances #-}
|
||||
module Data.Abstract.Cache where
|
||||
|
||||
import Prologue
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Configuration
|
||||
import Data.Abstract.Store
|
||||
import Data.Map as Map
|
||||
import Data.Map.Monoidal as Monoidal
|
||||
import Prologue
|
||||
|
||||
-- | A map of 'Configuration's to 'Set's of resulting values & 'Store's.
|
||||
newtype Cache l t v = Cache { unCache :: Map.Map (Configuration l t v) (Set (v, Store l v)) }
|
||||
newtype Cache l t v = Cache { unCache :: Monoidal.Map (Configuration l t v) (Set (v, Store l v)) }
|
||||
|
||||
deriving instance (Eq l, Eq t, Eq v, Eq (Cell l v)) => Eq (Cache l t v)
|
||||
deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Ord (Cache l t v)
|
||||
deriving instance (Show l, Show t, Show v, Show (Cell l v)) => Show (Cache l t v)
|
||||
deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Semigroup (Cache l t v)
|
||||
deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Monoid (Cache l t v)
|
||||
deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Reducer (Configuration l t v, (v, Store l v)) (Cache l t v)
|
||||
|
||||
-- | Look up the resulting value & 'Store' for a given 'Configuration'.
|
||||
cacheLookup :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Cache l t v -> Maybe (Set (v, Store l v))
|
||||
cacheLookup key = Map.lookup key . unCache
|
||||
cacheLookup key = Monoidal.lookup key . unCache
|
||||
|
||||
-- | Set the resulting value & 'Store' for a given 'Configuration', overwriting any previous entry.
|
||||
cacheSet :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Set (v, Store l v) -> Cache l t v -> Cache l t v
|
||||
cacheSet key value = Cache . Map.insert key value . unCache
|
||||
cacheSet key value = Cache . Monoidal.insert key value . unCache
|
||||
|
||||
-- | Insert the resulting value & 'Store' for a given 'Configuration', appending onto any previous entry.
|
||||
cacheInsert :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> (v, Store l v) -> Cache l t v -> Cache l t v
|
||||
cacheInsert key value = Cache . Map.insertWith (<>) key (point value) . unCache
|
||||
cacheInsert = curry cons
|
||||
|
||||
|
||||
instance (Eq l, Eq t, Eq1 (Cell l)) => Eq1 (Cache l t) where
|
||||
|
@ -6,6 +6,10 @@ import Data.Abstract.Address
|
||||
import Data.Abstract.Environment
|
||||
import Data.Abstract.Live
|
||||
import Data.Abstract.Store
|
||||
import Data.Abstract.Value
|
||||
|
||||
-- | The configuration for term and abstract value types.
|
||||
type ConfigurationFor term value = Configuration (LocationFor value) term value
|
||||
|
||||
-- | A single point in a program’s execution.
|
||||
data Configuration l t v
|
||||
|
@ -1,4 +1,4 @@
|
||||
{-# LANGUAGE DefaultSignatures, FunctionalDependencies, UndecidableInstances #-}
|
||||
{-# LANGUAGE DefaultSignatures, MultiParamTypeClasses, UndecidableInstances #-}
|
||||
module Data.Abstract.Evaluatable
|
||||
( Evaluatable(..)
|
||||
, module Addressable
|
||||
@ -12,15 +12,11 @@ module Data.Abstract.Evaluatable
|
||||
|
||||
import Control.Abstract.Addressable as Addressable
|
||||
import Control.Abstract.Analysis as Analysis
|
||||
import Control.Abstract.Evaluator
|
||||
import Control.Abstract.Value as Value
|
||||
import Control.Monad.Effect.Fail
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Environment
|
||||
import Data.Abstract.FreeVariables as FreeVariables
|
||||
import Data.Abstract.ModuleTable
|
||||
import Data.Abstract.Value
|
||||
import Data.Algebra
|
||||
import Data.Functor.Classes
|
||||
import Data.Proxy
|
||||
import Data.Semigroup
|
||||
@ -34,10 +30,7 @@ class Evaluatable constr where
|
||||
eval :: ( FreeVariables term
|
||||
, MonadAddressable (LocationFor value) value m
|
||||
, MonadAnalysis term value m
|
||||
, MonadEvaluator term value m
|
||||
, MonadValue term value m
|
||||
, Ord (LocationFor value)
|
||||
, Semigroup (Cell (LocationFor value) value)
|
||||
)
|
||||
=> SubtermAlgebra constr term (m value)
|
||||
default eval :: (MonadFail m, Show1 constr) => SubtermAlgebra constr term (m value)
|
||||
@ -77,27 +70,25 @@ instance Evaluatable [] where
|
||||
-- | Require/import another term/file and return an Effect.
|
||||
--
|
||||
-- Looks up the term's name in the cache of evaluated modules first, returns a value if found, otherwise loads/evaluates the module.
|
||||
require :: ( MonadAnalysis term v m
|
||||
, MonadEvaluator term v m
|
||||
, MonadValue term v m
|
||||
require :: ( MonadAnalysis term value m
|
||||
, MonadValue term value m
|
||||
)
|
||||
=> ModuleName
|
||||
-> m (EnvironmentFor v)
|
||||
-> m (EnvironmentFor value)
|
||||
require name = getModuleTable >>= maybe (load name) pure . moduleTableLookup name
|
||||
|
||||
-- | Load another term/file and return an Effect.
|
||||
--
|
||||
-- Always loads/evaluates.
|
||||
load :: ( MonadAnalysis term v m
|
||||
, MonadEvaluator term v m
|
||||
, MonadValue term v m
|
||||
load :: ( MonadAnalysis term value m
|
||||
, MonadValue term value m
|
||||
)
|
||||
=> ModuleName
|
||||
-> m (EnvironmentFor v)
|
||||
-> m (EnvironmentFor value)
|
||||
load name = askModuleTable >>= maybe notFound evalAndCache . moduleTableLookup name
|
||||
where notFound = fail ("cannot load module: " <> show name)
|
||||
evalAndCache e = do
|
||||
v <- evaluateTerm e
|
||||
v <- evaluateModule e
|
||||
env <- environment v
|
||||
modifyModuleTable (moduleTableInsert name env)
|
||||
pure env
|
||||
|
@ -1,14 +1,15 @@
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving, UndecidableInstances #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, UndecidableInstances #-}
|
||||
module Data.Abstract.Store where
|
||||
|
||||
import Prologue
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Live
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Map.Monoidal as Monoidal
|
||||
import Data.Semigroup.Reducer
|
||||
import Prologue
|
||||
|
||||
-- | A map of addresses onto cells holding their values.
|
||||
newtype Store l a = Store { unStore :: Map.Map l (Cell l a) }
|
||||
deriving (Generic1, Monoid, Semigroup)
|
||||
newtype Store l a = Store { unStore :: Monoidal.Map l (Cell l a) }
|
||||
deriving (Generic1)
|
||||
|
||||
deriving instance (Eq l, Eq (Cell l a)) => Eq (Store l a)
|
||||
deriving instance (Ord l, Ord (Cell l a)) => Ord (Store l a)
|
||||
@ -19,23 +20,26 @@ instance (Show l, Show1 (Cell l)) => Show1 (Store l) where liftShowsPrec = gener
|
||||
deriving instance Foldable (Cell l) => Foldable (Store l)
|
||||
deriving instance Functor (Cell l) => Functor (Store l)
|
||||
deriving instance Traversable (Cell l) => Traversable (Store l)
|
||||
deriving instance (Ord l, Semigroup (Cell l a)) => Semigroup (Store l a)
|
||||
deriving instance (Ord l, Semigroup (Cell l a)) => Monoid (Store l a)
|
||||
deriving instance (Ord l, Reducer a (Cell l a)) => Reducer (l, a) (Store l a)
|
||||
|
||||
-- | Look up the cell of values for an 'Address' in a 'Store', if any.
|
||||
storeLookup :: Ord l => Address l a -> Store l a -> Maybe (Cell l a)
|
||||
storeLookup (Address address) = Map.lookup address . unStore
|
||||
storeLookup (Address address) = Monoidal.lookup address . unStore
|
||||
|
||||
-- | Look up the list of values stored for a given address, if any.
|
||||
storeLookupAll :: (Ord l, Foldable (Cell l)) => Address l a -> Store l a -> Maybe [a]
|
||||
storeLookupAll address = fmap toList . storeLookup address
|
||||
|
||||
-- | Append a value onto the cell for a given address, inserting a new cell if none existed.
|
||||
storeInsert :: (Ord l, Semigroup (Cell l a), Pointed (Cell l)) => Address l a -> a -> Store l a -> Store l a
|
||||
storeInsert (Address address) value = Store . Map.insertWith (<>) address (point value) . unStore
|
||||
storeInsert :: (Ord l, Reducer a (Cell l a)) => Address l a -> a -> Store l a -> Store l a
|
||||
storeInsert (Address address) value = flip snoc (address, value)
|
||||
|
||||
-- | The number of addresses extant in a 'Store'.
|
||||
storeSize :: Store l a -> Int
|
||||
storeSize = Map.size . unStore
|
||||
storeSize = Monoidal.size . unStore
|
||||
|
||||
-- | Restrict a 'Store' to only those 'Address'es in the given 'Live' set (in essence garbage collecting the rest).
|
||||
storeRestrict :: Ord l => Store l a -> Live l a -> Store l a
|
||||
storeRestrict (Store m) roots = Store (Map.filterWithKey (\ address _ -> Address address `liveMember` roots) m)
|
||||
storeRestrict (Store m) roots = Store (Monoidal.filterWithKey (\ address _ -> Address address `liveMember` roots) m)
|
||||
|
@ -112,6 +112,9 @@ type EnvironmentFor v = Environment (LocationFor v) v
|
||||
-- | The store for an abstract value type.
|
||||
type StoreFor v = Store (LocationFor v) v
|
||||
|
||||
-- | The cell for an abstract value type.
|
||||
type CellFor value = Cell (LocationFor value) value
|
||||
|
||||
-- | The location type (the body of 'Address'es) which should be used for an abstract value type.
|
||||
type family LocationFor value :: * where
|
||||
LocationFor (Value location term) = location
|
||||
|
@ -14,6 +14,7 @@ module Data.Algebra
|
||||
, openFToOpenR
|
||||
) where
|
||||
|
||||
import Data.Bifunctor
|
||||
import Data.Functor.Foldable ( Base
|
||||
, Corecursive(embed)
|
||||
, Recursive(project)
|
||||
@ -45,7 +46,10 @@ type OpenRAlgebra f t a = forall b . (b -> (t, a)) -> f b -> a
|
||||
|
||||
-- | A subterm and its computed value, used in 'SubtermAlgebra'.
|
||||
data Subterm t a = Subterm { subterm :: !t, subtermValue :: !a }
|
||||
deriving (Eq, Ord, Show)
|
||||
deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
|
||||
|
||||
instance Bifunctor Subterm where
|
||||
bimap f g (Subterm a b) = Subterm (f a) (g b)
|
||||
|
||||
-- | Like an R-algebra, but using 'Subterm' to label the fields instead of an anonymous pair.
|
||||
type SubtermAlgebra f t a = f (Subterm t a) -> a
|
||||
|
@ -82,11 +82,6 @@ merging :: Functor syntax => Term syntax ann -> Diff syntax ann ann
|
||||
merging = cata (\ (In ann syntax) -> mergeF (In (ann, ann) syntax))
|
||||
|
||||
|
||||
diffPatch :: Diff syntax ann1 ann2 -> Maybe (Patch (TermF syntax ann1 (Diff syntax ann1 ann2)) (TermF syntax ann2 (Diff syntax ann1 ann2)))
|
||||
diffPatch diff = case unDiff diff of
|
||||
Patch patch -> Just patch
|
||||
_ -> Nothing
|
||||
|
||||
diffPatches :: (Foldable syntax, Functor syntax) => Diff syntax ann1 ann2 -> [Patch (TermF syntax ann1 (Diff syntax ann1 ann2)) (TermF syntax ann2 (Diff syntax ann1 ann2))]
|
||||
diffPatches = para $ \ diff -> case diff of
|
||||
Patch patch -> bimap (fmap fst) (fmap fst) patch : bifoldMap (foldMap snd) (foldMap snd) patch
|
||||
|
44
src/Data/Map/Monoidal.hs
Normal file
44
src/Data/Map/Monoidal.hs
Normal file
@ -0,0 +1,44 @@
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses #-}
|
||||
-- | This module defines a 'Map' type whose 'Monoid' and 'Reducer' instances merge values using the 'Semigroup' instance for the underlying type.
|
||||
module Data.Map.Monoidal
|
||||
( Map
|
||||
, lookup
|
||||
, size
|
||||
, insert
|
||||
, filterWithKey
|
||||
, module Reducer
|
||||
) where
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import Data.Semigroup.Reducer as Reducer
|
||||
import Prelude hiding (lookup)
|
||||
import Prologue hiding (Map)
|
||||
|
||||
newtype Map key value = Map { unMap :: Map.Map key value }
|
||||
deriving (Eq, Eq1, Eq2, Foldable, Functor, Ord, Ord1, Ord2, Show, Show1, Show2, Traversable)
|
||||
|
||||
|
||||
lookup :: Ord key => key -> Map key value -> Maybe value
|
||||
lookup key = Map.lookup key . unMap
|
||||
|
||||
size :: Map key value -> Int
|
||||
size = Map.size . unMap
|
||||
|
||||
insert :: Ord key => key -> value -> Map key value -> Map key value
|
||||
insert key value = Map . Map.insert key value . unMap
|
||||
|
||||
filterWithKey :: (key -> value -> Bool) -> Map key value -> Map key value
|
||||
filterWithKey f = Map . Map.filterWithKey f . unMap
|
||||
|
||||
|
||||
instance (Ord key, Semigroup value) => Semigroup (Map key value) where
|
||||
Map a <> Map b = Map (Map.unionWith (<>) a b)
|
||||
|
||||
instance (Ord key, Semigroup value) => Monoid (Map key value) where
|
||||
mempty = Map Map.empty
|
||||
mappend = (<>)
|
||||
|
||||
instance (Ord key, Reducer a value) => Reducer (key, a) (Map key value) where
|
||||
unit (key, a) = Map (Map.singleton key (unit a))
|
||||
cons (key, a) (Map m) = Map (Map.insertWith (<>) key (unit a) m)
|
||||
snoc (Map m) (key, a) = Map (Map.insertWith (flip (<>)) key (unit a) m)
|
@ -7,6 +7,7 @@ import Data.Abstract.Evaluatable
|
||||
import Data.AST
|
||||
import Data.Range
|
||||
import Data.Record
|
||||
import qualified Data.Set as Set
|
||||
import Data.Span
|
||||
import Data.Term
|
||||
import Diffing.Algorithm hiding (Empty)
|
||||
@ -112,7 +113,7 @@ instance Evaluatable Identifier where
|
||||
maybe (fail ("free variable: " <> show name)) deref (envLookup name env)
|
||||
|
||||
instance FreeVariables1 Identifier where
|
||||
liftFreeVariables _ (Identifier x) = point x
|
||||
liftFreeVariables _ (Identifier x) = Set.singleton x
|
||||
|
||||
|
||||
newtype Program a = Program [a]
|
||||
|
@ -51,7 +51,6 @@ import Data.Functor.Classes.Generic as X
|
||||
import Data.Functor.Foldable as X (Base, Recursive(..), Corecursive(..))
|
||||
import Data.Mergeable as X (Mergeable)
|
||||
import Data.Monoid as X (Monoid(..), First(..), Last(..))
|
||||
import Data.Pointed as X
|
||||
import Data.Proxy as X (Proxy(..))
|
||||
import Data.Semigroup as X (Semigroup(..))
|
||||
import Data.Traversable as X
|
||||
|
@ -1,11 +1,13 @@
|
||||
-- MonoLocalBinds is to silence a warning about a simplifiable constraint.
|
||||
{-# LANGUAGE DataKinds, MonoLocalBinds, TypeOperators, TypeApplications #-}
|
||||
{-# LANGUAGE DataKinds, MonoLocalBinds, TypeApplications, TypeOperators #-}
|
||||
module Semantic.Util where
|
||||
|
||||
import Prologue
|
||||
import Analysis.Abstract.Caching
|
||||
import Analysis.Abstract.Dead
|
||||
import Analysis.Abstract.Evaluating
|
||||
import Analysis.Abstract.Tracing
|
||||
import Analysis.Declaration
|
||||
import Control.Abstract.Analysis
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Type
|
||||
@ -20,13 +22,14 @@ import Data.Term
|
||||
import Diffing.Algorithm
|
||||
import Diffing.Interpreter
|
||||
import Parsing.Parser
|
||||
import Prologue
|
||||
import Semantic
|
||||
import Semantic.IO as IO
|
||||
import Semantic.Task
|
||||
|
||||
import qualified Language.Go.Assignment as Go
|
||||
import qualified Language.Ruby.Assignment as Ruby
|
||||
import qualified Language.Python.Assignment as Python
|
||||
import qualified Language.Ruby.Assignment as Ruby
|
||||
import qualified Language.TypeScript.Assignment as TypeScript
|
||||
|
||||
type Language a = Value Precise (Term (Union a) (Record Location))
|
||||
@ -40,41 +43,44 @@ file :: MonadIO m => FilePath -> m Blob
|
||||
file path = fromJust <$> IO.readFile path (languageForFilePath path)
|
||||
|
||||
-- Ruby
|
||||
evaluateRubyFile path = Prelude.fst . evaluate @RubyValue <$>
|
||||
(file path >>= runTask . parse rubyParser)
|
||||
evaluateRubyFile path = fst . evaluate @RubyValue . snd <$> parseFile rubyParser path
|
||||
|
||||
evaluateRubyFiles paths = do
|
||||
blobs@(b:bs) <- traverse file paths
|
||||
(t:ts) <- runTask $ traverse (parse rubyParser) blobs
|
||||
pure $ evaluates @RubyValue (zip bs ts) (b, t)
|
||||
first:rest <- traverse (parseFile rubyParser) paths
|
||||
pure $ evaluates @RubyValue rest first
|
||||
|
||||
-- Go
|
||||
typecheckGoFile path = evaluateCache @Type <$>
|
||||
(file path >>= runTask . parse goParser)
|
||||
typecheckGoFile path = runAnalysis @(Caching Evaluating Go.Term Type) . evaluateModule . snd <$>
|
||||
parseFile goParser path
|
||||
|
||||
evaluateGoFile path = evaluate @GoValue <$>
|
||||
(file path >>= runTask . parse goParser)
|
||||
evaluateGoFile path = runAnalysis @(Evaluating Go.Term GoValue) . evaluateModule . snd <$>
|
||||
parseFile goParser path
|
||||
|
||||
-- Python
|
||||
typecheckPythonFile path = evaluateCache @Type <$>
|
||||
(file path >>= runTask . parse pythonParser)
|
||||
typecheckPythonFile path = runAnalysis @(Caching Evaluating Python.Term Type) . evaluateModule . snd <$> parseFile pythonParser path
|
||||
|
||||
evaluatePythonFile path = evaluate @PythonValue <$>
|
||||
(file path >>= runTask . parse pythonParser)
|
||||
tracePythonFile path = runAnalysis @(Tracing [] Evaluating Python.Term PythonValue) . evaluateModule . snd <$> parseFile pythonParser path
|
||||
|
||||
evaluateDeadTracePythonFile path = runAnalysis @(DeadCode (Tracing [] Evaluating) Python.Term PythonValue) . evaluateModule . snd <$> parseFile pythonParser path
|
||||
|
||||
evaluatePythonFile path = evaluate @PythonValue . snd <$> parseFile pythonParser path
|
||||
|
||||
evaluatePythonFiles paths = do
|
||||
blobs@(b:bs) <- traverse file paths
|
||||
(t:ts) <- runTask $ traverse (parse pythonParser) blobs
|
||||
pure $ evaluates @PythonValue (zip bs ts) (b, t)
|
||||
first:rest <- traverse (parseFile pythonParser) paths
|
||||
pure $ evaluates @PythonValue rest first
|
||||
|
||||
-- TypeScript
|
||||
evaluateTypeScriptFile path = Prelude.fst . evaluate @TypeScriptValue <$>
|
||||
(file path >>= runTask . parse typescriptParser)
|
||||
evaluateTypeScriptFile path = fst . evaluate @TypeScriptValue . snd <$> parseFile typescriptParser path
|
||||
|
||||
evaluateTypeScriptFiles paths = do
|
||||
blobs@(b:bs) <- traverse file paths
|
||||
(t:ts) <- runTask $ traverse (parse typescriptParser) blobs
|
||||
pure $ evaluates @TypeScriptValue (zip bs ts) (b, t)
|
||||
first:rest <- traverse (parseFile typescriptParser) paths
|
||||
pure $ evaluates @TypeScriptValue rest first
|
||||
|
||||
|
||||
parseFile :: Parser term -> FilePath -> IO (Blob, term)
|
||||
parseFile parser path = runTask $ do
|
||||
blob <- file path
|
||||
(,) blob <$> parse parser blob
|
||||
|
||||
|
||||
-- Diff helpers
|
||||
|
Loading…
Reference in New Issue
Block a user