1
1
mirror of https://github.com/github/semantic.git synced 2025-01-04 13:34:31 +03:00

Split MonadAnalysis into AnalyzeModule & AnalyzeTerm classes.

This commit is contained in:
Rob Rix 2018-05-04 11:19:36 -04:00
parent da833e9ac7
commit 4108302aed
15 changed files with 195 additions and 189 deletions

View File

@ -9,8 +9,9 @@ import Prologue
newtype BadAddresses m (effects :: [* -> *]) a = BadAddresses { runBadAddresses :: m effects a } newtype BadAddresses m (effects :: [* -> *]) a = BadAddresses { runBadAddresses :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad) deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadAddresses m)
deriving instance Evaluator location term value m => Evaluator location term value (BadAddresses m) deriving instance Evaluator location term value m => Evaluator location term value (BadAddresses m)
deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (BadAddresses m)
deriving instance AnalyzeTerm location term value inner outer m => AnalyzeTerm location term value inner outer (BadAddresses m)
instance ( Interpreter m effects instance ( Interpreter m effects
, Evaluator location term value m , Evaluator location term value m

View File

@ -9,8 +9,9 @@ import Prologue
newtype BadModuleResolutions m (effects :: [* -> *]) a = BadModuleResolutions { runBadModuleResolutions :: m effects a } newtype BadModuleResolutions m (effects :: [* -> *]) a = BadModuleResolutions { runBadModuleResolutions :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad) deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadModuleResolutions m)
deriving instance Evaluator location term value m => Evaluator location term value (BadModuleResolutions m) deriving instance Evaluator location term value m => Evaluator location term value (BadModuleResolutions m)
deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (BadModuleResolutions m)
deriving instance AnalyzeTerm location term value inner outer m => AnalyzeTerm location term value inner outer (BadModuleResolutions m)
instance ( Interpreter m effects instance ( Interpreter m effects
, Evaluator location term value m , Evaluator location term value m

View File

@ -18,8 +18,9 @@ import Prologue
newtype BadSyntax m (effects :: [* -> *]) a = BadSyntax { runBadSyntax :: m effects a } newtype BadSyntax m (effects :: [* -> *]) a = BadSyntax { runBadSyntax :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad) deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadSyntax m)
deriving instance Evaluator location term value m => Evaluator location term value (BadSyntax m) deriving instance Evaluator location term value m => Evaluator location term value (BadSyntax m)
deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (BadSyntax m)
deriving instance AnalyzeTerm location term value inner outer m => AnalyzeTerm location term value inner outer (BadSyntax m)
instance ( AbstractHole value instance ( AbstractHole value
, Evaluator location term value m , Evaluator location term value m

View File

@ -9,8 +9,9 @@ import Prologue
newtype BadValues m (effects :: [* -> *]) a = BadValues { runBadValues :: m effects a } newtype BadValues m (effects :: [* -> *]) a = BadValues { runBadValues :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad) deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadValues m)
deriving instance Evaluator location term value m => Evaluator location term value (BadValues m) deriving instance Evaluator location term value m => Evaluator location term value (BadValues m)
deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (BadValues m)
deriving instance AnalyzeTerm location term value inner outer m => AnalyzeTerm location term value inner outer (BadValues m)
instance ( AbstractHole value instance ( AbstractHole value
, Evaluator location term value m , Evaluator location term value m

View File

@ -12,8 +12,9 @@ import Prologue
newtype BadVariables m (effects :: [* -> *]) a = BadVariables { runBadVariables :: m effects a } newtype BadVariables m (effects :: [* -> *]) a = BadVariables { runBadVariables :: m effects a }
deriving (Alternative, Applicative, Functor, Effectful, Monad) deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (BadVariables m)
deriving instance Evaluator location term value m => Evaluator location term value (BadVariables m) deriving instance Evaluator location term value m => Evaluator location term value (BadVariables m)
deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (BadVariables m)
deriving instance AnalyzeTerm location term value inner outer m => AnalyzeTerm location term value inner outer (BadVariables m)
instance ( AbstractHole value instance ( AbstractHole value
, Evaluator location term value m , Evaluator location term value m

View File

@ -48,23 +48,20 @@ putCache = raise . put
isolateCache :: forall location term value m effects a . (Applicative (m effects), Effectful m, Member (State (Cache location term value)) effects) => m effects a -> m effects (Cache location term value) isolateCache :: forall location term value m effects a . (Applicative (m effects), Effectful m, Member (State (Cache location term value)) effects) => m effects a -> m effects (Cache location term value)
isolateCache action = putCache @m @location @term @value lowerBound *> action *> raise get isolateCache action = putCache @m @location @term @value lowerBound *> action *> raise get
instance ( Alternative (m outer)
-- | This instance coinductively iterates the analysis of a term until the results converge. , AnalyzeTerm location term value inner outer m
instance ( Alternative (m effects) , Cacheable location term value
, Corecursive term , Corecursive term
, Effectful m , Effectful m
, Member Fresh effects , Member Fresh outer
, Member NonDet effects , Member NonDet outer
, Member (Reader (Cache location term value)) effects , Member (Reader (Cache location term value)) outer
, Member (Reader (Live location value)) effects , Member (Reader (Live location value)) outer
, Member (State (Cache location term value)) effects , Member (State (Cache location term value)) outer
, MonadAnalysis location term value effects m , Member (State (Environment location value)) outer
, Ord (Cell location value) , Member (State (Heap location value)) outer
, Ord location
, Ord term
, Ord value
) )
=> MonadAnalysis location term value effects (Caching m) where => AnalyzeTerm location term value inner outer (Caching m) where
-- Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache. -- Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache.
analyzeTerm recur e = do analyzeTerm recur e = do
c <- getConfiguration (embedSubterm e) c <- getConfiguration (embedSubterm e)
@ -73,8 +70,22 @@ instance ( Alternative (m effects)
Just pairs -> scatter pairs Just pairs -> scatter pairs
Nothing -> do Nothing -> do
pairs <- consultOracle c pairs <- consultOracle c
caching c pairs (liftAnalyze analyzeTerm recur e) caching c pairs (Caching (analyzeTerm (runCaching . recur) e))
instance ( Alternative (m outer)
, AnalyzeModule location term value inner outer m
, Cacheable location term value
, Corecursive term
, Effectful m
, Member Fresh outer
, Member NonDet outer
, Member (Reader (Cache location term value)) outer
, Member (Reader (Live location value)) outer
, Member (State (Cache location term value)) outer
, Member (State (Environment location value)) outer
, Member (State (Heap location value)) outer
)
=> AnalyzeModule location term value inner outer (Caching m) where
analyzeModule recur m = do analyzeModule recur m = do
c <- getConfiguration (subterm (moduleBody m)) c <- getConfiguration (subterm (moduleBody m))
-- Convergence here is predicated upon an Eq instance, not α-equivalence -- Convergence here is predicated upon an Eq instance, not α-equivalence
@ -87,9 +98,10 @@ instance ( Alternative (m effects)
-- that it doesn't "leak" to the calling context and diverge (otherwise this -- that it doesn't "leak" to the calling context and diverge (otherwise this
-- would never complete). We dont need to use the values, so we 'gather' the -- would never complete). We dont need to use the values, so we 'gather' the
-- nondeterministic values into @()@. -- nondeterministic values into @()@.
withOracle prevCache (raiseHandler (gather (const ())) (liftAnalyze analyzeModule recur m))) mempty withOracle prevCache (raiseHandler (gather (const ())) (Caching (analyzeModule (runCaching . recur) m)))) mempty
maybe empty scatter (cacheLookup c cache) maybe empty scatter (cacheLookup c cache)
reset :: (Effectful m, Member Fresh effects) => Int -> m effects a -> m effects a reset :: (Effectful m, Member Fresh effects) => Int -> m effects a -> m effects a
reset start = raiseHandler (interposeState start (const pure) (\ counter Fresh yield -> (yield $! succ counter) counter)) reset start = raiseHandler (interposeState start (const pure) (\ counter Fresh yield -> (yield $! succ counter) counter))

View File

@ -9,6 +9,7 @@ import Control.Abstract.Analysis
import Data.Abstract.Address import Data.Abstract.Address
import Data.Abstract.Heap import Data.Abstract.Heap
import Data.Abstract.Live import Data.Abstract.Live
import Data.Semilattice.Lower
import Prologue import Prologue
-- | An analysis performing GC after every instruction. -- | An analysis performing GC after every instruction.
@ -16,25 +17,23 @@ newtype Collecting m (effects :: [* -> *]) a = Collecting { runCollecting :: m e
deriving (Alternative, Applicative, Effectful, Functor, Monad) deriving (Alternative, Applicative, Effectful, Functor, Monad)
deriving instance Evaluator location term value m => Evaluator location term value (Collecting m) deriving instance Evaluator location term value m => Evaluator location term value (Collecting m)
deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (Collecting m)
instance ( Effectful m instance ( Effectful m
, Foldable (Cell location) , Foldable (Cell location)
, Member (Reader (Live location value)) effects , Member (Reader (Live location value)) outer
, MonadAnalysis location term value effects m , Member (State (Heap location value)) outer
, AnalyzeTerm location term value inner outer m
, Ord location , Ord location
, ValueRoots location value , ValueRoots location value
) )
=> MonadAnalysis location term value effects (Collecting m) where => AnalyzeTerm location term value inner outer (Collecting m) where
-- Small-step evaluation which garbage-collects any non-rooted addresses after evaluating each term.
analyzeTerm recur term = do analyzeTerm recur term = do
roots <- askRoots roots <- askRoots
v <- liftAnalyze analyzeTerm recur term v <- Collecting (analyzeTerm (runCollecting . recur) term)
modifyHeap (gc (roots <> valueRoots v)) modifyHeap (gc (roots <> valueRoots v))
pure v pure v
analyzeModule = liftAnalyze analyzeModule
-- | Collect any addresses in the heap not rooted in or reachable from the given 'Live' set. -- | Collect any addresses in the heap not rooted in or reachable from the given 'Live' set.
gc :: ( Ord location gc :: ( Ord location
@ -64,11 +63,10 @@ reachable roots heap = go mempty roots
instance ( Evaluator location term value m instance ( Evaluator location term value m
, Interpreter m effects , Interpreter m effects
, Ord location
) )
=> Interpreter (Collecting m) (Reader (Live location value) ': effects) where => Interpreter (Collecting m) (Reader (Live location value) ': effects) where
type Result (Collecting m) (Reader (Live location value) ': effects) result = Result m effects result type Result (Collecting m) (Reader (Live location value) ': effects) result = Result m effects result
interpret = interpret . runCollecting . raiseHandler (`runReader` mempty) interpret = interpret . runCollecting . handleReader lowerBound
-- | An analysis providing a 'Live' set, but never performing GC. -- | An analysis providing a 'Live' set, but never performing GC.
@ -76,12 +74,12 @@ newtype Retaining m (effects :: [* -> *]) a = Retaining { runRetaining :: m effe
deriving (Alternative, Applicative, Effectful, Functor, Monad) deriving (Alternative, Applicative, Effectful, Functor, Monad)
deriving instance Evaluator location term value m => Evaluator location term value (Retaining m) deriving instance Evaluator location term value m => Evaluator location term value (Retaining m)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (Retaining m) deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (Retaining m)
deriving instance AnalyzeTerm location term value inner outer m => AnalyzeTerm location term value inner outer (Retaining m)
instance ( Evaluator location term value m instance ( Evaluator location term value m
, Interpreter m effects , Interpreter m effects
, Ord location
) )
=> Interpreter (Retaining m) (Reader (Live location value) ': effects) where => Interpreter (Retaining m) (Reader (Live location value) ': effects) where
type Result (Retaining m) (Reader (Live location value) ': effects) result = Result m effects result type Result (Retaining m) (Reader (Live location value) ': effects) result = Result m effects result
interpret = interpret . runRetaining . raiseHandler (`runReader` mempty) interpret = interpret . runRetaining . handleReader lowerBound

View File

@ -38,19 +38,28 @@ subterms term = term `cons` para (foldMap (uncurry cons)) term
instance ( Corecursive term instance ( Corecursive term
, Effectful m , Effectful m
, Foldable (Base term) , Foldable (Base term)
, Member (State (Dead term)) effects , Member (State (Dead term)) outer
, MonadAnalysis location term value effects m , AnalyzeTerm location term value inner outer m
, Ord term , Ord term
, Recursive term , Recursive term
) )
=> MonadAnalysis location term value effects (DeadCode m) where => AnalyzeTerm location term value inner outer (DeadCode m) where
analyzeTerm recur term = do analyzeTerm recur term = do
revive (embedSubterm term) revive (embedSubterm term)
liftAnalyze analyzeTerm recur term DeadCode (analyzeTerm (runDeadCode . recur) term)
instance ( Corecursive term
, Effectful m
, Foldable (Base term)
, Member (State (Dead term)) outer
, AnalyzeModule location term value inner outer m
, Ord term
, Recursive term
)
=> AnalyzeModule location term value inner outer (DeadCode m) where
analyzeModule recur m = do analyzeModule recur m = do
killAll (subterms (subterm (moduleBody m))) killAll (subterms (subterm (moduleBody m)))
liftAnalyze analyzeModule recur m DeadCode (analyzeModule (runDeadCode . recur) m)
instance ( Evaluator location term value m instance ( Evaluator location term value m
, Interpreter m effects , Interpreter m effects

View File

@ -11,7 +11,8 @@ newtype Erroring (exc :: * -> *) m (effects :: [* -> *]) a = Erroring { runError
deriving (Alternative, Applicative, Effectful, Functor, Monad) deriving (Alternative, Applicative, Effectful, Functor, Monad)
deriving instance Evaluator location term value m => Evaluator location term value (Erroring exc m) deriving instance Evaluator location term value m => Evaluator location term value (Erroring exc m)
deriving instance MonadAnalysis location term value effects m => MonadAnalysis location term value effects (Erroring exc m) deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (Erroring exc m)
deriving instance AnalyzeTerm location term value inner outer m => AnalyzeTerm location term value inner outer (Erroring exc m)
instance Interpreter m effects instance Interpreter m effects
=> Interpreter (Erroring exc m) (Resumable exc ': effects) where => Interpreter (Erroring exc m) (Resumable exc ': effects) where

View File

@ -1,12 +1,13 @@
{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, UndecidableInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
module Analysis.Abstract.Evaluating module Analysis.Abstract.Evaluating
( Evaluating ( Evaluating
, EvaluatingState(..) , EvaluatingState(..)
) where ) where
import Control.Abstract.Analysis import Control.Abstract.Analysis
import qualified Control.Monad.Effect as Eff import qualified Control.Monad.Effect.Internal as Eff
import Data.Abstract.Address import Data.Abstract.Address
import Data.Abstract.Module
import Data.Abstract.Origin import Data.Abstract.Origin
import Data.Semilattice.Lower import Data.Semilattice.Lower
import Prologue import Prologue
@ -32,8 +33,7 @@ deriving instance (Show (Cell location value), Show location, Show term, Show va
-- | Effects necessary for evaluating (whether concrete or abstract). -- | Effects necessary for evaluating (whether concrete or abstract).
type EvaluatingEffects location term value type EvaluatingEffects location term value
= '[ EvalClosure term value = '[ Return value
, Return value
, LoopControl value , LoopControl value
, Fail -- Failure with an error message , Fail -- Failure with an error message
, Fresh -- For allocating new addresses and/or type variables. , Fresh -- For allocating new addresses and/or type variables.
@ -47,24 +47,17 @@ type EvaluatingEffects location term value
, State (JumpTable term) , State (JumpTable term)
] ]
instance ( Corecursive term instance (termInfo ~ Base term (), Recursive term) => AnalyzeTerm location term value (Reader termInfo ': effects) effects (Evaluating location term value) where
, Member (Reader (Environment location value)) effects analyzeTerm eval = handleReader . (() <$) <*> eval . fmap (second (raiseHandler weakenEff))
, Member (Reader LoadStack) effects
, Member (Reader (SomeOrigin term)) effects
, Member (State (Environment location value)) effects
, Member (State (Heap location value)) effects
, Member (State (ModuleTable (Environment location value, value))) effects
, Member (State (Exports location value)) effects
, Member (State (JumpTable term)) effects
, Recursive term
)
=> MonadAnalysis location term value effects (Evaluating location term value) where
analyzeTerm eval term = pushOrigin (termOrigin (embedSubterm term)) (eval term)
analyzeModule eval m = pushOrigin (moduleOrigin (subterm <$> m)) (eval m) instance AnalyzeModule location term value (Reader ModuleInfo ': effects) effects (Evaluating location term value) where
analyzeModule eval = handleReader . moduleInfo <*> eval . fmap (second (raiseHandler weakenEff))
weakenEff :: Eff effects a -> Eff (effect ': effects) a
weakenEff (Eff.Val a) = pure a
weakenEff (Eff.E u q) = Eff.E (weaken u) (Eff.tsingleton (q Eff.>>> weakenEff))
instance (AbstractHole value, Show term, Show value) => Interpreter (Evaluating location term value) (EvaluatingEffects location term value) where instance (AbstractHole value, Show value) => Interpreter (Evaluating location term value) (EvaluatingEffects location term value) where
type Result (Evaluating location term value) (EvaluatingEffects location term value) result type Result (Evaluating location term value) (EvaluatingEffects location term value) result
= ( Either String result = ( Either String result
, EvaluatingState location term value) , EvaluatingState location term value)
@ -72,22 +65,21 @@ instance (AbstractHole value, Show term, Show value) => Interpreter (Evaluating
= (\ (((((result, env), heap), modules), exports), jumps) -> (result, EvaluatingState env heap modules exports jumps)) = (\ (((((result, env), heap), modules), exports), jumps) -> (result, EvaluatingState env heap modules exports jumps))
. interpret . interpret
. runEvaluating . runEvaluating
. handleState lowerBound -- State (JumpTable term)
. handleState lowerBound -- State (Exports location value)
. handleState lowerBound -- State (ModuleTable (Environment location value, value))
. handleState lowerBound -- State (Heap location value)
. handleState lowerBound -- State (Environment location value)
. handleReader lowerBound -- Reader LoadStack
. handleReader lowerBound -- Reader (Environment location value)
. handleReader lowerBound -- Reader (SomeOrigin term)
. raiseHandler . raiseHandler
( flip runState lowerBound -- State (JumpTable term) ( flip runFresh' 0
. flip runState lowerBound -- State (Exports location value)
. flip runState lowerBound -- State (ModuleTable (Environment location value, value))
. flip runState lowerBound -- State (Heap location value)
. flip runState lowerBound -- State (Environment location value)
. flip runReader lowerBound -- Reader LoadStack
. flip runReader lowerBound -- Reader (Environment location value)
. flip runReader lowerBound -- Reader (SomeOrigin term)
. flip runFresh' 0
. runFail . runFail
-- NB: We should never have a 'Return', 'Break', or 'Continue' at this point in execution; the scope being returned from/broken from/continued should have intercepted the effect. This handler will therefore only be invoked if we issue a 'Return', 'Break', or 'Continue' outside of such a scope, and unfortunately if this happens it will handle it by resuming the scope being returned from. While it would be _slightly_ more correct to instead exit with the value being returned, we arent able to do that here since 'Interpreter's type is parametric in the value being returned—we dont know that were returning a @value@ (because we very well may not be). On the balance, I felt the strange behaviour in error cases is worth the improved behaviour in the common case—we get to lose a layer of 'Either' in the result for each. -- NB: We should never have a 'Return', 'Break', or 'Continue' at this point in execution; the scope being returned from/broken from/continued should have intercepted the effect. This handler will therefore only be invoked if we issue a 'Return', 'Break', or 'Continue' outside of such a scope, and unfortunately if this happens it will handle it by resuming the scope being returned from. While it would be _slightly_ more correct to instead exit with the value being returned, we arent able to do that here since 'Interpreter's type is parametric in the value being returned—we dont know that were returning a @value@ (because we very well may not be). On the balance, I felt the strange behaviour in error cases is worth the improved behaviour in the common case—we get to lose a layer of 'Either' in the result for each.
-- In general, its expected that none of the following effects will remain by the time 'interpret' is called—they should have been handled by local 'interpose's—but if they do, well at least trace. -- In general, its expected that none of the following effects will remain by the time 'interpret' is called—they should have been handled by local 'interpose's—but if they do, well at least trace.
. Eff.interpret (\ control -> case control of . Eff.interpret (\ control -> case control of
Break value -> traceM ("Evaluating.interpret: resuming uncaught break with " <> show value) $> value Break value -> traceM ("Evaluating.interpret: resuming uncaught break with " <> show value) $> value
Continue -> traceM "Evaluating.interpret: resuming uncaught continue with hole" $> hole) Continue -> traceM "Evaluating.interpret: resuming uncaught continue with hole" $> hole)
. Eff.interpret (\ (Return value) -> traceM ("Evaluating.interpret: resuming uncaught return with " <> show value) $> value) . Eff.interpret (\ (Return value) -> traceM ("Evaluating.interpret: resuming uncaught return with " <> show value) $> value))
. Eff.interpret (\ (EvalClosure term) -> traceM ("Evaluating.interpret: resuming uncaught EvalClosure of " <> show term <> " with hole") $> hole))
-- TODO: Replace 'traceM's with e.g. 'Telemetry'. -- TODO: Replace 'traceM's with e.g. 'Telemetry'.

View File

@ -58,16 +58,18 @@ newtype ImportGraphing m (effects :: [* -> *]) a = ImportGraphing { runImportGra
deriving instance Evaluator location term value m => Evaluator location term value (ImportGraphing m) deriving instance Evaluator location term value m => Evaluator location term value (ImportGraphing m)
instance ( Member (Reader (Environment (Located location term) value)) outer
instance ( Effectful m , Member (Reader (SomeOrigin term)) outer
, Member (Resumable (LoadError term)) effects , Member (Resumable (LoadError term)) outer
, Member (State ImportGraph) effects , Member (State (Environment (Located location term) value)) outer
, Member (State ImportGraph) outer
, Element Syntax.Identifier syntax , Element Syntax.Identifier syntax
, MonadAnalysis (Located location term) term value effects m , Evaluator (Located location term) term value m
, AnalyzeTerm (Located location term) term value inner outer m
, term ~ Term (Sum syntax) ann , term ~ Term (Sum syntax) ann
) )
=> MonadAnalysis (Located location term) term value effects (ImportGraphing m) where => AnalyzeTerm (Located location term) term value inner outer (ImportGraphing m) where
analyzeTerm eval term@(In _ syntax) = do analyzeTerm recur term@(In _ syntax) = do
case projectSum syntax of case projectSum syntax of
Just (Syntax.Identifier name) -> do Just (Syntax.Identifier name) -> do
moduleInclusion (Variable (unName name)) moduleInclusion (Variable (unName name))
@ -75,14 +77,22 @@ instance ( Effectful m
_ -> pure () _ -> pure ()
resume resume
@(LoadError term) @(LoadError term)
(liftAnalyze analyzeTerm eval term) (ImportGraphing (analyzeTerm (runImportGraphing . recur) term))
(\yield (LoadError name) -> moduleInclusion (Module (BC.pack name)) >> yield []) (\yield (LoadError name) -> moduleInclusion (Module (BC.pack name)) *> yield [])
instance ( Member (Reader (SomeOrigin term)) outer
, Member (State ImportGraph) outer
, Evaluator (Located location term) term value m
, AnalyzeModule (Located location term) term value inner outer m
, term ~ Term (Sum syntax) ann
)
=> AnalyzeModule (Located location term) term value inner outer (ImportGraphing m) where
analyzeModule recur m = do analyzeModule recur m = do
let name = BC.pack (modulePath (moduleInfo m)) let name = BC.pack (modulePath (moduleInfo m))
packageInclusion (Module name) packageInclusion (Module name)
moduleInclusion (Module name) moduleInclusion (Module name)
liftAnalyze analyzeModule recur m ImportGraphing (analyzeModule (runImportGraphing . recur) m)
packageGraph :: SomeOrigin term -> ImportGraph packageGraph :: SomeOrigin term -> ImportGraph
packageGraph = maybe empty (vertex . Package . unName . packageName) . withSomeOrigin originPackage packageGraph = maybe empty (vertex . Package . unName . packageName) . withSomeOrigin originPackage
@ -176,4 +186,4 @@ vertexToType Variable{} = "variable"
instance Interpreter m effects instance Interpreter m effects
=> Interpreter (ImportGraphing m) (State ImportGraph ': effects) where => Interpreter (ImportGraphing m) (State ImportGraph ': effects) where
type Result (ImportGraphing m) (State ImportGraph ': effects) result = Result m effects (result, ImportGraph) type Result (ImportGraphing m) (State ImportGraph ': effects) result = Result m effects (result, ImportGraph)
interpret = interpret . runImportGraphing . raiseHandler (`runState` mempty) interpret = interpret . runImportGraphing . handleState mempty

View File

@ -18,22 +18,23 @@ newtype Tracing (trace :: * -> *) m (effects :: [* -> *]) a = Tracing { runTraci
deriving (Alternative, Applicative, Functor, Effectful, Monad) deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance Evaluator location term value m => Evaluator location term value (Tracing trace m) deriving instance Evaluator location term value m => Evaluator location term value (Tracing trace m)
deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (Tracing trace m)
instance ( Corecursive term instance ( Corecursive term
, Effectful m , Effectful m
, Member (Reader (Live location value)) effects , Member (Reader (Live location value)) effectsOut
, Member (Writer (trace (Configuration location term value))) effects , Member (Writer (trace (Configuration location term value))) effectsOut
, MonadAnalysis location term value effects m , AnalyzeTerm location term value effectsIn effectsOut m
, Evaluator location term value m
, MonadEvaluator location term value effectsOut m
, Ord location , Ord location
, Reducer (Configuration location term value) (trace (Configuration location term value)) , Reducer (Configuration location term value) (trace (Configuration location term value))
) )
=> MonadAnalysis location term value effects (Tracing trace m) where => AnalyzeTerm location term value effectsIn effectsOut (Tracing trace m) where
analyzeTerm recur term = do analyzeTerm recur term = do
config <- getConfiguration (embedSubterm term) config <- getConfiguration (embedSubterm term)
raise (tell @(trace (Configuration location term value)) (Reducer.unit config)) raise (tell @(trace (Configuration location term value)) (Reducer.unit config))
liftAnalyze analyzeTerm recur term Tracing (analyzeTerm (runTracing . recur) term)
analyzeModule = liftAnalyze analyzeModule
instance ( Evaluator location term value m instance ( Evaluator location term value m
, Interpreter m effects , Interpreter m effects

View File

@ -1,5 +1,4 @@
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-} {-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
module Analysis.Abstract.TypeChecking module Analysis.Abstract.TypeChecking
( TypeChecking ( TypeChecking
) where ) where
@ -12,7 +11,8 @@ newtype TypeChecking m (effects :: [* -> *]) a = TypeChecking { runTypeChecking
deriving (Alternative, Applicative, Functor, Effectful, Monad) deriving (Alternative, Applicative, Functor, Effectful, Monad)
deriving instance Evaluator location term value m => Evaluator location term value (TypeChecking m) deriving instance Evaluator location term value m => Evaluator location term value (TypeChecking m)
deriving instance MonadAnalysis location term Type effects m => MonadAnalysis location term Type effects (TypeChecking m) deriving instance AnalyzeModule location term value inner outer m => AnalyzeModule location term value inner outer (TypeChecking m)
deriving instance AnalyzeTerm location term value inner outer m => AnalyzeTerm location term value inner outer (TypeChecking m)
instance Interpreter m effects instance Interpreter m effects
=> Interpreter (TypeChecking m) (Resumable TypeError ': effects) where => Interpreter (TypeChecking m) (Resumable TypeError ': effects) where

View File

@ -1,7 +1,7 @@
{-# LANGUAGE KindSignatures #-} {-# LANGUAGE FunctionalDependencies #-}
module Control.Abstract.Analysis module Control.Abstract.Analysis
( MonadAnalysis(..) ( AnalyzeTerm(..)
, liftAnalyze , AnalyzeModule(..)
, module X , module X
) where ) where
@ -17,25 +17,18 @@ import Control.Monad.Effect.Reader as X
import Control.Monad.Effect.State as X import Control.Monad.Effect.State as X
import Control.Monad.Effect.Resumable as X import Control.Monad.Effect.Resumable as X
import Data.Abstract.Module import Data.Abstract.Module
import Data.Coerce
import Data.Type.Coercion
import Prologue import Prologue
-- | A 'Monad' in which one can evaluate some specific term type to some specific value type. -- | A context enabling the analysis of terms, possibly providing effects to underlying analyses.
-- class (Evaluator location term value m, Monad (m outer)) => AnalyzeTerm location term value inner outer m | m inner -> outer, m outer -> inner where
-- This typeclass is left intentionally unconstrained to avoid circular dependencies between it and other typeclasses.
class MonadEvaluator location term value effects m => MonadAnalysis location term value effects m where
-- | Analyze a term using the semantics of the current analysis. -- | Analyze a term using the semantics of the current analysis.
analyzeTerm :: (Base term (Subterm term (outer value)) -> m effects value) analyzeTerm :: Effectful outside
-> (Base term (Subterm term (outer value)) -> m effects value) => (Base term (Subterm term (outside inner value)) -> m inner value)
-> (Base term (Subterm term (outside outer value)) -> m outer value)
-- | A context enabling the analysis of modules, possibly providing effects to underlying analyses.
class (Evaluator location term value m, Monad (m outer)) => AnalyzeModule location term value inner outer m | m inner -> outer, m outer -> inner where
-- | Analyze a module using the semantics of the current analysis. This should generally only be called by 'evaluateModule' and by definitions of 'analyzeModule' in instances for composite analyses. -- | Analyze a module using the semantics of the current analysis. This should generally only be called by 'evaluateModule' and by definitions of 'analyzeModule' in instances for composite analyses.
analyzeModule :: (Module (Subterm term (outer value)) -> m effects value) analyzeModule :: Effectful outside
-> (Module (Subterm term (outer value)) -> m effects value) => (Module (Subterm term (outside inner value)) -> m inner value)
-> (Module (Subterm term (outside outer value)) -> m outer value)
-- | 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 effects value) (t m (effects :: [* -> *]) value)
=> ((base (Subterm term (outer value)) -> m effects value) -> (base (Subterm term (outer value)) -> m effects value))
-> ((base (Subterm term (outer value)) -> t m effects value) -> (base (Subterm term (outer value)) -> t m effects value))
liftAnalyze analyze recur term = coerce (analyze (coerceWith (sym Coercion) . recur) term)

View File

@ -281,128 +281,113 @@ instance Applicative m => Monoid (Merging m location value) where
mappend = (<>) mappend = (<>)
mempty = Merging (pure Nothing) mempty = Merging (pure Nothing)
type ModuleEffects term value effects = Reader ModuleInfo ': EvalModule term value ': effects evalModule :: forall location term value inner outer m
. ( AnalyzeModule location term value inner (EvalModule term value ': outer) m
, Member (EvalClosure term value) outer
)
=> Module term
-> m outer value
evalModule
= evaluatingModules
. analyzeModule (subtermValue . moduleBody)
. fmap (Subterm <*> evaluateClosureBody)
-- | Evaluate a (root-level) term to a value using the semantics of the current analysis. evaluatingModules :: forall location term value inner outer m a
evalModule :: forall location term value effects m inner . ( AnalyzeModule location term value inner (EvalModule term value ': outer) m
. ( inner ~ ModuleEffects term value effects , Member (EvalClosure term value) outer
)
=> m (EvalModule term value ': outer) a
-> m outer a
evaluatingModules = raiseHandler (relay pure (\ (EvalModule m) yield -> lower @m (evalModule m) >>= yield))
evalTerm :: forall location term value inner outer m
. ( AnalyzeTerm location term value inner (EvalClosure term value ': outer) m
, Evaluatable (Base term) , Evaluatable (Base term)
, Member Fail effects , Member Fail inner
, Member (Reader PackageInfo) effects
, MonadAnalysis location term value inner m
, MonadEvaluatable location term value inner m , MonadEvaluatable location term value inner m
, Recursive term , Recursive term
) )
=> Module term
-> m effects value
evalModule m
= evaluatingModulesWith evalModule
. withReader (moduleInfo m)
. localLoadStack (loadStackPush (moduleInfo m))
$ analyzeModule (subtermValue . moduleBody) (fmap (Subterm <*> evalTerm) m)
evalTerm :: forall location term value effects m
. ( Evaluatable (Base term)
, Member (EvalModule term value) effects
, Member Fail effects
, Member (Reader ModuleInfo) effects
, Member (Reader PackageInfo) effects
, MonadAnalysis location term value effects m
, MonadEvaluatable location term value effects m
, Recursive term
)
=> term => term
-> m effects value -> m outer value
evalTerm evalTerm
= handleReturn @m @value (\ (Return value) -> pure value) = evaluatingClosures
. raiseHandler (interpose @(EvalClosure term value) pure (\ (EvalClosure term) yield -> lower @m (evalTerm term) >>= yield))
. foldSubterms (analyzeTerm eval) . foldSubterms (analyzeTerm eval)
evaluatingClosures :: forall location term value inner outer m a
evaluatingModulesWith :: Effectful m => (Module term -> m effects value) -> m (EvalModule term value ': effects) a -> m effects a . ( AnalyzeTerm location term value inner (EvalClosure term value ': outer) m
evaluatingModulesWith evalModule = raiseHandler (relay pure (\ (EvalModule m) yield -> lower (evalModule m) >>= yield)) , Evaluatable (Base term)
, Member Fail inner
withReader :: Effectful m => info -> m (Reader info ': effects) a -> m effects a , MonadEvaluatable location term value inner m
withReader = raiseHandler . flip runReader , Recursive term
)
=> m (EvalClosure term value ': outer) a
-> m outer a
evaluatingClosures = raiseHandler (relay pure (\ (EvalClosure m) yield -> lower @m (evalTerm m) >>= yield))
-- | Evaluate a given package. -- | Evaluate a given package.
evaluatePackage :: ( moduleEffects ~ ModuleEffects term value packageEffects evaluatePackage :: ( AnalyzeModule location term value inner (EvalModule term value ': EvalClosure term value ': Reader (ModuleTable [Module term]) ': Reader PackageInfo ': outer) m
, packageEffects ~ (Reader (ModuleTable [Module term]) ': Reader PackageInfo ': effects) , AnalyzeTerm location term value inner (EvalClosure term value ': Reader (ModuleTable [Module term]) ': Reader PackageInfo ': outer) m
, Evaluatable (Base term) , Evaluatable (Base term)
, Member Fail effects , Member Fail inner
, Member (Resumable (AddressError location value)) effects , Member (Resumable (AddressError location value)) outer
, Member (Resumable (EvalError value)) effects , Member (Resumable (EvalError value)) outer
, Member (Resumable (LoadError term)) effects , Member (Resumable (LoadError term)) outer
, MonadAddressable location packageEffects m , MonadAddressable location (EvalModule term value ': EvalClosure term value ': Reader (ModuleTable [Module term]) ': Reader PackageInfo ': outer) m
, MonadAnalysis location term value moduleEffects m , MonadEvaluatable location term value inner m
, MonadEvaluatable location term value moduleEffects m , MonadEvaluator location term value (Reader PackageInfo ': outer) m
, MonadEvaluator location term value packageEffects m , MonadValue location value (EvalModule term value ': EvalClosure term value ': Reader (ModuleTable [Module term]) ': Reader PackageInfo ': outer) m
, MonadValue location value packageEffects m
, Recursive term , Recursive term
) )
=> Package term => Package term
-> m effects [value] -> m outer [value]
evaluatePackage p = withReader (packageInfo p) (evaluatePackageBody (packageBody p)) evaluatePackage = handleReader . packageInfo <*> evaluatePackageBody . packageBody
-- | Evaluate a given package body (module table and entry points). -- | Evaluate a given package body (module table and entry points).
evaluatePackageBody :: ( moduleEffects ~ ModuleEffects term value packageEffects evaluatePackageBody :: ( AnalyzeModule location term value inner (EvalModule term value ': EvalClosure term value ': Reader (ModuleTable [Module term]) ': outer) m
, packageEffects ~ (Reader (ModuleTable [Module term]) ': effects) , AnalyzeTerm location term value inner (EvalClosure term value ': Reader (ModuleTable [Module term]) ': outer) m
, Evaluatable (Base term) , Evaluatable (Base term)
, Member Fail effects , Member Fail inner
, Member (Reader PackageInfo) effects , Member (Resumable (AddressError location value)) outer
, Member (Resumable (AddressError location value)) effects , Member (Resumable (EvalError value)) outer
, Member (Resumable (EvalError value)) effects , Member (Resumable (LoadError term)) outer
, Member (Resumable (LoadError term)) effects , MonadAddressable location (EvalModule term value ': EvalClosure term value ': Reader (ModuleTable [Module term]) ': outer) m
, MonadAddressable location packageEffects m , MonadEvaluatable location term value inner m
, MonadAnalysis location term value moduleEffects m , MonadEvaluator location term value outer m
, MonadEvaluatable location term value moduleEffects m , MonadValue location value (EvalModule term value ': EvalClosure term value ': Reader (ModuleTable [Module term]) ': outer) m
, MonadEvaluator location term value packageEffects m
, MonadValue location value packageEffects m
, Recursive term , Recursive term
) )
=> PackageBody term => PackageBody term
-> m effects [value] -> m outer [value]
evaluatePackageBody body evaluatePackageBody body
= withReader (packageModules body) = handleReader (packageModules body)
. evaluatingClosures
. evaluatingModules
. withPrelude (packagePrelude body) . withPrelude (packagePrelude body)
$ traverse (uncurry evaluateEntryPoint) (ModuleTable.toPairs (packageEntryPoints body)) $ traverse (uncurry evaluateEntryPoint) (ModuleTable.toPairs (packageEntryPoints body))
evaluateEntryPoint :: ( inner ~ ModuleEffects term value effects evaluateEntryPoint :: ( Member (EvalModule term value) effects
, Evaluatable (Base term)
, Member (Reader (ModuleTable [Module term])) effects , Member (Reader (ModuleTable [Module term])) effects
, Member (Resumable (AddressError location value)) effects , Member (Resumable (AddressError location value)) effects
, Member (Resumable (EvalError value)) effects , Member (Resumable (EvalError value)) effects
, Member (Resumable (LoadError term)) effects , Member (Resumable (LoadError term)) effects
, Member Fail effects
, Member (Reader PackageInfo) effects
, MonadAddressable location effects m , MonadAddressable location effects m
, MonadAnalysis location term value inner m
, MonadEvaluatable location term value inner m
, MonadEvaluator location term value effects m , MonadEvaluator location term value effects m
, MonadValue location value effects m , MonadValue location value effects m
, Recursive term
) )
=> ModulePath => ModulePath
-> Maybe Name -> Maybe Name
-> m effects value -> m effects value
evaluateEntryPoint m sym = do evaluateEntryPoint m sym = do
v <- maybe unit (pure . snd) <$> requireWith evalModule m v <- maybe unit (pure . snd) <$> require m
maybe v ((`call` []) <=< variable) sym maybe v ((`call` []) <=< variable) sym
withPrelude :: forall location term value effects m a inner withPrelude :: ( Member (EvalModule term value) effects
. ( inner ~ ModuleEffects term value effects
, Evaluatable (Base term)
, Member Fail effects
, Member (Reader PackageInfo) effects
, MonadAnalysis location term value inner m
, MonadEvaluatable location term value inner m
, MonadEvaluator location term value effects m , MonadEvaluator location term value effects m
, Recursive term
) )
=> Maybe (Module term) => Maybe (Module term)
-> m effects a -> m effects a
-> m effects a -> m effects a
withPrelude Nothing a = a withPrelude Nothing a = a
withPrelude (Just prelude) a = do withPrelude (Just prelude) a = do
preludeEnv <- evalModule @location @term @value prelude *> getEnv preludeEnv <- evaluateModule prelude *> getEnv
withDefaultEnvironment preludeEnv a withDefaultEnvironment preludeEnv a