Agda.TypeChecking.Monad.Imports

Documentation

addImport :: ModuleName -> TCM ()

addImportCycleCheck :: TopLevelModuleName -> TCM a -> TCM a

getImports :: TCM (Set ModuleName)

isImported :: ModuleName -> TCM Bool

getImportPath :: TCM [TopLevelModuleName]

visitModule :: ModuleInfo -> TCM ()

setVisitedModules :: VisitedModules -> TCM ()

getVisitedModules :: TCM VisitedModules

isVisited :: TopLevelModuleName -> TCM Bool

getVisitedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)

getDecodedModules :: TCM DecodedModules

setDecodedModules :: DecodedModules -> TCM ()

getDecodedModule :: TopLevelModuleName -> TCM (Maybe Interface)

storeDecodedModule :: Interface -> TCM ()

dropDecodedModule :: TopLevelModuleName -> TCM ()

withImportPath :: [TopLevelModuleName] -> TCM a -> TCM a

checkForImportCycle :: TCM ()

Assumes that the first module in the import path is the module we are worried about.