-- {-# OPTIONS_GHC -Wunused-imports #-}

-- | Setup up the emacs mode for Agda.

module Agda.Setup.EmacsMode
  ( help
  -- * Locate
  , locateFlag
  , printEmacsModeFile
  -- * Setup
  , setupFlag
  , setupDotEmacs
  -- * Compile
  , compileFlag
  , compileElispFiles
  -- * Utilities
  , inform
  )
where

import Control.Applicative    ( liftA2 )
import Control.Exception as E ( bracket, catch, evaluate, IOException )
import Control.Monad          ( unless )

import Data.Bifunctor         ( first, second )
import Data.Bool              ( bool )
import Data.Char              ( isAscii, isPrint )
import Data.Functor           ( (<&>) )
import Data.List              ( isInfixOf )
import Data.Maybe             ( catMaybes, fromMaybe )

import Numeric                ( showHex )

import System.Directory       ( doesFileExist, findExecutable, getTemporaryDirectory, removeFile )
import System.Exit            ( exitFailure, ExitCode(ExitSuccess) )
import System.FilePath        ( (</>), getSearchPath )
import System.IO              ( IOMode(ReadMode)
                              , hClose, hSetEncoding, hGetContents, hPutStr, hPutStrLn
                              , openTempFile, stderr, stdout, utf8, withFile
                              )
import System.Process         ( rawSystem, showCommandForUser )

import Agda.Setup             ( getDataDir )
import Agda.Setup.DataFiles   ( emacsLispFiles, emacsModeDir )

-- Command line options.

setupFlag :: String
setupFlag   = "setup"

locateFlag :: String
locateFlag  = "locate"

compileFlag :: String
compileFlag = "compile"

-- | Help topic for @--emacs-mode@.

help :: String
help = unlines
  [ "Option --emacs-mode allows to administer the Agda Emacs mode."
  , "It accepts three commands:"
  , ""
  , setupFlag
  , ""
  , "  This command unpacks Agda's data files, including the Emacs mode,"
  , "  into Agda's data directory (see option --print-agda-data-dir)."
  , ""
  , "  It then tries to add setup code for Agda's Emacs mode to the"
  , "  current user's .emacs file. It is assumed that the .emacs file"
  , "  uses the character encoding specified by the locale."
  , ""
  , compileFlag
  , ""
  , "  This command unpacks Agda's data files, including the Emacs mode,"
  , "  into Agda's data directory."
  , ""
  , "  It then tries to compile Agda's Emacs mode's source files."
  , ""
  , "  WARNING: If you reinstall the Agda mode without recompiling the Emacs"
  , "  Lisp files, then Emacs may continue using the old, compiled files."
  , ""
  , locateFlag
  , ""
  , "  The path to the Emacs mode's main file is printed on standard"
  , "  output (using the UTF-8 character encoding and no trailing"
  , "  newline)."
  ]

------------------------------------------------------------------------
-- Locating the Agda mode

-- | Prints out the path to the Agda mode's main file (using UTF-8 and
-- without any trailing newline).

printEmacsModeFile :: IO ()
printEmacsModeFile = do
  dataDir <- getDataDir
  let path = dataDir </> emacsModeDir </> "agda2.el"
  hSetEncoding stdout utf8
  putStr path

------------------------------------------------------------------------
-- Setting up the .emacs file

-- | Tries to set up the Agda mode in the given .emacs file.

setupDotEmacs :: String -> IO ()
setupDotEmacs agda = do
  let cmd   = agda ++ " --emacs-mode"
  let elisp = setupString cmd

  dotEmacs <- findDotEmacs
  informLn $ "The .emacs file used: " ++ dotEmacs

  alreadyInstalled cmd dotEmacs >>= \case
    True  -> do
      informLn "It seems as if setup has already been performed."
    False -> do
      appendFile dotEmacs elisp
      inform $ unlines $
        [ "Setup done. Try to (re)start Emacs and open an Agda file."
        , "The following text was appended to the .emacs file:"
        ] ++ lines elisp

-- | Tries to find the user's .emacs file by querying Emacs.

findDotEmacs :: IO FilePath
findDotEmacs = askEmacs "(expand-file-name user-init-file)"

-- | Has the Agda mode already been set up?

alreadyInstalled :: String -> FilePath -> IO Bool
alreadyInstalled cmd dotEmacs = do
  doesFileExist dotEmacs >>= \case
    False -> return False
    True  -> withFile dotEmacs ReadMode \ f -> do
      txt <- hGetContents f
      evaluate $ identifier cmd `isInfixOf` txt
        -- Uses evaluate to ensure that the file is not closed prematurely.

-- | If this string occurs in the .emacs file, then it is assumed that
-- setup has already been performed.

identifier :: String -> String
identifier cmd = cmd ++ " " ++ locateFlag

-- | The string appended to the end of the .emacs file.

setupString :: String -> String
setupString cmd = unlines
  [ ""
  , "(load-file (let ((coding-system-for-read 'utf-8))"
  , "                (shell-command-to-string \""
                        ++ identifier cmd ++ "\")))"
  ]

------------------------------------------------------------------------
-- Querying Emacs

