mirror of
https://github.com/github/semantic.git
synced 2024-12-22 22:31:36 +03:00
🔥 MonadNonDet.
This commit is contained in:
parent
4120622002
commit
cc0f73b1ed
@ -9,7 +9,7 @@ import Prologue
|
||||
|
||||
-- An analysis that resumes from evaluation errors and records the list of unresolved free variables.
|
||||
newtype BadVariables m (effects :: [* -> *]) a = BadVariables (m effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
|
||||
|
||||
deriving instance MonadControl term (m effects) => MonadControl term (BadVariables m effects)
|
||||
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (BadVariables m effects)
|
||||
|
@ -13,14 +13,14 @@ import Prologue
|
||||
|
||||
-- | The effects necessary for caching analyses.
|
||||
type CachingEffects location term value effects
|
||||
= NonDet -- For 'Alternative' and 'MonadNonDet'.
|
||||
= NonDet -- For 'Alternative' and 'gather'.
|
||||
': Reader (Cache location term value) -- The in-cache used as an oracle while converging on a result.
|
||||
': State (Cache location term value) -- The out-cache used to record results in each iteration of convergence.
|
||||
': effects
|
||||
|
||||
-- | A (coinductively-)cached analysis suitable for guaranteeing termination of (suitably finitized) analyses over recursive programs.
|
||||
newtype Caching m (effects :: [* -> *]) a = Caching (m effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
|
||||
|
||||
deriving instance MonadControl term (m effects) => MonadControl term (Caching m effects)
|
||||
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (Caching m effects)
|
||||
@ -65,12 +65,12 @@ instance ( Effectful m
|
||||
isolateCache action = raise (put (mempty :: Cache location term value)) *> action *> raise get
|
||||
|
||||
-- | This instance coinductively iterates the analysis of a term until the results converge.
|
||||
instance ( Corecursive term
|
||||
instance ( Alternative (m effects)
|
||||
, Corecursive term
|
||||
, Effectful m
|
||||
, Members (CachingEffects location term value '[]) effects
|
||||
, MonadAnalysis location term value (m effects)
|
||||
, MonadFresh (m effects)
|
||||
, MonadNonDet (m effects)
|
||||
, Ord (Cell location value)
|
||||
, Ord location
|
||||
, Ord term
|
||||
@ -102,7 +102,7 @@ instance ( Corecursive term
|
||||
-- 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 ()) (liftAnalyze analyzeModule recur m))) mempty
|
||||
withOracle prevCache (raise (gather (const ()) (lower (liftAnalyze analyzeModule recur m))))) mempty
|
||||
maybe empty scatter (cacheLookup c cache)
|
||||
|
||||
-- | Iterate a monadic action starting from some initial seed until the results converge.
|
||||
|
@ -11,7 +11,7 @@ import Data.Abstract.Live
|
||||
import Prologue
|
||||
|
||||
newtype Collecting m (effects :: [* -> *]) a = Collecting (m effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
|
||||
|
||||
deriving instance MonadControl term (m effects) => MonadControl term (Collecting m effects)
|
||||
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (Collecting m effects)
|
||||
|
@ -11,7 +11,7 @@ import Prologue
|
||||
|
||||
-- | An analysis tracking dead (unreachable) code.
|
||||
newtype DeadCode m (effects :: [* -> *]) a = DeadCode (m effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
|
||||
|
||||
deriving instance MonadControl term (m effects) => MonadControl term (DeadCode m effects)
|
||||
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (DeadCode m effects)
|
||||
|
@ -27,7 +27,6 @@ newtype Evaluating location term value effects a = Evaluating (Eff effects a)
|
||||
deriving instance Member Fail effects => MonadFail (Evaluating location term value effects)
|
||||
deriving instance Member Fresh effects => MonadFresh (Evaluating location term value effects)
|
||||
deriving instance Member NonDet effects => Alternative (Evaluating location term value effects)
|
||||
deriving instance Member NonDet effects => MonadNonDet (Evaluating location term value effects)
|
||||
|
||||
-- | Effects necessary for evaluating (whether concrete or abstract).
|
||||
type EvaluatingEffects location term value
|
||||
|
@ -25,7 +25,7 @@ renderImportGraph :: ImportGraph -> ByteString
|
||||
renderImportGraph = export (defaultStyle friendlyName) . unImportGraph
|
||||
|
||||
newtype ImportGraphing m (effects :: [* -> *]) a = ImportGraphing (m effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
|
||||
|
||||
deriving instance MonadControl term (m effects) => MonadControl term (ImportGraphing m effects)
|
||||
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (ImportGraphing m effects)
|
||||
|
@ -15,7 +15,7 @@ import Prologue
|
||||
--
|
||||
-- Note that exceptions thrown by other analyses may not be caught if 'Quietly' doesn’t know about them, i.e. if they’re not part of the generic 'MonadValue', 'MonadAddressable', etc. machinery.
|
||||
newtype Quietly m (effects :: [* -> *]) a = Quietly (m effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
|
||||
|
||||
deriving instance MonadControl term (m effects) => MonadControl term (Quietly m effects)
|
||||
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (Quietly m effects)
|
||||
|
@ -14,7 +14,7 @@ import Prologue
|
||||
--
|
||||
-- Instantiating @trace@ to @[]@ yields a linear trace analysis, while @Set@ yields a reachable state analysis.
|
||||
newtype Tracing (trace :: * -> *) m (effects :: [* -> *]) a = Tracing (m effects a)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
|
||||
deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
|
||||
|
||||
deriving instance MonadControl term (m effects) => MonadControl term (Tracing trace m effects)
|
||||
deriving instance MonadEnvironment location value (m effects) => MonadEnvironment location value (Tracing trace m effects)
|
||||
|
Loading…
Reference in New Issue
Block a user