    {-# 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 qualified Data.Text as Text

    import System.Directory
    import System.FilePath

    import Agda.Utils.Monad

    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

    -- | 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.
      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 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)
    -> (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
        newExist <- FilePath -> IO Bool
    doesFileExist FilePath
    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 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@.

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

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