    {-# OPTIONS_GHC -Wunused-imports #-}

    ------------------------------------------------------------------------
    -- | 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 FilePath
         -- ^ The working directory that should be used when the compiler
         -- is invoked. The default is the current working directory.
      -> 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 [Char]
    -> Maybe TextEncoding
    -> TCM ()
    callCompiler Bool
    doCall [Char]
    cmd [[Char]]
    args Maybe [Char]
    cwd Maybe TextEncoding
    enc =
      if Bool
    doCall then do
        merrors <- [Char]
    -> [[Char]]
    -> Maybe [Char]
    -> Maybe TextEncoding
    -> TCM (Maybe [Char])
    callCompiler' [Char]
    cmd [[Char]]
    args Maybe [Char]
    cwd Maybe TextEncoding
    enc
        case merrors of
          Maybe [Char]
    Nothing     -> () -> TCM ()
    forall a. a -> TCMT IO a
    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 ()
    alwaysReportSLn [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 FilePath
         -- ^ The working directory that should be used when the compiler
         -- is invoked. The default is the current working directory.
      -> 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 [Char]
    -> Maybe TextEncoding
    -> TCM (Maybe [Char])
    callCompiler' [Char]
    cmd [[Char]]
    args Maybe [Char]
    cwd Maybe TextEncoding
    enc = do
      [Char] -> VerboseLevel -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    alwaysReportSLn [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)
      (_, out, err, p) <-
        IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
    -> TCMT
         IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
    forall a. IO a -> TCMT IO a
    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 = CreatePipe
                                   , std_out = CreatePipe
                                   , cwd     = cwd
                                   }

      -- In -v0 mode we throw away any progress information printed to
      -- stdout.
      case out of
        Maybe Handle
    Nothing  -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Just Handle
    out -> TCM () -> TCM ()
    forkTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          -- The handle should be in text mode.
          IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            Just TextEncoding
    enc -> IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    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
          progressInfo <- IO [Char] -> TCMT IO [Char]
    forall a. IO a -> TCMT IO a
    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
          mapM_ (alwaysReportSLn "compile.output" 1) $ lines progressInfo

      errors <- liftIO $ case 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 a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            Just TextEncoding
    enc -> IO () -> IO ()
    forall a. IO a -> IO a
    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 <- liftIO $ do
        -- Ensure that the output has been read before waiting for the
        -- process.
        _ <- E.evaluate (length errors)
        waitForProcess p

      case exitcode of
        ExitFailure VerboseLevel
    _ -> Maybe [Char] -> TCM (Maybe [Char])
    forall a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [Char]
    forall a. Maybe a
    Nothing