-- | Evaluates the given Elisp command using Emacs. The output of the
-- command (whatever was written into the current buffer) is returned.
--
-- Note: The input is not checked. The input is assumed to come from a
-- trusted source.

askEmacs :: String -> IO String
askEmacs query = do
  tempDir <- getTemporaryDirectory
  bracket (openTempFile tempDir "askEmacs")
          (removeFile . fst) $ \ (file, h) -> do
    hClose h
    exit <- rawSystemWithDiagnostics "emacs"
      [ "--batch"
          -- Andreas, 2022-10-15, issue #5901, suggested by Spencer Baugh (catern):
          -- Use Emacs batch mode so that it can run without a terminal.
      , "--user", ""
          -- The flag --user is necessary with --batch so that user-init-file is defined.
          -- The empty user is the default user.
          -- (Option --batch includes --no-init-file, this is reverted by supplying --user.)
      -- Andreas, 2022-05-25, issue #5901 reloaded:
      -- Loading the init file without loading the site fails for some users:
      -- , "--quick"
      --     -- Option --quick includes --no-site-file.
      , "--eval"
      , apply [ "with-temp-file", escape file, apply [ "insert", query ] ]
          -- Short cutting the temp file via just [ "princ", query ]
          -- does not work if the loading of the user-init-file prints extra stuff.
          -- Going via the temp file we can let this stuff go to stdout without
          -- affecting the output we care about.
      ]
    unless (exit == ExitSuccess) do
      informLn "Unable to query Emacs."
      exitFailure
    withFile file ReadMode \ h -> do
      result <- hGetContents h
      _ <- evaluate (length result)
        -- Uses evaluate to ensure that the file is not closed prematurely.
      return result

-- | Like 'rawSystem' but handles 'IOException' by printing diagnostics
-- (@PATH@) before 'exitFailure'.

rawSystemWithDiagnostics
  :: FilePath  -- ^ Command to run.
  -> [String]  -- ^ Arguments to command.
  -> IO ExitCode
rawSystemWithDiagnostics cmd args =
    rawSystem cmd args
  `E.catch` \ (e :: IOException) -> do
     informLn $ unwords [ "FAILED:", showCommandForUser cmd args ]
     informLn $ unwords [ "Exception:", show e ]
     -- The PATH might be useful in other exceptions, like "permission denied".
     path <- fromMaybe "(not found)" <$> findExecutable cmd
     informLn $ unwords [ "Executable", cmd, "at:", path ]
     informLn "PATH:"
     mapM_ (informLn . ("  - " ++)) =<< getSearchPath
     exitFailure

-- | Escapes the string so that Emacs can parse it as an Elisp string.

escape :: FilePath -> FilePath
escape s = "\"" ++ concatMap esc s ++ "\""
  where
  esc c | c `elem` ['\\', '"']   = '\\' : [c]
        | isAscii c && isPrint c = [c]
        | otherwise              = "\\x" ++ showHex (fromEnum c) "\\ "

------------------------------------------------------------------------
-- Compiling Emacs Lisp files

-- | Tries to compile the Agda mode's Emacs Lisp files.

compileElispFiles :: IO ()
compileElispFiles = do
  dataDir <- getDataDir <&> (</> emacsModeDir)
  let elFiles = map (dataDir </>) emacsLispFiles
  (existing, missing) <- partitionM doesFileExist elFiles
  failed <- catMaybes <$> mapM (compile dataDir) existing

  -- If any of the .el files was missing or failed to compile, fail execution.
  unless (null missing) $ do
    informLn "Missing Emacs Lisp files:"
    mapM_ (informLn . ("  " ++)) missing
  unless (null failed) $ do
    informLn "Unable to compile the following Emacs Lisp files:"
    mapM_ (informLn . ("  " ++)) failed
  unless (null missing && null failed) exitFailure

  where
  compile dataDir f = do
    exit <- rawSystemWithDiagnostics "emacs" $
      [ "--quick"                -- 'quick' implies 'no-site-file'
      , "--directory", dataDir
      , "--batch"                -- 'batch' implies 'no-init-file' but not 'no-site-file'.
      , "--eval"
      , "(progn \
           \(setq byte-compile-error-on-warn t) \
           \(byte-compile-disable-warning 'cl-functions) \
           \(batch-byte-compile))"
      , f
      ]
    return $ if exit == ExitSuccess then Nothing else Just f

------------------------------------------------------------------------
-- Helper functions

-- These functions inform the user about something by printing on
-- stderr.

inform :: String -> IO ()
inform   = hPutStr   stderr

informLn :: String -> IO ()
informLn = hPutStrLn stderr

parens :: String -> String
parens s = concat [ "(", s, ")" ]

-- LISP application
apply :: [String] -> String
apply = parens . unwords

-- Utilities

-- | A ``monadic'' version of @'partition' :: (a -> Bool) -> [a] -> ([a],[a])
partitionM :: Applicative m => (a -> m Bool) -> [a] -> m ([a], [a])
partitionM f =
  foldr (\ x -> liftA2 (bool (second (x:)) (first (x:))) $ f x)
        (pure ([], []))