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

import System.Environment
import System.Exit
import System.Console.GetOpt
import qualified System.IO as IO

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

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.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 = TCM () -> IO ()
runTCMPrettyErrors (TCM () -> IO ()) -> TCM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  [Char]
progName <- IO [Char] -> TCMT IO [Char]
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [Char]
getProgName
  [[Char]]
argv     <- IO [[Char]] -> TCMT IO [[Char]]
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [[Char]]
getArgs
  let (Either [Char] ([Backend], CommandLineOptions)
z, OptionWarnings
warns) = OptM ([Backend], CommandLineOptions)
-> (Either [Char] ([Backend], CommandLineOptions), OptionWarnings)
forall opts. OptM opts -> (Either [Char] opts, OptionWarnings)
runOptM (OptM ([Backend], CommandLineOptions)
 -> (Either [Char] ([Backend], CommandLineOptions), OptionWarnings))
-> OptM ([Backend], CommandLineOptions)
-> (Either [Char] ([Backend], CommandLineOptions), OptionWarnings)
forall a b. (a -> b) -> a -> b
$ [Backend]
-> [[Char]]
-> CommandLineOptions
-> OptM ([Backend], CommandLineOptions)
parseBackendOptions [Backend]
backends [[Char]]
argv CommandLineOptions
defaultOptions
  (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
  Either [Char] ([Backend], CommandLineOptions, MainMode)
conf     <- IO (Either [Char] ([Backend], CommandLineOptions, MainMode))
-> TCMT
     IO (Either [Char] ([Backend], CommandLineOptions, MainMode))
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either [Char] ([Backend], CommandLineOptions, MainMode))
 -> TCMT
      IO (Either [Char] ([Backend], CommandLineOptions, MainMode)))
-> IO (Either [Char] ([Backend], CommandLineOptions, MainMode))
-> TCMT
     IO (Either [Char] ([Backend], CommandLineOptions, MainMode))
forall a b. (a -> b) -> a -> b
$ ExceptT [Char] IO ([Backend], CommandLineOptions, MainMode)
-> IO (Either [Char] ([Backend], CommandLineOptions, MainMode))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT [Char] IO ([Backend], CommandLineOptions, MainMode)
 -> IO (Either [Char] ([Backend], CommandLineOptions, MainMode)))
-> ExceptT [Char] IO ([Backend], CommandLineOptions, MainMode)
-> IO (Either [Char] ([Backend], CommandLineOptions, MainMode))
forall a b. (a -> b) -> a -> b
$ do
    ([Backend]
bs, CommandLineOptions
opts) <- IO (Either [Char] ([Backend], CommandLineOptions))
-> ExceptT [Char] IO ([Backend], CommandLineOptions)
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (Either [Char] ([Backend], CommandLineOptions))
 -> ExceptT [Char] IO ([Backend], CommandLineOptions))
-> IO (Either [Char] ([Backend], CommandLineOptions))
-> ExceptT [Char] IO ([Backend], CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ Either [Char] ([Backend], CommandLineOptions)
-> IO (Either [Char] ([Backend], CommandLineOptions))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either [Char] ([Backend], CommandLineOptions)
z
    -- The absolute path of the input file, if provided
    Maybe AbsolutePath
inputFile <- IO (Maybe AbsolutePath) -> ExceptT [Char] IO (Maybe AbsolutePath)
forall a. IO a -> ExceptT [Char] IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe AbsolutePath) -> ExceptT [Char] IO (Maybe AbsolutePath))
-> IO (Maybe AbsolutePath)
-> ExceptT [Char] 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
    MainMode
mode      <- [Backend]
-> Maybe AbsolutePath
-> CommandLineOptions
-> ExceptT [Char] IO MainMode
forall (m :: * -> *).
MonadError [Char] m =>
[Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
getMainMode [Backend]
bs Maybe AbsolutePath
inputFile CommandLineOptions
opts
    ([Backend], CommandLineOptions, MainMode)
-> ExceptT [Char] IO ([Backend], CommandLineOptions, MainMode)
forall a. a -> ExceptT [Char] IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Backend]
bs, CommandLineOptions
opts, MainMode
mode)

  case Either [Char] ([Backend], CommandLineOptions, MainMode)
conf of
    Left [Char]
err -> 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
$ [Char] -> IO ()
optionError [Char]
err
    Right ([Backend]
bs, CommandLineOptions
opts, MainMode
mode) -> do

      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
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.
          TextEncoding
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")
          Handle -> TextEncoding -> IO ()
IO.hSetEncoding Handle
IO.stdout TextEncoding
enc
          Handle -> TextEncoding -> IO ()
IO.hSetEncoding Handle
IO.stderr TextEncoding
enc

      case MainMode
mode of
        MainModePrintHelp Help
hp   -> 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
$ [Backend] -> Help -> IO ()
printUsage [Backend]
bs Help
hp
        MainModePrintVersion PrintAgdaVersion
o -> 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
$ [Backend] -> PrintAgdaVersion -> IO ()
printVersion [Backend]
bs PrintAgdaVersion
o
        MainMode
MainModePrintAgdaDir   -> 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
$ IO ()
printAgdaDir
        MainModeRun Interactor ()
interactor -> do
          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

-- | Main execution mode
data MainMode
  = MainModeRun (Interactor ())
  | MainModePrintHelp Help
  | MainModePrintVersion PrintAgdaVersion
  | 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 [Char] 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 a. a -> m a
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
  | Just PrintAgdaVersion
