From 0b0bd2a1a821e9bd41a11e3c98ac2410a7071ddb Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Wed, 25 Apr 2018 10:40:58 -0400 Subject: [PATCH] :fire: Control.Effect.Fresh in favour of Control.Monad.Effect.Fresh. --- semantic.cabal | 2 -- src/Analysis/Abstract/Caching.hs | 8 ++++++-- src/Analysis/Abstract/Evaluating.hs | 2 +- src/Control/Abstract/Addressable.hs | 4 ++-- src/Control/Abstract/Analysis.hs | 2 +- src/Control/Effect/Fresh.hs | 25 ------------------------- src/Data/Abstract/Type.hs | 4 ++-- 7 files changed, 12 insertions(+), 35 deletions(-) delete mode 100644 src/Control/Effect/Fresh.hs diff --git a/semantic.cabal b/semantic.cabal index 6e715627f..b41291640 100644 --- a/semantic.cabal +++ b/semantic.cabal @@ -45,8 +45,6 @@ library , Control.Abstract.Value -- Control flow , Control.Effect - -- Effects used for program analysis - , Control.Effect.Fresh -- Datatypes for abstract interpretation , Data.Abstract.Address , Data.Abstract.Cache diff --git a/src/Analysis/Abstract/Caching.hs b/src/Analysis/Abstract/Caching.hs index e9e547125..3a31734c7 100644 --- a/src/Analysis/Abstract/Caching.hs +++ b/src/Analysis/Abstract/Caching.hs @@ -5,6 +5,7 @@ module Analysis.Abstract.Caching ) where import Control.Abstract.Analysis +import Control.Monad.Effect hiding (interpret) import Data.Abstract.Address import Data.Abstract.Cache import Data.Abstract.Configuration @@ -93,15 +94,18 @@ instance ( Alternative (m effects) cache <- converge (\ prevCache -> isolateCache $ do putHeap (configurationHeap c) -- We need to reset fresh generation so that this invocation converges. - reset 0 + 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). We don’t need to use the values, so we 'gather' the -- nondeterministic values into @()@. - withOracle prevCache (raise (gather (const ()) (lower (liftAnalyze analyzeModule recur m))))) mempty + withOracle prevCache (raise (gather (const ()) (lower (liftAnalyze analyzeModule recur m))))) mempty maybe empty scatter (cacheLookup c cache) +reset :: (Effectful m, Member Fresh effects) => Int -> m effects a -> m effects a +reset start = raise . interposeState start (const pure) (\ counter Fresh yield -> (yield $! succ counter) counter) . lower + -- | 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 diff --git a/src/Analysis/Abstract/Evaluating.hs b/src/Analysis/Abstract/Evaluating.hs index 3182f6f52..3ccad25e0 100644 --- a/src/Analysis/Abstract/Evaluating.hs +++ b/src/Analysis/Abstract/Evaluating.hs @@ -77,7 +77,7 @@ instance ( Ord location . flip runReader mempty -- Reader (Environment location value) . flip runReader mempty -- Reader (ModuleTable [Module term]) . flip runReader mempty -- Reader (SomeOrigin term) - . runFresh + . flip runFresh' 0 . runFail . Res.runError . Exc.runError diff --git a/src/Control/Abstract/Addressable.hs b/src/Control/Abstract/Addressable.hs index c5f070e97..0fe6f8b0d 100644 --- a/src/Control/Abstract/Addressable.hs +++ b/src/Control/Abstract/Addressable.hs @@ -4,7 +4,7 @@ module Control.Abstract.Addressable where import Control.Abstract.Evaluator import Control.Applicative import Control.Effect -import Control.Effect.Fresh +import Control.Monad.Effect.Fresh import Control.Monad.Effect.Resumable as Eff import Data.Abstract.Address import Data.Abstract.Environment (insert) @@ -57,7 +57,7 @@ letrec' name body = do -- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written. instance (Effectful m, Member Fresh effects, Monad (m effects)) => MonadAddressable Precise effects m where derefCell _ = pure . unLatest - allocLoc _ = Precise <$> fresh + allocLoc _ = Precise <$> raise fresh -- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically. instance (Alternative (m effects), Effectful m, Member Fresh effects, Monad (m effects)) => MonadAddressable Monovariant effects m where diff --git a/src/Control/Abstract/Analysis.hs b/src/Control/Abstract/Analysis.hs index 64667a90b..28a4e1e60 100644 --- a/src/Control/Abstract/Analysis.hs +++ b/src/Control/Abstract/Analysis.hs @@ -15,8 +15,8 @@ import Control.Abstract.Addressable as X import Control.Abstract.Evaluator as X import Control.Abstract.Value as X import Control.Effect as X -import Control.Effect.Fresh as X import Control.Monad.Effect.Fail as X +import Control.Monad.Effect.Fresh as X import Control.Monad.Effect.Internal as X (Eff, relay) import Control.Monad.Effect.NonDet as X import Control.Monad.Effect.Reader as X diff --git a/src/Control/Effect/Fresh.hs b/src/Control/Effect/Fresh.hs deleted file mode 100644 index 35515ef85..000000000 --- a/src/Control/Effect/Fresh.hs +++ /dev/null @@ -1,25 +0,0 @@ -{-# LANGUAGE GADTs, MultiParamTypeClasses, TypeOperators, UndecidableInstances #-} -module Control.Effect.Fresh where - -import Control.Effect -import Control.Monad.Effect.Internal - --- | An effect offering a (resettable) sequence of always-incrementing, and therefore “fresh,” type variables. -data Fresh a where - -- | Request a reset of the sequence of variable names. - Reset :: Int -> Fresh () - -- | Request a fresh variable name. - Fresh :: Fresh Int - --- | Get a fresh variable name, guaranteed unused (since the last 'reset'). -fresh :: (Effectful m, Member Fresh effects) => m effects Int -fresh = raise (send Fresh) - --- | Reset the sequence of variable names. Useful to avoid complicated alpha-equivalence comparisons when iteratively recomputing the results of an analysis til convergence. -reset :: (Effectful m, Member Fresh effects) => Int -> m effects () -reset = raise . send . Reset - -runFresh :: Eff (Fresh ': effects) a -> Eff effects a -runFresh = relayState (0 :: Int) (const pure) (\ s action k -> case action of - Fresh -> k (succ s) s - Reset s' -> k s' ()) diff --git a/src/Data/Abstract/Type.hs b/src/Data/Abstract/Type.hs index 6d0c06a61..002cc70d8 100644 --- a/src/Data/Abstract/Type.hs +++ b/src/Data/Abstract/Type.hs @@ -67,7 +67,7 @@ instance ( Alternative (m effects) lambda names (Subterm _ body) = do (env, tvars) <- foldr (\ name rest -> do a <- alloc name - tvar <- Var <$> fresh + tvar <- Var <$> raise fresh assign a tvar (env, tvars) <- rest pure (Env.insert name a env, tvar : tvars)) (pure mempty) names @@ -126,7 +126,7 @@ instance ( Alternative (m effects) _ -> unify left right $> Bool call op params = do - tvar <- fresh + tvar <- raise fresh paramTypes <- sequenceA params unified <- op `unify` (Product paramTypes :-> Var tvar) case unified of