Agda.Interaction.FindFile

SourceFiles must exist and be registered in our file dictionary.

File must exist.

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

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

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

Invariant: All paths are absolute.

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

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.

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

SIDE EFFECT: Updates stModuleToSource.

A variant of findFile' which manipulates an extra ModuleToSourceId

A variant of findFile' which does not require TCM.

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.

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.

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.

Remove an existing Agda file extension from a file path.

Check if a file path has an Agda extension.

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