{-# OPTIONS_GHC -Wunused-imports #-}

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 _ m <- Lens' TCState NameId -> m NameId
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
stFreshNameId
    stFreshNameId `setTCLens` NameId 1 m
    stFreshOpaqueId `setTCLens` OpaqueId 1 m
    stAreWeCaching `setTCLens` True
    validateCache m -- fixes issue #4835
    where
      validateCache :: ModuleNameHash -> m ()
validateCache ModuleNameHash
m = (m (Maybe (TypeCheckAction, PostScopeState))
-> m (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
localCache m (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog) m (Maybe (TypeCheckAction, PostScopeState))
-> (Maybe (TypeCheckAction, PostScopeState) -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
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
            OpaqueId Word64
_ ModuleNameHash
m'' = PostScopeState -> OpaqueId
stPostFreshOpaqueId PostScopeState
s
            stale :: Bool
stale = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ ModuleNameHash
m' ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
/= ModuleNameHash
m, ModuleNameHash
m'' ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
/= ModuleNameHash
m ]
          Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
stale m ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
        Maybe (TypeCheckAction, PostScopeState)
_ -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

areWeCaching :: (ReadTCState m) => m Bool
areWeCaching :: forall (m :: * -> *). ReadTCState m => m Bool
areWeCaching = Lens' TCState Bool -> m Bool
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
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
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"cachePostScopeState"
  !l <- (TCState -> PostScopeState) -> m PostScopeState
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PostScopeState
stPostScopeState
  modifyCache $ fmap $ \LoadedFileCache
lfc -> LoadedFileCache
lfc{ lfcCurrent = (d, l) : lfcCurrent 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
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"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 :: BiMap InteractionId InteractionPoint
ipoints = TCState
s TCState
-> Lens' TCState (BiMap InteractionId InteractionPoint)
-> BiMap InteractionId InteractionPoint
forall o i. o -> Lens' o i -> i
^. (BiMap InteractionId InteractionPoint
 -> f (BiMap InteractionId InteractionPoint))
-> TCState -> f TCState
Lens' TCState (BiMap InteractionId InteractionPoint)
stInteractionPoints
        ws :: [TCWarning]
ws = TCState
s TCState -> Lens' TCState [TCWarning] -> [TCWarning]
forall o i. o -> Lens' o i -> i
^. ([TCWarning] -> f [TCWarning]) -> TCState -> f TCState
Lens' TCState [TCWarning]
stTCWarnings
        pss' :: PostScopeState
pss' = PostScopeState
pss{stPostInteractionPoints = stPostInteractionPoints pss `mergeIPMap` ipoints
                  ,stPostTCWarnings = stPostTCWarnings pss `mergeWarnings` ws
                  ,stPostOpaqueBlocks = s ^. stOpaqueBlocks
                  ,stPostOpaqueIds = s ^. stOpaqueIds
                  }
    in  TCState
s{stPostScopeState = pss'}
  where
    mergeIPMap :: BiMap k InteractionPoint
-> BiMap k InteractionPoint -> BiMap k InteractionPoint
mergeIPMap BiMap k InteractionPoint
lm BiMap k InteractionPoint
sm = (k -> InteractionPoint -> InteractionPoint)
-> BiMap k InteractionPoint -> BiMap k InteractionPoint
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 -> 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 -> BiMap k InteractionPoint -> Maybe InteractionPoint
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 = ipRange 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 :: forall (m :: * -> *).
MonadTCState m =>
(Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
modifyCache = Lens' TCState (Maybe LoadedFileCache)
-> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (Maybe LoadedFileCache -> f (Maybe LoadedFileCache))
-> TCState -> f TCState
Lens' TCState (Maybe LoadedFileCache)
stLoadedFileCache

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

{-# SPECIALIZE putCache :: Maybe LoadedFileCache -> TCM () #-}
putCache :: MonadTCState m => Maybe LoadedFileCache -> m ()
putCache :: forall (m :: * -> *).
MonadTCState m =>
Maybe LoadedFileCache -> m ()
putCache = Lens' TCState (Maybe LoadedFileCache)
-> Maybe LoadedFileCache -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (Maybe LoadedFileCache -> f (Maybe LoadedFileCache))
-> TCState -> f TCState
Lens' TCState (Maybe LoadedFileCache)
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 = 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 :: forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
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 :: forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog = do
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"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 a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just LoadedFileCache
lfc | ((TypeCheckAction, PostScopeState)
entry : [(TypeCheckAction, PostScopeState)]
entries) <- LoadedFileCache -> [(TypeCheckAction, PostScopeState)]
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 = entries}
      Maybe (TypeCheckAction, PostScopeState)
-> m (Maybe (TypeCheckAction, PostScopeState))
forall a. a -> m a
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 a. a -> m a
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 :: forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog = do
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"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 a b. (a -> b) -> Maybe a -> Maybe b
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 = []}

-- | 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
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"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
$ [(TypeCheckAction, PostScopeState)]
-> [(TypeCheckAction, PostScopeState)] -> LoadedFileCache
LoadedFileCache [] []
         Just LoadedFileCache
lfc | [(TypeCheckAction, PostScopeState)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (LoadedFileCache -> [(TypeCheckAction, PostScopeState)]
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 :: forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog = do
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"cache" VerboseLevel
10 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"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 a b. (a -> b) -> Maybe a -> Maybe b
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 = reverse (lfcCurrent lfc), lfcCurrent = []}