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

Agda.TypeChecking.Monad.Imports

Synopsis

addImport :: ModuleName -> TCM () addImportCycleCheck :: ModuleName -> TCM a -> TCM a getImports :: TCM (Set ModuleName) isImported :: ModuleName -> TCM Bool getImportPath :: TCM [ModuleName] visitModule :: ModuleName -> Interface -> ClockTime -> TCM () setVisitedModules :: VisitedModules -> TCM () getVisitedModules :: TCM VisitedModules isVisited :: ModuleName -> TCM Bool getVisitedModule :: ModuleName -> TCM (Maybe (Interface, ClockTime)) getAllModules :: TCM (Map ModuleName Interface) getDecodedModules :: TCM DecodedModules setDecodedModules :: DecodedModules -> TCM () preserveDecodedModules :: TCM a -> TCM a getDecodedModule :: ModuleName -> TCM (Maybe (Interface, ClockTime)) storeDecodedModule :: ModuleName -> Interface -> ClockTime -> TCM () dropDecodedModule :: ModuleName -> TCM () withImportPath :: [ModuleName] -> TCM a -> TCM a checkForImportCycle :: TCM ()

Documentation

addImport :: ModuleName -> TCM () Source

addImportCycleCheck :: ModuleName -> TCM a -> TCM a Source

getImports :: TCM (Set ModuleName) Source

isImported :: ModuleName -> TCM Bool Source

getImportPath :: TCM [ModuleName] Source

visitModule :: ModuleName -> Interface -> ClockTime -> TCM () Source

setVisitedModules :: VisitedModules -> TCM () Source

getVisitedModules :: TCM VisitedModules Source

isVisited :: ModuleName -> TCM Bool Source

getVisitedModule :: ModuleName -> TCM (Maybe (Interface, ClockTime)) Source

getAllModules :: TCM (Map ModuleName Interface) Source

This map includes the current module, if it has been type checked, along with the visited modules.

getDecodedModules :: TCM DecodedModules Source

setDecodedModules :: DecodedModules -> TCM () Source

preserveDecodedModules :: TCM a -> TCM a Source

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

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

dropDecodedModule :: ModuleName -> TCM () Source

withImportPath :: [ModuleName] -> 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