|
Agda.Interaction.FindFile |
|
|
Description |
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.
|
|
Synopsis |
|
|
|
Documentation |
|
|
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.
| Constructors | 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.
|
|
|
|
|
Given the module name which the error applies to this function
converts a FindError to a TypeError.
|
|
|
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.
|
|
|
Tries to find the source file corresponding to a given top-level
module name. The returned paths are absolute.
|
|
|
|
|
|
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.
|
|
|
|
Maps top-level module names to the corresponding source file
names.
|
|
|
Maps source file names to the corresponding top-level module
names.
|
|
|
Creates a SourceToModule map based on stModuleToSource.
|
|
tests |
|
Produced by Haddock version 2.4.2 |