{-# 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 )

-- | What to append to the @AGDA_DIR@ to construct the Agda data directory.

dataDirNameParts :: [FilePath]
dataDirNameParts :: [String]
dataDirNameParts = [ String
"share", String
versionWithCommitInfo ]

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

mkDataDir :: FilePath -> FilePath
mkDataDir :: String -> String
mkDataDir String
base = [String] -> String
joinPath ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
base String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
dataDirNameParts


-- 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 :: [(String, 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 String
getAgdaAppDir = do
  -- The default can be overwritten by setting the AGDA_DIR environment variable
  String -> IO (Maybe String)
lookupEnv String
"AGDA_DIR" IO (Maybe String) -> (Maybe String -> IO String) -> IO String
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 String
Nothing -> IO String
agdaDir
    Just String
dir -> String -> IO Bool
doesDirectoryExist String
dir IO Bool -> (Bool -> IO String) -> IO String
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  -> String -> IO String
canonicalizePath String
dir
      Bool
False -> do
        d <- IO String
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 String
agdaDir = do
      legacyAgdaDir <- String -> IO String
getAppUserDataDirectory String
"agda"
      doesDirectoryExist legacyAgdaDir >>= \case
        Bool
True  -> String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
legacyAgdaDir
        Bool
False -> XdgDirectory -> String -> IO String
getXdgDirectory XdgDirectory
XdgConfig String
"agda"

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

getDataDir :: IO FilePath
getDataDir :: IO String
getDataDir = String -> String
mkDataDir (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String
getAgdaAppDir

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

getDataFileName :: FilePath -> IO FilePath
getDataFileName :: String -> IO String
getDataFileName String
f = IO String
getDataDir IO String -> (String -> String) -> IO String
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (String -> String -> String
</> String
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 String
getAgdaAppDir
  let doSetup = Bool -> String -> IO ()
dumpDataDir Bool
force String
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 -> String -> IO ()
dumpDataDir Bool
verbose String
agdaDir = do
  let dataDir :: String
dataDir = String -> String
mkDataDir String
agdaDir
  Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
dataDir

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

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

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

      -- Write out the file contents.
      let path :: String
path = String
dir String -> String -> String
</> String
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
$ String -> IO ()
inform (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Writing " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
path
      String -> ByteString -> IO ()
BS.writeFile String
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
$ String -> IO ()
removeFile String
lock

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