Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Monad.Imports

Synopsis

- addImport :: ModuleName -> TCM ()
- addImportCycleCheck :: TopLevelModuleName -> TCM a -> TCM a
- checkForImportCycle :: TCM ()
- dropDecodedModule :: TopLevelModuleName -> TCM ()
- getDecodedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)
- getDecodedModules :: TCM DecodedModules
- getImportPath :: TCM [TopLevelModuleName]
- getImports :: TCM (Set ModuleName)
- getPrettyVisitedModules :: ReadTCState m => m Doc
- getVisitedModule :: ReadTCState m => TopLevelModuleName -> m (Maybe ModuleInfo)
- getVisitedModules :: ReadTCState m => m VisitedModules
- isImported :: ModuleName -> TCM Bool
- setDecodedModules :: DecodedModules -> TCM ()
- setVisitedModules :: VisitedModules -> TCM ()
- storeDecodedModule :: ModuleInfo -> TCM ()
- visitModule :: ModuleInfo -> TCM ()
- withImportPath :: [TopLevelModuleName] -> TCM a -> TCM a

# Documentation

addImport :: ModuleName -> TCM () Source #

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 #

getDecodedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo) Source #

getDecodedModules :: TCM DecodedModules Source #

getImportPath :: TCM [TopLevelModuleName] Source #

getImports :: TCM (Set ModuleName) Source #

getPrettyVisitedModules :: ReadTCState m => m Doc Source #

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

getVisitedModules :: ReadTCState m => m VisitedModules Source #

isImported :: ModuleName -> TCM Bool Source #

setDecodedModules :: DecodedModules -> TCM () Source #

setVisitedModules :: VisitedModules -> TCM () Source #

storeDecodedModule :: ModuleInfo -> TCM () Source #

visitModule :: ModuleInfo -> TCM () Source #

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