    {-# 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, 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, 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