{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

{-| Operations on file names. -}
module Agda.Utils.FileName
  ( AbsolutePath(AbsolutePath)
  , filePath
  , mkAbsolute
  , absolute
  , (===)
  , doesFileExistCaseSensitive
  , rootPath
  ) where

import System.Directory
import System.FilePath

#ifdef mingw32_HOST_OS
import Control.Exception (bracket)
import System.Win32 (findFirstFile, findClose, getFindDataFileName)
import Agda.Utils.Monad
#endif

import Data.Text (Text)
import qualified Data.Text as Text
import Data.Function
import Data.Hashable (Hashable)
import Data.Data (Data)

import Agda.Utils.Pretty

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 { AbsolutePath -> Text
byteStringPath :: Text }
  deriving (AbsolutePath -> AbsolutePath -> Bool
(AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool) -> Eq AbsolutePath
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AbsolutePath -> AbsolutePath -> Bool
$c/= :: AbsolutePath -> AbsolutePath -> Bool
== :: AbsolutePath -> AbsolutePath -> Bool
$c== :: AbsolutePath -> AbsolutePath -> Bool
Eq, Eq AbsolutePath
Eq AbsolutePath
-> (AbsolutePath -> AbsolutePath -> Ordering)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> AbsolutePath)
-> (AbsolutePath -> AbsolutePath -> AbsolutePath)
-> Ord AbsolutePath
AbsolutePath -> AbsolutePath -> Bool
AbsolutePath -> AbsolutePath -> Ordering
AbsolutePath -> AbsolutePath -> AbsolutePath
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: AbsolutePath -> AbsolutePath -> AbsolutePath
$cmin :: AbsolutePath -> AbsolutePath -> AbsolutePath
max :: AbsolutePath -> AbsolutePath -> AbsolutePath
$cmax :: AbsolutePath -> AbsolutePath -> AbsolutePath
>= :: AbsolutePath -> AbsolutePath -> Bool
$c>= :: AbsolutePath -> AbsolutePath -> Bool
> :: AbsolutePath -> AbsolutePath -> Bool
$c> :: AbsolutePath -> AbsolutePath -> Bool
<= :: AbsolutePath -> AbsolutePath -> Bool
$c<= :: AbsolutePath -> AbsolutePath -> Bool
< :: AbsolutePath -> AbsolutePath -> Bool
$c< :: AbsolutePath -> AbsolutePath -> Bool
compare :: AbsolutePath -> AbsolutePath -> Ordering
$ccompare :: AbsolutePath -> AbsolutePath -> Ordering
$cp1Ord :: Eq AbsolutePath
Ord, Typeable AbsolutePath
DataType
Constr
Typeable AbsolutePath
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> AbsolutePath -> c AbsolutePath)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AbsolutePath)
-> (AbsolutePath -> Constr)
-> (AbsolutePath -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AbsolutePath))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c AbsolutePath))
-> ((forall b. Data b => b -> b) -> AbsolutePath -> AbsolutePath)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r)
-> (forall u. (forall d. Data d => d -> u) -> AbsolutePath -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> AbsolutePath -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath)
-> Data AbsolutePath
AbsolutePath -> DataType
AbsolutePath -> Constr
(forall b. Data b => b -> b) -> AbsolutePath -> AbsolutePath
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AbsolutePath -> c AbsolutePath
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AbsolutePath
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> AbsolutePath -> u
forall u. (forall d. Data d => d -> u) -> AbsolutePath -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AbsolutePath
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AbsolutePath -> c AbsolutePath
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AbsolutePath)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AbsolutePath)
$cAbsolutePath :: Constr
$tAbsolutePath :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath
gmapMp :: (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath
gmapM :: (forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AbsolutePath -> m AbsolutePath
gmapQi :: Int -> (forall d. Data d => d -> u) -> AbsolutePath -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AbsolutePath -> u
gmapQ :: (forall d. Data d => d -> u) -> AbsolutePath -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> AbsolutePath -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AbsolutePath -> r
gmapT :: (forall b. Data b => b -> b) -> AbsolutePath -> AbsolutePath
$cgmapT :: (forall b. Data b => b -> b) -> AbsolutePath -> AbsolutePath
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AbsolutePath)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AbsolutePath)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c AbsolutePath)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AbsolutePath)
dataTypeOf :: AbsolutePath -> DataType
$cdataTypeOf :: AbsolutePath -> DataType
toConstr :: AbsolutePath -> Constr
$ctoConstr :: AbsolutePath -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AbsolutePath
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AbsolutePath
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AbsolutePath -> c AbsolutePath
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AbsolutePath -> c AbsolutePath
$cp1Data :: Typeable AbsolutePath
Data, Int -> AbsolutePath -> Int
AbsolutePath -> Int
(Int -> AbsolutePath -> Int)
-> (AbsolutePath -> Int) -> Hashable AbsolutePath
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: AbsolutePath -> Int
$chash :: AbsolutePath -> Int
hashWithSalt :: Int -> AbsolutePath -> Int
$chashWithSalt :: Int -> AbsolutePath -> Int
Hashable)

