{-# LANGUAGE CPP #-}

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

import Prelude hiding (null)

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

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

import GHC.Conc (getNumProcessors)

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

import Mikan.Interaction.BuildLibrary (buildLibrary, printAccumulatedWarnings)
import Mikan.Interaction.ExitCode as ExitCode (AgdaError(..), exitSuccess, exitAgdaWith)
import Mikan.Interaction.Highlighting.LaTeX.Backend (latexBackendName)
import Mikan.Interaction.Options
import Mikan.Interaction.Options.BashCompletion (bashComplete, printedOptions)
import Mikan.Interaction.Options.Help (Help (..), helpTopicUsage)
import Mikan.Interaction.EmacsTop (mimicGHCi)
import Mikan.Interaction.JSONTop (jsonREPL)
import Mikan.Interaction.FindFile ( SourceFile(SourceFile) )
import Mikan.Interaction.Imports qualified as Imp

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

import Mikan.Compiler.Backend
import Mikan.Compiler.Builtin

import Mikan.Setup ( getAppDir, getDataDir, setup )
import Mikan.Setup.EmacsMode

import Mikan.Version (version)
import Mikan.VersionCommit ( versionWithCommitInfo )

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

import Mikan.Utils.Impossible
import Mikan.Utils.Function (applyWhen)

-- | The main function
runMikan :: [Backend] -> IO ()
runMikan :: [Backend] -> IO ()
runMikan [Backend]
backends = [Backend] -> IO ()
runMikan' ([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
runMikan' :: [Backend] -> IO ()
runMikan' :: [Backend] -> IO ()
runMikan' [Backend]
backends = do
  IO [[Char]]
getArgs IO [[Char]] -> ([[Char]] -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

    -- Special mode of operation for @--bash-complete@.
    [Char]
"--bash-complete" : [[Char]]
args ->
      case Truncate -> [[Char]] -> Either [Char] [Char]
bashComplete Truncate
trunc [[Char]]
args of
        Right [Char]
s -> [Char] -> IO ()
putStr [Char]
s
        Left [Char]
err -> do
          [Char] -> IO ()
putStrLn [Char]
err
          AgdaError -> IO ()
forall a. AgdaError -> IO a
exitAgdaWith AgdaError
ExitCode.OptionError
      where
        -- Truncate to max 50 completion suggestions.
        trunc :: Truncate
trunc = Int -> Truncate
forall a. a -> Maybe a
Just Int
50

    -- Ordinary entrypoint.
    [[Char]]
args -> [Backend] -> [[Char]] -> IO ()
runAgdaArgs [Backend]
backends [[Char]]
args

runAgdaArgs :: [Backend] -> [String] -> IO ()
runAgdaArgs :: [Backend] -> [[Char]] -> IO ()
runAgdaArgs [Backend]
backends [[Char]]
args = do
  progName <- IO [Char]
getProgName
  let (conf, warns) = runOptM $ parseBackendOptions backends args defaultOptions

  case conf of
    Left [Char]
err -> [Char] -> IO ()
optionError [Char]
err
    Right ([Backend]
bs, CommandLineOptions
opts) -> 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 ()
Mikan.Setup.setup Bool
True

      -- Print information as requested
      Maybe PrintVersion -> (PrintVersion -> IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (CommandLineOptions -> Maybe PrintVersion
optPrintVersion CommandLineOptions
opts) ((PrintVersion -> IO ()) -> IO ())
-> (PrintVersion -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ [Backend] -> PrintVersion -> 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
optPrintAppDir      CommandLineOptions
opts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ IO ()
printAppDir
      Bool -> IO () -> IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (CommandLineOptions -> Bool
optPrintDataDir     CommandLineOptions
opts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ IO ()
printDataDir
      Bool -> IO () -> IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (CommandLineOptions -> Bool
optPrintOptions     CommandLineOptions
opts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ IO ()
printOptions

      -- 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 ()
Mikan.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 ()
Mikan.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 ()
Mikan.Setup.setup Bool
False
        IO ()
printEmacsModeFile

      -- The absolute path of the input file, if provided
      inputFile <- IO (Maybe AbsolutePath) -> IO (Maybe AbsolutePath)
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe AbsolutePath) -> IO (Maybe AbsolutePath))
-> IO (Maybe AbsolutePath) -> IO (Maybe AbsolutePath)
forall a b. (a -> b) -> a -> b
$ ([Char] -> IO AbsolutePath)
-> Maybe [Char] -> IO (Maybe AbsolutePath)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Maybe a -> m (Maybe b)
mapM [Char] -> IO AbsolutePath
absolute (Maybe [Char] -> IO (Maybe AbsolutePath))
-> Maybe [Char] -> IO (Maybe AbsolutePath)
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> Maybe [Char]
optInputFile CommandLineOptions
opts

      (runExceptT $ getInteractor bs inputFile opts) >>= \case
        Left [Char]
err -> [Char] -> IO ()
optionError [Char]
err
        Right 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 PrintVersion) -> Maybe PrintVersion
forall a b. a -> (a -> b) -> b
& CommandLineOptions -> Maybe PrintVersion
optPrintVersion Maybe PrintVersion -> (Maybe PrintVersion -> Bool) -> Bool
forall a b. a -> (a -> b) -> b
& Maybe PrintVersion -> 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
optPrintAppDir
              , CommandLineOptions
opts CommandLineOptions -> (CommandLineOptions -> Bool) -> Bool
forall a b. a -> (a -> b) -> b
& CommandLineOptions -> Bool
optPrintDataDir
              , CommandLineOptions
opts CommandLineOptions -> (CommandLineOptions -> Bool) -> Bool
forall a b. a -> (a -> b) -> b
& CommandLineOptions -> Bool
optPrintOptions
              , 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
              ]
          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."

        Right (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 ()
Mikan.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 :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> 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' SessionState [Backend] -> [Backend] -> TCM ()
forall (m :: * -> *) a.
ModifySession m =>
Lens' SessionState a -> a -> m ()
setSession ([Backend] -> f [Backend]) -> SessionState -> f SessionState
Lens' SessionState [Backend]
lensBackends [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@.
  | FrontEndBuildLibrary
      -- ^ @--build-library@.

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

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

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

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

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 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
        -- --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
          FrontendType -> m ()
noBackends FrontendType
fe  -- Issue #8024: Backends are not supported yet.
          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 front-end 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
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" [ ShortText -> [Char]
TS.unpack (ShortText -> [Char]) -> ShortText -> [Char]
forall a b. (a -> b) -> a -> b
$ Backend'_boot Definition (TCMT IO) opts env menv mod def
-> ShortText
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def -> ShortText
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
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 Mikan 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 =>
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
=<< Getter TCState Statistics -> TCMT IO Statistics
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Statistics -> f Statistics) -> TCState -> f TCState
Lens' TCState Statistics
Getter 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

      -- The GHC runtime has some funky behaviour if we ask it to set
      -- the number of capabilities on startup.
      --
      -- a) The minimum heap size seems to shoot up to approx. the GC
      -- allocation area times the number of processors, which means the
      -- performance regression tests with very low memory usage limit
      -- simply fail to start;
      --
      -- b) Even if we set the number of capabilities back down to 1,
      -- the parallel GC seems to be used unconditionally if we have
      -- more capabilities on startup, which adds a noticeable amount of
      -- overhead.
      liftIO case optParallelChecking opts of
        Parallel Truncate
Nothing  -> Int -> IO ()
setNumCapabilities (Int -> IO ()) -> IO Int -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO Int
getNumProcessors
        Parallel (Just Int
i) -> Int -> IO ()
setNumCapabilities Int
i
        Parallelism
Sequential        -> Int -> IO ()
setNumCapabilities Int
1

    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 (crWarnings result)

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

          printAccumulatedWarnings
          return result


-- | Print usage information.
printUsage :: [Backend] -> Help -> IO ()
printUsage :: [Backend] -> Help -> IO ()
printUsage [Backend]
backends Help
hp = do
  progName <- IO [Char]
getProgName
  putStr $ unlines
    [ "Agda version " ++ version
    , ""
    , "Usage: " ++ progName ++ " [OPTIONS...] [FILE]"
    ]
  case hp of
    Help
GeneralHelp -> do
      [([Char], [OptDescr (Flag CommandLineOptions)])]
-> (([Char], [OptDescr (Flag CommandLineOptions)]) -> IO ())
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [([Char], [OptDescr (Flag CommandLineOptions)])]
optionGroups \ ([Char]
header, [OptDescr (Flag CommandLineOptions)]
opts) -> do
        [Char] -> [OptDescr (Flag CommandLineOptions)] -> IO ()
forall a. [Char] -> [OptDescr a] -> IO ()
usage [Char]
header [OptDescr (Flag CommandLineOptions)]
opts
      [Backend] -> (Backend -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Backend]
backends \ (Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
b) -> do
        let
          opts :: [OptDescr ()]
opts = Bool
-> ([OptDescr ()] -> [OptDescr ()])
-> [OptDescr ()]
-> [OptDescr ()]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Backend'_boot Definition (TCMT IO) opts env menv mod def
-> ShortText
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def -> ShortText
backendName Backend'_boot Definition (TCMT IO) opts env menv mod def
b ShortText -> ShortText -> Bool
forall a. Eq a => a -> a -> Bool
== ShortText
latexBackendName)
            ([OptDescr ()] -> [OptDescr ()] -> [OptDescr ()]
forall a. [a] -> [a] -> [a]
++ (OptDescr (Flag PragmaOptions) -> OptDescr ())
-> [OptDescr (Flag PragmaOptions)] -> [OptDescr ()]
forall a b. (a -> b) -> [a] -> [b]
map OptDescr (Flag PragmaOptions) -> OptDescr ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (([Char], [OptDescr (Flag PragmaOptions)])
-> [OptDescr (Flag PragmaOptions)]
forall a b. (a, b) -> b
snd ([Char], [OptDescr (Flag PragmaOptions)])
latexPragmaOptions))
            ((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))
            -- NB: @map void@ to make the 'OptDescr' types match.
        [Char] -> [OptDescr ()] -> IO ()
