module Agda.Utils.FileName
( AbsolutePath
, filePath
, mkAbsolute
, absolute
, (===)
, tests
) where
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
import Data.Function
import Data.Generics (Typeable, Data)
import Data.List
import Data.Maybe
import Control.Applicative
import Control.Monad
import System.Directory
import System.FilePath
#include "../undefined.h"
import Agda.Utils.Impossible
newtype AbsolutePath = AbsolutePath { filePath :: FilePath }
deriving (Show, Eq, Ord, Typeable, Data)
absolutePathInvariant :: AbsolutePath -> Bool
absolutePathInvariant (AbsolutePath f) =
isAbsolute f &&
isValid f &&
f == normalise f &&
f == dropTrailingPathSeparator f
mkAbsolute :: FilePath -> AbsolutePath
mkAbsolute f
| isAbsolute f =
AbsolutePath $ dropTrailingPathSeparator $ normalise f
| otherwise = __IMPOSSIBLE__
prop_mkAbsolute f =
let path = rootPath ++ f
in
#if mingw32_HOST_OS
isValid path ==>
#endif
absolutePathInvariant $ mkAbsolute $ path
#if mingw32_HOST_OS
rootPath = joinDrive "C:" [pathSeparator]
#else
rootPath = [pathSeparator]
#endif
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
instance Arbitrary AbsolutePath where
arbitrary = mk . take 3 . map (take 2) <$>
listOf (listOf1 (elements "a1"))
where mk ps = mkAbsolute (joinPath $ rootPath : ps)
tests = runTests "Agda.Utils.FileName"
[ quickCheck' absolutePathInvariant
, quickCheck' prop_mkAbsolute
]