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.Text (Text)
import qualified Data.Text as Text
import Data.Function
import Data.Hashable
import Data.Typeable (Typeable)
import Agda.Utils.Pretty
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
#include "undefined.h"
import Agda.Utils.Impossible
newtype AbsolutePath = AbsolutePath { byteStringPath :: Text }
deriving (Eq, Ord, Typeable, Hashable)
filePath :: AbsolutePath -> FilePath
filePath = Text.unpack . byteStringPath
instance Show AbsolutePath where
show = filePath
instance Pretty AbsolutePath where
pretty = text . 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 $ Text.pack $ dropTrailingPathSeparator $ normalise f
| otherwise = __IMPOSSIBLE__
prop_mkAbsolute :: FilePath -> Property
prop_mkAbsolute f =
let path = rootPath ++ f
in isValid path ==> 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)
instance CoArbitrary AbsolutePath where
coarbitrary (AbsolutePath t) = coarbitrary (Text.unpack t)
tests :: IO Bool
tests = runTests "Agda.Utils.FileName"
[ quickCheck' absolutePathInvariant
, quickCheck' prop_mkAbsolute
]