module Agda.Utils.FileName
( AbsolutePath
, filePath
, mkAbsolute
, absolute
, (===)
, tests
) where
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
import Data.Function
import Data.Generics
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 =
absolutePathInvariant $ mkAbsolute (pathSeparator : f)
absolute :: FilePath -> IO AbsolutePath
absolute f = mkAbsolute <$> canonicalizePath f
infix 4 ===
(===) :: FilePath -> FilePath -> IO Bool
p1 === p2 = do
p1 <- canonicalizePath p1
p2 <- canonicalizePath p2
return $ equalFilePath p1 p2
instance Arbitrary AbsolutePath where
arbitrary = mk . take 3 . map (take 2) <$>
listOf (listOf1 (elements "a1"))
where mk ps = AbsolutePath (joinPath $ [pathSeparator] : ps)
tests = runTests "Agda.Utils.FileName"
[ quickCheck' absolutePathInvariant
, quickCheck' prop_mkAbsolute
]