module Agda.TypeChecking.Monad.Caching
(
writeToCurrentLog
, readFromCachedLog
, cleanCachedLog
, cacheCurrentLog
, activateLoadedFileCache
, cachingStarts
, areWeCaching
, localCache, withoutCache
, 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
{-# 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 <- Lens' NameId TCState -> m NameId
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC (NameId -> f NameId) -> TCState -> f TCState
Lens' NameId TCState
stFreshNameId
(NameId -> f NameId) -> TCState -> f TCState
Lens' NameId TCState
stFreshNameId Lens' NameId TCState -> NameId -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Word64 -> ModuleNameHash -> NameId
NameId Word64
1 ModuleNameHash
m
(Bool -> f Bool) -> TCState -> f TCState
Lens' Bool TCState
stAreWeCaching Lens' Bool TCState -> Bool -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Bool
True
ModuleNameHash -> m ()
forall {m :: * -> *}.
(MonadTCState m, ReadTCState m, MonadDebug m) =>
ModuleNameHash -> m ()
validateCache ModuleNameHash
m
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
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ModuleNameHash
m' ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
/= ModuleNameHash
m) m ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
Maybe (TypeCheckAction, PostScopeState)
_ -> do
() -> 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' Bool TCState -> m Bool
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR (Bool -> f Bool) -> TCState -> f TCState
Lens' Bool TCState
stAreWeCaching
{-# 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"
!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 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{ 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 :: 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
sTCState
-> Lens' (BiMap InteractionId InteractionPoint) TCState
-> BiMap InteractionId InteractionPoint
forall o i. o -> Lens' i o -> i
^.(BiMap InteractionId InteractionPoint
-> f (BiMap InteractionId InteractionPoint))
-> TCState -> f TCState
Lens' (BiMap InteractionId InteractionPoint) TCState
stInteractionPoints
ws :: [TCWarning]
ws = TCState
sTCState -> Lens' [TCWarning] TCState -> [TCWarning]
forall o i. o -> Lens' i o -> i
^.([TCWarning] -> f [TCWarning]) -> TCState -> f TCState
Lens' [TCWarning] TCState
stTCWarnings
pss' :: PostScopeState
pss' = PostScopeState
pss{stPostInteractionPoints :: BiMap InteractionId InteractionPoint
stPostInteractionPoints = PostScopeState -> BiMap InteractionId InteractionPoint
stPostInteractionPoints PostScopeState
pss BiMap InteractionId InteractionPoint
-> BiMap InteractionId InteractionPoint
-> BiMap InteractionId InteractionPoint
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 = (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
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 :: forall (m :: * -> *).
MonadTCState m =>
(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 (Maybe LoadedFileCache -> f (Maybe LoadedFileCache))
-> TCState -> f TCState
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 = Lens' (Maybe LoadedFileCache) TCState -> m (Maybe LoadedFileCache)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC (Maybe LoadedFileCache -> f (Maybe LoadedFileCache))
-> TCState -> f TCState
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 = Lens' (Maybe LoadedFileCache) TCState
-> Maybe LoadedFileCache -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens (Maybe LoadedFileCache -> f (Maybe LoadedFileCache))
-> TCState -> f TCState
Lens' (Maybe LoadedFileCache) TCState
stLoadedFileCache
{-# 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
{-# 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
{-# 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 : 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 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
{-# 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 :: CurrentTypeCheckLog
lfcCached = []}
{-# 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
$ CurrentTypeCheckLog -> CurrentTypeCheckLog -> LoadedFileCache
LoadedFileCache [] []
Just LoadedFileCache
lfc | CurrentTypeCheckLog -> Bool
forall a. [a] -> 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__
{-# 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 :: CurrentTypeCheckLog
lfcCached = CurrentTypeCheckLog -> CurrentTypeCheckLog
forall a. [a] -> [a]
reverse (LoadedFileCache -> CurrentTypeCheckLog
lfcCurrent LoadedFileCache
lfc), lfcCurrent :: CurrentTypeCheckLog
lfcCurrent = []}