🔥 Control.Effect.Fresh in favour of Control.Monad.Effect.Fresh.

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

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

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

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

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

src/Control/Effect/Fresh.hs

@@ -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' ())

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