HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

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
  • 13 values
  • PackageAgda-2.7.0.1
  • Exports16
  • LanguageHaskell2010
  • LicenceMIT
  • SourceFindFile.hs
newtypenewtype SourceFile
#

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

Instances4Eq, Ord, Show, Pretty
valuetoIFile :: 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
  1. :: AbsolutePath

    Path to the candidate interface file

  2. -> 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 [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.

Instances1Show
  • Show FindErrorDefined in Agda-2.7.0.1 · Agda.Interaction.FindFile
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.

valuecheckModuleName
  1. :: TopLevelModuleName

    The name of the module.

  2. -> SourceFile

    The file from which it was loaded.

  3. -> Maybe TopLevelModuleName

    The expected name, coming from an import statement.

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

valuemoduleName
  1. :: AbsolutePath

    The path to the file.

  2. -> Module

    The parsed module.

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