content: {-# 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 =
  #ifdef USE_XDG_DATA_HOME
    (</> versionWithCommitInfo)
  #else
    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 = $(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 = do
    -- The default can be overwritten by setting the AGDA_DIR environment variable
    lookupEnv "AGDA_DIR" >>= \case
      Nothing -> agdaDir
      Just dir -> doesDirectoryExist dir >>= \case
        True  -> canonicalizePath dir
        False -> do
          d <- 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 = do
        legacyAgdaDir <- getAppUserDataDirectory "agda"
        doesDirectoryExist legacyAgdaDir >>= \case
          True  -> return legacyAgdaDir
          False -> getXdgDirectory XdgConfig "agda"
  
  -- | This overrides the 'getDataDir' from ''Paths_Agda''.
  --   See the documentation for the @--print-agda-data-dir@ flag.
  
  getDataDir :: IO FilePath
  getDataDir = mkDataDir <$> getBaseDataDir
  
  getBaseDataDir :: IO FilePath
  getBaseDataDir = do
    lookupEnv "Agda_datadir" >>= \case
      Just dir -> doesDirectoryExist dir >>= \case
        True  -> canonicalizePath dir
        False -> do
          d <- defaultBaseDataDir
          inform $ "Warning: Environment variable Agda_datadir points to non-existing directory " ++ show dir ++ ", using " ++ show d ++ " instead."
          return d
      Nothing -> defaultBaseDataDir
  
  defaultBaseDataDir :: IO FilePath
  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 f = getDataDir <&> (</> 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 force = do
    dir <- getBaseDataDir
    let doSetup = dumpDataDir force 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 verbose baseDataDir = do
    let dataDir = mkDataDir baseDataDir
    createDirectoryIfMissing True dataDir
  
    -- Create a file lock to prevent races caused by the dataDir already created
    -- but not filled with its contents.
    let lock = baseDataDir </> intercalate "-" [".lock", versionWithCommitInfo]
    withFileLock lock Exclusive \ _lock -> do
  
      forM_ embeddedDataDir \ (relativePath, content) -> do
  
        -- Make sure we also create the directories along the way.
        let (relativeDir, file) = splitFileName relativePath
        let dir  = dataDir </> relativeDir
        createDirectoryIfMissing True dir
  
        -- Write out the file contents.
        let path = dir </> file
        when verbose $ inform $ "Writing " ++ path
        BS.writeFile path content
  
    -- Remove the lock (this is surprisingly not done by withFileLock).
    -- Ignore any IOException (e.g. if the file does not exist).
    void $ try @IOException $ removeFile lock
  
  -- | Dump line of warning or information to stderr.
  inform :: String -> IO ()
  inform = hPutStrLn stderr
  