Safe Haskell | None |
---|---|
Language | Haskell98 |
Functions which map between module names and file names.
Note that file name lookups are cached in the TCState
. The code
assumes that no Agda source files are added or removed from the
include directories while the code is being type checked.
- toIFile :: AbsolutePath -> AbsolutePath
- data FindError
- findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
- findFile :: TopLevelModuleName -> TCM AbsolutePath
- findFile' :: TopLevelModuleName -> TCM (Either FindError AbsolutePath)
- findFile'' :: [AbsolutePath] -> TopLevelModuleName -> ModuleToSource -> IO (Either FindError AbsolutePath, ModuleToSource)
- findInterfaceFile :: TopLevelModuleName -> TCM (Maybe AbsolutePath)
- checkModuleName :: TopLevelModuleName -> AbsolutePath -> TCM ()
- moduleName' :: AbsolutePath -> TCM TopLevelModuleName
- moduleName :: AbsolutePath -> TCM TopLevelModuleName
- tests :: IO Bool
Documentation
toIFile :: AbsolutePath -> AbsolutePath Source
Converts an Agda file name to the corresponding interface file name.
Errors which can arise when trying to find a source file.
Invariant: All paths are absolute.
NotFound [AbsolutePath] | The file was not found. It should have had one of the given file names. |
Ambiguous [AbsolutePath] | Several matching files were found. Invariant: The list of matching files has at least two elements. |
findFile :: TopLevelModuleName -> TCM AbsolutePath Source
Finds the source file corresponding to a given top-level module name. The returned paths are absolute.
Raises an error if the file cannot be found.
findFile' :: TopLevelModuleName -> TCM (Either FindError AbsolutePath) Source
Tries to find the source file corresponding to a given top-level module name. The returned paths are absolute.
SIDE EFFECT: Updates stModuleToSource
.
:: [AbsolutePath] | Include paths. |
-> TopLevelModuleName | |
-> ModuleToSource | Cached invocations of |
-> IO (Either FindError AbsolutePath, ModuleToSource) |
findInterfaceFile :: TopLevelModuleName -> TCM (Maybe AbsolutePath) Source
Finds the interface file corresponding to a given top-level module name. The returned paths are absolute.
Raises an error if the source file cannot be found, and returns
Nothing
if the source file can be found but not the interface
file.
:: TopLevelModuleName | The name of the module. |
-> AbsolutePath | The file from which it was loaded. |
-> TCM () |
Ensures that the module name matches the file name. The file corresponding to the module name (according to the include path) has to be the same as the given file name.
moduleName' :: AbsolutePath -> TCM TopLevelModuleName Source
Computes the module name of the top-level module in the given file.
Warning! Parses the whole file to get the module name out. Use wisely!
moduleName :: AbsolutePath -> TCM TopLevelModuleName Source
A variant of moduleName'
which raises an error if the file name
does not match the module name.
The file name is interpreted relative to the current working directory (unless it is absolute).