packages feed

Agda-2.8.0.2: src/full/Agda/Utils/FileName.hs

{-# 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 { textPath :: Text }
  deriving (Show, Eq, Ord, Hashable, NFData)

-- | Extract the 'AbsolutePath' to be used as 'FilePath'.
filePath :: AbsolutePath -> FilePath
filePath = Text.unpack . textPath

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

mkAbsolute :: FilePath -> AbsolutePath
mkAbsolute f
  | isAbsolute f =
      AbsolutePath $ Text.pack $ dropTrailingPathSeparator $ normalise f
        -- normalize does not resolve symlinks
  | otherwise    = __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 f = mkAbsolute <$> do
  -- canonicalizePath sometimes truncates paths pointing to
  -- non-existing files/directories.
  ex <- doesFileExist f `or2M` doesDirectoryExist 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 f) =
  AbsolutePath . Text.pack <$> canonicalizePath (Text.unpack 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 = liftA2 equalFilePath `on` (canonicalizePath . 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 = 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 new old = do
    newExist <- doesFileExist 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 apath aroot
  | rest /= path = Just rest
  | otherwise    = Nothing
  where
  path = filePath apath
  root = filePath aroot
  rest = makeRelative root 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 = liftA2 makeRelative `on` canonicalizePath

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