Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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 {
  - srcFileId :: FileId
  }
- data InterfaceFile
- toIFile :: HasCallStack => SourceFile -> TCM AbsolutePath
- mkInterfaceFile :: AbsolutePath -> IO (Maybe InterfaceFile)
- data FindError
  - = NotFound [AbsolutePath]
  - | Ambiguous (List2 AbsolutePath)
- findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
- findFile :: TopLevelModuleName -> TCM SourceFile
- findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
- findFile'_ :: List1 AbsolutePath -> TopLevelModuleName -> StateT ModuleToSourceId TCM (Either FindError SourceFile)
- findFile'' :: List1 AbsolutePath -> TopLevelModuleName -> StateT ModuleToSource IO (Either FindError SourceFile)
- findInterfaceFile' :: HasCallStack => SourceFile -> TCM (Maybe InterfaceFile)
- findInterfaceFile :: HasCallStack => TopLevelModuleName -> TCM (Maybe InterfaceFile)
- checkModuleName :: TopLevelModuleName -> SourceFile -> Maybe TopLevelModuleName -> TCM ()
- rootNameModule :: AbsolutePath -> String
- replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
- dropAgdaExtension :: FilePath -> FilePath
- hasAgdaExtension :: FilePath -> Bool
- stripAgdaExtension :: FilePath -> Maybe FilePath

# Documentation

newtype SourceFile Source #

`SourceFile`s must exist and be registered in our file dictionary.

Constructors

SourceFile |

Fields

- srcFileId :: FileId

#### Instances

Instances details

NFData SourceFile Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods rnf :: SourceFile -> () Source #
Generic SourceFile Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep SourceFile |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types type Rep SourceFile = D1 ('MetaData "SourceFile" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))

Methods

from :: SourceFile -> Rep SourceFile x Source #

to :: Rep SourceFile x -> SourceFile Source #

Show SourceFile Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> SourceFile -> ShowS Source # show :: SourceFile -> String Source # showList :: [SourceFile] -> ShowS Source #
Eq SourceFile Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: SourceFile -> SourceFile -> Bool Source # (/=) :: SourceFile -> SourceFile -> Bool Source #
Ord SourceFile Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

compare :: SourceFile -> SourceFile -> Ordering Source #

(<) :: SourceFile -> SourceFile -> Bool Source #

(<=) :: SourceFile -> SourceFile -> Bool Source #

(>) :: SourceFile -> SourceFile -> Bool Source #

(>=) :: SourceFile -> SourceFile -> Bool Source #

max :: SourceFile -> SourceFile -> SourceFile Source #

min :: SourceFile -> SourceFile -> SourceFile Source #

type Rep SourceFile Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types type Rep SourceFile = D1 ('MetaData "SourceFile" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))

data InterfaceFile Source #

File must exist.

#### 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 :: HasCallStack => 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 [AbsolutePath] | The file was not found. It should have had one of the given file names.
Ambiguous (List2 AbsolutePath) | Several matching files were found.

#### Instances

Instances details

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

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

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

A variant of `findFile'` which manipulates an extra `ModuleToSourceId`

findFile'' Source #

Arguments

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

A variant of `findFile'` which does not require `TCM`.

findInterfaceFile' Source #

Arguments

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

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

rootNameModule :: AbsolutePath -> String Source #

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

dropAgdaExtension :: FilePath -> FilePath Source #

Remove an existing Agda file extension from a file path.

hasAgdaExtension :: FilePath -> Bool Source #

Check if a file path has an Agda extension.

stripAgdaExtension :: FilePath -> Maybe FilePath Source #

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