Agda.TypeChecking.Monad.Imports

Documentation

addImport :: TopLevelModuleName -> TCM ()

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

checkForImportCycle :: TCM ()

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

dropDecodedModule :: TopLevelModuleName -> TCM ()

getDecodedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)

getDecodedModules :: TCM DecodedModules

getImportPath :: TCM [TopLevelModuleName]

getPrettyVisitedModules :: ReadTCState m => m Doc

getVisitedModule :: ReadTCState m => TopLevelModuleName -> m (Maybe ModuleInfo)

getVisitedModules :: ReadTCState m => m VisitedModules

setDecodedModules :: DecodedModules -> TCM ()

setVisitedModules :: VisitedModules -> TCM ()

storeDecodedModule :: ModuleInfo -> TCM ()

visitModule :: ModuleInfo -> TCM ()

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