module Agda.TypeChecking.Monad.Imports where
import Control.Monad.State
import Control.Monad.Reader
import Data.Set (Set)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Agda.Syntax.Abstract.Name
import qualified Agda.Syntax.Concrete.Name as C
import Agda.TypeChecking.Monad.Base
import Agda.Utils.Monad
import Agda.Utils.Time
import Agda.Utils.Hash
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 = stDecodedModules . stPersistent <$> get
setDecodedModules :: DecodedModules -> TCM ()
setDecodedModules ms = modify $ \s ->
s { stPersistent = (stPersistent s) { stDecodedModules = ms } }
getDecodedModule :: C.TopLevelModuleName -> TCM (Maybe Interface)
getDecodedModule x = Map.lookup x . stDecodedModules . stPersistent <$> get
storeDecodedModule :: Interface -> TCM ()
storeDecodedModule i = modify $ \s ->
s { stPersistent =
(stPersistent s) { stDecodedModules =
Map.insert (toTopLevelModuleName $ iModuleName i) i $
(stDecodedModules $ stPersistent s)
}
}
dropDecodedModule :: C.TopLevelModuleName -> TCM ()
dropDecodedModule x = modify $ \s ->
s { stPersistent = (stPersistent s) { stDecodedModules =
Map.delete x $ stDecodedModules $ stPersistent s
}
}
withImportPath :: [C.TopLevelModuleName] -> TCM a -> TCM a
withImportPath path = local $ \e -> e { envImportPath = path }
checkForImportCycle :: TCM ()
checkForImportCycle = do
m:ms <- getImportPath
when (m `elem` ms) $ typeError $ CyclicModuleDependency
$ dropWhile (/= m) $ reverse (m:ms)