Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Operations on file names.



data AbsolutePath Source #

Paths which are known to be absolute.

Note that the Eq and Ord instances do not check if different paths point to the same files or directories.


Eq AbsolutePath Source # 
Ord AbsolutePath Source # 
Show AbsolutePath Source # 
Arbitrary AbsolutePath Source # 
CoArbitrary AbsolutePath Source # 


coarbitrary :: AbsolutePath -> Gen b -> Gen b #

Hashable AbsolutePath Source # 
Pretty AbsolutePath Source # 
KillRange Range Source # 
SetRange Range Source # 


setRange :: Range -> Range -> Range Source #

HasRange Range Source # 


getRange :: Range -> Range Source #

HasRange Interval Source # 
FreshName Range Source # 
GenC Range Source # 
PrettyTCM Range Source # 


prettyTCM :: Range -> TCM Doc Source #

FreshName (Range, String) Source # 

filePath :: AbsolutePath -> FilePath Source #

Extract the AbsolutePath to be used as FilePath.

rootName :: AbsolutePath -> String Source #

maps to

mkAbsolute :: FilePath -> AbsolutePath Source #

Constructs AbsolutePaths.

Precondition: The path must be absolute and valid.

absolute :: FilePath -> IO AbsolutePath Source #

Makes the path absolute.

This function may raise an __IMPOSSIBLE__ error if canonicalizePath does not return an absolute path.

(===) :: AbsolutePath -> AbsolutePath -> Bool infix 4 Source #

Tries to establish if the two file paths point to the same file (or directory).

doesFileExistCaseSensitive :: FilePath -> IO Bool Source #

Case-sensitive doesFileExist for Windows. This is case-sensitive only on the file name part, not on the directory part. (Ideally, path components coming from module name components should be checked case-sensitively and the other path components should be checked case insenstively.)