ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.FindFile

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.

3 types
16 values

PackageAgda-2.8.0.2
Exports19
LanguageHaskell2010
LicenceMIT
SourceFindFile.hs

newtypenewtype SourceFile

SourceFiles must exist and be registered in our file dictionary.

Constructors

SourceFile
- srcFileId :: FileId

Instances6Eq, Ord, Show, Generic, NFData, Rep

Eq SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
Ord SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
Show SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
Generic SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
NFData SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
type Rep SourceFile = D1 ('MetaData "SourceFile" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types

newtypenewtype InterfaceFile

File must exist.

Instances1Pretty

Pretty InterfaceFileDefined in Agda-2.8.0.2 · Agda.Interaction.FindFile

valueintFilePath :: InterfaceFile -> AbsolutePath

valuetoIFile :: HasCallStack => SourceFile -> TCM AbsolutePath

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

valuemkInterfaceFile

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

datadata FindError

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 (List2 AbsolutePath)
Several matching files were found.

Instances1Show

Show FindErrorDefined in Agda-2.8.0.2 · Agda.Interaction.FindFile

valuefindErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError

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

valuefindFile :: TopLevelModuleName -> TCM SourceFile

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.

valuefindFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)

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

SIDE EFFECT: Updates stModuleToSource.

valuefindFile'_

:: List1 AbsolutePath
Include paths.
-> TopLevelModuleName
-> StateT ModuleToSourceId TCM (Either FindError SourceFile)

A variant of findFile' which manipulates an extra ModuleToSourceId

valuefindFile''

:: List1 AbsolutePath
Include paths.
-> TopLevelModuleName
-> StateT ModuleToSource IO (Either FindError SourceFile)

A variant of findFile' which does not require TCM.

valuefindInterfaceFile'

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

valuefindInterfaceFile

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.

valuecheckModuleName

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

valuerootNameModule :: AbsolutePath -> String

valuereplaceModuleExtension :: String -> AbsolutePath -> AbsolutePath

valuedropAgdaExtension :: FilePath -> FilePath

Remove an existing Agda file extension from a file path.

valuehasAgdaExtension :: FilePath -> Bool

Check if a file path has an Agda extension.

valuestripAgdaExtension :: FilePath -> Maybe FilePath

Remove an Agda file extension from a filepath, if possible.