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

    import Prelude hiding (null)

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

    import System.Environment
    import System.Console.GetOpt

    import Paths_Agda            ( getDataDir )

    import Agda.Interaction.CommandLine
    import Agda.Interaction.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 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.VersionCommit

    import Agda.Utils.FileName (absolute, filePath, AbsolutePath)
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.String
    import qualified Agda.Utils.Benchmark as UtilsBench

    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
      String
    progName <- IO String
    getProgName
      [String]
    argv     <- IO [String]
    getArgs
      Either String ([Backend], CommandLineOptions, MainMode)
    conf     <- ExceptT String IO ([Backend], CommandLineOptions, MainMode)
    -> IO (Either String ([Backend], CommandLineOptions, MainMode))
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT String IO ([Backend], CommandLineOptions, MainMode)
     -> IO (Either String ([Backend], CommandLineOptions, MainMode)))
    -> ExceptT String IO ([Backend], CommandLineOptions, MainMode)
    -> IO (Either String ([Backend], CommandLineOptions, MainMode))
    forall a b. (a -> b) -> a -> b
    $ do
        ([Backend]
    bs, CommandLineOptions
    opts) <- IO (Either String ([Backend], CommandLineOptions))
    -> ExceptT String IO ([Backend], CommandLineOptions)
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (IO (Either String ([Backend], CommandLineOptions))
     -> ExceptT String IO ([Backend], CommandLineOptions))
    -> IO (Either String ([Backend], CommandLineOptions))
    -> ExceptT String IO ([Backend], CommandLineOptions)
    forall a b. (a -> b) -> a -> b
    $ OptM ([Backend], CommandLineOptions)
    -> IO (Either String ([Backend], CommandLineOptions))
    forall (m :: * -> *) opts.
    Monad m =>
    OptM opts -> m (Either String opts)
    runOptM (OptM ([Backend], CommandLineOptions)
     -> IO (Either String ([Backend], CommandLineOptions)))
    -> OptM ([Backend], CommandLineOptions)
    -> IO (Either String ([Backend], CommandLineOptions))
    forall a b. (a -> b) -> a -> b
    $ [Backend]
    -> [String]
    -> CommandLineOptions
    -> OptM ([Backend], CommandLineOptions)
    parseBackendOptions [Backend]
    backends [String]
    argv CommandLineOptions
    defaultOptions
        -- The absolute path of the input file, if provided
        Maybe AbsolutePath
    inputFile <- IO (Maybe AbsolutePath) -> ExceptT String IO (Maybe AbsolutePath)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe AbsolutePath) -> ExceptT String IO (Maybe AbsolutePath))
    -> IO (Maybe AbsolutePath)
    -> ExceptT String IO (Maybe AbsolutePath)
    forall a b. (a -> b) -> a -> b
    $ (String -> IO AbsolutePath)
    -> Maybe String -> IO (Maybe AbsolutePath)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM String -> IO AbsolutePath
    absolute (Maybe String -> IO (Maybe AbsolutePath))
    -> Maybe String -> IO (Maybe AbsolutePath)
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions -> Maybe String
    optInputFile CommandLineOptions
    opts
        MainMode
    mode      <- [Backend]
    -> Maybe AbsolutePath
    -> CommandLineOptions
    -> ExceptT String IO MainMode
    forall (m :: * -> *).
    MonadError String m =>
    [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
    getMainMode [Backend]
    bs Maybe AbsolutePath
    inputFile CommandLineOptions
    opts
        ([Backend], CommandLineOptions, MainMode)
    -> ExceptT String IO ([Backend], CommandLineOptions, MainMode)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Backend]
    bs, CommandLineOptions
    opts, MainMode
    mode)

      case Either String ([Backend], CommandLineOptions, MainMode)
    conf of
        Left String
    err -> String -> IO ()
    optionError String
    err
        Right ([Backend]
    bs, CommandLineOptions
    opts, MainMode
    mode) -> case MainMode
    mode of
          MainModePrintHelp Help
    hp   -> [Backend] -> Help -> IO ()
    printUsage [Backend]
    bs Help
    hp
          MainMode
    MainModePrintVersion   -> [Backend] -> IO ()
    printVersion [Backend]
    bs
          MainMode
    MainModePrintAgdaDir   -> IO ()
    printAgdaDir
          MainModeRun Interactor ()
    interactor -> TCM () -> IO ()
    runTCMPrettyErrors (TCM () -> IO ()) -> TCM () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do
            Lens' [Backend] TCState -> [Backend] -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' [Backend] TCState
    stBackends [Backend]
    bs
            Interactor () -> String -> CommandLineOptions -> TCM ()
    forall a. Interactor a -> String -> CommandLineOptions -> TCM a
    runAgdaWithOptions Interactor ()
    interactor String
    progName CommandLineOptions
    opts

    -- | Main execution mode
    data MainMode
      = MainModeRun (Interactor ())
      | MainModePrintHelp Help
      | MainModePrintVersion
      | MainModePrintAgdaDir

    -- | Determine the main execution mode to run, based on the configured backends and command line options.
    -- | This is pure.
    getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
    getMainMode :: forall (m :: * -> *).
    MonadError String m =>
    [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
    getMainMode [Backend]
    configuredBackends Maybe AbsolutePath
    maybeInputFile CommandLineOptions
    opts
      | Just Help
    hp <- CommandLineOptions -> Maybe Help
    optPrintHelp CommandLineOptions
    opts = MainMode -> m MainMode
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MainMode -> m MainMode) -> MainMode -> m MainMode
    forall a b. (a -> b) -> a -> b
    $ Help -> MainMode
    MainModePrintHelp Help
    hp
      | CommandLineOptions -> Bool
    optPrintVersion CommandLineOptions
    opts         = MainMode -> m MainMode
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MainMode -> m MainMode) -> MainMode -> m MainMode
    forall a b. (a -> b) -> a -> b
    $ MainMode
    MainModePrintVersion
      | CommandLineOptions -> Bool
    optPrintAgdaDir CommandLineOptions
    opts         = MainMode -> m MainMode
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MainMode -> m MainMode) -> MainMode -> m MainMode
    forall a b. (a -> b) -> a -> b
    $ MainMode
    MainModePrintAgdaDir
      | Bool
    otherwise                    = do
          Maybe (Interactor ())
    mi <- [Backend]
    -> Maybe AbsolutePath
    -> CommandLineOptions
    -> m (Maybe (Interactor ()))
    forall (m :: * -> *).
    MonadError String m =>
    [Backend]
    -> Maybe AbsolutePath
    -> CommandLineOptions
    -> m (Maybe (Interactor ()))
    getInteractor [Backend]
    configuredBackends Maybe AbsolutePath
    maybeInputFile CommandLineOptions
    opts
          -- If there was no selection whatsoever (e.g. just invoked "agda"), we just show help and exit.
          MainMode -> m MainMode
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MainMode -> m MainMode) -> MainMode -> m MainMode
    forall a b. (a -> b) -> a -> b
    $ MainMode
    -> (Interactor () -> MainMode) -> Maybe (Interactor ()) -> MainMode
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Help -> MainMode
    MainModePrintHelp Help
    GeneralHelp) Interactor () -> MainMode
    MainModeRun Maybe (Interactor ())
    mi

    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

    data FrontendType
      = FrontEndEmacs
      | FrontEndJson
      | FrontEndRepl

    -- Emacs mode. Note that it ignores the "check" action because it calls typeCheck directly.
    emacsModeInteractor :: Interactor ()
    emacsModeInteractor :: Interactor ()
    emacsModeInteractor TCM ()
    setup AbsolutePath -> TCM CheckResult
    _check = TCM () -> TCM ()
    mimicGHCi TCM ()
    setup

    -- JSON mode. Note that it ignores the "check" action because it calls typeCheck directly.
    jsonModeInteractor :: Interactor ()
    jsonModeInteractor :: Interactor ()
    jsonModeInteractor 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 String m =>
    [Backend]
    -> Maybe AbsolutePath
    -> CommandLineOptions
    -> m (Maybe (Interactor ()))
    getInteractor [Backend]
    configuredBackends Maybe AbsolutePath
    maybeInputFile CommandLineOptions
    opts =
      case (Maybe AbsolutePath
    maybeInputFile, [FrontendType]
    enabledFrontends, [Backend]
    enabledBackends) of
        (Just AbsolutePath
    inputFile, [],             Backend
    _:[Backend]
    _) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    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 (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 (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]
    _) -> String -> m (Maybe (Interactor ()))
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> m (Maybe (Interactor ())))
    -> String -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    "No input file specified for ", String
    enabledBackendNames]
        (Maybe AbsolutePath
    _,              FrontendType
    _:[FrontendType]
    _,            Backend
    _:[Backend]
    _) -> String -> m (Maybe (Interactor ()))
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> m (Maybe (Interactor ())))
    -> String -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    "Cannot mix ", String
    enabledFrontendNames, String
    " with ", String
    enabledBackendNames]
        (Maybe AbsolutePath
    _,              FrontendType
    _:FrontendType
    _:[FrontendType]
    _,           []) -> String -> m (Maybe (Interactor ()))
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> m (Maybe (Interactor ())))
    -> String -> m (Maybe (Interactor ()))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    "Must not specify multiple ", String
    enabledFrontendNames]
        (Maybe AbsolutePath
    _,              [FrontendType
    fe],            []) | CommandLineOptions -> Bool
    optOnlyScopeChecking CommandLineOptions
    opts -> FrontendType -> m (Maybe (Interactor ()))
    forall {m :: * -> *} {a}.
    MonadError String m =>
    FrontendType -> m a
    errorFrontendScopeChecking FrontendType
    fe
        (Maybe AbsolutePath
    _,              [FrontendType
    FrontEndRepl],  []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    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
        (Maybe AbsolutePath
    Nothing,        [FrontendType
    FrontEndEmacs], []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    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
    $ Interactor ()
    emacsModeInteractor
        (Maybe AbsolutePath
    Nothing,        [FrontendType
    FrontEndJson],  []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
    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
    $ Interactor ()
    jsonModeInteractor
        (Just AbsolutePath
    inputFile, [FrontendType
    FrontEndEmacs], []) -> AbsolutePath -> FrontendType -> m (Maybe (Interactor ()))
    forall {m :: * -> *} {a}.
    MonadError String m =>
    AbsolutePath -> FrontendType -> m a
    errorFrontendFileDisallowed AbsolutePath
    inputFile FrontendType
    FrontEndEmacs
        (Just AbsolutePath
    inputFile, [FrontendType
    FrontEndJson],  []) -> AbsolutePath -> FrontendType -> m (Maybe (Interactor ()))
    forall {m :: * -> *} {a}.
    MonadError String m =>
    AbsolutePath -> FrontendType -> m a
    errorFrontendFileDisallowed AbsolutePath
    inputFile FrontendType
    FrontEndJson
      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 -> Bool
    isBackendEnabled (Backend Backend' opts env menv mod def
    b) = Backend' opts env menv mod def -> opts -> Bool
    forall opts env menv mod def.
    Backend' opts env menv mod def -> opts -> Bool
    isEnabled Backend' opts env menv mod def
    b (Backend' opts env menv mod def -> opts
    forall opts env menv mod def.
    Backend' opts env menv mod def -> opts
    options Backend' opts env menv mod def
    b)
        enabledBackends :: [Backend]
    enabledBackends = (Backend -> Bool) -> [Backend] -> [Backend]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Backend -> 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 ]
          ]
        -- Constructs messages like "(no backend)", "backend ghc", "backends (ghc, ocaml)"
        pluralize :: String -> [String] -> String
    pluralize String
    w []  = [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    "(no ", String
    w, String
    ")"]
        pluralize String
    w [String
    x] = [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    w, String
    " ", String
    x]
        pluralize String
    w [String]
    xs  = [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    w, String
    "s (", String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    List.intercalate String
    ", " [String]
    xs, String
    ")"]
        enabledBackendNames :: String
    enabledBackendNames  = String -> [String] -> String
    pluralize String
    "backend" [ Backend' opts env menv mod def -> String
    forall opts env menv mod def.
    Backend' opts env menv mod def -> String
    backendName Backend' opts env menv mod def
    b | Backend Backend' opts env menv mod def
    b <- [Backend]
    enabledBackends ]
        enabledFrontendNames :: String
    enabledFrontendNames = String -> [String] -> String
    pluralize String
    "frontend" (FrontendType -> String
    frontendFlagName (FrontendType -> String) -> [FrontendType] -> [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FrontendType]
    enabledFrontends)
        frontendFlagName :: FrontendType -> String
    frontendFlagName = (String
    "--" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> String)
    -> (FrontendType -> String) -> FrontendType -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
          FrontendType
    FrontEndEmacs -> String
    "interaction"
          FrontendType
    FrontEndJson -> String
    "interaction-json"
          FrontendType
    FrontEndRepl -> String
    "interactive"
        errorFrontendScopeChecking :: FrontendType -> m a
    errorFrontendScopeChecking FrontendType
    fe = String -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> m a) -> String -> m a
    forall a b. (a -> b) -> a -> b
    $
          [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    "The --only-scope-checking flag cannot be combined with ", FrontendType -> String
    frontendFlagName FrontendType
    fe]
        errorFrontendFileDisallowed :: AbsolutePath -> FrontendType -> m a
    errorFrontendFileDisallowed AbsolutePath
    inputFile FrontendType
    fe = String -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> m a) -> String -> m a
    forall a b. (a -> b) -> a -> b
    $
          [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    "Must not specify an input file (", AbsolutePath -> String
    filePath AbsolutePath
    inputFile, String
    ") with ", FrontendType -> String
    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 -> String -> CommandLineOptions -> TCM a
    runAgdaWithOptions Interactor a
    interactor String
    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))
    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)) -> TCM a -> TCM a
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [] (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
                Interactor a
    interactor TCM ()
    initialSetup AbsolutePath -> TCM CheckResult
    checkFile
              TCM a -> TCM () -> TCM 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.
                Int -> Maybe TopLevelModuleName -> Statistics -> TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m, HasOptions m) =>
    Int -> Maybe TopLevelModuleName -> Statistics -> m ()
    printStatistics Int
    1 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' Statistics TCState -> TCMT IO Statistics
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' Statistics TCState
    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
          CommandLineOptions
    opts <- CommandLineOptions -> TCM CommandLineOptions
    addTrustedExecutables CommandLineOptions
    opts
          CommandLineOptions -> TCM ()
    setCommandLineOptions CommandLineOptions
    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

              CheckResult
    result <- Mode -> Source -> TCM CheckResult
    Imp.typeCheckMain Mode
    mode (Source -> TCM CheckResult) -> TCMT IO Source -> TCM CheckResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SourceFile -> TCMT IO Source
    Imp.parseSource (AbsolutePath -> SourceFile
    SourceFile AbsolutePath
    inputFile)

              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (CheckResult -> ModuleCheckMode
    crMode CheckResult
    result ModuleCheckMode -> ModuleCheckMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleCheckMode
    ModuleScopeChecked) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                TCMT IO [TCWarning] -> ([TCWarning] -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    m a -> (a -> m ()) -> m ()
    unlessNullM ([TCWarning] -> TCMT IO [TCWarning]
    forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
    applyFlagsToTCWarnings (CheckResult -> [TCWarning]
    crWarnings CheckResult
    result)) (([TCWarning] -> TCM ()) -> TCM ())
    -> ([TCWarning] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ [TCWarning]
    ws ->
                  TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCWarning] -> TypeError
    NonFatalErrors [TCWarning]
    ws

              let i :: Interface
    i = CheckResult -> Interface
    crInterface CheckResult
    result
              String -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "main" Int
    50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Interface -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Interface
    i

              -- Print accumulated warnings
              TCMT IO [TCWarning] -> ([TCWarning] -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    m a -> (a -> m ()) -> m ()
    unlessNullM (WarningsAndNonFatalErrors -> [TCWarning]
    tcWarnings (WarningsAndNonFatalErrors -> [TCWarning])
    -> ([TCWarning] -> WarningsAndNonFatalErrors)
    -> [TCWarning]
    -> [TCWarning]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [TCWarning] -> WarningsAndNonFatalErrors
    classifyWarnings ([TCWarning] -> [TCWarning])
    -> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> WhichWarnings -> TCMT IO [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    WhichWarnings -> m [TCWarning]
    getAllWarnings WhichWarnings
    AllWarnings) (([TCWarning] -> TCM ()) -> TCM ())
    -> ([TCWarning] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ [TCWarning]
    ws -> do
                let banner :: TCMT IO Doc
    banner = String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    delimiter String
    "All done; warnings encountered"
                String -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "warning" Int
    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
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    "\n" ([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]
    : (TCWarning -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [TCWarning]
    ws)

              CheckResult -> TCM CheckResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return CheckResult
    result

    -- | Print usage information.
    printUsage :: [Backend] -> Help -> IO ()
    printUsage :: [Backend] -> Help -> IO ()
    printUsage [Backend]
    backends Help
    hp = do
      String
    progName <- IO String
    getProgName
      String -> IO ()
    putStr (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [OptDescr ()] -> String -> Help -> String
    usage [OptDescr ()]
    standardOptions_ String
    progName Help
    hp
      Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Help
    hp Help -> Help -> Bool
    forall a. Eq a => a -> a -> Bool
    == Help
    GeneralHelp) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ (Backend -> IO ()) -> [Backend] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (String -> IO ()
    putStr (String -> IO ()) -> (Backend -> String) -> Backend -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Backend -> String
    backendUsage) [Backend]
    backends

    backendUsage :: Backend -> String
    backendUsage :: Backend -> String
    backendUsage (Backend Backend' opts env menv mod def
    b) =
      String -> [OptDescr ()] -> String
    forall a. String -> [OptDescr a] -> String
    usageInfo (String
    "\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Backend' opts env menv mod def -> String
    forall opts env menv mod def.
    Backend' opts env menv mod def -> String
    backendName Backend' opts env menv mod def
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " backend options") ([OptDescr ()] -> String) -> [OptDescr ()] -> String
    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' opts env menv mod def -> [OptDescr (Flag opts)]
    forall opts env menv mod def.
    Backend' opts env menv mod def -> [OptDescr (Flag opts)]
    commandLineFlags Backend' opts env menv mod def
    b)

    -- | Print version information.
    printVersion :: [Backend] -> IO ()
    printVersion :: [Backend] -> IO ()
    printVersion [Backend]
    backends = do
      String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Agda version " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    versionWithCommitInfo
      (String -> IO ()) -> [String] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ String -> IO ()
    putStrLn
        [ String
    "  - " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    name String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " backend version " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ver
        | Backend Backend'{ backendName :: forall opts env menv mod def.
    Backend' opts env menv mod def -> String
    backendName = String
    name, backendVersion :: forall opts env menv mod def.
    Backend' opts env menv mod def -> Maybe String
    backendVersion = Just String
    ver } <- [Backend]
    backends ]

    printAgdaDir :: IO ()
    printAgdaDir :: IO ()
    printAgdaDir = String -> IO ()
    putStrLn (String -> IO ()) -> IO String -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO String
    getDataDir

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

    -- | Run a TCM action in IO; catch and pretty print errors.
    runTCMPrettyErrors :: TCM () -> IO ()
    runTCMPrettyErrors :: TCM () -> IO ()
    runTCMPrettyErrors TCM ()
    tcm = do
        Either TCErr ()
    r <- TCM () -> IO (Either TCErr ())
    forall a. TCM a -> IO (Either TCErr a)
    runTCMTop (TCM () -> IO (Either TCErr ())) -> TCM () -> IO (Either TCErr ())
    forall a b. (a -> b) -> a -> b
    $ TCM ()
    tcm TCM () -> (TCErr -> TCM ()) -> TCM ()
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    err -> do
          [String]
    s2s <- [TCWarning] -> TCM [String]
    prettyTCWarnings' ([TCWarning] -> TCM [String])
    -> TCMT IO [TCWarning] -> TCM [String]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCErr -> TCMT IO [TCWarning]
    getAllWarningsOfTCErr TCErr
    err
          String
    s1  <- TCErr -> TCMT IO String
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
    prettyError TCErr
    err
          let ss :: [String]
    ss = (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Bool
    forall a. Null a => a -> Bool
    null) ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ [String]
    s2s [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    s1]
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (String -> Bool
    forall a. Null a => a -> Bool
    null String
    s1) (IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStr (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [String]
    ss)
          TCErr -> TCM ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
        case Either TCErr ()
    r of
          Right ()
    _ -> IO ()
    forall a. IO a
    exitSuccess
          Left TCErr
    _  -> AgdaError -> IO ()
    exitAgdaWith AgdaError
    TCMError
      IO () -> (Impossible -> IO ()) -> IO ()
    forall (m :: * -> *) a.
    CatchImpossible m =>
    m a -> (Impossible -> m a) -> m a
    `catchImpossible` \Impossible
    e -> do
        String -> IO ()
    putStr (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Impossible -> String
    forall a. Show a => a -> String
    show Impossible
    e
        AgdaError -> IO ()
    exitAgdaWith AgdaError
    ImpossibleError