{-# LANGUAGE CPP                        #-}

{-| Operations on file names. -}
module Agda.Utils.FileName
  ( AbsolutePath(AbsolutePath)
  , filePath
  , mkAbsolute
  , absolute
  , canonicalizeAbsolutePath
  , sameFile
  , doesFileExistCaseSensitive
  , isNewerThan
  , relativizeAbsolutePath
  ) 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.Function (on)
import Data.Hashable       ( Hashable )
import Data.Text           ( Text )
import qualified Data.Text as Text

import Agda.Utils.Monad
import Agda.Syntax.Common.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 -> FilePath
(Int -> AbsolutePath -> ShowS)
-> (AbsolutePath -> FilePath)
-> ([AbsolutePath] -> ShowS)
-> Show AbsolutePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbsolutePath -> ShowS
showsPrec :: Int -> AbsolutePath -> ShowS
$cshow :: AbsolutePath -> FilePath
show :: AbsolutePath -> FilePath
$cshowList :: [AbsolutePath] -> ShowS
showList :: [AbsolutePath] -> ShowS
Show, AbsolutePath -> AbsolutePath -> Bool
(AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool) -> Eq AbsolutePath
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbsolutePath -> AbsolutePath -> Bool
== :: AbsolutePath -> AbsolutePath -> Bool
$c/= :: AbsolutePath -> AbsolutePath -> Bool
/= :: 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
$ccompare :: AbsolutePath -> AbsolutePath -> Ordering
compare :: AbsolutePath -> AbsolutePath -> Ordering
$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
>= :: AbsolutePath -> AbsolutePath -> Bool
$cmax :: AbsolutePath -> AbsolutePath -> AbsolutePath
max :: AbsolutePath -> AbsolutePath -> AbsolutePath
$cmin :: AbsolutePath -> AbsolutePath -> AbsolutePath
min :: AbsolutePath -> AbsolutePath -> AbsolutePath
Ord, 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
$chashWithSalt :: Int -> AbsolutePath -> Int
hashWithSalt :: Int -> AbsolutePath -> Int
$chash :: AbsolutePath -> Int
hash :: AbsolutePath -> Int
Hashable, AbsolutePath -> ()
(AbsolutePath -> ()) -> NFData AbsolutePath
forall a. (a -> ()) -> NFData a
$crnf :: AbsolutePath -> ()
rnf :: AbsolutePath -> ()
NFData)

-- | 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
textPath

instance Pretty AbsolutePath where
  pretty :: AbsolutePath -> Doc
pretty = FilePath -> Doc
forall a. FilePath -> Doc a
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
        -- 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 :: 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
`or2M` FilePath -> IO Bool
doesDirectoryExist FilePath
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.
    FilePath
dir <- FilePath -> IO FilePath
canonicalizePath (ShowS
takeDirectory FilePath
f)
    FilePath -> IO FilePath
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
dir FilePath -> ShowS
</> ShowS
takeFileName FilePath
f)
   else do
    FilePath
cwd <- IO FilePath
getCurrentDirectory
    FilePath -> IO FilePath
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
cwd FilePath -> ShowS
</> FilePath
f)

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

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

-- | Tries to establish if the two file paths point to the same file
-- (or directory). False negatives may be returned.

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

-- | 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 :: FilePath -> FilePath -> IO Bool
isNewerThan FilePath
new FilePath
old = do
    Bool
newExist <- FilePath -> IO Bool
doesFileExist FilePath
new
    Bool
oldExist <- FilePath -> IO Bool
doesFileExist FilePath
old
    if Bool -> Bool
not (Bool
newExist Bool -> Bool -> Bool
&& Bool
oldExist)
        then Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
newExist
        else do
            UTCTime
newT <- FilePath -> IO UTCTime
getModificationTime FilePath
new
            UTCTime
oldT <- FilePath -> IO UTCTime
getModificationTime FilePath
old
            Bool -> IO Bool
forall a. a -> IO a
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

-- | A partial version of 'System.FilePath.makeRelative' with flipped arguments,
--   returning 'Nothing' if the given path cannot be relativized to the given @root@.
relativizeAbsolutePath ::
     AbsolutePath
       -- ^ The absolute path we see to relativize.
  -> AbsolutePath
       -- ^ The root for relativization.
  -> Maybe FilePath
       -- ^ The relative path, if any.
relativizeAbsolutePath :: AbsolutePath -> AbsolutePath -> Maybe FilePath
relativizeAbsolutePath AbsolutePath
apath AbsolutePath
aroot
  | FilePath
rest FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
/= FilePath
path = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
rest
  | Bool
otherwise    = Maybe FilePath
forall a. Maybe a
Nothing
  where
  path :: FilePath
path = AbsolutePath -> FilePath
filePath AbsolutePath
apath
  root :: FilePath
root = AbsolutePath -> FilePath
filePath AbsolutePath
aroot
  rest :: FilePath
rest = FilePath -> ShowS
makeRelative FilePath
root FilePath
path
    -- Andreas, 2022-10-10
    -- See https://gitlab.haskell.org/haskell/filepath/-/issues/130.
    -- 'System.FilePath.makeRelative' is strangely enough a total function,
    -- and it returns the original @path@ if it could not be relativized to
    -- the @root@, or if the @root@ was ".".
    -- In our case, the @root@ is absolute, so we should expect @rest@ to
    -- always be different from @path@ if @path@ is relative to @root@.
    -- In the extreme case, @root = "/"@ and @path == "/" ++ rest@.