Safe Haskell	Safe-Inferred
Language	Haskell2010

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

newtype SourceFile = SourceFile {
- srcFilePath :: AbsolutePath
}
data InterfaceFile
toIFile :: SourceFile -> TCM AbsolutePath
mkInterfaceFile :: AbsolutePath -> IO (Maybe InterfaceFile)
data FindError
- = NotFound [SourceFile]
- | Ambiguous [SourceFile]
findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
findFile :: TopLevelModuleName -> TCM SourceFile
findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile'' :: [AbsolutePath] -> TopLevelModuleName -> ModuleToSource -> IO (Either FindError SourceFile, ModuleToSource)
findInterfaceFile' :: SourceFile -> TCM (Maybe InterfaceFile)
findInterfaceFile :: TopLevelModuleName -> TCM (Maybe InterfaceFile)
checkModuleName :: TopLevelModuleName -> SourceFile -> Maybe TopLevelModuleName -> TCM ()
moduleName :: AbsolutePath -> Module -> TCM TopLevelModuleName
rootNameModule :: AbsolutePath -> String
replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath

Documentation

newtype SourceFile Source #

Type aliases for source files and interface files. We may only produce one of these if we know for sure that the file does exist. We can always output an AbsolutePath if we are not sure.

Constructors

SourceFile
Fields srcFilePath :: AbsolutePath

Instances

Instances details

Pretty SourceFile Source #
Instance details Defined in Agda.Interaction.FindFile Methods pretty :: SourceFile -> Doc Source # prettyPrec :: Int -> SourceFile -> Doc Source # prettyList :: [SourceFile] -> Doc Source #
Show SourceFile Source #
Instance details Defined in Agda.Interaction.FindFile Methods showsPrec :: Int -> SourceFile -> ShowS # show :: SourceFile -> String # showList :: [SourceFile] -> ShowS #
Eq SourceFile Source #
Instance details Defined in Agda.Interaction.FindFile Methods (==) :: SourceFile -> SourceFile -> Bool # (/=) :: SourceFile -> SourceFile -> Bool #
Ord SourceFile Source #
Instance details Defined in Agda.Interaction.FindFile Methods compare :: SourceFile -> SourceFile -> Ordering # (<) :: SourceFile -> SourceFile -> Bool # (<=) :: SourceFile -> SourceFile -> Bool # (>) :: SourceFile -> SourceFile -> Bool # (>=) :: SourceFile -> SourceFile -> Bool # max :: SourceFile -> SourceFile -> SourceFile # min :: SourceFile -> SourceFile -> SourceFile #

data InterfaceFile Source #

Instances

Instances details

Pretty InterfaceFile Source #
Instance details Defined in Agda.Interaction.FindFile Methods pretty :: InterfaceFile -> Doc Source # prettyPrec :: Int -> InterfaceFile -> Doc Source # prettyList :: [InterfaceFile] -> Doc Source #

toIFile :: SourceFile -> TCM AbsolutePath Source #

Converts an Agda file name to the corresponding interface file name. Note that we do not guarantee that the file exists.

mkInterfaceFile Source #

Arguments

:: AbsolutePath	Path to the candidate interface file
-> IO (Maybe InterfaceFile)	Interface file iff it exists

Makes an interface file from an AbsolutePath candidate. If the file does not exist, then fail by returning Nothing.

data FindError Source #

Errors which can arise when trying to find a source file.

Invariant: All paths are absolute.

Constructors

NotFound [SourceFile]

The file was not found. It should have had one of the given file names.

Ambiguous [SourceFile]

Several matching files were found.

Invariant: The list of matching files has at least two elements.

Instances

Instances details

Show FindError Source #
Instance details Defined in Agda.Interaction.FindFile Methods showsPrec :: Int -> FindError -> ShowS # show :: FindError -> String # showList :: [FindError] -> ShowS #

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 SourceFile 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 SourceFile) Source #

Tries to find the source file corresponding to a given top-level module name. The returned paths are absolute.

SIDE EFFECT: Updates stModuleToSource.

findFile'' Source #

Arguments

:: [AbsolutePath]	Include paths.
-> TopLevelModuleName
-> ModuleToSource	Cached invocations of `findFile''`. An updated copy is returned.
-> IO (Either FindError SourceFile, ModuleToSource)

A variant of findFile' which does not require TCMT.

findInterfaceFile' Source #

Arguments

:: SourceFile	Path to the source file
-> TCM (Maybe InterfaceFile)	Maybe path to the interface file

Finds the interface file corresponding to a given top-level module file. The returned paths are absolute.

Raises Nothing if the interface file cannot be found.

findInterfaceFile :: TopLevelModuleName -> TCM (Maybe InterfaceFile) Source #

Finds the interface file corresponding to a given top-level module file. 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 #

Arguments

:: TopLevelModuleName	The name of the module.
-> SourceFile	The file from which it was loaded.
-> Maybe TopLevelModuleName	The expected name, coming from an import statement.
-> 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 Source #

Arguments

:: AbsolutePath	The path to the file.
-> Module	The parsed module.
-> TCM TopLevelModuleName

Computes the module name of the top-level module in the given file.

If no top-level module name is given, then an attempt is made to use the file name as a module name.

rootNameModule :: AbsolutePath -> String Source #

replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath Source #