{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Monad.Caching
  ( -- * Log reading/writing operations
    writeToCurrentLog
  , readFromCachedLog
  , cleanCachedLog
  , cacheCurrentLog

    -- * Activating/deactivating
  , activateLoadedFileCache
  , cachingStarts
  , areWeCaching
  , noCacheForImportedModule

    -- * Restoring the 'PostScopeState'
  , 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

-- | To be called before any write or restore calls.
cachingStarts :: TCM ()
cachingStarts = do
    NameId _ m <- use stFreshNameId
    stFreshNameId .= NameId 1 m
    stAreWeCaching .= True

areWeCaching :: TCM Bool
areWeCaching = use stAreWeCaching

-- | Writes a 'TypeCheckAction' to the current log, using the current
-- 'PostScopeState'
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
        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
    -- see #1338 on why we need to use the new ranges.
    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
  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

-- | The cache should not be used for an imported module, and it
-- should be restored after the module has been type-checked. This
-- combinator takes care of that.

noCacheForImportedModule :: TCM a -> TCM a
noCacheForImportedModule m =
  bracket_ getCache putCache $ do
    modifyCache (const Nothing)
    m

-- | Reads the next entry in the cached type check log, if present.
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

-- | Empties the "to read" CachedState. To be used when it gets invalid.
cleanCachedLog :: TCM ()
cleanCachedLog = do
  reportSLn "cache" 10 $ "cleanCachedLog"
  modifyCache $ fmap $ \lfc -> 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.
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__

-- | Caches the current type check log.  Discardes the old cache.  Does
-- nothing if caching is inactive.
cacheCurrentLog :: TCM ()
cacheCurrentLog = do
  reportSLn "cache" 10 $ "cacheCurrentTypeCheckLog"
  modifyCache $ fmap $ \lfc ->
    lfc{lfcCached = reverse (lfcCurrent lfc), lfcCurrent = []}