{-# LANGUAGE CPP                        #-}

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

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.Maybe          ( catMaybes, listToMaybe )
import Data.Text           ( Text )
import Data.Text qualified as Text

import System.Directory
import System.FilePath

import Agda.Utils.Monad
import Agda.Utils.Null

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 -> [Char]
(Int -> AbsolutePath -> ShowS)
-> (AbsolutePath -> [Char])
-> ([AbsolutePath] -> ShowS)
-> Show AbsolutePath
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbsolutePath -> ShowS
showsPrec :: Int -> AbsolutePath -> ShowS
$cshow :: AbsolutePath -> [Char]
show :: AbsolutePath -> [Char]
$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, AbsolutePath
AbsolutePath -> Bool
AbsolutePath -> (AbsolutePath -> Bool) -> Null AbsolutePath
forall a. a -> (a -> Bool) -> Null a
$cempty :: AbsolutePath
empty :: AbsolutePath
$cnull :: AbsolutePath -> Bool
null :: AbsolutePath -> Bool
Null)

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

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

mkAbsolute :: FilePath -> AbsolutePath
mkAbsolute :: [Char] -> AbsolutePath
mkAbsolute [Char]
f
  | [Char] -> Bool
isAbsolute [Char]
f =
      Text -> AbsolutePath
AbsolutePath (Text -> AbsolutePath) -> Text -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
Text.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ ShowS
dropTrailingPathSeparator ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
normalise [Char]
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 :: [Char] -> IO AbsolutePath
absolute [Char]
f = [Char] -> AbsolutePath
mkAbsolute ([Char] -> AbsolutePath) -> IO [Char] -> 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.
  ex <- [Char] -> IO Bool
doesFileExist [Char]
f IO Bool -> IO Bool -> IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` [Char] -> IO Bool
doesDirectoryExist [Char]
f
  if 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.
    dir <- canonicalizePath (takeDirectory f)
    return (dir </> takeFileName f)
   else do
    cwd <- getCurrentDirectory
    return (cwd </> f)

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

canonicalizeAbsolutePath :: AbsolutePath -> IO AbsolutePath
canonicalizeAbsolutePath :: AbsolutePath -> IO AbsolutePath
canonicalizeAbsolutePath (AbsolutePath Text
f) =
  Text -> AbsolutePath
AbsolutePath (Text -> AbsolutePath)
-> ([Char] -> Text) -> [Char] -> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Text
Text.pack ([Char] -> AbsolutePath) -> IO [Char] -> IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO [Char]
canonicalizePath (Text -> [Char]
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 = ([Char] -> [Char] -> Bool) -> IO [Char] -> IO [Char] -> 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 [Char] -> [Char] -> Bool
equalFilePath (IO [Char] -> IO [Char] -> IO Bool)
-> (AbsolutePath -> IO [Char])
-> AbsolutePath
-> AbsolutePath
-> IO Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ([Char] -> IO [Char]
canonicalizePath ([Char] -> IO [Char])
-> (AbsolutePath -> [Char]) -> AbsolutePath -> IO [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
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 :: [Char] -> IO Bool
doesFileExistCaseSensitive = [Char] -> 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 :: [Char] -> [Char] -> IO Bool
isNewerThan [Char]
new [Char]
old = do
    newExist <- [Char] -> IO Bool
doesFileExist [Char]
new
    oldExist <- doesFileExist old
    if not (newExist && oldExist)
        then return newExist
        else do
            newT <- getModificationTime new
            oldT <- getModificationTime old
            return $ newT >= 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 seek to relativize.
  -> AbsolutePath
       -- ^ The root for relativization.
  -> Maybe FilePath
       -- ^ The relative path, if any.
relativizeAbsolutePath :: AbsolutePath -> AbsolutePath -> Maybe [Char]
relativizeAbsolutePath AbsolutePath
apath AbsolutePath
aroot
  | [Char]
rest [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
path = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
rest
  | Bool
otherwise    = Maybe [Char]
forall a. Maybe a
Nothing
  where
  path :: [Char]
path = AbsolutePath -> [Char]
filePath AbsolutePath
apath
  root :: [Char]
root = AbsolutePath -> [Char]
filePath AbsolutePath
aroot
  rest :: [Char]
rest = [Char] -> ShowS
makeRelative [Char]
root [Char]
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@.

-- -- Andreas, 2024-11-10, extracted from 'stripPrimitiveLibDir':
-- -- This is a simple implementation of 'relativizeAbsolutePath' using 'splitDirectories'.
-- stripDir :: AbsolutePath -> AbsolutePath -> Maybe FilePath
-- stripDir dir file =
--   joinPath <$> List.stripPrefix (split dir) (split file)
--   where
--     split = splitDirectories . filePath

-- | Makes a path relative to a root without assuming that either path is
-- canonical.

makeRelativeCanonical :: FilePath -> FilePath -> IO FilePath
makeRelativeCanonical :: [Char] -> [Char] -> IO [Char]
makeRelativeCanonical = ([Char] -> ShowS) -> IO [Char] -> IO [Char] -> IO [Char]
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 [Char] -> ShowS
makeRelative (IO [Char] -> IO [Char] -> IO [Char])
-> ([Char] -> IO [Char]) -> [Char] -> [Char] -> IO [Char]
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [Char] -> IO [Char]
canonicalizePath

-- | Generalizes 'stripExtension'.
stripAnyOfExtensions :: [String] -> FilePath -> Maybe FilePath
stripAnyOfExtensions :: [[Char]] -> [Char] -> Maybe [Char]
stripAnyOfExtensions [[Char]]
exts [Char]
p = [[Char]] -> Maybe [Char]
forall a. [a] -> Maybe a
listToMaybe ([[Char]] -> Maybe [Char]) -> [[Char]] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [Maybe [Char]] -> [[Char]]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe [Char]] -> [[Char]]) -> [Maybe [Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ ([Char] -> Maybe [Char]) -> [[Char]] -> [Maybe [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char] -> Maybe [Char]
`stripExtension` [Char]
p) [[Char]]
exts