    {-# LANGUAGE CPP #-}

    {-| Agda main module.
    -}
    module Agda.Main where

    import Prelude hiding (null)

    import qualified Control.Exception as E
    import Control.Monad          ( void )
    import Control.Monad.Except   ( MonadError(..), ExceptT(..), runExceptT )
    import Control.Monad.IO.Class ( MonadIO(..) )

    import qualified Data.List as List
    import Data.Function          ( (&) )
    import Data.Functor
    import Data.Maybe
    import qualified Data.Set as Set
    import qualified Data.Text as T

    import System.Environment ( getArgs, getProgName )
    import System.Exit ( exitSuccess, ExitCode )
    import System.FilePath ( takeFileName )
    import Agda.Utils.GetOpt
    import qualified System.IO as IO

    import Agda.Interaction.BuildLibrary (buildLibrary)
    import Agda.Interaction.CommandLine
    import Agda.Interaction.ExitCode as ExitCode (AgdaError(..), exitSuccess, exitAgdaWith)
    import Agda.Interaction.Options
    import Agda.Interaction.Options.Help (Help (..))
    import Agda.Interaction.EmacsTop (mimicGHCi)
    import Agda.Interaction.JSONTop (jsonREPL)
    import Agda.Interaction.FindFile ( SourceFile(SourceFile) )
    import qualified Agda.Interaction.Imports as Imp

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Errors
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Warnings
    import Agda.TypeChecking.Pretty

    import Agda.Compiler.Backend
    import Agda.Compiler.Builtin

    import Agda.Setup ( getAgdaAppDir, getDataDir, setup )
    import Agda.Setup.EmacsMode
    import Agda.VersionCommit ( versionWithCommitInfo )

    import qualified Agda.Utils.Benchmark as UtilsBench
    import qualified Agda.Syntax.Common.Pretty.ANSI as ANSI
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Utils.FileName (absolute, filePath, AbsolutePath)
    import Agda.Utils.String
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null

    import Agda.Utils.Impossible

    -- | The main function
    runAgda :: [Backend] -> IO ()
    runAgda :: [Backend] -> IO ()
    runAgda [Backend]
    backends = [Backend] -> IO ()
    runAgda' ([Backend] -> IO ()) -> [Backend] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Backend]
    builtinBackends [Backend] -> [Backend] -> [Backend]
    forall a. [a] -> [a] -> [a]
    ++ [Backend]
    backends

    -- | The main function without importing built-in backends
    runAgda' :: [Backend] -> IO ()
    runAgda' :: [Backend] -> IO ()
    runAgda' [Backend]
    backends = do
      progName <- IO [Char]
    getProgName
      argv     <- getArgs
      let (z, warns) = runOptM $ parseBackendOptions backends argv defaultOptions
      conf     <- runExceptT $ do
        (bs, opts) <- ExceptT $ pure z
        -- The absolute path of the input file, if provided
        inputFile <- liftIO $ mapM absolute $ optInputFile opts
        mode      <- getInteractor bs inputFile opts
        return (bs, opts, mode)

      case conf of
        Left [Char]
    err -> [Char] -> IO ()
    optionError [Char]
    err
        Right ([Backend]
    bs, CommandLineOptions
    opts, Maybe (Interactor ())
    mode) -> do

          -- Setup Agda if requested
          Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (CommandLineOptions -> Bool
    optSetup CommandLineOptions
    opts) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> IO ()
    Agda.Setup.setup Bool
    True

          -- Print information as requested
          Maybe PrintAgdaVersion -> (PrintAgdaVersion -> IO ()) -> IO ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (CommandLineOptions -> Maybe PrintAgdaVersion
    optPrintVersion CommandLineOptions
    opts) ((PrintAgdaVersion -> IO ()) -> IO ())
    -> (PrintAgdaVersion -> IO ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Backend] -> PrintAgdaVersion -> IO ()
    printVersion [Backend]
    bs
          Maybe Help -> (Help -> IO ()) -> IO ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (CommandLineOptions -> Maybe Help
    optPrintHelp    CommandLineOptions
    opts) ((Help -> IO ()) -> IO ()) -> (Help -> IO ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Backend] -> Help -> IO ()
    printUsage   [Backend]
    bs
          Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (CommandLineOptions -> Bool
    optPrintAgdaAppDir  CommandLineOptions
    opts) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ IO ()
    printAgdaAppDir
          Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (CommandLineOptions -> Bool
    optPrintAgdaDataDir CommandLineOptions
    opts) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ IO ()
    printAgdaDataDir

          -- Setup emacs mode
          Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (EmacsModeCommand
    EmacsModeSetup EmacsModeCommand -> Set EmacsModeCommand -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` CommandLineOptions -> Set EmacsModeCommand
    optEmacsMode CommandLineOptions
    opts) do
            Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (CommandLineOptions -> Bool
    optSetup CommandLineOptions
    opts) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> IO ()
    Agda.Setup.setup Bool
    False
            [Char] -> IO ()
    setupDotEmacs ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    takeFileName [Char]
    progName

          -- Compile emacs mode
          Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (EmacsModeCommand
    EmacsModeCompile EmacsModeCommand -> Set EmacsModeCommand -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` CommandLineOptions -> Set EmacsModeCommand
    optEmacsMode CommandLineOptions
    opts) do
            Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (CommandLineOptions -> Bool
    optSetup CommandLineOptions
    opts) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> IO ()
    Agda.Setup.setup Bool
    False
            IO ()
    compileElispFiles

          -- Locate emacs mode
          Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (EmacsModeCommand
    EmacsModeLocate EmacsModeCommand -> Set EmacsModeCommand -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` CommandLineOptions -> Set EmacsModeCommand
    optEmacsMode CommandLineOptions
    opts) do
            Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (CommandLineOptions -> Bool
    optSetup CommandLineOptions
    opts) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> IO ()
    Agda.Setup.setup Bool
    False
            IO ()
    printEmacsModeFile

          case Maybe (Interactor ())
    mode of
            Maybe (Interactor ())
    Nothing -> do
              let
                something :: Bool
    something = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or
                  [ CommandLineOptions
    opts CommandLineOptions -> (CommandLineOptions -> Bool) -> Bool
    forall a b. a -> (a -> b) -> b
    & CommandLineOptions -> Bool
    optSetup
                  , CommandLineOptions
    opts CommandLineOptions
    -> (CommandLineOptions -> Maybe PrintAgdaVersion)
    -> Maybe PrintAgdaVersion
    forall a b. a -> (a -> b) -> b
    & CommandLineOptions -> Maybe PrintAgdaVersion
    optPrintVersion Maybe PrintAgdaVersion -> (Maybe PrintAgdaVersion -> Bool) -> Bool
    forall a b. a -> (a -> b) -> b
    & Maybe PrintAgdaVersion -> Bool
    forall a. Maybe a -> Bool
    isJust
                  , CommandLineOptions
    opts CommandLineOptions
    -> (CommandLineOptions -> Maybe Help) -> Maybe Help
    forall a b. a -> (a -> b) -> b
    & CommandLineOptions -> Maybe Help
    optPrintHelp    Maybe Help -> (Maybe Help -> Bool) -> Bool
    forall a b. a -> (a -> b) -> b
    & Maybe Help -> Bool
    forall a. Maybe a -> Bool
    isJust
                  , CommandLineOptions
    opts CommandLineOptions -> (CommandLineOptions -> Bool) -> Bool
    forall a b. a -> (a -> b) -> b
    & CommandLineOptions -> Bool
    optPrintAgdaAppDir
                  , CommandLineOptions
    opts CommandLineOptions -> (CommandLineOptions -> Bool) -> Bool
    forall a b. a -> (a -> b) -> b
    & CommandLineOptions -> Bool
    optPrintAgdaDataDir
                  , CommandLineOptions
    opts CommandLineOptions
    -> (CommandLineOptions -> Set EmacsModeCommand)
    -> Set EmacsModeCommand
    forall a b. a -> (a -> b) -> b
    & CommandLineOptions -> Set EmacsModeCommand
    optEmacsMode    Set EmacsModeCommand -> (Set EmacsModeCommand -> Bool) -> Bool
    forall a b. a -> (a -> b) -> b
    & Bool -> Bool
    not (Bool -> Bool)
    -> (Set EmacsModeCommand -> Bool) -> Set EmacsModeCommand -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set EmacsModeCommand -> Bool
    forall a. Null a => a -> Bool
    null
                  ]
              -- if no task was given to Agda
              Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless Bool
    something (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ()
    optionError [Char]
    "No task given."

            Just Interactor ()
    interactor -> do
             Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (CommandLineOptions -> Bool
    optSetup CommandLineOptions
    opts) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> IO ()
    Agda.Setup.setup Bool
    False

             TCM () -> IO ()
    runTCMPrettyErrors do

              (OptionWarning -> TCM ()) -> OptionWarnings -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ())
    -> (OptionWarning -> Warning) -> OptionWarning -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OptionWarning -> Warning
    OptionWarning) OptionWarnings
    warns

              Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (CommandLineOptions -> Bool
    optTransliterate CommandLineOptions
    opts) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    $ do
                -- When --interaction or --interaction-json is used, then we
                -- use UTF-8 when writing to stdout (and when reading from
                -- stdin).
                if CommandLineOptions -> Bool
    optGHCiInteraction CommandLineOptions
    opts Bool -> Bool -> Bool
    || CommandLineOptions -> Bool
    optJSONInteraction CommandLineOptions
    opts
                then [Char] -> IO ()
    optionError ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $
                       [Char]
    "The option --transliterate must not be combined with " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                       [Char]
    "--interaction or --interaction-json"
                else do
                  -- Transliterate unsupported code points.
                  enc <- [Char] -> IO TextEncoding
    IO.mkTextEncoding (TextEncoding -> [Char]
    forall a. Show a => a -> [Char]
    show TextEncoding
    IO.localeEncoding [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "//TRANSLIT")
                  IO.hSetEncoding IO.stdout enc
                  IO.hSetEncoding IO.stderr enc

              Lens' TCState [Backend] -> [Backend] -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    setTCLens ([Backend] -> f [Backend]) -> TCState -> f TCState
    Lens' TCState [Backend]
    stBackends [Backend]
    bs
              Interactor () -> [Char] -> CommandLineOptions -> TCM ()
    forall a. Interactor a -> [Char] -> CommandLineOptions -> TCM a
    runAgdaWithOptions Interactor ()
    interactor [Char]
    progName CommandLineOptions
    opts

    type Interactor a
        -- Setup/initialization action.
        -- This is separated so that errors can be reported in the appropriate format.
        = TCM ()
        -- Type-checking action
        -> (AbsolutePath -> TCM CheckResult)
        -- Main transformed action.
        -> TCM a

    -- | Major mode of operation, not including the standard mode (checking the given main module).
    data FrontendType
      = FrontEndInteraction InteractionFormat
          -- ^ @--interaction@ or @--interaction-json@.
      | FrontEndRepl
          -- ^ @--interactive@.
      | FrontEndBuildLibrary
          -- ^ @--build-library@.

    data InteractionFormat
      = InteractionEmacs
          -- ^ @--interaction@.
      | InteractionJson
          -- ^ @--interaction-json@.

    pattern FrontEndEmacs :: FrontendType
    pattern $mFrontEndEmacs :: forall {r}. FrontendType -> ((# #) -> r) -> ((# #) -> r) -> r
    $bFrontEndEmacs :: FrontendType
    FrontEndEmacs = FrontEndInteraction InteractionEmacs

    pattern FrontEndJson :: FrontendType
    pattern $mFrontEndJson :: forall {r}. FrontendType -> ((# #) -> r) -> ((# #) -> r) -> r
    $bFrontEndJson :: FrontendType
    FrontEndJson  = FrontEndInteraction InteractionJson

    {-# COMPLETE FrontEndBuildLibrary, FrontEndEmacs, FrontEndJson, FrontEndRepl #-}

    buildLibraryInteractor :: Interactor ()
    buildLibraryInteractor :: Interactor ()
    buildLibraryInteractor TCM ()
    setup AbsolutePath -> TCM CheckResult
    _check = do TCM ()
    setup; TCM ()
    buildLibrary

    -- | Emacs/JSON mode. Note that it ignores the "check" action because it calls typeCheck directly.
    interactionInteractor :: InteractionFormat -> Interactor ()
    interactionInteractor :: InteractionFormat -> Interactor ()
    interactionInteractor InteractionFormat
    InteractionEmacs TCM ()
    setup AbsolutePath -> TCM CheckResult
    _check = TCM () -> TCM ()
    mimicGHCi TCM ()
    setup
    interactionInteractor InteractionFormat
    InteractionJson  TCM ()
    setup AbsolutePath -> TCM CheckResult
    _check = TCM () -> TCM ()
    jsonREPL  TCM ()
    setup

    -- | The (deprecated) repl mode.
    replInteractor :: Maybe AbsolutePath -> Interactor ()
    replInteractor :: Maybe AbsolutePath -> Interactor ()
    replInteractor = Maybe AbsolutePath -> Interactor ()
    runInteractionLoop

    -- | The interactor to use when there are no frontends or backends specified.
    defaultInteractor :: AbsolutePath -> Interactor ()
    defaultInteractor :: AbsolutePath -> Interactor ()
    defaultInteractor AbsolutePath
    file TCM ()
    setup AbsolutePath -> TCM CheckResult
    check = do TCM ()
    setup; TCM CheckResult -> TCM ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (TCM CheckResult -> TCM ()) -> TCM CheckResult -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> TCM CheckResult
    check AbsolutePath
    file

    getInteractor :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m (Maybe (Interactor ()))
    getInteractor :: forall (m :: * -> *).
    MonadError [Char] m =>
    [Backend]
    -> Maybe AbsolutePath
    -> CommandLineOptions
    -> m (Maybe (Interactor ()))
    getInteractor [Backend]
    configuredBackends Maybe AbsolutePath
    maybeInputFile CommandLineOptions
    opts = do

      case [FrontendType]
    enabledFrontends of
        FrontendType
    _:FrontendType
    _:[FrontendType]
    _ -> [Char] -> m (Maybe (Interactor ()))
    forall a. [Char] -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> m (Maybe (Interactor ())))
    -> [Char] -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "Must not specify multiple ", [Char]
    enabledFrontendNames]

        -- standard mode of operation
        [] -> do
          case (Maybe AbsolutePath
    maybeInputFile, [Backend]
    enabledBackends) of
            (Just AbsolutePath
    inputFile, Backend
    _:[Backend]
    _) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
    -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ Interactor () -> Maybe (Interactor ())
    forall a. a -> Maybe a
    Just (Interactor () -> Maybe (Interactor ()))
    -> Interactor () -> Maybe (Interactor ())
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> [Backend] -> Interactor ()
    backendInteraction AbsolutePath
    inputFile [Backend]
    enabledBackends
            (Just AbsolutePath
    inputFile,  []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
    -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ Interactor () -> Maybe (Interactor ())
    forall a. a -> Maybe a
    Just (Interactor () -> Maybe (Interactor ()))
    -> Interactor () -> Maybe (Interactor ())
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> Interactor ()
    defaultInteractor AbsolutePath
    inputFile
            (Maybe AbsolutePath
    Nothing,         []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Interactor ())
    forall a. Maybe a
    Nothing -- No backends, frontends, or input files specified.
            (Maybe AbsolutePath
    Nothing,        Backend
    _:[Backend]
    _) -> [Char] -> m (Maybe (Interactor ()))
    forall a. [Char] -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> m (Maybe (Interactor ())))
    -> [Char] -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "No input file specified for ", [Char]
    enabledBackendNames]

        -- special mode of operation
        [FrontendType
    fe] -> do
          case FrontendType
    fe of
            -- --interactive
            FrontendType
    FrontEndRepl -> do
              FrontendType -> m ()
    noBackends FrontendType
    fe
              FrontendType -> m ()
    notJustScopeChecking FrontendType
    fe
              Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
    -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ Interactor () -> Maybe (Interactor ())
    forall a. a -> Maybe a
    Just (Interactor () -> Maybe (Interactor ()))
    -> Interactor () -> Maybe (Interactor ())
    forall a b. (a -> b) -> a -> b
    $ Maybe AbsolutePath -> Interactor ()
    replInteractor Maybe AbsolutePath
    maybeInputFile
            -- --interaction(-json)
            FrontEndInteraction InteractionFormat
    i -> do
              FrontendType -> m ()
    noBackends FrontendType
    fe
              FrontendType -> m ()
    notJustScopeChecking FrontendType
    fe
              FrontendType -> m ()
    noInputFile FrontendType
    fe
              Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
    -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ Interactor () -> Maybe (Interactor ())
    forall a. a -> Maybe a
    Just (Interactor () -> Maybe (Interactor ()))
    -> Interactor () -> Maybe (Interactor ())
    forall a b. (a -> b) -> a -> b
    $ InteractionFormat -> Interactor ()
    interactionInteractor InteractionFormat
    i
            -- --build-library
            FrontendType
    FrontEndBuildLibrary -> do
              Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (CommandLineOptions -> Bool
    optUseLibs CommandLineOptions
    opts) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                [Char] -> m ()
    forall a. [Char] -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "--build-library cannot be combined with --no-libraries"
              FrontendType -> m ()
    noInputFile FrontendType
    fe
              Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
    -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ Interactor () -> Maybe (Interactor ())
    forall a. a -> Maybe a
    Just Interactor ()
    buildLibraryInteractor
      where
        -- NOTE: The notion of a backend being "enabled" *just* refers to this top-level interaction mode selection. The
        -- interaction/interactive front-ends may still invoke available backends even if they are not "enabled".
        isBackendEnabled :: Backend_boot definition tcm -> Bool
    isBackendEnabled (Backend Backend'_boot definition tcm opts env menv mod def
    b) = Backend'_boot definition tcm opts env menv mod def -> opts -> Bool
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> opts -> Bool
    isEnabled Backend'_boot definition tcm opts env menv mod def
    b (Backend'_boot definition tcm opts env menv mod def -> opts
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> opts
    options Backend'_boot definition tcm opts env menv mod def
    b)
        enabledBackends :: [Backend]
    enabledBackends = (Backend -> Bool) -> [Backend] -> [Backend]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Backend -> Bool
    forall {definition} {tcm :: * -> *}.
    Backend_boot definition tcm -> Bool
    isBackendEnabled [Backend]
    configuredBackends
        enabledFrontends :: [FrontendType]
    enabledFrontends = [[FrontendType]] -> [FrontendType]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
          [ [ FrontendType
    FrontEndRepl  | CommandLineOptions -> Bool
    optInteractive     CommandLineOptions
    opts ]
          , [ FrontendType
    FrontEndEmacs | CommandLineOptions -> Bool
    optGHCiInteraction CommandLineOptions
    opts ]
          , [ FrontendType
    FrontEndJson  | CommandLineOptions -> Bool
    optJSONInteraction CommandLineOptions
    opts ]
          , [ FrontendType
    FrontEndBuildLibrary | CommandLineOptions -> Bool
    optBuildLibrary CommandLineOptions
    opts ]
          ]
        -- Constructs messages like "(no backend)", "backend ghc", "backends (ghc, ocaml)"
        pluralize :: [Char] -> [[Char]] -> [Char]
    pluralize [Char]
    w []  = [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "(no ", [Char]
    w, [Char]
    ")"]
        pluralize [Char]
    w [[Char]
    x] = [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    w, [Char]
    " ", [Char]
    x]
        pluralize [Char]
    w [[Char]]
    xs  = [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    w, [Char]
    "s (", [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    ", " [[Char]]
    xs, [Char]
    ")"]
        enabledBackendNames :: [Char]
    enabledBackendNames  = [Char] -> [[Char]] -> [Char]
    pluralize [Char]
    "backend" [ Text -> [Char]
    T.unpack (Text -> [Char]) -> Text -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Backend'_boot Definition (TCMT IO) opts env menv mod def -> Text
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> Text
    backendName Backend'_boot Definition (TCMT IO) opts env menv mod def
    b | Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
    b <- [Backend]
    enabledBackends ]
        enabledFrontendNames :: [Char]
    enabledFrontendNames = [Char] -> [[Char]] -> [Char]
    pluralize [Char]
    "frontend" (FrontendType -> [Char]
    frontendFlagName (FrontendType -> [Char]) -> [FrontendType] -> [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FrontendType]
    enabledFrontends)
        frontendFlagName :: FrontendType -> [Char]
    frontendFlagName = ([Char]
    "--" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) ([Char] -> [Char])
    -> (FrontendType -> [Char]) -> FrontendType -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
          FrontendType
    FrontEndEmacs -> [Char]
    "interaction"
          FrontendType
    FrontEndJson -> [Char]
    "interaction-json"
          FrontendType
    FrontEndRepl -> [Char]
    "interactive"
          FrontendType
    FrontEndBuildLibrary -> [Char]
    "build-library"
        noBackends :: FrontendType -> m ()
    noBackends FrontendType
    fe = Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([Backend] -> Bool
    forall a. Null a => a -> Bool
    null [Backend]
    enabledBackends) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> m ()
    forall a. [Char] -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "Cannot mix ", FrontendType -> [Char]
    frontendFlagName FrontendType
    fe, [Char]
    " with ", [Char]
    enabledBackendNames]
        noInputFile :: FrontendType -> m ()
    noInputFile FrontendType
    fe = Maybe AbsolutePath -> (AbsolutePath -> m ()) -> m ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe AbsolutePath
    maybeInputFile \ AbsolutePath
    inputFile -> AbsolutePath -> FrontendType -> m ()
    forall {m :: * -> *} {a}.
    MonadError [Char] m =>
    AbsolutePath -> FrontendType -> m a
    errorFrontendFileDisallowed AbsolutePath
    inputFile FrontendType
    fe
        notJustScopeChecking :: FrontendType -> m ()
    notJustScopeChecking = Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (CommandLineOptions -> Bool
    optOnlyScopeChecking CommandLineOptions
    opts) (m () -> m ()) -> (FrontendType -> m ()) -> FrontendType -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FrontendType -> m ()
    forall {m :: * -> *} {a}.
    MonadError [Char] m =>
    FrontendType -> m a
    errorFrontendScopeChecking
        errorFrontendScopeChecking :: FrontendType -> m a
    errorFrontendScopeChecking FrontendType
    fe = [Char] -> m a
    forall a. [Char] -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> m a) -> [Char] -> m a
    forall a b. (a -> b) -> a -> b
    $
          [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "The --only-scope-checking flag cannot be combined with ", FrontendType -> [Char]
    frontendFlagName FrontendType
    fe]
        errorFrontendFileDisallowed :: AbsolutePath -> FrontendType -> m a
    errorFrontendFileDisallowed AbsolutePath
    inputFile FrontendType
    fe = [Char] -> m a
    forall a. [Char] -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> m a) -> [Char] -> m a
    forall a b. (a -> b) -> a -> b
    $
          [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "Must not specify an input file (", AbsolutePath -> [Char]
    filePath AbsolutePath
    inputFile, [Char]
    ") with ", FrontendType -> [Char]
    frontendFlagName FrontendType
    fe]

    -- | Run Agda with parsed command line options
    runAgdaWithOptions
      :: Interactor a       -- ^ Backend interaction
      -> String             -- ^ program name
      -> CommandLineOptions -- ^ parsed command line options
      -> TCM a
    runAgdaWithOptions :: forall a. Interactor a -> [Char] -> CommandLineOptions -> TCM a
    runAgdaWithOptions Interactor a
    interactor [Char]
    progName CommandLineOptions
    opts = do
              -- Main function.
              -- Bill everything to root of Benchmark trie.
              BenchmarkOn (BenchPhase (TCMT IO)) -> TCM ()
    forall (m :: * -> *).
    MonadBench m =>
    BenchmarkOn (BenchPhase m) -> m ()
    UtilsBench.setBenchmarking BenchmarkOn (BenchPhase (TCMT IO))
    BenchmarkOn Phase
    forall a. BenchmarkOn a
    UtilsBench.BenchmarkOn
                -- Andreas, Nisse, 2016-10-11 AIM XXIV
                -- Turn benchmarking on provisionally, otherwise we lose track of time spent
                -- on e.g. LaTeX-code generation.
                -- Benchmarking might be turned off later by setCommandlineOptions

              Account (BenchPhase (TCMT IO)) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [] (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $
                Interactor a
    interactor TCM ()
    initialSetup AbsolutePath -> TCM CheckResult
    checkFile
              TCMT IO a -> TCM () -> TCMT IO a
    forall a b. TCM a -> TCM b -> TCM a
    `finally_` do
                -- Print benchmarks.
                TCM ()
    forall (tcm :: * -> *). MonadTCM tcm => tcm ()
    Bench.print

                -- Print accumulated statistics.
                Maybe TopLevelModuleName -> Statistics -> TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m, HasOptions m) =>
    Maybe TopLevelModuleName -> Statistics -> m ()
    printStatistics Maybe TopLevelModuleName
    forall a. Maybe a
    Nothing (Statistics -> TCM ()) -> TCMT IO Statistics -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Lens' TCState Statistics -> TCMT IO Statistics
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Statistics -> f Statistics) -> TCState -> f TCState
    Lens' TCState Statistics
    lensAccumStatistics
      where
        -- Options are fleshed out here so that (most) errors like
        -- "bad library path" are validated within the interactor,
        -- so that they are reported with the appropriate protocol/formatting.
        initialSetup :: TCM ()
        initialSetup :: TCM ()
    initialSetup = do
          opts <- CommandLineOptions -> TCM CommandLineOptions
    addTrustedExecutables CommandLineOptions
    opts
          setCommandLineOptions opts

        checkFile :: AbsolutePath -> TCM CheckResult
        checkFile :: AbsolutePath -> TCM CheckResult
    checkFile AbsolutePath
    inputFile = do
            -- Andreas, 2013-10-30 The following 'resetState' kills the
            -- verbosity options.  That does not make sense (see fail/Issue641).
            -- 'resetState' here does not seem to serve any purpose,
            -- thus, I am removing it.
            -- resetState
              let mode :: Mode
    mode = if CommandLineOptions -> Bool
    optOnlyScopeChecking CommandLineOptions
    opts
                         then Mode
    Imp.ScopeCheck
                         else Mode
    Imp.TypeCheck

              src <- AbsolutePath -> TCMT IO SourceFile
    forall (m :: * -> *). MonadFileId m => AbsolutePath -> m SourceFile
    srcFromPath AbsolutePath
    inputFile
              result <- Imp.typeCheckMain mode =<< Imp.parseSource src

              unless (crMode result == ModuleScopeChecked) $
                Imp.raiseNonFatalErrors result

              let i = CheckResult -> Interface
    crInterface CheckResult
    result
              reportSDoc "main" 50 $ pretty i

              -- Print accumulated warnings
              unlessNullM (tcWarnings . classifyWarnings . Set.toAscList <$> getAllWarnings AllWarnings) $ \ Set TCWarning
    ws -> do
                let banner :: TCMT IO Doc
    banner = [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [Char]
    delimiter [Char]
    "All done; warnings encountered"
                [Char] -> VerboseLevel -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> TCMT IO Doc -> m ()
    alwaysReportSDoc [Char]
    "warning" VerboseLevel
    1 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                  [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (TCMT IO Doc
    banner TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    :) ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TCWarning -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
    prettyTCM ([TCWarning] -> [TCMT IO Doc]) -> [TCWarning] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ Set TCWarning -> [TCWarning]
    forall a. Set a -> [a]
    Set.toAscList Set TCWarning
    ws

              return result

    -- | Print usage information.
    printUsage :: [Backend] -> Help -> IO ()
    printUsage :: [Backend] -> Help -> IO ()
    printUsage [Backend]
    backends Help
    hp = do
      progName <- IO [Char]
    getProgName
      putStr $ usage standardOptions_ progName hp
      when (hp == GeneralHelp) $ mapM_ (putStr . backendUsage) backends

    backendUsage :: Backend -> String
    backendUsage :: Backend -> [Char]
    backendUsage (Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
    b) =
      [Char] -> [OptDescr ()] -> [Char]
    forall a. [Char] -> [OptDescr a] -> [Char]
    usageInfo ([Char]
    "\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Text -> [Char]
    T.unpack (Backend'_boot Definition (TCMT IO) opts env menv mod def -> Text
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> Text
    backendName Backend'_boot Definition (TCMT IO) opts env menv mod def
    b) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " backend options") ([OptDescr ()] -> [Char]) -> [OptDescr ()] -> [Char]
    forall a b. (a -> b) -> a -> b
    $
        (OptDescr (Flag opts) -> OptDescr ())
    -> [OptDescr (Flag opts)] -> [OptDescr ()]
    forall a b. (a -> b) -> [a] -> [b]
    map OptDescr (Flag opts) -> OptDescr ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (Backend'_boot Definition (TCMT IO) opts env menv mod def
    -> [OptDescr (Flag opts)]
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def
    -> [OptDescr (Flag opts)]
    commandLineFlags Backend'_boot Definition (TCMT IO) opts env menv mod def
    b)

    -- | Print version information.
    printVersion :: [Backend] -> PrintAgdaVersion -> IO ()
    printVersion :: [Backend] -> PrintAgdaVersion -> IO ()
    printVersion [Backend]
    _ PrintAgdaVersion
    PrintAgdaNumericVersion = [Char] -> IO ()
    putStrLn [Char]
    versionWithCommitInfo
    printVersion [Backend]
    backends PrintAgdaVersion
    PrintAgdaVersion = do
      [Char] -> IO ()
    putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Agda version " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    versionWithCommitInfo
      Bool -> IO () -> IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([[Char]] -> Bool
    forall a. Null a => a -> Bool
    null [[Char]]
    flags) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
        ([Char] -> IO ()) -> [[Char]] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [Char] -> IO ()
    putStrLn ([[Char]] -> IO ()) -> [[Char]] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ([Char]
    "Built with flags (cabal -f)" [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :) ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> [Char]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map [Char] -> [Char]
    bullet [[Char]]
    flags
      ([Char] -> IO ()) -> [[Char]] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [Char] -> IO ()
    putStrLn
        [ [Char] -> [Char]
    bullet ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Text -> [Char]
    T.unpack (Text -> [Char]) -> Text -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Text] -> Text
    T.unwords [ Text
    name, Text
    "backend version", Text
    ver ]
        | Backend Backend'{ backendName :: forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> Text
    backendName = Text
    name, backendVersion :: forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> Maybe Text
    backendVersion = Just Text
    ver } <- [Backend]
    backends ]
      where
      bullet :: [Char] -> [Char]
    bullet = ([Char]
    " - " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++)
      -- Print cabal flags that were involved in compilation.
      flags :: [[Char]]
    flags =
    #ifdef COUNT_CLUSTERS
        "enable-cluster-counting: unicode cluster counting in LaTeX backend using the ICU library" :
    #endif
    #ifdef OPTIMISE_HEAVILY
        [Char]
    "optimise-heavily: extra optimisations" [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :
    #endif
    #ifdef DEBUG
        "debug: enable debug printing ('-v' verbosity flags)" :
    #endif
    #ifdef DEBUG_PARSING
        "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'" :
    #endif
    #ifdef DEBUG_SERIALISATION
        "debug-serialisation: extra debug info during serialisation into '.agdai' files" :
    #endif
    #ifdef USE_XDG_DATA_HOME
        concat
          [ "use-xdg-data-home: install and locate data files under $XDG_DATA_HOME/agda/"
          , "$AGDA_VERSION" -- , versionWithCommitInfo
               -- Andreas, 2025-06-28, we could put in the actual version here
               -- but I think the text is clearer in the generic form
          , " by default instead of the location defined by Cabal"
          ]
        :
    #endif
        []

    printAgdaDataDir :: IO ()
    printAgdaDataDir :: IO ()
    printAgdaDataDir = [Char] -> IO ()
    putStrLn ([Char] -> IO ()) -> IO [Char] -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO [Char]
    getDataDir

    printAgdaAppDir :: IO ()
    printAgdaAppDir :: IO ()
    printAgdaAppDir = [Char] -> IO ()
    putStrLn ([Char] -> IO ()) -> IO [Char] -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO [Char]
    getAgdaAppDir

    -- | What to do for bad options.
    optionError :: String -> IO ()
    optionError :: [Char] -> IO ()
    optionError [Char]
    err = do
      prog <- IO [Char]
    getProgName
      putStrLn $ "Error: " ++ err ++ "\nRun '" ++ prog ++ " --help' for help on command line options."
      exitAgdaWith ExitCode.OptionError

    -- | Run a TCM action in IO; catch and pretty print errors.

    -- If some error message cannot be printed due to locale issues, then
    -- one may get the "Error when handling error" error message. There is
    -- currently no test case for this error, but on some systems one can
    -- (at the time of writing) trigger it by running @LC_CTYPE=C agda
    -- --no-libraries Bug.agda@, where @Bug.agda@ contains the following
    -- code (if there is some other file in the same directory, for
    -- instance @Bug.lagda@, then the error message may be different):
    --
    -- @
    -- _ : Set
    -- _ = Set
    -- @

    runTCMPrettyErrors :: TCM () -> IO ()
    runTCMPrettyErrors :: TCM () -> IO ()
    runTCMPrettyErrors TCM ()
    tcm = do
      r <- TCM (Maybe AgdaError) -> IO (Either TCErr (Maybe AgdaError))
    forall a. TCM a -> IO (Either TCErr a)
    runTCMTop
        ( ( (Maybe AgdaError
    forall a. Maybe a
    Nothing Maybe AgdaError -> TCM () -> TCM (Maybe AgdaError)
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCM ()
    tcm)
              TCM (Maybe AgdaError)
    -> (TCErr -> TCM (Maybe AgdaError)) -> TCM (Maybe AgdaError)
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    err -> do
                s2s <- Set TCWarning -> TCM [Doc]
    prettyTCWarnings' (Set TCWarning -> TCM [Doc])
    -> TCMT IO (Set TCWarning) -> TCM [Doc]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCErr -> TCMT IO (Set TCWarning)
    getAllWarningsOfTCErr TCErr
    err
                s1  <- prettyError err
                ANSI.putDoc $ P.vsep $ s2s ++ [ s1 ]
                liftIO $ do
                  helpForLocaleError err
                return (Just TCMError)
          ) TCM (Maybe AgdaError)
    -> (Impossible -> TCM (Maybe AgdaError)) -> TCM (Maybe AgdaError)
    forall a. TCMT IO a -> (Impossible -> TCMT IO a) -> TCMT IO a
    forall (m :: * -> *) a.
    CatchImpossible m =>
    m a -> (Impossible -> m a) -> m a
    `catchImpossible` \Impossible
    e -> do
              Impossible -> TCM ()
    forall {m :: * -> *} {e}. (MonadIO m, Exception e) => e -> m ()
    printException Impossible
    e
              Maybe AgdaError -> TCM (Maybe AgdaError)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AgdaError -> Maybe AgdaError
    forall a. a -> Maybe a
    Just AgdaError
    ImpossibleError)
        ) IO (Either TCErr (Maybe AgdaError))
    -> [Handler (Either TCErr (Maybe AgdaError))]
    -> IO (Either TCErr (Maybe AgdaError))
    forall a. IO a -> [Handler a] -> IO a
    `E.catches`
            -- Catch all exceptions except for those of type ExitCode
            -- (which are thrown by exitWith) and asynchronous exceptions
            -- (which are for instance raised when Ctrl-C is used, or if
            -- the program runs out of heap or stack space).
            [ (ExitCode -> IO (Either TCErr (Maybe AgdaError)))
    -> Handler (Either TCErr (Maybe AgdaError))
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler ((ExitCode -> IO (Either TCErr (Maybe AgdaError)))
     -> Handler (Either TCErr (Maybe AgdaError)))
    -> (ExitCode -> IO (Either TCErr (Maybe AgdaError)))
    -> Handler (Either TCErr (Maybe AgdaError))
    forall a b. (a -> b) -> a -> b
    $ \(ExitCode
    e :: ExitCode)         -> ExitCode -> IO (Either TCErr (Maybe AgdaError))
    forall a e. (HasCallStack, Exception e) => e -> a
    E.throw ExitCode
    e
            , (AsyncException -> IO (Either TCErr (Maybe AgdaError)))
    -> Handler (Either TCErr (Maybe AgdaError))
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler ((AsyncException -> IO (Either TCErr (Maybe AgdaError)))
     -> Handler (Either TCErr (Maybe AgdaError)))
    -> (AsyncException -> IO (Either TCErr (Maybe AgdaError)))
    -> Handler (Either TCErr (Maybe AgdaError))
    forall a b. (a -> b) -> a -> b
    $ \(AsyncException
    e :: E.AsyncException) -> AsyncException -> IO (Either TCErr (Maybe AgdaError))
    forall a e. (HasCallStack, Exception e) => e -> a
    E.throw AsyncException
    e
            , (SomeException -> IO (Either TCErr (Maybe AgdaError)))
    -> Handler (Either TCErr (Maybe AgdaError))
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler ((SomeException -> IO (Either TCErr (Maybe AgdaError)))
     -> Handler (Either TCErr (Maybe AgdaError)))
    -> (SomeException -> IO (Either TCErr (Maybe AgdaError)))
    -> Handler (Either TCErr (Maybe AgdaError))
    forall a b. (a -> b) -> a -> b
    $ \(SomeException
    e :: E.SomeException)  -> do
                SomeException -> IO ()
    forall {m :: * -> *} {e}. (MonadIO m, Exception e) => e -> m ()
    printException SomeException
    e
                Either TCErr (Maybe AgdaError)
    -> IO (Either TCErr (Maybe AgdaError))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either TCErr (Maybe AgdaError)
     -> IO (Either TCErr (Maybe AgdaError)))
    -> Either TCErr (Maybe AgdaError)
    -> IO (Either TCErr (Maybe AgdaError))
    forall a b. (a -> b) -> a -> b
    $ Maybe AgdaError -> Either TCErr (Maybe AgdaError)
    forall a b. b -> Either a b
    Right (AgdaError -> Maybe AgdaError
    forall a. a -> Maybe a
    Just AgdaError
    UnknownError)
            ]
      case r of
        Right Maybe AgdaError
    Nothing       -> IO ()
    forall a. IO a
    exitSuccess
        Right (Just AgdaError
    reason) -> AgdaError -> IO ()
    forall a. AgdaError -> IO a
    exitAgdaWith AgdaError
    reason
        Left TCErr
    err            -> do
          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
    $ do
            [Char] -> IO ()
    putStrLn [Char]
    "\n\nError when handling error:"
            [Char] -> IO ()
    putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ TCErr -> [Char]
    tcErrString TCErr
    err
            TCErr -> IO ()
    helpForLocaleError TCErr
    err
          AgdaError -> IO ()
    forall a. AgdaError -> IO a
    exitAgdaWith AgdaError
    UnknownError
      where
        printException :: e -> m ()
    printException e
    e = IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ()
    putStr ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $
          -- Andreas, 2024-07-03, issue #7299
          -- Regression in base-4.20: printing of exception produces trailing whitespace.
          -- https://gitlab.haskell.org/ghc/ghc/-/issues/25052
    #if MIN_VERSION_base(4,20,0)
          [Char] -> [Char]
    rtrim ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $
    #endif
          e -> [Char]
    forall e. Exception e => e -> [Char]
    E.displayException e
    e

    -- | If the error is an IO error, and the error message suggests that
    -- the problem is related to locales or code pages, print out some
    -- extra information.

    helpForLocaleError :: TCErr -> IO ()
    helpForLocaleError :: TCErr -> IO ()
    helpForLocaleError TCErr
    e = case TCErr
    e of
      (IOException Maybe TCState
    _ Range
    _ IOException
    e)
        | [Char]
    "invalid argument" [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isInfixOf` IOException -> [Char]
    forall a. Show a => a -> [Char]
    show IOException
    e -> IO ()
    msg
      TCErr
    _                                              -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      where
      msg :: IO ()
    msg = [Char] -> IO ()
    putStr ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
        [ [Char]
    ""
        , [Char]
    "This error may be due to the use of a locale or code page that does not"
        , [Char]
    "support some character used in the program being type-checked."
        , [Char]
    ""
        , [Char]
    "If it is, then one option is to use the option --transliterate, in which"
        , [Char]
    "case unsupported characters are (hopefully) replaced with something else,"
        , [Char]
    "perhaps question marks. However, that could make the output harder to"
        , [Char]
    "read."
        , [Char]
    ""
        , [Char]
    "If you want to fix the problem \"properly\", then you could try one of the"
        , [Char]
    "following suggestions:"
        , [Char]
    ""
        , [Char]
    "* If you are using Windows, try switching to a different code page (for"
        , [Char]
    "  instance by running the command 'CHCP 65001')."
        , [Char]
    ""
        , [Char]
    "* If you are using a Unix-like system, try using a different locale. The"
        , [Char]
    "  installed locales are perhaps printed by the command 'locale -a'. If"
        , [Char]
    "  you have a UTF-8 locale installed (for instance sv_SE.UTF-8), then you"
        , [Char]
    "  can perhaps make Agda use this locale by running something like"
        , [Char]
    "  'LC_ALL=sv_SE.UTF-8 agda <...>'."
        ]