    {-# LANGUAGE CPP #-}
    {-# LANGUAGE TemplateHaskell #-}

    -- | Agda's self-setup.

    module Agda.Setup
      ( getAgdaAppDir
      , getDataDir
      , getDataFileName
      , setup
      )
    where

    import           Control.Exception          ( IOException, try )
    import           Control.Monad              ( forM, forM_, unless, void, when )

    import           Data.ByteString            ( ByteString )
    import qualified Data.ByteString            as BS
    import           Data.Functor               ( (<&>) )
    import           Data.List                  ( intercalate )

    import           Language.Haskell.TH.Syntax ( qAddDependentFile, runIO )

    -- Import instance Lift ByteString if not supplied by bytestring.
    #if !MIN_VERSION_bytestring(0,11,2)
    import           Instances.TH.Lift          ()
    #endif

    import           System.Directory
      ( XdgDirectory (..)
      , canonicalizePath, createDirectoryIfMissing, doesDirectoryExist
      , getAppUserDataDirectory, getXdgDirectory, removeFile
      )
    import           System.Environment         ( lookupEnv )
    import           System.FileLock            ( pattern Exclusive, withFileLock )
    import           System.FilePath            ( (</>), joinPath, splitFileName, takeFileName )
    import           System.IO                  ( hPutStrLn, stderr )

    import           Agda.Setup.DataFiles       ( dataFiles, dataPath )
    import           Agda.VersionCommit         ( versionWithCommitInfo )

    import qualified Paths_Agda                 as Paths

    -- | Given the `Agda_datadir`, what should the Agda data dir be?

    mkDataDir :: FilePath -> FilePath
    mkDataDir :: [Char] -> [Char]
    mkDataDir =
    #ifdef USE_XDG_DATA_HOME
      (</> versionWithCommitInfo)
    #else
      [Char] -> [Char]
    forall a. a -> a
    id
    #endif

    -- Tell TH that all the dataFiles are needed for compilation.
    [] <$ mapM_ (qAddDependentFile . dataPath) dataFiles

    -- | The embedded contents of the Agda data directory,
    --   generated by Template Haskell at compile time.

    embeddedDataDir :: [(FilePath, ByteString)]
    embeddedDataDir :: [([Char], ByteString)]
    embeddedDataDir = $(do

        -- Load all the dataFiles.
        contents <- runIO $ mapM (BS.readFile . dataPath) dataFiles

        -- Return the association list as Exp.
        [| zip dataFiles contents |]
      )

    -- | Get the path to @~/.agda@ (system-specific).
    --   Can be overwritten by the @AGDA_DIR@ environment variable.
    --
    --   (This is not to be confused with the directory 'getDataDir' for the data files
    --   that Agda needs (e.g. the primitive modules).)
    --
    getAgdaAppDir :: IO FilePath
    getAgdaAppDir :: IO [Char]
    getAgdaAppDir = do
      -- The default can be overwritten by setting the AGDA_DIR environment variable
      [Char] -> IO (Maybe [Char])
    lookupEnv [Char]
    "AGDA_DIR" IO (Maybe [Char]) -> (Maybe [Char] -> IO [Char]) -> IO [Char]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe [Char]
    Nothing -> IO [Char]
    agdaDir
        Just [Char]
    dir -> [Char] -> IO Bool
    doesDirectoryExist [Char]
    dir IO Bool -> (Bool -> IO [Char]) -> IO [Char]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Bool
    True  -> [Char] -> IO [Char]
    canonicalizePath [Char]
    dir
          Bool
    False -> do
            d <- IO [Char]
    agdaDir
            inform $ "Warning: Environment variable AGDA_DIR points to non-existing directory " ++ show dir ++ ", using " ++ show d ++ " instead."
            return d
      where
        -- System-specific command to build the path to ~/.agda (Unix) or %APPDATA%\agda (Win)
        agdaDir :: IO [Char]
    agdaDir = do
          legacyAgdaDir <- [Char] -> IO [Char]
    getAppUserDataDirectory [Char]
    "agda"
          doesDirectoryExist legacyAgdaDir >>= \case
            Bool
    True  -> [Char] -> IO [Char]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Char]
    legacyAgdaDir
            Bool
    False -> XdgDirectory -> [Char] -> IO [Char]
    getXdgDirectory XdgDirectory
    XdgConfig [Char]
    "agda"

    -- | This overrides the 'getDataDir' from ''Paths_Agda''.
    --   See the documentation for the @--print-agda-data-dir@ flag.

    getDataDir :: IO FilePath
    getDataDir :: IO [Char]
    getDataDir = [Char] -> [Char]
    mkDataDir ([Char] -> [Char]) -> IO [Char] -> IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO [Char]
    getBaseDataDir

    getBaseDataDir :: IO FilePath
    getBaseDataDir :: IO [Char]
    getBaseDataDir = do
      [Char] -> IO (Maybe [Char])
    lookupEnv [Char]
    "Agda_datadir" IO (Maybe [Char]) -> (Maybe [Char] -> IO [Char]) -> IO [Char]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just [Char]
    dir -> [Char] -> IO Bool
    doesDirectoryExist [Char]
    dir IO Bool -> (Bool -> IO [Char]) -> IO [Char]
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Bool
    True  -> [Char] -> IO [Char]
    canonicalizePath [Char]
    dir
          Bool
    False -> do
            d <- IO [Char]
    defaultBaseDataDir
            inform $ "Warning: Environment variable Agda_datadir points to non-existing directory " ++ show dir ++ ", using " ++ show d ++ " instead."
            return d
        Maybe [Char]
    Nothing -> IO [Char]
    defaultBaseDataDir

    defaultBaseDataDir :: IO FilePath
    defaultBaseDataDir :: IO [Char]
    defaultBaseDataDir = do
    #ifdef USE_XDG_DATA_HOME
      getXdgDirectory XdgData "agda"
    #else
      Paths.getDataDir
    #endif

    -- | This overrides the 'getDataFileName' from ''Paths_Agda''.

    getDataFileName :: FilePath -> IO FilePath
    getDataFileName :: [Char] -> IO [Char]
    getDataFileName [Char]
    f = IO [Char]
    getDataDir IO [Char] -> ([Char] -> [Char]) -> IO [Char]
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> ([Char] -> [Char] -> [Char]
    </> [Char]
    f)

    -- | @False@: Check whether we need to setup Agda.
    --   This function can be called when starting up Agda.
    --
    -- @True@: force a setup e.g. when passing Agda option @--setup@.
    --
    -- Copies the embedded data files to the designated data directory.

    setup :: Bool -> IO ()
    setup :: Bool -> IO ()
    setup Bool
    force = do
      dir <- IO [Char]
    getBaseDataDir
      let doSetup = Bool -> [Char] -> IO ()
    dumpDataDir Bool
    force [Char]
    dir

      if force then doSetup else do
        ex <- doesDirectoryExist $ mkDataDir dir
        unless ex doSetup

    -- | Spit out the embedded files into Agda data directory relative to the given directory.
    --   Lock the directory while doing so.

    dumpDataDir :: Bool -> FilePath -> IO ()
    dumpDataDir :: Bool -> [Char] -> IO ()
    dumpDataDir Bool
    verbose [Char]
    baseDataDir = do
      let dataDir :: [Char]
    dataDir = [Char] -> [Char]
    mkDataDir [Char]
    baseDataDir
      Bool -> [Char] -> IO ()
    createDirectoryIfMissing Bool
    True [Char]
    dataDir

      -- Create a file lock to prevent races caused by the dataDir already created
      -- but not filled with its contents.
      let lock :: [Char]
    lock = [Char]
    baseDataDir [Char] -> [Char] -> [Char]
    </> [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "-" [[Char]
    ".lock", [Char]
    versionWithCommitInfo]
      [Char] -> SharedExclusive -> (FileLock -> IO ()) -> IO ()
    forall a. [Char] -> SharedExclusive -> (FileLock -> IO a) -> IO a
    withFileLock [Char]
    lock SharedExclusive
    Exclusive \ FileLock
    _lock -> do

        [([Char], ByteString)] -> (([Char], ByteString) -> IO ()) -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [([Char], ByteString)]
    embeddedDataDir \ ([Char]
    relativePath, ByteString
    content) -> do

          -- Make sure we also create the directories along the way.
          let ([Char]
    relativeDir, [Char]
    file) = [Char] -> ([Char], [Char])
    splitFileName [Char]
    relativePath
          let dir :: [Char]
    dir  = [Char]
    dataDir [Char] -> [Char] -> [Char]
    </> [Char]
    relativeDir
          Bool -> [Char] -> IO ()
    createDirectoryIfMissing Bool
    True [Char]
    dir

          -- Write out the file contents.
          let path :: [Char]
    path = [Char]
    dir [Char] -> [Char] -> [Char]
    </> [Char]
    file
          Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    verbose (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ()
    inform ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Writing " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    path
          [Char] -> ByteString -> IO ()
    BS.writeFile [Char]
    path ByteString
    content

      -- Remove the lock (this is surprisingly not done by withFileLock).
      -- Ignore any IOException (e.g. if the file does not exist).
      IO (Either IOException ()) -> IO ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (IO (Either IOException ()) -> IO ())
    -> IO (Either IOException ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ forall e a. Exception e => IO a -> IO (Either e a)
    try @IOException (IO () -> IO (Either IOException ()))
    -> IO () -> IO (Either IOException ())
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ()
    removeFile [Char]
    lock

    -- | Dump line of warning or information to stderr.
    inform :: String -> IO ()
    inform :: [Char] -> IO ()
    inform = Handle -> [Char] -> IO ()
    hPutStrLn Handle
    stderr