o  <- CommandLineOptions -> Maybe PrintAgdaVersion
optPrintVersion CommandLineOptions
opts = MainMode -> m MainMode
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MainMode -> m MainMode) -> MainMode -> m MainMode
forall a b. (a -> b) -> a -> b
$ PrintAgdaVersion -> MainMode
MainModePrintVersion PrintAgdaVersion
o
  | CommandLineOptions -> Bool
optPrintAgdaDir CommandLineOptions
opts            = MainMode -> m MainMode
forall a. a -> m a
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 [Char] 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 a. a -> m a
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 [Char] 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 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]
    (Maybe AbsolutePath
_,              FrontendType
_:[FrontendType]
_,            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]
"Cannot mix ", [Char]
enabledFrontendNames, [Char]
" with ", [Char]
enabledBackendNames]
    (Maybe AbsolutePath
_,              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]
    (Maybe AbsolutePath
_,              [FrontendType
fe],            []) | CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts -> FrontendType -> m (Maybe (Interactor ()))
forall {m :: * -> *} {a}.
MonadError [Char] m =>
FrontendType -> m a
errorFrontendScopeChecking FrontendType
fe
    (Maybe AbsolutePath
_,              [FrontendType
FrontEndRepl],  []) -> 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
    (Maybe AbsolutePath
Nothing,        [FrontendType
FrontEndEmacs], []) -> 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
$ Interactor ()
emacsModeInteractor
    (Maybe AbsolutePath
Nothing,        [FrontendType
FrontEndJson],  []) -> 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
$ Interactor ()
jsonModeInteractor
    (Just AbsolutePath
inputFile, [FrontendType
FrontEndEmacs], []) -> AbsolutePath -> FrontendType -> m (Maybe (Interactor ()))
forall {m :: * -> *} {a}.
MonadError [Char] m =>
AbsolutePath -> FrontendType -> m a
errorFrontendFileDisallowed AbsolutePath
inputFile FrontendType
FrontEndEmacs
    (Just AbsolutePath
inputFile, [FrontendType
FrontEndJson],  []) -> AbsolutePath -> FrontendType -> m (Maybe (Interactor ()))
forall {m :: * -> *} {a}.
MonadError [Char] 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 :: [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" [ Backend' opts env menv mod def -> [Char]
forall opts env menv mod def.
Backend' opts env menv mod def -> [Char]
backendName Backend' opts env menv mod def
b | Backend Backend' 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"
    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)) -> 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.
            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
      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
          [Char] -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"main" VerboseLevel
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, MonadTCM 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 = [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 ()
reportSDoc [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
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
forall (m :: * -> *). MonadPretty m => TCWarning -> 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 a. a -> TCMT IO a
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
  [Char]
progName <- IO [Char]
getProgName
  [Char] -> IO ()
putStr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [OptDescr ()] -> [Char] -> Help -> [Char]
usage [OptDescr ()]
standardOptions_ [Char]
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_ ([Char] -> IO ()
putStr ([Char] -> IO ()) -> (Backend -> [Char]) -> Backend -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Backend -> [Char]
backendUsage) [Backend]
backends

backendUsage :: Backend -> String
backendUsage :: Backend -> [Char]
backendUsage (Backend Backend' 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]
++ Backend' opts env menv mod def -> [Char]
forall opts env menv mod def.
Backend' opts env menv mod def -> [Char]
backendName Backend' 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' 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] -> 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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Any] -> Bool
forall a. Null a => a -> Bool
null [Any]
forall a. [a]
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]]
forall a. [a]
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
$ [Char]
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" backend version " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
ver
    | Backend Backend'{ backendName :: forall opts env menv mod def.
Backend' opts env menv mod def -> [Char]
backendName = [Char]
name, backendVersion :: forall opts env menv mod def.
Backend' opts env menv mod def -> Maybe [Char]
backendVersion = Just [Char]
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 :: [a]
flags =
#ifdef COUNT_CLUSTERS
    "enable-cluster-counting: unicode cluster counting in LaTeX backend using the ICU library" :
#endif
#ifdef OPTIMISE_HEAVILY
    "optimise-heavily: extra optimizations" :
#endif
#ifdef DEBUG
    "debug: extra debug info" :
#endif
    []

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

-- | What to do for bad options.
optionError :: String -> IO ()
optionError :: [Char] -> IO ()
optionError [Char]
err = do
  [Char]
prog <- IO [Char]
getProgName
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Error: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
err [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\nRun '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
prog [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" --help' for help on command line options."
  AgdaError -> IO ()
forall a. AgdaError -> IO a
exitAgdaWith AgdaError
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
  Either TCErr (Maybe AgdaError)
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
            [Doc]
s2s <- [TCWarning] -> TCM [Doc]
prettyTCWarnings' ([TCWarning] -> TCM [Doc]) -> TCMT IO [TCWarning] -> TCM [Doc]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err
            Doc
s1  <- TCErr -> TCMT IO Doc
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm Doc
prettyError TCErr
err
            Doc -> TCM ()
forall (m :: * -> *). (MonadIO m, HasOptions m) => Doc -> m ()
ANSI.putDoc ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat [Doc]
s2s Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.$+$ Doc
s1)
            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
              TCErr -> IO ()
helpForLocaleError TCErr
err
            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
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
          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
$ [Char] -> IO ()
putStr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Impossible -> [Char]
forall e. Exception e => e -> [Char]
E.displayException 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. 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. 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
            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
$ [Char] -> IO ()
putStr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ SomeException -> [Char]
forall e. Exception e => e -> [Char]
E.displayException 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 Either TCErr (Maybe AgdaError)
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

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