{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Utils.FileName
( AbsolutePath(AbsolutePath)
, filePath
, mkAbsolute
, absolute
, (===)
, doesFileExistCaseSensitive
, rootPath
) where
import System.Directory
import System.FilePath
#ifdef mingw32_HOST_OS
import Control.Exception (bracket)
import System.Win32 (findFirstFile, findClose, getFindDataFileName)
#endif
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Function
import Data.Hashable (Hashable)
import Data.Data (Data)
import Agda.Utils.Monad
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
newtype AbsolutePath = AbsolutePath { byteStringPath :: Text }
deriving (Eq, Ord, Data, Hashable)
filePath :: AbsolutePath -> FilePath
filePath = Text.unpack . byteStringPath
instance Show AbsolutePath where
show = filePath
instance Pretty AbsolutePath where
pretty = text . filePath
mkAbsolute :: FilePath -> AbsolutePath
mkAbsolute f
| isAbsolute f =
AbsolutePath $ Text.pack $ dropTrailingPathSeparator $ normalise f
| otherwise = __IMPOSSIBLE__
rootPath :: FilePath
#ifdef mingw32_HOST_OS
rootPath = joinDrive "C:" [pathSeparator]
#else
rootPath = [pathSeparator]
#endif
rootName :: AbsolutePath -> String
rootName = dropExtension . snd . splitFileName . filePath
absolute :: FilePath -> IO AbsolutePath
absolute f = mkAbsolute <$> do
ex <- doesFileExist f .||. doesDirectoryExist f
if ex then
canonicalizePath f
else do
cwd <- getCurrentDirectory
return (cwd </> f)
where
m1 .||. m2 = do
b1 <- m1
if b1 then return True else m2
infix 4 ===
(===) :: AbsolutePath -> AbsolutePath -> Bool
(===) = equalFilePath `on` filePath
doesFileExistCaseSensitive :: FilePath -> IO Bool
#ifdef mingw32_HOST_OS
doesFileExistCaseSensitive f = do
doesFileExist f `and2M` do
bracket (findFirstFile f) (findClose . fst) $
fmap (takeFileName f ==) . getFindDataFileName . snd
#else
doesFileExistCaseSensitive f = doesFileExist f
#endif