{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Monad.Caching
(
writeToCurrentLog
, readFromCachedLog
, cleanCachedLog
, cacheCurrentLog
, activateLoadedFileCache
, cachingStarts
, areWeCaching
, withoutCache
, restorePostScopeState
) where
import Control.Monad.State
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 {-# SOURCE #-} Agda.TypeChecking.Monad.Options
import Agda.Utils.Lens
import Agda.Utils.Monad
#include "undefined.h"
import Agda.Utils.Impossible
cachingStarts :: TCM ()
cachingStarts = do
NameId _ m <- useTC stFreshNameId
stFreshNameId `setTCLens` NameId 1 m
stAreWeCaching `setTCLens` True
areWeCaching :: TCM Bool
areWeCaching = useTC stAreWeCaching
writeToCurrentLog :: TypeCheckAction -> TCM ()
writeToCurrentLog !d = do
reportSLn "cache" 10 $ "cachePostScopeState"
!l <- getsTC stPostScopeState
modifyCache $ fmap $ \lfc -> lfc{ lfcCurrent = (d, l) : lfcCurrent lfc}
restorePostScopeState :: PostScopeState -> TCM ()
restorePostScopeState pss = do
reportSLn "cache" 10 $ "restorePostScopeState"
modifyTC $ \s ->
let ipoints = s^.stInteractionPoints
ws = s^.stTCWarnings
pss' = pss{stPostInteractionPoints = stPostInteractionPoints pss `mergeIPMap` ipoints
,stPostTCWarnings = stPostTCWarnings pss `mergeWarnings` ws
}
in s{stPostScopeState = pss'}
where
mergeIPMap lm sm = Map.mapWithKey (\k v -> maybe v (`mergeIP` v) (Map.lookup k lm)) sm
mergeIP li si = li { ipRange = ipRange si }
mergeWarnings loading current = [ w | w <- current, not $ tcWarningCached w ]
++ [ w | w <- loading, tcWarningCached w ]
modifyCache
:: (Maybe LoadedFileCache -> Maybe LoadedFileCache)
-> TCM ()
modifyCache f = do
modifyTC $ \s -> let !p = stPersistentState s in s
{ stPersistentState =
p { stLoadedFileCache = f (stLoadedFileCache p)}
}
getCache :: TCM (Maybe LoadedFileCache)
getCache = do
getsTC (stLoadedFileCache . stPersistentState)
putCache :: Maybe LoadedFileCache -> TCM ()
putCache cs = modifyCache $ const cs
withoutCache :: TCM a -> TCM a
withoutCache m =
bracket_ getCache putCache $ do
modifyCache (const Nothing)
m
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"
whenM (optGHCiInteraction <$> commandLineOptions) $
whenM enableCaching $ do
modifyCache $ \case
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 = []}