    module Agda.Utils.IO.Directory
      ( copyDirContent
      )
    where

    import Control.Monad
    import Control.Monad.Writer ( WriterT, execWriterT, tell )
    import Control.Monad.Trans  ( lift )

    import Data.Monoid          ( Endo(Endo, appEndo) )

    import System.Directory
    import System.FilePath
    import Data.ByteString as BS

    -- | @copyDirContent src dest@ recursively copies directory @src@ onto @dest@.
    --
    --   First, a to-do list of copy actions is created.
    --   Then, the to-do list is carried out.
    --
    --   This avoids copying files we have just created again, which can happen
    --   if @src@ and @dest@ are not disjoint.
    --   (See issue #2705.)
    --
    copyDirContent :: FilePath -> FilePath -> IO ()
    copyDirContent :: FilePath -> FilePath -> IO ()
    copyDirContent FilePath
    src FilePath
    dest = (CopyDirAction -> IO ()) -> [CopyDirAction] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ CopyDirAction -> IO ()
    performAction ([CopyDirAction] -> IO ()) -> IO [CopyDirAction] -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
      (Endo [CopyDirAction] -> [CopyDirAction] -> [CopyDirAction]
    forall a. Endo a -> a -> a
    `appEndo` []) (Endo [CopyDirAction] -> [CopyDirAction])
    -> IO (Endo [CopyDirAction]) -> IO [CopyDirAction]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> WriterT (Endo [CopyDirAction]) IO () -> IO (Endo [CopyDirAction])
    forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
    execWriterT (FilePath -> FilePath -> WriterT (Endo [CopyDirAction]) IO ()
    copyDirContentDryRun FilePath
    src FilePath
    dest)

    -- | Action to be carried out for copying a directory recursively.
    --
    data CopyDirAction
      = MkDir    FilePath
          -- ^ Create directory if missing.
      | CopyFile FilePath FilePath
          -- ^ Copy file if changed.

    -- | Perform scheduled 'CopyDirAction'.
    --
    performAction :: CopyDirAction -> IO ()
    performAction :: CopyDirAction -> IO ()
    performAction = \case
      MkDir FilePath
    d           -> Bool -> FilePath -> IO ()
    createDirectoryIfMissing Bool
    True FilePath
    d
      CopyFile FilePath
    src FilePath
    dest -> FilePath -> FilePath -> IO ()
    copyIfChanged FilePath
    src FilePath
    dest

    -- | @copyDirContentDryRun src dest@ creates a to-do list
    --   for recursively copying directory @src@ onto @dest@.
    --
    copyDirContentDryRun :: FilePath -> FilePath -> WriterT (Endo [CopyDirAction]) IO ()
    copyDirContentDryRun :: FilePath -> FilePath -> WriterT (Endo [CopyDirAction]) IO ()
    copyDirContentDryRun FilePath
    src FilePath
    dest = do
      Endo [CopyDirAction] -> WriterT (Endo [CopyDirAction]) IO ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (Endo [CopyDirAction] -> WriterT (Endo [CopyDirAction]) IO ())
    -> Endo [CopyDirAction] -> WriterT (Endo [CopyDirAction]) IO ()
    forall a b. (a -> b) -> a -> b
    $ ([CopyDirAction] -> [CopyDirAction]) -> Endo [CopyDirAction]
    forall a. (a -> a) -> Endo a
    Endo (FilePath -> CopyDirAction
    MkDir FilePath
    dest CopyDirAction -> [CopyDirAction] -> [CopyDirAction]
    forall a. a -> [a] -> [a]
    :)
      [FilePath]
    chlds <- IO [FilePath] -> WriterT (Endo [CopyDirAction]) IO [FilePath]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO [FilePath] -> WriterT (Endo [CopyDirAction]) IO [FilePath])
    -> IO [FilePath] -> WriterT (Endo [CopyDirAction]) IO [FilePath]
    forall a b. (a -> b) -> a -> b
    $ FilePath -> IO [FilePath]
    getDirectoryContents FilePath
    src
      [FilePath]
    -> (FilePath -> WriterT (Endo [CopyDirAction]) IO ())
    -> WriterT (Endo [CopyDirAction]) IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [FilePath]
    chlds ((FilePath -> WriterT (Endo [CopyDirAction]) IO ())
     -> WriterT (Endo [CopyDirAction]) IO ())
    -> (FilePath -> WriterT (Endo [CopyDirAction]) IO ())
    -> WriterT (Endo [CopyDirAction]) IO ()
    forall a b. (a -> b) -> a -> b
    $ \ FilePath
    x -> do
        Bool
    isDir <- IO Bool -> WriterT (Endo [CopyDirAction]) IO Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO Bool -> WriterT (Endo [CopyDirAction]) IO Bool)
    -> IO Bool -> WriterT (Endo [CopyDirAction]) IO Bool
    forall a b. (a -> b) -> a -> b
    $ FilePath -> IO Bool
    doesDirectoryExist (FilePath
    src FilePath -> FilePath -> FilePath
    </> FilePath
    x)
        case Bool
    isDir of
          Bool
    _ | FilePath
    x FilePath -> FilePath -> Bool
    forall a. Eq a => a -> a -> Bool
    == FilePath
    "." Bool -> Bool -> Bool
    || FilePath
    x FilePath -> FilePath -> Bool
    forall a. Eq a => a -> a -> Bool
    == FilePath
    ".." -> () -> WriterT (Endo [CopyDirAction]) IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Bool
    True  -> FilePath -> FilePath -> WriterT (Endo [CopyDirAction]) IO ()
    copyDirContentDryRun (FilePath
    src FilePath -> FilePath -> FilePath
    </> FilePath
    x) (FilePath
    dest FilePath -> FilePath -> FilePath
    </> FilePath
    x)
          Bool
    False -> Endo [CopyDirAction] -> WriterT (Endo [CopyDirAction]) IO ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (Endo [CopyDirAction] -> WriterT (Endo [CopyDirAction]) IO ())
    -> Endo [CopyDirAction] -> WriterT (Endo [CopyDirAction]) IO ()
    forall a b. (a -> b) -> a -> b
    $ ([CopyDirAction] -> [CopyDirAction]) -> Endo [CopyDirAction]
    forall a. (a -> a) -> Endo a
    Endo (FilePath -> FilePath -> CopyDirAction
    CopyFile (FilePath
    src FilePath -> FilePath -> FilePath
    </> FilePath
    x) (FilePath
    dest FilePath -> FilePath -> FilePath
    </> FilePath
    x) CopyDirAction -> [CopyDirAction] -> [CopyDirAction]
    forall a. a -> [a] -> [a]
    :)

    -- | @copyIfChanged src dst@ makes sure that @dst@ exists
    --   and has the same content as @dst@.
    --
    copyIfChanged :: FilePath -> FilePath -> IO ()
    copyIfChanged :: FilePath -> FilePath -> IO ()
    copyIfChanged FilePath
    src FilePath
    dst = do
      Bool
    exist <- FilePath -> IO Bool
    doesFileExist FilePath
    dst
      if Bool -> Bool
    not Bool
    exist then FilePath -> FilePath -> IO ()
    copyFile FilePath
    src FilePath
    dst else do
        ByteString
    new <- FilePath -> IO ByteString
    BS.readFile FilePath
    src
        ByteString
    old <- FilePath -> IO ByteString
    BS.readFile FilePath
    dst
        Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ByteString
    old ByteString -> ByteString -> Bool
    forall a. Eq a => a -> a -> Bool
    == ByteString
    new) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath -> IO ()
    copyFile FilePath
    src FilePath
    dst