module Agda.Utils.FileName
( AbsolutePath
, filePath
, rootName
, mkAbsolute
, absolute
, (===)
, doesFileExistCaseSensitive
, tests
) where
import Control.Applicative
import System.Directory
import System.FilePath
#if mingw32_HOST_OS
import Control.Exception (bracket)
import System.Win32 (findFirstFile, findClose, getFindDataFileName)
#endif
import Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString
import Data.Function
import Data.Typeable (Typeable)
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
#include "undefined.h"
import Agda.Utils.Impossible
newtype AbsolutePath = AbsolutePath { byteStringPath :: ByteString }
deriving (Eq, Ord, Typeable)
filePath :: AbsolutePath -> FilePath
filePath = ByteString.unpack . byteStringPath
instance Show AbsolutePath where
show = filePath
absolutePathInvariant :: AbsolutePath -> Bool
absolutePathInvariant x =
isAbsolute f &&
isValid f &&
f == normalise f &&
f == dropTrailingPathSeparator f
where f = filePath x
mkAbsolute :: FilePath -> AbsolutePath
mkAbsolute f
| isAbsolute f =
AbsolutePath $ ByteString.pack $ dropTrailingPathSeparator $ normalise f
| otherwise = __IMPOSSIBLE__
#if mingw32_HOST_OS
prop_mkAbsolute :: FilePath -> Property
#else
prop_mkAbsolute :: FilePath -> Bool
#endif
prop_mkAbsolute f =
let path = rootPath ++ f
in
#if mingw32_HOST_OS
isValid path ==>
#endif
absolutePathInvariant $ mkAbsolute $ path
rootPath :: FilePath
#if 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
#if mingw32_HOST_OS
doesFileExistCaseSensitive f = do
ex <- doesFileExist f
if ex then bracket (findFirstFile f) (findClose . fst) $
fmap (takeFileName f ==) . getFindDataFileName . snd
else return False
#else
doesFileExistCaseSensitive f = doesFileExist f
#endif
instance Arbitrary AbsolutePath where
arbitrary = mk . take 3 . map (take 2) <$>
listOf (listOf1 (elements "a1"))
where mk ps = mkAbsolute (joinPath $ rootPath : ps)
tests :: IO Bool
tests = runTests "Agda.Utils.FileName"
[ quickCheck' absolutePathInvariant
, quickCheck' prop_mkAbsolute
]