-- | Extract the 'AbsolutePath' to be used as 'FilePath'.
filePath :: AbsolutePath -> FilePath
filePath :: AbsolutePath -> FilePath
filePath = Text -> FilePath
Text.unpack (Text -> FilePath)
-> (AbsolutePath -> Text) -> AbsolutePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> Text
byteStringPath

-- TODO: 'Show' should output Haskell-parseable representations.
-- The following instance is deprecated, and Pretty should be used
-- instead.  Later, simply derive Show for this type.

instance Show AbsolutePath where
  show :: AbsolutePath -> FilePath
show = AbsolutePath -> FilePath
filePath

instance Pretty AbsolutePath where
  pretty :: AbsolutePath -> Doc
pretty = FilePath -> Doc
text (FilePath -> Doc)
-> (AbsolutePath -> FilePath) -> AbsolutePath -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> FilePath
filePath

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

mkAbsolute :: FilePath -> AbsolutePath
mkAbsolute :: FilePath -> AbsolutePath
mkAbsolute FilePath
f
  | FilePath -> Bool
isAbsolute FilePath
f =
      Text -> AbsolutePath
AbsolutePath (Text -> AbsolutePath) -> Text -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ FilePath -> Text
Text.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ ShowS
dropTrailingPathSeparator ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
normalise FilePath
f
  | Bool
otherwise    = AbsolutePath
forall a. HasCallStack => a
__IMPOSSIBLE__

rootPath :: FilePath
#ifdef mingw32_HOST_OS
rootPath = joinDrive "C:" [pathSeparator]
#else
rootPath :: FilePath
rootPath = [Char
pathSeparator]
#endif

-- UNUSED Linag-Ting Chen 2019-07-16
---- | maps @/bla/bla/bla/foo.bar.xxx@ to @foo.bar@.
--rootName :: AbsolutePath -> String
--rootName = dropExtension . snd . splitFileName . filePath

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

absolute :: FilePath -> IO AbsolutePath
absolute :: FilePath -> IO AbsolutePath
absolute FilePath
f = FilePath -> AbsolutePath
mkAbsolute (FilePath -> AbsolutePath) -> IO FilePath -> IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  -- canonicalizePath sometimes truncates paths pointing to
  -- non-existing files/directories.
  Bool
ex <- FilePath -> IO Bool
doesFileExist FilePath
f IO Bool -> IO Bool -> IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
.||. FilePath -> IO Bool
doesDirectoryExist FilePath
f
  if Bool
ex then
    FilePath -> IO FilePath
canonicalizePath FilePath
f
   else do
    FilePath
cwd <- IO FilePath
getCurrentDirectory
    FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
cwd FilePath -> ShowS
</> FilePath
f)
  where
  m Bool
m1 .||. :: m Bool -> m Bool -> m Bool
.||. m Bool
m2 = do
    Bool
b1 <- m Bool
m1
    if Bool
b1 then Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else m Bool
m2

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

infix 4 ===

(===) :: AbsolutePath -> AbsolutePath -> Bool
=== :: AbsolutePath -> AbsolutePath -> Bool
(===) = FilePath -> FilePath -> Bool
equalFilePath (FilePath -> FilePath -> Bool)
-> (AbsolutePath -> FilePath)
-> AbsolutePath
-> AbsolutePath
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` AbsolutePath -> FilePath
filePath

-- | Case-sensitive 'doesFileExist' for Windows.
--
-- This is case-sensitive only on the file name part, not on the directory part.
-- (Ideally, path components coming from module name components should be
--  checked case-sensitively and the other path components should be checked
--  case insensitively.)

doesFileExistCaseSensitive :: FilePath -> IO Bool
#ifdef mingw32_HOST_OS
doesFileExistCaseSensitive f = do
  doesFileExist f `and2M` do
    bracket (findFirstFile f) (findClose . fst) $
      fmap (takeFileName f ==) . getFindDataFileName . snd
#else
doesFileExistCaseSensitive :: FilePath -> IO Bool
doesFileExistCaseSensitive = FilePath -> IO Bool
doesFileExist
#endif