------------------------------------------------------------------------
-- | A command which calls a compiler
------------------------------------------------------------------------

module Agda.Compiler.CallCompiler where

import qualified Control.Exception as E
import Control.Monad.Trans

import System.Exit
import System.IO
import System.Process

import Agda.TypeChecking.Monad

import Agda.Utils.Impossible

-- | Calls a compiler:
--
-- * Checks the exit code to see if the compiler exits successfully.
--   If not, then an exception is raised, containing the text the
--   compiler printed to stderr (if any).
--
-- * Uses the debug printout machinery to relay any progress
--   information the compiler prints to stdout.

callCompiler
  :: Bool
     -- ^ Should we actually call the compiler
  -> FilePath
     -- ^ The path to the compiler
  -> [String]
     -- ^ Command-line arguments.
  -> Maybe TextEncoding
     -- ^ Use the given text encoding, if any, when reading the output
     -- from the process (stdout and stderr).
  -> TCM ()
callCompiler :: Bool -> [Char] -> [[Char]] -> Maybe TextEncoding -> TCM ()
callCompiler Bool
doCall [Char]
cmd [[Char]]
args Maybe TextEncoding
enc =
  if Bool
doCall then do
    Maybe [Char]
merrors <- [Char] -> [[Char]] -> Maybe TextEncoding -> TCM (Maybe [Char])
callCompiler' [Char]
cmd [[Char]]
args Maybe TextEncoding
enc
    case Maybe [Char]
merrors of
      Maybe [Char]
Nothing     -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just [Char]
errors -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError ([Char] -> TypeError
CompilationError [Char]
errors)
  else
    [Char] -> VerboseLevel -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"compile.cmd" VerboseLevel
1 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"NOT calling: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords ([Char]
cmd [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]]
args)

-- | Generalisation of @callCompiler@ where the raised exception is
-- returned.
callCompiler'
  :: FilePath
     -- ^ The path to the compiler
  -> [String]
     -- ^ Command-line arguments.
  -> Maybe TextEncoding
     -- ^ Use the given text encoding, if any, when reading the output
     -- from the process (stdout and stderr).
  -> TCM (Maybe String)
callCompiler' :: [Char] -> [[Char]] -> Maybe TextEncoding -> TCM (Maybe [Char])
callCompiler' [Char]
cmd [[Char]]
args Maybe TextEncoding
enc = do
  [Char] -> VerboseLevel -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"compile.cmd" VerboseLevel
1 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Calling: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords ([Char]
cmd [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]]
args)
  (Maybe Handle
_, Maybe Handle
out, Maybe Handle
err, ProcessHandle
p) <-
    IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
-> TCMT
     IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
 -> TCMT
      IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle))
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
-> TCMT
     IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$ CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess
               ([Char] -> [[Char]] -> CreateProcess
proc [Char]
cmd [[Char]]
args) { std_err :: StdStream
std_err = StdStream
CreatePipe
                               , std_out :: StdStream
std_out = StdStream
CreatePipe
                               }

  -- In -v0 mode we throw away any progress information printed to
  -- stdout.
  case Maybe Handle
out of
    Maybe Handle
Nothing  -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Just Handle
out -> TCM () -> TCM ()
forall a. TCM a -> TCM ()
forkTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      -- The handle should be in text mode.
      IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Handle -> Bool -> IO ()
hSetBinaryMode Handle
out Bool
False
      case Maybe TextEncoding
enc of
        Maybe TextEncoding
Nothing  -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just TextEncoding
enc -> IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Handle -> TextEncoding -> IO ()
hSetEncoding Handle
out TextEncoding
enc
      [Char]
progressInfo <- IO [Char] -> TCMT IO [Char]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Char] -> TCMT IO [Char]) -> IO [Char] -> TCMT IO [Char]
forall a b. (a -> b) -> a -> b
$ Handle -> IO [Char]
hGetContents Handle
out
      ([Char] -> TCM ()) -> [[Char]] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> VerboseLevel -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"compile.output" VerboseLevel
1) ([[Char]] -> TCM ()) -> [[Char]] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
lines [Char]
progressInfo

  [Char]
errors <- IO [Char] -> TCMT IO [Char]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Char] -> TCMT IO [Char]) -> IO [Char] -> TCMT IO [Char]
forall a b. (a -> b) -> a -> b
$ case Maybe Handle
err of
    Maybe Handle
Nothing  -> IO [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
    Just Handle
err -> do
      -- The handle should be in text mode.
      Handle -> Bool -> IO ()
hSetBinaryMode Handle
err Bool
False
      case Maybe TextEncoding
enc of
        Maybe TextEncoding
Nothing  -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just TextEncoding
enc -> IO () -> IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Handle -> TextEncoding -> IO ()
hSetEncoding Handle
err TextEncoding
enc
      Handle -> IO [Char]
hGetContents Handle
err

  ExitCode
exitcode <- IO ExitCode -> TCMT IO ExitCode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ExitCode -> TCMT IO ExitCode)
-> IO ExitCode -> TCMT IO ExitCode
forall a b. (a -> b) -> a -> b
$ do
    -- Ensure that the output has been read before waiting for the
    -- process.
    VerboseLevel
_ <- VerboseLevel -> IO VerboseLevel
forall a. a -> IO a
E.evaluate ([Char] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Char]
errors)
    ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
p

  case ExitCode
exitcode of
    ExitFailure VerboseLevel
_ -> Maybe [Char] -> TCM (Maybe [Char])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> TCM (Maybe [Char]))
-> Maybe [Char] -> TCM (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
errors
    ExitCode
_             -> Maybe [Char] -> TCM (Maybe [Char])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Char]
forall a. Maybe a
Nothing