{-# LANGUAGE CPP, DeriveDataTypeable #-}

{-| Operations on file names. -}
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

-- | Paths which are known to be absolute.
--
-- Note that the 'Eq' and 'Ord' instances do not check if different
-- paths point to the same files or directories.

newtype AbsolutePath = AbsolutePath { filePath :: FilePath }
  deriving (Show, Eq, Ord, Typeable, Data)

-- | The paths have to be absolute, valid and normalised, without
-- trailing path separators.

absolutePathInvariant :: AbsolutePath -> Bool
absolutePathInvariant (AbsolutePath f) =
  isAbsolute f &&
  isValid f &&
  f == normalise f &&
  f == dropTrailingPathSeparator f

-- | Constructs 'AbsolutePath's.
--
-- Precondition: The path must be absolute.

mkAbsolute :: FilePath -> AbsolutePath
mkAbsolute f
  | isAbsolute f =
      AbsolutePath $ dropTrailingPathSeparator $ normalise f
  | otherwise    = __IMPOSSIBLE__

prop_mkAbsolute f =
  absolutePathInvariant $ mkAbsolute (pathSeparator : f)

-- | Makes the path absolute.
--
-- This function raises an @\_\_IMPOSSIBLE\_\_@ error if
-- 'canonicalizePath' does not return an absolute path.

absolute :: FilePath -> IO AbsolutePath
absolute f = mkAbsolute <$> canonicalizePath f

-- | Tries to establish if the two file paths point to the same file
-- (or directory).

infix 4 ===

(===) :: FilePath -> FilePath -> IO Bool
p1 === p2 = do
  p1 <- canonicalizePath p1
  p2 <- canonicalizePath p2
  return $ equalFilePath p1 p2

------------------------------------------------------------------------
-- Generators

instance Arbitrary AbsolutePath where
  arbitrary = mk . take 3 . map (take 2) <$>
                listOf (listOf1 (elements "a1"))
    where mk ps = AbsolutePath (joinPath $ [pathSeparator] : ps)

------------------------------------------------------------------------
-- All tests

tests = runTests "Agda.Utils.FileName"
  [ quickCheck' absolutePathInvariant
  , quickCheck' prop_mkAbsolute
  ]