| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Monad.Imports

Synopsis

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 ()
preserveDecodedModules :: TCM a -> TCM a
getDecodedModule :: TopLevelModuleName -> TCM (Maybe (Interface, ClockTime))
storeDecodedModule :: Interface -> ClockTime -> TCM ()
dropDecodedModule :: TopLevelModuleName -> TCM ()
withImportPath :: [TopLevelModuleName] -> TCM a -> TCM a
checkForImportCycle :: TCM ()

Documentation

addImport :: ModuleName -> TCM () | Source

addImportCycleCheck :: TopLevelModuleName -> TCM a -> TCM a | Source

getImports :: TCM (Set ModuleName) | Source

isImported :: ModuleName -> TCM Bool | Source

getImportPath :: TCM [TopLevelModuleName] | Source

visitModule :: ModuleInfo -> TCM () | Source

setVisitedModules :: VisitedModules -> TCM () | Source

getVisitedModules :: TCM VisitedModules | Source

isVisited :: TopLevelModuleName -> TCM Bool | Source

getVisitedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo) | Source

getDecodedModules :: TCM DecodedModules | Source

setDecodedModules :: DecodedModules -> TCM () | Source

preserveDecodedModules :: TCM a -> TCM a | Source

getDecodedModule :: TopLevelModuleName -> TCM (Maybe (Interface, ClockTime)) | Source

storeDecodedModule :: Interface -> ClockTime -> TCM () | Source

dropDecodedModule :: TopLevelModuleName -> TCM () | Source

withImportPath :: [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.
Produced by Haddock version 2.4.2