{-# 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
        [Char]
d <- IO [Char]
agdaDir
        [Char] -> IO ()
inform ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Warning: Environment variable AGDA_DIR points to non-existing directory " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
dir [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", using " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
d [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" instead."
        [Char] -> IO [Char]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
d
  where
    -- System-specific command to build the path to ~/.agda (Unix) or %APPDATA%\agda (Win)
    agdaDir :: IO [Char]
agdaDir = do
      [Char]
legacyAgdaDir <- [Char] -> IO [Char]
getAppUserDataDirectory [Char]
"agda"
      [Char] -> IO Bool
doesDirectoryExist [Char]
legacyAgdaDir 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]
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
        [Char]
d <- IO [Char]
defaultBaseDataDir
        [Char] -> IO ()
inform ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Warning: Environment variable Agda_datadir points to non-existing directory " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
dir [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", using " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
d [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" instead."
        [Char] -> IO [Char]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
d
    Maybe [Char]
Nothing -> IO [Char]
defaultBaseDataDir

defaultBaseDataDir :: IO FilePath
defaultBaseDataDir :: IO [Char]
defaultBaseDataDir = do
#ifdef USE_XDG_DATA_HOME
  getXdgDirectory XdgData "agda"
#else
  IO [Char]
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
  [Char]
dir <- IO [Char]
getBaseDataDir
  let doSetup :: IO ()
doSetup = Bool -> [Char] -> IO ()
dumpDataDir Bool
force [Char]
dir

  if Bool
force then IO ()
doSetup else do
    Bool
ex <- [Char] -> IO Bool
doesDirectoryExist ([Char] -> IO Bool) -> [Char] -> IO Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
mkDataDir [Char]
dir
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ex IO ()
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