module Agda.Main where
import Prelude hiding (null)
import Control.Monad ( void )
import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT )
import Control.Monad.IO.Class ( MonadIO(..) )
import qualified Data.List as List
import Data.Maybe
import System.Environment
import System.Console.GetOpt
import Paths_Agda ( getDataDir )
import Agda.Interaction.CommandLine
import Agda.Interaction.ExitCode (AgdaError(..), exitSuccess, exitAgdaWith)
import Agda.Interaction.Options
import Agda.Interaction.Options.Help (Help (..))
import Agda.Interaction.EmacsTop (mimicGHCi)
import Agda.Interaction.JSONTop (jsonREPL)
import Agda.Interaction.FindFile ( SourceFile(SourceFile) )
import qualified Agda.Interaction.Imports as Imp
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Pretty
import Agda.Compiler.Backend
import Agda.Compiler.Builtin
import Agda.VersionCommit
import Agda.Utils.FileName (absolute, filePath, AbsolutePath)
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.String
import qualified Agda.Utils.Benchmark as UtilsBench
import Agda.Utils.Impossible
runAgda :: [Backend] -> IO ()
runAgda :: [Backend] -> IO ()
runAgda [Backend]
backends = [Backend] -> IO ()
runAgda' forall a b. (a -> b) -> a -> b
$ [Backend]
builtinBackends forall a. [a] -> [a] -> [a]
++ [Backend]
backends
runAgda' :: [Backend] -> IO ()
runAgda' :: [Backend] -> IO ()
runAgda' [Backend]
backends = do
String
progName <- IO String
getProgName
[String]
argv <- IO [String]
getArgs
Either String ([Backend], CommandLineOptions, MainMode)
conf <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
([Backend]
bs, CommandLineOptions
opts) <- forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either String opts)
runOptM forall a b. (a -> b) -> a -> b
$ [Backend]
-> [String]
-> CommandLineOptions
-> OptM ([Backend], CommandLineOptions)
parseBackendOptions [Backend]
backends [String]
argv CommandLineOptions
defaultOptions
Maybe AbsolutePath
inputFile <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> IO AbsolutePath
absolute forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> Maybe String
optInputFile CommandLineOptions
opts
MainMode
mode <- forall (m :: * -> *).
MonadError String m =>
[Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
getMainMode [Backend]
bs Maybe AbsolutePath
inputFile CommandLineOptions
opts
forall (m :: * -> *) a. Monad m => a -> m a
return ([Backend]
bs, CommandLineOptions
opts, MainMode
mode)
case Either String ([Backend], CommandLineOptions, MainMode)
conf of
Left String
err -> String -> IO ()
optionError String
err
Right ([Backend]
bs, CommandLineOptions
opts, MainMode
mode) -> case MainMode
mode of
MainModePrintHelp Help
hp -> [Backend] -> Help -> IO ()
printUsage [Backend]
bs Help
hp
MainMode
MainModePrintVersion -> [Backend] -> IO ()
printVersion [Backend]
bs
MainMode
MainModePrintAgdaDir -> IO ()
printAgdaDir
MainModeRun Interactor ()
interactor -> TCM () -> IO ()
runTCMPrettyErrors forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' [Backend] TCState
stBackends [Backend]
bs
forall a. Interactor a -> String -> CommandLineOptions -> TCM a
runAgdaWithOptions Interactor ()
interactor String
progName CommandLineOptions
opts
data MainMode
= MainModeRun (Interactor ())
| MainModePrintHelp Help
| MainModePrintVersion
| MainModePrintAgdaDir
getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
getMainMode :: forall (m :: * -> *).
MonadError String m =>
[Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
getMainMode [Backend]
configuredBackends Maybe AbsolutePath
maybeInputFile CommandLineOptions
opts
| Just Help
hp <- CommandLineOptions -> Maybe Help
optPrintHelp CommandLineOptions
opts = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Help -> MainMode
MainModePrintHelp Help
hp
| CommandLineOptions -> Bool
optPrintVersion CommandLineOptions
opts = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MainMode
MainModePrintVersion
| CommandLineOptions -> Bool
optPrintAgdaDir CommandLineOptions
opts = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MainMode
MainModePrintAgdaDir
| Bool
otherwise = do
Maybe (Interactor ())
mi <- forall (m :: * -> *).
MonadError String m =>
[Backend]
-> Maybe AbsolutePath
-> CommandLineOptions
-> m (Maybe (Interactor ()))
getInteractor [Backend]
configuredBackends Maybe AbsolutePath
maybeInputFile CommandLineOptions
opts
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Help -> MainMode
MainModePrintHelp Help
GeneralHelp) Interactor () -> MainMode
MainModeRun Maybe (Interactor ())
mi
type Interactor a
= TCM ()
-> (AbsolutePath -> TCM CheckResult)
-> TCM a
data FrontendType
= FrontEndEmacs
| FrontEndJson
| FrontEndRepl
emacsModeInteractor :: Interactor ()
emacsModeInteractor :: Interactor ()
emacsModeInteractor TCM ()
setup AbsolutePath -> TCM CheckResult
_check = TCM () -> TCM ()
mimicGHCi TCM ()
setup
jsonModeInteractor :: Interactor ()
jsonModeInteractor :: Interactor ()
jsonModeInteractor TCM ()
setup AbsolutePath -> TCM CheckResult
_check = TCM () -> TCM ()
jsonREPL TCM ()
setup
replInteractor :: Maybe AbsolutePath -> Interactor ()
replInteractor :: Maybe AbsolutePath -> Interactor ()
replInteractor = Maybe AbsolutePath -> Interactor ()
runInteractionLoop
defaultInteractor :: AbsolutePath -> Interactor ()
defaultInteractor :: AbsolutePath -> Interactor ()
defaultInteractor AbsolutePath
file TCM ()
setup AbsolutePath -> TCM CheckResult
check = do TCM ()
setup; forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TCM CheckResult
check AbsolutePath
file
getInteractor :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m (Maybe (Interactor ()))
getInteractor :: forall (m :: * -> *).
MonadError String m =>
[Backend]
-> Maybe AbsolutePath
-> CommandLineOptions
-> m (Maybe (Interactor ()))
getInteractor [Backend]
configuredBackends Maybe AbsolutePath
maybeInputFile CommandLineOptions
opts =
case (Maybe AbsolutePath
maybeInputFile, [FrontendType]
enabledFrontends, [Backend]
enabledBackends) of
(Just AbsolutePath
inputFile, [], Backend
_:[Backend]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Backend] -> Interactor ()
backendInteraction AbsolutePath
inputFile [Backend]
enabledBackends
(Just AbsolutePath
inputFile, [], []) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ AbsolutePath -> Interactor ()
defaultInteractor AbsolutePath
inputFile
(Maybe AbsolutePath
Nothing, [], []) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
(Maybe AbsolutePath
Nothing, [], Backend
_:[Backend]
_) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"No input file specified for ", String
enabledBackendNames]
(Maybe AbsolutePath
_, FrontendType
_:[FrontendType]
_, Backend
_:[Backend]
_) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Cannot mix ", String
enabledFrontendNames, String
" with ", String
enabledBackendNames]
(Maybe AbsolutePath
_, FrontendType
_:FrontendType
_:[FrontendType]
_, []) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Must not specify multiple ", String
enabledFrontendNames]
(Maybe AbsolutePath
_, [FrontendType
fe], []) | CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts -> forall {m :: * -> *} {a}.
MonadError String m =>
FrontendType -> m a
errorFrontendScopeChecking FrontendType
fe
(Maybe AbsolutePath
_, [FrontendType
FrontEndRepl], []) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Maybe AbsolutePath -> Interactor ()
replInteractor Maybe AbsolutePath
maybeInputFile
(Maybe AbsolutePath
Nothing, [FrontendType
FrontEndEmacs], []) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Interactor ()
emacsModeInteractor
(Maybe AbsolutePath
Nothing, [FrontendType
FrontEndJson], []) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Interactor ()
jsonModeInteractor
(Just AbsolutePath
inputFile, [FrontendType
FrontEndEmacs], []) -> forall {m :: * -> *} {a}.
MonadError String m =>
AbsolutePath -> FrontendType -> m a
errorFrontendFileDisallowed AbsolutePath
inputFile FrontendType
FrontEndEmacs
(Just AbsolutePath
inputFile, [FrontendType
FrontEndJson], []) -> forall {m :: * -> *} {a}.
MonadError String m =>
AbsolutePath -> FrontendType -> m a
errorFrontendFileDisallowed AbsolutePath
inputFile FrontendType
FrontEndJson
where
isBackendEnabled :: Backend -> Bool
isBackendEnabled (Backend Backend' opts env menv mod def
b) = forall opts env menv mod def.
Backend' opts env menv mod def -> opts -> Bool
isEnabled Backend' opts env menv mod def
b (forall opts env menv mod def.
Backend' opts env menv mod def -> opts
options Backend' opts env menv mod def
b)
enabledBackends :: [Backend]
enabledBackends = forall a. (a -> Bool) -> [a] -> [a]
filter Backend -> Bool
isBackendEnabled [Backend]
configuredBackends
enabledFrontends :: [FrontendType]
enabledFrontends = 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 ]
]
pluralize :: String -> [String] -> String
pluralize String
w [] = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(no ", String
w, String
")"]
pluralize String
w [String
x] = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
w, String
" ", String
x]
pluralize String
w [String]
xs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
w, String
"s (", forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " [String]
xs, String
")"]
enabledBackendNames :: String
enabledBackendNames = String -> [String] -> String
pluralize String
"backend" [ forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
b | Backend Backend' opts env menv mod def
b <- [Backend]
enabledBackends ]
enabledFrontendNames :: String
enabledFrontendNames = String -> [String] -> String
pluralize String
"frontend" (FrontendType -> String
frontendFlagName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FrontendType]
enabledFrontends)
frontendFlagName :: FrontendType -> String
frontendFlagName = (String
"--" forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
FrontendType
FrontEndEmacs -> String
"interaction"
FrontendType
FrontEndJson -> String
"interaction-json"
FrontendType
FrontEndRepl -> String
"interactive"
errorFrontendScopeChecking :: FrontendType -> m a
errorFrontendScopeChecking FrontendType
fe = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"The --only-scope-checking flag cannot be combined with ", FrontendType -> String
frontendFlagName FrontendType
fe]
errorFrontendFileDisallowed :: AbsolutePath -> FrontendType -> m a
errorFrontendFileDisallowed AbsolutePath
inputFile FrontendType
fe = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Must not specify an input file (", AbsolutePath -> String
filePath AbsolutePath
inputFile, String
") with ", FrontendType -> String
frontendFlagName FrontendType
fe]
runAgdaWithOptions
:: Interactor a
-> String
-> CommandLineOptions
-> TCM a
runAgdaWithOptions :: forall a. Interactor a -> String -> CommandLineOptions -> TCM a
runAgdaWithOptions Interactor a
interactor String
progName CommandLineOptions
opts = do
forall (m :: * -> *).
MonadBench m =>
BenchmarkOn (BenchPhase m) -> m ()
UtilsBench.setBenchmarking forall a. BenchmarkOn a
UtilsBench.BenchmarkOn
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [] forall a b. (a -> b) -> a -> b
$
Interactor a
interactor TCM ()
initialSetup AbsolutePath -> TCM CheckResult
checkFile
forall a b. TCM a -> TCM b -> TCM a
`finally_` do
forall (tcm :: * -> *). MonadTCM tcm => tcm ()
Bench.print
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Int -> Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics Int
1 forall a. Maybe a
Nothing forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' Statistics TCState
lensAccumStatistics
where
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
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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SourceFile -> TCM Source
Imp.parseSource (AbsolutePath -> SourceFile
SourceFile AbsolutePath
inputFile)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (CheckResult -> ModuleCheckMode
crMode CheckResult
result forall a. Eq a => a -> a -> Bool
== ModuleCheckMode
ModuleScopeChecked) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM (forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings (CheckResult -> [TCWarning]
crWarnings CheckResult
result)) forall a b. (a -> b) -> a -> b
$ \ [TCWarning]
ws ->
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [TCWarning]
ws
let i :: Interface
i = CheckResult -> Interface
crInterface CheckResult
result
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"main" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Interface
i
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings) forall a b. (a -> b) -> a -> b
$ \ [TCWarning]
ws -> do
let banner :: TCMT IO Doc
banner = forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"\n" forall a. [a] -> [a] -> [a]
++ String -> String
delimiter String
"All done; warnings encountered"
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"warning" Int
1 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
"\n" forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
banner forall a. a -> [a] -> [a]
: (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
ws)
forall (m :: * -> *) a. Monad m => a -> m a
return CheckResult
result
printUsage :: [Backend] -> Help -> IO ()
printUsage :: [Backend] -> Help -> IO ()
printUsage [Backend]
backends Help
hp = do
String
progName <- IO String
getProgName
String -> IO ()
putStr forall a b. (a -> b) -> a -> b
$ [OptDescr ()] -> String -> Help -> String
usage [OptDescr ()]
standardOptions_ String
progName Help
hp
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Help
hp forall a. Eq a => a -> a -> Bool
== Help
GeneralHelp) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStr forall b c a. (b -> c) -> (a -> b) -> a -> c
. Backend -> String
backendUsage) [Backend]
backends
backendUsage :: Backend -> String
backendUsage :: Backend -> String
backendUsage (Backend Backend' opts env menv mod def
b) =
forall a. String -> [OptDescr a] -> String
usageInfo (String
"\n" forall a. [a] -> [a] -> [a]
++ forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
b forall a. [a] -> [a] -> [a]
++ String
" backend options") forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Functor f => f a -> f ()
void (forall opts env menv mod def.
Backend' opts env menv mod def -> [OptDescr (Flag opts)]
commandLineFlags Backend' opts env menv mod def
b)
printVersion :: [Backend] -> IO ()
printVersion :: [Backend] -> IO ()
printVersion [Backend]
backends = do
String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Agda version " forall a. [a] -> [a] -> [a]
++ String
versionWithCommitInfo
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn
[ String
" - " forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" backend version " forall a. [a] -> [a] -> [a]
++ String
ver
| Backend Backend'{ backendName :: forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName = String
name, backendVersion :: forall opts env menv mod def.
Backend' opts env menv mod def -> Maybe String
backendVersion = Just String
ver } <- [Backend]
backends ]
printAgdaDir :: IO ()
printAgdaDir :: IO ()
printAgdaDir = String -> IO ()
putStrLn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO String
getDataDir
optionError :: String -> IO ()
optionError :: String -> IO ()
optionError String
err = do
String
prog <- IO String
getProgName
String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Error: " forall a. [a] -> [a] -> [a]
++ String
err forall a. [a] -> [a] -> [a]
++ String
"\nRun '" forall a. [a] -> [a] -> [a]
++ String
prog forall a. [a] -> [a] -> [a]
++ String
" --help' for help on command line options."
AgdaError -> IO ()
exitAgdaWith AgdaError
OptionError
runTCMPrettyErrors :: TCM () -> IO ()
runTCMPrettyErrors :: TCM () -> IO ()
runTCMPrettyErrors TCM ()
tcm = do
Either TCErr ()
r <- forall a. TCM a -> IO (Either TCErr a)
runTCMTop forall a b. (a -> b) -> a -> b
$ TCM ()
tcm forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> do
[String]
s2s <- [TCWarning] -> TCMT IO [String]
prettyTCWarnings' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err
String
s1 <- forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
err
let ss :: [String]
ss = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null) forall a b. (a -> b) -> a -> b
$ [String]
s2s forall a. [a] -> [a] -> [a]
++ [String
s1]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null String
s1) (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
ss)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
case Either TCErr ()
r of
Right ()
_ -> forall a. IO a
exitSuccess
Left TCErr
_ -> AgdaError -> IO ()
exitAgdaWith AgdaError
TCMError
forall (m :: * -> *) a.
CatchImpossible m =>
m a -> (Impossible -> m a) -> m a
`catchImpossible` \Impossible
e -> do
String -> IO ()
putStr forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Impossible
e
AgdaError -> IO ()
exitAgdaWith AgdaError
ImpossibleError