Rephrase Caching as cachingTerms, convergingModules, and caching handlers.

src/Analysis/Abstract/Caching.hs

@@ -1,12 +1,12 @@
-{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
-{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the Interpreter instance’s Evaluator constraint
+{-# LANGUAGE GADTs, TypeOperators #-}
 module Analysis.Abstract.Caching
-( Caching
+( cachingTerms
+, convergingModules
+, caching
 ) where
 
-import Control.Abstract.Analysis
+import Control.Abstract.Evaluator
 import Control.Monad.Effect hiding (interpret)
-import Data.Abstract.Address
 import Data.Abstract.Cache
 import Data.Abstract.Configuration
 import Data.Abstract.Live
@@ -14,92 +14,84 @@ import Data.Abstract.Module
 import Data.Semilattice.Lower
 import Prologue
 
--- | A (coinductively-)cached analysis suitable for guaranteeing termination of (suitably finitized) analyses over recursive programs.
-newtype Caching m (effects :: [* -> *]) a = Caching { runCaching :: m effects a }
-  deriving (Alternative, Applicative, Functor, Effectful, Monad)
-
-deriving instance Evaluator location term value m => Evaluator location term value (Caching m)
-
 -- | Look up the set of values for a given configuration in the in-cache.
-consultOracle :: (Cacheable location term value, Effectful m, Member (Reader (Cache location term value)) effects) => Configuration location term value -> m effects (Set (value, Heap location value))
+consultOracle :: (Cacheable location term value, Member (Reader (Cache location term value)) effects) => Configuration location term value -> Evaluator location term value effects (Set (value, Heap location value))
 consultOracle configuration = raise (fromMaybe mempty . cacheLookup configuration <$> ask)
 
 -- | Run an action with the given in-cache.
-withOracle :: (Effectful m, Member (Reader (Cache location term value)) effects) => Cache location term value -> m effects a -> m effects a
+withOracle :: Member (Reader (Cache location term value)) effects => Cache location term value -> Evaluator location term value effects a -> Evaluator location term value effects a
 withOracle cache = raiseHandler (local (const cache))
 
 
 -- | Look up the set of values for a given configuration in the out-cache.
-lookupCache :: (Cacheable location term value, Effectful m, Member (State (Cache location term value)) effects) => Configuration location term value -> m effects (Maybe (Set (value, Heap location value)))
+lookupCache :: (Cacheable location term value, Member (State (Cache location term value)) effects) => Configuration location term value -> Evaluator location term value effects (Maybe (Set (value, Heap location value)))
 lookupCache configuration = raise (cacheLookup configuration <$> get)
 
 -- | Run an action, caching its result and 'Heap' under the given configuration.
-caching :: (Cacheable location term value, Effectful m, Member (State (Cache location term value)) effects, Member (State (Heap location value)) effects, Monad (m effects)) => Configuration location term value -> Set (value, Heap location value) -> m effects value -> m effects value
-caching configuration values action = do
+cachingConfiguration :: (Cacheable location term value, Member (State (Cache location term value)) effects, Member (State (Heap location value)) effects, Monad (Evaluator location term value effects)) => Configuration location term value -> Set (value, Heap location value) -> Evaluator location term value effects value -> Evaluator location term value effects value
+cachingConfiguration configuration values action = do
   raise (modify (cacheSet configuration values))
   result <- (,) <$> action <*> raise get
   raise (modify (cacheInsert configuration result))
   pure (fst result)
 
-putCache :: (Effectful m, Member (State (Cache location term value)) effects) => Cache location term value -> m effects ()
+putCache :: (Member (State (Cache location term value)) effects) => Cache location term value -> Evaluator location term value effects ()
 putCache = raise . put
 
 -- | Run an action starting from an empty out-cache, and return the out-cache afterwards.
-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 :: Member (State (Cache location term value)) effects => Evaluator location term value effects a -> Evaluator location term value effects (Cache location term value)
+isolateCache action = putCache lowerBound *> action *> raise get
 
-instance ( Alternative (m outer)
-         , AnalyzeTerm 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
-         )
-      => 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.
-  analyzeTerm recur e = do
-    c <- getConfiguration (embedSubterm e)
-    cached <- lookupCache c
-    case cached of
-      Just pairs -> scatter pairs
-      Nothing -> do
-        pairs <- consultOracle c
-        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
-    c <- getConfiguration (subterm (moduleBody m))
-    -- Convergence here is predicated upon an Eq instance, not α-equivalence
-    cache <- converge (\ prevCache -> isolateCache $ do
-      putHeap (configurationHeap 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). We don’t need to use the values, so we 'gather' the
-      -- nondeterministic values into @()@.
-        withOracle prevCache (raiseHandler  (gather (const ())) (Caching (analyzeModule (runCaching . recur) m)))) mempty
-    maybe empty scatter (cacheLookup c cache)
+-- | Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache.
+cachingTerms :: ( Cacheable location term value
+                , Corecursive term
+                , Members '[ Fresh
+                           , NonDet
+                           , Reader (Cache location term value)
+                           , Reader (Live location value)
+                           , State (Cache location term value)
+                           , State (Environment location value)
+                           , State (Heap location value)
+                           ] effects
+                )
+             => SubtermAlgebra (Base term) term (Evaluator location term value effects value)
+             -> SubtermAlgebra (Base term) term (Evaluator location term value effects value)
+cachingTerms recur term = do
+  c <- getConfiguration (embedSubterm term)
+  cached <- lookupCache c
+  case cached of
+    Just pairs -> scatter pairs
+    Nothing -> do
+      pairs <- consultOracle c
+      cachingConfiguration c pairs (recur term)
+
+convergingModules :: ( Cacheable location term value
+                     , Members '[ Fresh
+                                , NonDet
+                                , Reader (Cache location term value)
+                                , Reader (Live location value)
+                                , State (Cache location term value)
+                                , State (Environment location value)
+                                , State (Heap location value)
+                                ] effects
+                     )
+                  => SubtermAlgebra Module term (Evaluator location term value effects value)
+                  -> SubtermAlgebra Module term (Evaluator location term value effects value)
+convergingModules recur m = do
+  c <- getConfiguration (subterm (moduleBody m))
+  -- Convergence here is predicated upon an Eq instance, not α-equivalence
+  cache <- converge (\ prevCache -> isolateCache $ do
+    putHeap (configurationHeap 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). We don’t need to use the values, so we 'gather' the
+    -- nondeterministic values into @()@.
+      withOracle prevCache (raiseHandler (gather (const ())) (recur m))) lowerBound
+  maybe empty scatter (cacheLookup c cache)
 
 
 reset :: (Effectful m, Member Fresh effects) => Int -> m effects a -> m effects a
@@ -121,23 +113,12 @@ converge f = loop
             loop x'
 
 -- | Nondeterministically write each of a collection of stores & return their associated results.
-scatter :: (Alternative (m effects), Evaluator location term value m, Foldable t, Member (State (Heap location value)) effects) => t (a, Heap location value) -> m effects a
+scatter :: (Foldable t, Members '[NonDet, State (Heap location value)] effects) => t (a, Heap location value) -> Evaluator location term value effects a
 scatter = foldMapA (\ (value, heap') -> putHeap heap' $> value)
 
 
-instance ( Interpreter m effects
-         , Evaluator location term value m
-         , Ord (Cell location value)
-         , Ord location
-         , Ord term
-         , Ord value
-         )
-      => Interpreter (Caching m) (NonDet ': Reader (Cache location term value) ': State (Cache location term value) ': effects) where
-  type Result (Caching m) (NonDet ': Reader (Cache location term value) ': State (Cache location term value) ': effects) result = Result m effects ([result], Cache location term value)
-  interpret
-    = interpret
-    . runCaching
-    . raiseHandler
-      ( flip runState mempty
-      . flip runReader mempty
-      . makeChoiceA @[])
+caching :: Alternative f => Evaluator location term value (NonDet ': Reader (Cache location term value) ': State (Cache location term value) ': effects) a -> Evaluator location term value effects (f a, Cache location term value)
+caching
+  = handleState lowerBound
+  . handleReader lowerBound
+  . raiseHandler makeChoiceA