    {-# 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 qualified Data.Set as Set

    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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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 :: Set TCWarning
    ws = TCState
    s TCState -> Lens' TCState (Set TCWarning) -> Set TCWarning
    forall o i. o -> Lens' o i -> i
    ^. (Set TCWarning -> f (Set TCWarning)) -> TCState -> f TCState
    Lens' TCState (Set 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 :: Set TCWarning -> Set TCWarning -> Set TCWarning
    mergeWarnings Set TCWarning
    loading Set TCWarning
    current = (TCWarning -> Bool) -> Set TCWarning -> Set TCWarning
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (Bool -> Bool
    not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCWarning -> Bool
    tcWarningCached) Set TCWarning
    current
                            Set TCWarning -> Set TCWarning -> Set TCWarning
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` (TCWarning -> Bool) -> Set TCWarning -> Set TCWarning
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (      TCWarning -> Bool
    tcWarningCached) Set TCWarning
    loading

    {-# 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 = []}