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

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

toIFile :: AbsolutePath -> AbsolutePath

data FindError

= NotFound [AbsolutePath]
| Ambiguous [AbsolutePath]

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 ()
type ModuleToSource = Map TopLevelModuleName AbsolutePath
type SourceToModule = Map AbsolutePath TopLevelModuleName
sourceToModule :: TCM SourceToModule
tests

Documentation

toIFile :: AbsolutePath -> AbsolutePath | Source

Converts an Agda file name to the corresponding interface file name.

data FindError | Source

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.

findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError | Source

Given the module name which the error applies to this function converts a `FindError` to a `TypeError`.

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.

findFile'' | Source

:: [AbsolutePath] | Include paths.
-> TopLevelModuleName |
-> ModuleToSource | Cached invocations of `findFile''`. An updated copy is returned.
-> IO (Either FindError AbsolutePath, ModuleToSource) |
A variant of `findFile'` which does not require `TCM`.

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.

checkModuleName | Source

:: 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.

type ModuleToSource = Map TopLevelModuleName AbsolutePath | Source

Maps top-level module names to the corresponding source file names.

type SourceToModule = Map AbsolutePath TopLevelModuleName | Source

Maps source file names to the corresponding top-level module names.

sourceToModule :: TCM SourceToModule | Source

Creates a `SourceToModule` map based on `stModuleToSource`.
tests
Produced by Haddock version 2.4.2