module Agda.TypeChecking.Monad.Imports where

import Control.Monad.State
import Control.Monad.Reader

import Data.Maybe
import Data.Map (Map)
import Data.Set (Set)
import qualified Data.Map as Map
import qualified Data.List as List
import qualified Data.Set as Set

import System.Time

import Agda.Syntax.Abstract.Name
import qualified Agda.Syntax.Concrete.Name as C
import Agda.TypeChecking.Monad.Base
import Agda.Utils.Monad

addImport :: ModuleName -> TCM ()
addImport m =
    modify $ \s -> s { stImportedModules = Set.insert m $ stImportedModules s }

addImportCycleCheck :: C.TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck m =
    local $ \e -> e { envImportPath = m : envImportPath e }

getImports :: TCM (Set ModuleName)
getImports = gets stImportedModules

isImported :: ModuleName -> TCM Bool
isImported m = Set.member m <$> getImports

getImportPath :: TCM [C.TopLevelModuleName]
getImportPath = asks envImportPath

visitModule :: ModuleInfo -> TCM ()
visitModule mi = modify $ \s ->
  s { stVisitedModules =
        Map.insert (toTopLevelModuleName $ iModuleName $ miInterface mi)
                   mi $
          stVisitedModules s }

setVisitedModules :: VisitedModules -> TCM ()
setVisitedModules ms = modify $ \s -> s { stVisitedModules = ms }

getVisitedModules :: TCM VisitedModules
getVisitedModules = gets stVisitedModules

isVisited :: C.TopLevelModuleName -> TCM Bool
isVisited x = gets $ Map.member x . stVisitedModules

getVisitedModule :: C.TopLevelModuleName
                 -> TCM (Maybe ModuleInfo)
getVisitedModule x = gets $ Map.lookup x . stVisitedModules

getDecodedModules :: TCM DecodedModules
getDecodedModules = gets stDecodedModules

setDecodedModules :: DecodedModules -> TCM ()
setDecodedModules ms = modify $ \s -> s { stDecodedModules = ms }

preserveDecodedModules :: TCM a -> TCM a
preserveDecodedModules tcm = do ms <- getDecodedModules
                                a  <- tcm
                                setDecodedModules ms
                                return a

getDecodedModule :: C.TopLevelModuleName -> TCM (Maybe (Interface, ClockTime))
getDecodedModule x = gets $ Map.lookup x . stDecodedModules

storeDecodedModule :: Interface -> ClockTime -> TCM ()
storeDecodedModule i t = modify $ \s ->
  s { stDecodedModules =
        Map.insert (toTopLevelModuleName $ iModuleName i) (i, t) $
          stDecodedModules s }

dropDecodedModule :: C.TopLevelModuleName -> TCM ()
dropDecodedModule x = modify $ \s -> s { stDecodedModules = Map.delete x $ stDecodedModules s }

withImportPath :: [C.TopLevelModuleName] -> TCM a -> TCM a
withImportPath path = local $ \e -> e { envImportPath = path }

-- | Assumes that the first module in the import path is the module we are
--   worried about.
checkForImportCycle :: TCM ()
checkForImportCycle = do
    m:ms <- getImportPath
    when (m `elem` ms) $ typeError $ CyclicModuleDependency
				   $ dropWhile (/= m) $ reverse (m:ms)