    ------------------------------------------------------------------------
    -- | 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