{-# LANGUAGE CPP                        #-}

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

import System.Directory
import System.FilePath

import Control.Applicative ( liftA2 )
import Control.DeepSeq
#ifdef mingw32_HOST_OS
import Control.Exception   ( bracket )
import System.Win32        ( findFirstFile, findClose, getFindDataFileName )
#endif

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

import Agda.Utils.Monad
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
textPath :: Text }
  deriving (Int -> AbsolutePath -> ShowS
[AbsolutePath] -> ShowS
AbsolutePath -> String
(Int -> AbsolutePath -> ShowS)
-> (AbsolutePath -> String)
-> ([AbsolutePath] -> ShowS)
-> Show AbsolutePath
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AbsolutePath] -> ShowS
$cshowList :: [AbsolutePath] -> ShowS
show :: AbsolutePath -> String
$cshow :: AbsolutePath -> String
showsPrec :: Int -> AbsolutePath -> ShowS
$cshowsPrec :: Int -> AbsolutePath -> ShowS
Show, 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
Ord, Typeable AbsolutePath
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 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> AbsolutePath -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AbsolutePath -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> AbsolutePath -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> AbsolutePath -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Eq AbsolutePath
Eq AbsolutePath
-> (Int -> AbsolutePath -> Int)
-> (AbsolutePath -> Int)
-> Hashable AbsolutePath
Int -> AbsolutePath -> Int
AbsolutePath -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: AbsolutePath -> Int
$chash :: AbsolutePath -> Int
hashWithSalt :: Int -> AbsolutePath -> Int
$chashWithSalt :: Int -> AbsolutePath -> Int
Hashable, AbsolutePath -> ()
(AbsolutePath -> ()) -> NFData AbsolutePath
forall a. (a -> ()) -> NFData a
rnf :: AbsolutePath -> ()
$crnf :: AbsolutePath -> ()
NFData)

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

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

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

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

-- UNUSED Liang-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 :: String -> IO AbsolutePath
absolute String
f = String -> AbsolutePath
mkAbsolute (String -> AbsolutePath) -> IO String -> 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 <- String -> IO Bool
doesFileExist String
f IO Bool -> IO Bool -> IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` String -> IO Bool
doesDirectoryExist String
f
  if Bool
ex then do
    -- Andreas, 2020-08-11, issue #4828
    -- Do not use @canonicalizePath@ on the full path as it resolves symlinks,
    -- which leads to wrong placement of the .agdai file.
    String
dir <- String -> IO String
canonicalizePath (ShowS
takeDirectory String
f)
    String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String
dir String -> ShowS
</> ShowS
takeFileName String
f)
   else do
    String
cwd <- IO String
getCurrentDirectory
    String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String
cwd String -> ShowS
</> String
f)

-- | Resolve symlinks etc.  Preserves 'sameFile'.

canonicalizeAbsolutePath :: AbsolutePath -> IO AbsolutePath
canonicalizeAbsolutePath :: AbsolutePath -> IO AbsolutePath
canonicalizeAbsolutePath (AbsolutePath Text
f) =
  Text -> AbsolutePath
AbsolutePath (Text -> AbsolutePath)
-> (String -> Text) -> String -> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
Text.pack (String -> AbsolutePath) -> IO String -> IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
canonicalizePath (Text -> String
Text.unpack Text
f)

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

sameFile :: AbsolutePath -> AbsolutePath -> IO Bool
sameFile :: AbsolutePath -> AbsolutePath -> IO Bool
sameFile = (String -> String -> Bool) -> IO String -> IO String -> IO Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 String -> String -> Bool
equalFilePath (IO String -> IO String -> IO Bool)
-> (AbsolutePath -> IO String)
-> AbsolutePath
-> AbsolutePath
-> IO Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (String -> IO String
canonicalizePath (String -> IO String)
-> (AbsolutePath -> String) -> AbsolutePath -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
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 :: String -> IO Bool
doesFileExistCaseSensitive = String -> IO Bool
doesFileExist
#endif

-- | True if the first file is newer than the second file. If a file doesn't
-- exist it is considered to be infinitely old.
isNewerThan :: FilePath -> FilePath -> IO Bool
isNewerThan :: String -> String -> IO Bool
isNewerThan String
new String
old = do
    Bool
newExist <- String -> IO Bool
doesFileExist String
new
    Bool
oldExist <- String -> IO Bool
doesFileExist String
old
    if Bool -> Bool
not (Bool
newExist Bool -> Bool -> Bool
&& Bool
oldExist)
        then Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
newExist
        else do
            UTCTime
newT <- String -> IO UTCTime
getModificationTime String
new
            UTCTime
oldT <- String -> IO UTCTime
getModificationTime String
old
            Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ UTCTime
newT UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
>= UTCTime
oldT