{-# LANGUAGE BangPatterns #-}

module Agda.TypeChecking.Monad.Caching
  ( -- * Log reading/writing operations
    writeToCurrentLog
  , readFromCachedLog
  , cleanCachedLog
  , cacheCurrentLog

    -- * Activating/deactivating
  , activateLoadedFileCache
  , cachingStarts
  , areWeCaching
  , localCache, withoutCache

    -- * Restoring the 'PostScopeState'
  , restorePostScopeState
  ) where


import qualified Data.Map as Map

import Agda.Syntax.Common

import Agda.Interaction.Options

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug

import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Null (empty)

import Agda.Utils.Impossible

-- | To be called before any write or restore calls.
{-# SPECIALIZE cachingStarts :: TCM () #-}
cachingStarts :: (MonadTCState m, ReadTCState m) => m ()
cachingStarts :: m ()
cachingStarts = do
    NameId Word64
_ Word64
m <- Lens' NameId TCState -> m NameId
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' NameId TCState
stFreshNameId
    Lens' NameId TCState
stFreshNameId Lens' NameId TCState -> NameId -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Word64 -> Word64 -> NameId
NameId Word64
1 Word64
m
    Lens' Bool TCState
stAreWeCaching Lens' Bool TCState -> Bool -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Bool
True

areWeCaching :: (ReadTCState m) => m Bool
areWeCaching :: m Bool
areWeCaching = Lens' Bool TCState -> m Bool
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' Bool TCState
stAreWeCaching

-- | Writes a 'TypeCheckAction' to the current log, using the current
-- 'PostScopeState'
{-# SPECIALIZE writeToCurrentLog :: TypeCheckAction -> TCM () #-}
writeToCurrentLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => TypeCheckAction -> m ()
writeToCurrentLog :: TypeCheckAction -> m ()
writeToCurrentLog !TypeCheckAction
d = do
  VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache" VerboseLevel
10 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"cachePostScopeState"
  !PostScopeState
l <- (TCState -> PostScopeState) -> m PostScopeState
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PostScopeState
stPostScopeState
  (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache ((Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ())
-> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall a b. (a -> b) -> a -> b
$ (LoadedFileCache -> LoadedFileCache)
-> Maybe LoadedFileCache -> Maybe LoadedFileCache
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LoadedFileCache -> LoadedFileCache)
 -> Maybe LoadedFileCache -> Maybe LoadedFileCache)
-> (LoadedFileCache -> LoadedFileCache)
-> Maybe LoadedFileCache
-> Maybe LoadedFileCache
forall a b. (a -> b) -> a -> b
$ \LoadedFileCache
lfc -> LoadedFileCache
lfc{ lfcCurrent :: CurrentTypeCheckLog
lfcCurrent = (TypeCheckAction
d, PostScopeState
l) (TypeCheckAction, PostScopeState)
-> CurrentTypeCheckLog -> CurrentTypeCheckLog
forall a. a -> [a] -> [a]
: LoadedFileCache -> CurrentTypeCheckLog
lfcCurrent LoadedFileCache
lfc}

{-# SPECIALIZE restorePostScopeState :: PostScopeState -> TCM () #-}
restorePostScopeState :: (MonadDebug m, MonadTCState m) => PostScopeState -> m ()
restorePostScopeState :: PostScopeState -> m ()
restorePostScopeState PostScopeState
pss = do
  VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache" VerboseLevel
10 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"restorePostScopeState"
  (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> m ()) -> (TCState -> TCState) -> m ()
forall a b. (a -> b) -> a -> b
$ \TCState
s ->
    let ipoints :: InteractionPoints
ipoints = TCState
sTCState -> Lens' InteractionPoints TCState -> InteractionPoints
forall o i. o -> Lens' i o -> i
^.Lens' InteractionPoints TCState
stInteractionPoints
        ws :: [TCWarning]
ws = TCState
sTCState -> Lens' [TCWarning] TCState -> [TCWarning]
forall o i. o -> Lens' i o -> i
^.Lens' [TCWarning] TCState
stTCWarnings
        pss' :: PostScopeState
pss' = PostScopeState
pss{stPostInteractionPoints :: InteractionPoints
stPostInteractionPoints = PostScopeState -> InteractionPoints
stPostInteractionPoints PostScopeState
pss InteractionPoints -> InteractionPoints -> InteractionPoints
forall k.
Ord k =>
Map k InteractionPoint
-> Map k InteractionPoint -> Map k InteractionPoint
`mergeIPMap` InteractionPoints
ipoints
                  ,stPostTCWarnings :: [TCWarning]
stPostTCWarnings = PostScopeState -> [TCWarning]
stPostTCWarnings PostScopeState
pss [TCWarning] -> [TCWarning] -> [TCWarning]
`mergeWarnings` [TCWarning]
ws
                  }
    in  TCState
s{stPostScopeState :: PostScopeState
stPostScopeState = PostScopeState
pss'}
  where
    mergeIPMap :: Map k InteractionPoint
-> Map k InteractionPoint -> Map k InteractionPoint
mergeIPMap Map k InteractionPoint
lm Map k InteractionPoint
sm = (k -> InteractionPoint -> InteractionPoint)
-> Map k InteractionPoint -> Map k InteractionPoint
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\k
k InteractionPoint
v -> InteractionPoint
-> (InteractionPoint -> InteractionPoint)
-> Maybe InteractionPoint
-> InteractionPoint
forall b a. b -> (a -> b) -> Maybe a -> b
maybe InteractionPoint
v (InteractionPoint -> InteractionPoint -> InteractionPoint
`mergeIP` InteractionPoint
v) (k -> Map k InteractionPoint -> Maybe InteractionPoint
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k InteractionPoint
lm)) Map k InteractionPoint
sm
    -- see #1338 on why we need to use the new ranges.
    mergeIP :: InteractionPoint -> InteractionPoint -> InteractionPoint
mergeIP InteractionPoint
li InteractionPoint
si = InteractionPoint
li { ipRange :: Range
ipRange = InteractionPoint -> Range
ipRange InteractionPoint
si }

    mergeWarnings :: [TCWarning] -> [TCWarning] -> [TCWarning]
mergeWarnings [TCWarning]
loading [TCWarning]
current = [ TCWarning
w | TCWarning
w <- [TCWarning]
current, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TCWarning -> Bool
tcWarningCached TCWarning
w ]
                                 [TCWarning] -> [TCWarning] -> [TCWarning]
forall a. [a] -> [a] -> [a]
++ [ TCWarning
w | TCWarning
w <- [TCWarning]
loading,       TCWarning -> Bool
tcWarningCached TCWarning
w ]

{-# SPECIALIZE modifyCache :: (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> TCM () #-}
modifyCache
  :: MonadTCState m
  => (Maybe LoadedFileCache -> Maybe LoadedFileCache)
  -> m ()
modifyCache :: (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache = Lens' (Maybe LoadedFileCache) TCState
-> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (Maybe LoadedFileCache) TCState
stLoadedFileCache

{-# SPECIALIZE getCache :: TCM (Maybe LoadedFileCache) #-}
getCache :: ReadTCState m => m (Maybe LoadedFileCache)
getCache :: m (Maybe LoadedFileCache)
getCache = Lens' (Maybe LoadedFileCache) TCState -> m (Maybe LoadedFileCache)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Maybe LoadedFileCache) TCState
stLoadedFileCache

{-# SPECIALIZE putCache :: Maybe LoadedFileCache -> TCM () #-}
putCache :: MonadTCState m => Maybe LoadedFileCache -> m ()
putCache :: Maybe LoadedFileCache -> m ()
putCache = Lens' (Maybe LoadedFileCache) TCState
-> Maybe LoadedFileCache -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' (Maybe LoadedFileCache) TCState
stLoadedFileCache

-- | Runs the action and restores the current cache at the end of it.
{-# SPECIALIZE localCache :: TCM a -> TCM a #-}
localCache :: (MonadTCState m, ReadTCState m) => m a -> m a
localCache :: m a -> m a
localCache = m (Maybe LoadedFileCache)
-> (Maybe LoadedFileCache -> m ()) -> m a -> m a
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ m (Maybe LoadedFileCache)
forall (m :: * -> *). ReadTCState m => m (Maybe LoadedFileCache)
getCache Maybe LoadedFileCache -> m ()
forall (m :: * -> *).
MonadTCState m =>
Maybe LoadedFileCache -> m ()
putCache

-- | Runs the action without cache and restores the current cache at
-- the end of it.
{-# SPECIALIZE withoutCache :: TCM a -> TCM a #-}
withoutCache :: (MonadTCState m, ReadTCState m) => m a -> m a
withoutCache :: m a -> m a
withoutCache m a
m = m a -> m a
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
localCache (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
    Maybe LoadedFileCache -> m ()
forall (m :: * -> *).
MonadTCState m =>
Maybe LoadedFileCache -> m ()
putCache Maybe LoadedFileCache
forall a. Null a => a
empty
    m a
m

-- | Reads the next entry in the cached type check log, if present.
{-# SPECIALIZE readFromCachedLog :: TCM (Maybe (TypeCheckAction, PostScopeState)) #-}
readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog :: m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog = do
  VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache" VerboseLevel
10 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"getCachedTypeCheckAction"
  m (Maybe LoadedFileCache)
forall (m :: * -> *). ReadTCState m => m (Maybe LoadedFileCache)
getCache m (Maybe LoadedFileCache)
-> (Maybe LoadedFileCache
    -> m (Maybe (TypeCheckAction, PostScopeState)))
-> m (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just LoadedFileCache
lfc | ((TypeCheckAction, PostScopeState)
entry : CurrentTypeCheckLog
entries) <- LoadedFileCache -> CurrentTypeCheckLog
lfcCached LoadedFileCache
lfc -> do
      Maybe LoadedFileCache -> m ()
forall (m :: * -> *).
MonadTCState m =>
Maybe LoadedFileCache -> m ()
putCache (Maybe LoadedFileCache -> m ()) -> Maybe LoadedFileCache -> m ()
forall a b. (a -> b) -> a -> b
$ LoadedFileCache -> Maybe LoadedFileCache
forall a. a -> Maybe a
Just LoadedFileCache
lfc{lfcCached :: CurrentTypeCheckLog
lfcCached = CurrentTypeCheckLog
entries}
      Maybe (TypeCheckAction, PostScopeState)
-> m (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *) a. Monad m => a -> m a
return ((TypeCheckAction, PostScopeState)
-> Maybe (TypeCheckAction, PostScopeState)
forall a. a -> Maybe a
Just (TypeCheckAction, PostScopeState)
entry)
    Maybe LoadedFileCache
_ -> do
      Maybe (TypeCheckAction, PostScopeState)
-> m (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TypeCheckAction, PostScopeState)
forall a. Maybe a
Nothing

-- | Empties the "to read" CachedState. To be used when it gets invalid.
{-# SPECIALIZE cleanCachedLog :: TCM () #-}
cleanCachedLog :: (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog :: m ()
cleanCachedLog = do
  VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache" VerboseLevel
10 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"cleanCachedLog"
  (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache ((Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ())
-> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall a b. (a -> b) -> a -> b
$ (LoadedFileCache -> LoadedFileCache)
-> Maybe LoadedFileCache -> Maybe LoadedFileCache
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LoadedFileCache -> LoadedFileCache)
 -> Maybe LoadedFileCache -> Maybe LoadedFileCache)
-> (LoadedFileCache -> LoadedFileCache)
-> Maybe LoadedFileCache
-> Maybe LoadedFileCache
forall a b. (a -> b) -> a -> b
$ \LoadedFileCache
lfc -> LoadedFileCache
lfc{lfcCached :: CurrentTypeCheckLog
lfcCached = []}

-- | Makes sure that the 'stLoadedFileCache' is 'Just', with a clean
-- current log. Crashes is 'stLoadedFileCache' is already active with a
-- dirty log.  Should be called when we start typechecking the current
-- file.
{-# SPECIALIZE activateLoadedFileCache :: TCM () #-}
activateLoadedFileCache :: (HasOptions m, MonadDebug m, MonadTCState m) => m ()
activateLoadedFileCache :: m ()
activateLoadedFileCache = do
  VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache" VerboseLevel
10 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"activateLoadedFileCache"

  m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (CommandLineOptions -> Bool
optGHCiInteraction (CommandLineOptions -> Bool) -> m CommandLineOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM m Bool
forall (m :: * -> *). HasOptions m => m Bool
enableCaching (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache ((Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ())
-> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall a b. (a -> b) -> a -> b
$ \case
         Maybe LoadedFileCache
Nothing                          -> LoadedFileCache -> Maybe LoadedFileCache
forall a. a -> Maybe a
Just (LoadedFileCache -> Maybe LoadedFileCache)
-> LoadedFileCache -> Maybe LoadedFileCache
forall a b. (a -> b) -> a -> b
$ CurrentTypeCheckLog -> CurrentTypeCheckLog -> LoadedFileCache
LoadedFileCache [] []
         Just LoadedFileCache
lfc | CurrentTypeCheckLog -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (LoadedFileCache -> CurrentTypeCheckLog
lfcCurrent LoadedFileCache
lfc) -> LoadedFileCache -> Maybe LoadedFileCache
forall a. a -> Maybe a
Just LoadedFileCache
lfc
         Maybe LoadedFileCache
_                                -> Maybe LoadedFileCache
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Caches the current type check log.  Discardes the old cache.  Does
-- nothing if caching is inactive.
{-# SPECIALIZE cacheCurrentLog :: TCM () #-}
cacheCurrentLog :: (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog :: m ()
cacheCurrentLog = do
  VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"cache" VerboseLevel
10 (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"cacheCurrentTypeCheckLog"
  (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache ((Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ())
-> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall a b. (a -> b) -> a -> b
$ (LoadedFileCache -> LoadedFileCache)
-> Maybe LoadedFileCache -> Maybe LoadedFileCache
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LoadedFileCache -> LoadedFileCache)
 -> Maybe LoadedFileCache -> Maybe LoadedFileCache)
-> (LoadedFileCache -> LoadedFileCache)
-> Maybe LoadedFileCache
-> Maybe LoadedFileCache
forall a b. (a -> b) -> a -> b
$ \LoadedFileCache
lfc ->
    LoadedFileCache
lfc{lfcCached :: CurrentTypeCheckLog
lfcCached = CurrentTypeCheckLog -> CurrentTypeCheckLog
forall a. [a] -> [a]
reverse (LoadedFileCache -> CurrentTypeCheckLog
lfcCurrent LoadedFileCache
lfc), lfcCurrent :: CurrentTypeCheckLog
lfcCurrent = []}