module Agda.TypeChecking.Monad.Caching
(
writeToCurrentLog
, readFromCachedLog
, cleanCachedLog
, cacheCurrentLog
, activateLoadedFileCache
, cachingStarts
, restorePostScopeState
) where
import Control.Monad.State
import qualified Data.Map as Map
import Agda.Syntax.Common
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
cachingStarts :: TCM ()
cachingStarts = do
NameId _ m <- use stFreshNameId
stFreshNameId .= NameId 1 m
writeToCurrentLog :: TypeCheckAction -> TCM ()
writeToCurrentLog !d = do
reportSLn "cache" 10 $ "cachePostScopeState"
!l <- gets stPostScopeState
modifyCache $ fmap $ \lfc -> lfc{ lfcCurrent = (d, l) : lfcCurrent lfc}
restorePostScopeState :: PostScopeState -> TCM ()
restorePostScopeState pss = do
reportSLn "cache" 10 $ "restorePostScopeState"
modify $ \s ->
let ipoints = s^.stInteractionPoints
pss' = pss{stPostInteractionPoints = stPostInteractionPoints pss `mergeIPMap` ipoints}
in s{stPostScopeState = pss'}
where
mergeIPMap lm sm = Map.mapWithKey (\k v -> maybe v (`mergeIP` v) (Map.lookup k lm)) sm
mergeIP li si = si {ipMeta = ipMeta li}
modifyCache
:: (Maybe LoadedFileCache -> Maybe LoadedFileCache)
-> TCM ()
modifyCache f = do
modify $ \s -> let !p = stPersistentState s in s
{ stPersistentState =
p { stLoadedFileCache = f (stLoadedFileCache p)}
}
getCache :: TCM (Maybe LoadedFileCache)
getCache = do
gets (stLoadedFileCache . stPersistentState)
putCache :: Maybe LoadedFileCache -> TCM ()
putCache cs = modifyCache $ const cs
readFromCachedLog :: TCM (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog = do
reportSLn "cache" 10 $ "getCachedTypeCheckAction"
mbCache <- getCache
case mbCache of
Just lfc | (entry : entries) <- lfcCached lfc -> do
putCache $ Just lfc{lfcCached = entries}
return (Just entry)
_ -> do
return Nothing
cleanCachedLog :: TCM ()
cleanCachedLog = do
reportSLn "cache" 10 $ "cleanCachedLog"
modifyCache $ fmap $ \lfc -> lfc{lfcCached = []}
activateLoadedFileCache :: TCM ()
activateLoadedFileCache = do
reportSLn "cache" 10 $ "activateLoadedFileCache"
b <- enableCaching
if not b then return ()
else do
modifyCache $ \mbLfc -> case mbLfc of
Nothing -> Just $ LoadedFileCache [] []
Just lfc | null (lfcCurrent lfc) -> Just lfc
_ -> __IMPOSSIBLE__
cacheCurrentLog :: TCM ()
cacheCurrentLog = do
reportSLn "cache" 10 $ "cacheCurrentTypeCheckLog"
modifyCache $ fmap $ \lfc ->
lfc{lfcCached = reverse (lfcCurrent lfc), lfcCurrent = []}