| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Imports
Synopsis
- addImport :: TopLevelModuleName -> TCM ()
- addImportCycleCheck :: TopLevelModuleName -> TCM a -> TCM a
- checkForImportCycle :: TCM ()
- 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
Documentation
addImport :: TopLevelModuleName -> TCM () Source #
Register the given module as imported in the current state. Also recursively add its imports to the cumulative imports.
addImportCycleCheck :: TopLevelModuleName -> TCM a -> TCM a Source #
checkForImportCycle :: TCM () Source #
Assumes that the first module in the import path is the module we are worried about.
dropDecodedModule :: TopLevelModuleName -> TCM () Source #
getPrettyVisitedModules :: ReadTCState m => m Doc Source #
getVisitedModule :: ReadTCState m => TopLevelModuleName -> m (Maybe ModuleInfo) Source #
getVisitedModules :: ReadTCState m => m VisitedModules Source #
setDecodedModules :: DecodedModules -> TCM () Source #
setVisitedModules :: VisitedModules -> TCM () Source #
storeDecodedModule :: ModuleInfo -> TCM () Source #
visitModule :: ModuleInfo -> TCM () Source #
withImportPath :: [TopLevelModuleName] -> TCM a -> TCM a Source #