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 Agda.Syntax.Common

import Agda.Interaction.Options

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

import qualified Agda.Utils.BiMap as BiMap
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 :: (MonadDebug m, MonadTCState m, ReadTCState m) => m ()
cachingStarts :: forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m ()
cachingStarts = do
    NameId Word64
_ ModuleNameHash
m <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' NameId TCState
stFreshNameId
    Lens' NameId TCState
stFreshNameId forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Word64 -> ModuleNameHash -> NameId
NameId Word64
1 ModuleNameHash
m
    Lens' Bool TCState
stAreWeCaching forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Bool
True
    forall {m :: * -> *}.
(MonadTCState m, ReadTCState m, MonadDebug m) =>
ModuleNameHash -> m ()
validateCache ModuleNameHash
m -- fixes issue #4835
    where
      validateCache :: ModuleNameHash -> m ()
validateCache ModuleNameHash
m = (forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
localCache forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (TypeCheckAction
_ , PostScopeState
s) -> do
          let NameId Word64
_ ModuleNameHash
m' = PostScopeState -> NameId
stPostFreshNameId PostScopeState
s
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ModuleNameHash
m' forall a. Eq a => a -> a -> Bool
/= ModuleNameHash
m) forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
        Maybe (TypeCheckAction, PostScopeState)
_ -> do
          forall (m :: * -> *) a. Monad m => a -> m a
return ()

areWeCaching :: (ReadTCState m) => m Bool
areWeCaching :: forall (m :: * -> *). ReadTCState m => m Bool
areWeCaching = 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 :: forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog !TypeCheckAction
d = do
  forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 forall a b. (a -> b) -> a -> b
$ String
"cachePostScopeState"
  !PostScopeState
l <- forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PostScopeState
stPostScopeState
  forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \LoadedFileCache
lfc -> LoadedFileCache
lfc{ lfcCurrent :: CurrentTypeCheckLog
lfcCurrent = (TypeCheckAction
d, PostScopeState
l) forall a. a -> [a] -> [a]
: LoadedFileCache -> CurrentTypeCheckLog
lfcCurrent LoadedFileCache
lfc}

{-# SPECIALIZE restorePostScopeState :: PostScopeState -> TCM () #-}
restorePostScopeState :: (MonadDebug m, MonadTCState m) => PostScopeState -> m ()
restorePostScopeState :: forall (m :: * -> *).
(MonadDebug m, MonadTCState m) =>
PostScopeState -> m ()
restorePostScopeState PostScopeState
pss = do
  forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 forall a b. (a -> b) -> a -> b
$ String
"restorePostScopeState"
  forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall a b. (a -> b) -> a -> b
$ \TCState
s ->
    let ipoints :: BiMap InteractionId InteractionPoint
ipoints = TCState
sforall o i. o -> Lens' i o -> i
^.Lens' (BiMap InteractionId InteractionPoint) TCState
stInteractionPoints
        ws :: [TCWarning]
ws = TCState
sforall o i. o -> Lens' i o -> i
^.Lens' [TCWarning] TCState
stTCWarnings
        pss' :: PostScopeState
pss' = PostScopeState
pss{stPostInteractionPoints :: BiMap InteractionId InteractionPoint
stPostInteractionPoints = PostScopeState -> BiMap InteractionId InteractionPoint
stPostInteractionPoints PostScopeState
pss forall {k}.
Ord k =>
BiMap k InteractionPoint
-> BiMap k InteractionPoint -> BiMap k InteractionPoint
`mergeIPMap` BiMap InteractionId InteractionPoint
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 :: BiMap k InteractionPoint
-> BiMap k InteractionPoint -> BiMap k InteractionPoint
mergeIPMap BiMap k InteractionPoint
lm BiMap k InteractionPoint
sm = forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(k -> v -> v) -> BiMap k v -> BiMap k v
BiMap.mapWithKey (\k
k InteractionPoint
v -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe InteractionPoint
v (InteractionPoint -> InteractionPoint -> InteractionPoint
`mergeIP` InteractionPoint
v) (forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup k
k BiMap k InteractionPoint
lm)) BiMap 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 forall a b. (a -> b) -> a -> b
$ TCWarning -> Bool
tcWarningCached TCWarning
w ]
                                 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 :: forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache = 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 :: forall (m :: * -> *). ReadTCState m => m (Maybe LoadedFileCache)
getCache = 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 :: forall (m :: * -> *).
MonadTCState m =>
Maybe LoadedFileCache -> m ()
putCache = 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 :: forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
localCache = forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ forall (m :: * -> *). ReadTCState m => m (Maybe LoadedFileCache)
getCache 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 :: forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
withoutCache m a
m = forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
localCache forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadTCState m =>
Maybe LoadedFileCache -> m ()
putCache 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 :: forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog = do
  forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 forall a b. (a -> b) -> a -> b
$ String
"getCachedTypeCheckAction"
  forall (m :: * -> *). ReadTCState m => m (Maybe LoadedFileCache)
getCache 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
      forall (m :: * -> *).
MonadTCState m =>
Maybe LoadedFileCache -> m ()
putCache forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just LoadedFileCache
lfc{lfcCached :: CurrentTypeCheckLog
lfcCached = CurrentTypeCheckLog
entries}
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (TypeCheckAction, PostScopeState)
entry)
    Maybe LoadedFileCache
_ -> do
      forall (m :: * -> *) a. Monad m => a -> m a
return 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 :: forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog = do
  forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 forall a b. (a -> b) -> a -> b
$ String
"cleanCachedLog"
  forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 :: forall (m :: * -> *).
(HasOptions m, MonadDebug m, MonadTCState m) =>
m ()
activateLoadedFileCache = do
  forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 forall a b. (a -> b) -> a -> b
$ String
"activateLoadedFileCache"

  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (CommandLineOptions -> Bool
optGHCiInteraction forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
enableCaching forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache forall a b. (a -> b) -> a -> b
$ \case
         Maybe LoadedFileCache
Nothing                          -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ CurrentTypeCheckLog -> CurrentTypeCheckLog -> LoadedFileCache
LoadedFileCache [] []
         Just LoadedFileCache
lfc | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (LoadedFileCache -> CurrentTypeCheckLog
lfcCurrent LoadedFileCache
lfc) -> forall a. a -> Maybe a
Just LoadedFileCache
lfc
         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 :: forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog = do
  forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 forall a b. (a -> b) -> a -> b
$ String
"cacheCurrentTypeCheckLog"
  forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \LoadedFileCache
lfc ->
    LoadedFileCache
lfc{lfcCached :: CurrentTypeCheckLog
lfcCached = forall a. [a] -> [a]
reverse (LoadedFileCache -> CurrentTypeCheckLog
lfcCurrent LoadedFileCache
lfc), lfcCurrent :: CurrentTypeCheckLog
lfcCurrent = []}