Agda-2.2.4: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.Imports
Description
This modules deals with how to find imported modules and loading their interface files.
Synopsis
toIFile :: FilePath -> FilePath
mergeInterface :: Interface -> TCM ()
addImportedThings :: Signature -> BuiltinThings PrimFun -> TCM ()
data FileType
= SourceFile
| InterfaceFile
findFile :: FileType -> ModuleName -> TCM FilePath
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
alreadyVisited :: ModuleName -> TCM (Interface, ClockTime) -> TCM (Interface, ClockTime)
getInterface :: ModuleName -> TCM (Interface, ClockTime)
readInterface :: FilePath -> IO (Maybe Interface)
writeInterface :: FilePath -> Interface -> IO ()
data CreateInterfaceResult
= Success {
cirVisited :: VisitedModules
cirDecoded :: DecodedModules
cirInterface :: Interface
cirSignature :: Signature
cirBuiltin :: BuiltinThings PrimFun
}
| Warnings {
terminationProblems :: [([QName], [Range])]
unsolvedMetaVariables :: [Range]
}
createInterface :: CommandLineOptions -> CallTrace -> [ModuleName] -> VisitedModules -> DecodedModules -> Signature -> BuiltinThings PrimFun -> Maybe ModuleName -> FilePath -> Bool -> TCM (TopLevelInfo, CreateInterfaceResult)
buildInterface :: ModuleName -> HighlightingInfo -> TCM Interface
setWorkingDirectory :: FilePath -> [Declaration] -> IO ()
matchFileName :: ModuleName -> FilePath -> Bool
checkModuleName :: Maybe ModuleName -> FilePath -> TopLevelInfo -> TCM ()
isNewerThan :: FilePath -> FilePath -> IO Bool
Documentation
toIFile :: FilePath -> FilePathSource
Converts an Agda file name to the corresponding interface file name.
mergeInterface :: Interface -> TCM ()Source
Merge an interface into the current proof state.
addImportedThings :: Signature -> BuiltinThings PrimFun -> TCM ()Source
data FileType Source
Constructors
SourceFile
InterfaceFile
findFile :: FileType -> ModuleName -> TCM FilePathSource
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)Source
Scope checks the given module. A proper version of the module name (with correct definition sites) is returned.
alreadyVisited :: ModuleName -> TCM (Interface, ClockTime) -> TCM (Interface, ClockTime)Source
getInterface :: ModuleName -> TCM (Interface, ClockTime)Source
readInterface :: FilePath -> IO (Maybe Interface)Source
writeInterface :: FilePath -> Interface -> IO ()Source
data CreateInterfaceResult Source
Return type used by createInterface.
Constructors
SuccessEverything completed successfully, and an interface file was written.
cirVisited :: VisitedModules
cirDecoded :: DecodedModules
cirInterface :: Interface
cirSignature :: Signature
cirBuiltin :: BuiltinThings PrimFun
Warnings

Type checking was successful, except for some termination checking problems or unsolved meta-variables.

Meta-variable problems are reported as type errors unless we are type checking a top-level module and the flag to allow unsolved meta-variables has been selected.

terminationProblems :: [([QName], [Range])]
unsolvedMetaVariables :: [Range]
createInterfaceSource
:: CommandLineOptions
-> CallTrace
-> [ModuleName]
-> VisitedModules
-> DecodedModules
-> Signature
-> BuiltinThings PrimFun
-> Maybe ModuleNameExpected module name.
-> FilePathThe file to type check. Must be an absolute path.
-> BoolShould the working directory be changed to the root directory of the "project" containing the file?
-> TCM (TopLevelInfo, CreateInterfaceResult)

Tries to type check a module and write out its interface.

If appropriate this function writes out syntax highlighting information.

buildInterfaceSource
:: ModuleNameThe name of the current module.
-> HighlightingInfoSyntax highlighting info for the module.
-> TCM Interface
Builds an interface for the current module, which should already have been successfully type checked.
setWorkingDirectory :: FilePath -> [Declaration] -> IO ()Source

Set the current working directory based on the file name of the current module and its module name, so that when the module is imported qualified it will be found.

The given list of declarations should correspond to a module, i.e. it should be non-empty and the last declaration should be Module something.

matchFileName :: ModuleName -> FilePath -> BoolSource
Move somewhere else.
checkModuleNameSource
:: Maybe ModuleNameThe module should have this name (might be unknown).
-> FilePathThe module is defined in this file, whose file name is known to be consistent with the previous argument.
-> TopLevelInfoThe module.
-> TCM ()
Checks that the top-level module name, the file name and what we expect are consistent.
isNewerThan :: FilePath -> FilePath -> IO BoolSource
True if the first file is newer than the second file. If a file doesn't exist it is considered to be infinitely old.
Produced by Haddock version 2.4.2