forall a. [Char] -> [OptDescr a] -> IO ()
usage (ShortText -> [Char]
TS.unpack (Backend'_boot Definition (TCMT IO) opts env menv mod def
-> ShortText
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def -> ShortText
backendName Backend'_boot Definition (TCMT IO) opts env menv mod def
b) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" backend options") [OptDescr ()]
opts
    HelpFor HelpTopic
topic -> [Char] -> IO ()
putStr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ HelpTopic -> [Char]
helpTopicUsage HelpTopic
topic
  where
    fmt :: [Char] -> [Char]
fmt [Char]
h = [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
h [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
":\n"
    width :: Int
width = Int
40
    usage :: String -> [OptDescr a] -> IO ()
    usage :: forall a. [Char] -> [OptDescr a] -> IO ()
usage [Char]
header [OptDescr a]
opts = [Char] -> IO ()
putStr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> [Char] -> [OptDescr a] -> [Char]
forall a. Int -> [Char] -> [OptDescr a] -> [Char]
usageInfo Int
width ([Char] -> [Char]
fmt [Char]
header) [OptDescr a]
opts

-- | Print version information.
printVersion :: [Backend] -> PrintVersion -> IO ()
printVersion :: [Backend] -> PrintVersion -> IO ()
printVersion [Backend]
_ PrintVersion
PrintNumericVersion = [Char] -> IO ()
putStrLn [Char]
versionWithCommitInfo
printVersion [Backend]
backends PrintVersion
PrintVersion = 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
$ ShortText -> [Char]
TS.unpack (ShortText -> [Char]) -> ShortText -> [Char]
forall a b. (a -> b) -> a -> b
$ [ShortText] -> ShortText
TS.unwords [ ShortText
name, ShortText
"backend version", Text -> ShortText
TS.fromText Text
ver ]
    | Backend Backend'{ backendName :: forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def -> ShortText
backendName = ShortText
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
    [Char]
"enable-cluster-counting: unicode cluster counting in LaTeX backend using the ICU library" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
#endif
#ifdef OPTIMISE_HEAVILY
    [Char]
"optimise-heavily: extra optimisations" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
#endif
#ifdef DEBUG
    [Char]
"debug: enable debug printing ('-v' verbosity flags)" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
#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
    []

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

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

printOptions :: IO ()
printOptions :: IO ()
printOptions = ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn [[Char]]
printedOptions

-- | 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):
--
-- @
-- _ : Type
-- _ = Type
-- @

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.putDocLn $ 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 <...>'."
    ]