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

import Control.Monad.State

import Data.Maybe

import System.Environment
import System.Exit
import System.Console.GetOpt

import Agda.Interaction.CommandLine
import Agda.Interaction.Options
import Agda.Interaction.Options.Help (Help (..))
import Agda.Interaction.Monad
import Agda.Interaction.EmacsTop (mimicGHCi)
import Agda.Interaction.JSONTop (jsonREPL)
import Agda.Interaction.Imports (MaybeWarnings'(..))
import Agda.Interaction.FindFile ( SourceFile(SourceFile) )
import qualified Agda.Interaction.Imports as Imp
import qualified Agda.Interaction.Highlighting.Dot as Dot
import qualified Agda.Interaction.Highlighting.LaTeX as LaTeX
import Agda.Interaction.Highlighting.HTML

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.MAlonzo.Compiler (ghcBackend)
import Agda.Compiler.JS.Compiler (jsBackend)

import Agda.Compiler.Backend

import Agda.Utils.Monad
import Agda.Utils.String

import Agda.VersionCommit

import qualified Agda.Utils.Benchmark as UtilsBench
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Impossible

builtinBackends :: [Backend]
builtinBackends :: [Backend]
builtinBackends = [ Backend
ghcBackend, Backend
jsBackend ]

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

runAgda' :: [Backend] -> IO ()
runAgda' :: [Backend] -> IO ()
runAgda' [Backend]
backends = TCM () -> IO ()
runTCMPrettyErrors (TCM () -> IO ()) -> TCM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  String
progName <- IO String -> TCMT IO String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
getProgName
  [String]
argv     <- IO [String] -> TCMT IO [String]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [String]
getArgs
  Either String ([Backend], CommandLineOptions)
opts     <- IO (Either String ([Backend], CommandLineOptions))
-> TCMT IO (Either String ([Backend], CommandLineOptions))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String ([Backend], CommandLineOptions))
 -> TCMT IO (Either String ([Backend], CommandLineOptions)))
-> IO (Either String ([Backend], CommandLineOptions))
-> TCMT IO (Either String ([Backend], CommandLineOptions))
forall a b. (a -> b) -> a -> b
$ OptM ([Backend], CommandLineOptions)
-> IO (Either String ([Backend], CommandLineOptions))
forall a. OptM a -> IO (Either String a)
runOptM (OptM ([Backend], CommandLineOptions)
 -> IO (Either String ([Backend], CommandLineOptions)))
-> OptM ([Backend], CommandLineOptions)
-> IO (Either String ([Backend], CommandLineOptions))
forall a b. (a -> b) -> a -> b
$ [Backend]
-> [String]
-> CommandLineOptions
-> OptM ([Backend], CommandLineOptions)
parseBackendOptions [Backend]
backends [String]
argv CommandLineOptions
defaultOptions
  case Either String ([Backend], CommandLineOptions)
opts of
    Left  String
err        -> IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
optionError String
err
    Right ([Backend]
bs, CommandLineOptions
opts) -> do
      Lens' [Backend] TCState -> [Backend] -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' [Backend] TCState
stBackends [Backend]
bs
      let enabled :: Backend -> Bool
enabled (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)
          bs' :: [Backend]
bs' = (Backend -> Bool) -> [Backend] -> [Backend]
forall a. (a -> Bool) -> [a] -> [a]
filter Backend -> Bool
enabled [Backend]
bs
      () () -> TCMT IO (Maybe ()) -> TCM ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Backend]
-> TCM ()
-> (TCM (Maybe Interface) -> TCM ())
-> String
-> CommandLineOptions
-> TCMT IO (Maybe ())
forall a.
[Backend]
-> TCM ()
-> (TCM (Maybe Interface) -> TCM a)
-> String
-> CommandLineOptions
-> TCM (Maybe a)
runAgdaWithOptions [Backend]
backends TCM ()
generateHTML ([Backend] -> TCM (Maybe Interface) -> TCM ()
interaction [Backend]
bs') String
progName CommandLineOptions
opts
      where
        interaction :: [Backend] -> TCM (Maybe Interface) -> TCM ()
interaction [Backend]
bs = [Backend]
-> (TCM (Maybe Interface) -> TCM ())
-> TCM (Maybe Interface)
-> TCM ()
backendInteraction [Backend]
bs ((TCM (Maybe Interface) -> TCM ())
 -> TCM (Maybe Interface) -> TCM ())
-> (TCM (Maybe Interface) -> TCM ())
-> TCM (Maybe Interface)
-> TCM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCM (Maybe Interface) -> TCM ()
defaultInteraction CommandLineOptions
opts

defaultInteraction :: CommandLineOptions -> TCM (Maybe Interface) -> TCM ()
defaultInteraction :: CommandLineOptions -> TCM (Maybe Interface) -> TCM ()
defaultInteraction CommandLineOptions
opts
  | Bool
i         = IM () -> TCM ()
forall a. IM a -> TCM a
runIM (IM () -> TCM ())
-> (TCM (Maybe Interface) -> IM ())
-> TCM (Maybe Interface)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM (Maybe Interface) -> IM ()
interactionLoop
  | Bool
ghci      = TCM () -> TCM ()
mimicGHCi (TCM () -> TCM ())
-> (TCM (Maybe Interface) -> TCM ())
-> TCM (Maybe Interface)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Interface -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> m ()
failIfInt (Maybe Interface -> TCM ()) -> TCM (Maybe Interface) -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<)
  | Bool
json      = TCM () -> TCM ()
jsonREPL (TCM () -> TCM ())
-> (TCM (Maybe Interface) -> TCM ())
-> TCM (Maybe Interface)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Interface -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> m ()
failIfInt (Maybe Interface -> TCM ()) -> TCM (Maybe Interface) -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<)
  | Bool
otherwise = (() () -> TCM (Maybe Interface) -> TCM ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$)
  where
    i :: Bool
i    = CommandLineOptions -> Bool
optInteractive     CommandLineOptions
opts
    ghci :: Bool
ghci = CommandLineOptions -> Bool
optGHCiInteraction CommandLineOptions
opts
    json :: Bool
json = CommandLineOptions -> Bool
optJSONInteraction CommandLineOptions
opts

    failIfInt :: Maybe a -> m ()
failIfInt Maybe a
Nothing  = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    failIfInt (Just a
_) = m ()
forall a. HasCallStack => a
__IMPOSSIBLE__


-- | Run Agda with parsed command line options and with a custom HTML generator
runAgdaWithOptions
  :: [Backend]          -- ^ Backends only for printing usage and version information
  -> TCM ()             -- ^ HTML generating action
  -> (TCM (Maybe Interface) -> TCM a) -- ^ Backend interaction
  -> String             -- ^ program name
  -> CommandLineOptions -- ^ parsed command line options
  -> TCM (Maybe a)
runAgdaWithOptions :: [Backend]
-> TCM ()
-> (TCM (Maybe Interface) -> TCM a)
-> String
-> CommandLineOptions
-> TCM (Maybe a)
runAgdaWithOptions [Backend]
backends TCM ()
generateHTML TCM (Maybe Interface) -> TCM a
interaction String
progName CommandLineOptions
opts
      | Just Help
hp <- CommandLineOptions -> Maybe Help
optShowHelp CommandLineOptions
opts = Maybe a
forall a. Maybe a
Nothing Maybe a -> TCM () -> TCM (Maybe a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ([Backend] -> Help -> IO ()
printUsage [Backend]
backends Help
hp)
      | CommandLineOptions -> Bool
optShowVersion CommandLineOptions
opts         = Maybe a
forall a. Maybe a
Nothing Maybe a -> TCM () -> TCM (Maybe a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ([Backend] -> IO ()
printVersion [Backend]
backends)
      | Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (CommandLineOptions -> Maybe String
optInputFile CommandLineOptions
opts)
          Bool -> Bool -> Bool
&& Bool -> Bool
not (CommandLineOptions -> Bool
optInteractive CommandLineOptions
opts)
          Bool -> Bool -> Bool
&& Bool -> Bool
not (CommandLineOptions -> Bool
optGHCiInteraction CommandLineOptions
opts)
          Bool -> Bool -> Bool
&& Bool -> Bool
not (CommandLineOptions -> Bool
optJSONInteraction CommandLineOptions
opts)
                            = Maybe a
forall a. Maybe a
Nothing Maybe a -> TCM () -> TCM (Maybe a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ([Backend] -> Help -> IO ()
printUsage [Backend]
backends Help
GeneralHelp)
      | Bool
otherwise           = do
          -- Main function.
          -- Bill everything to root of Benchmark trie.
          BenchmarkOn Phase -> TCM ()
forall a (m :: * -> *). MonadBench a m => BenchmarkOn a -> m ()
UtilsBench.setBenchmarking 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 Phase -> TCM (Maybe a) -> TCM (Maybe a)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [] TCM (Maybe a)
checkFile TCM (Maybe a) -> TCM () -> TCM (Maybe a)
forall a b. TCM a -> TCM b -> TCM a
`finally_` do

            -- Print benchmarks.
            TCM ()
forall (tcm :: * -> *). MonadTCM tcm => tcm ()
Bench.print

            -- Print accumulated statistics.
            Int -> Maybe TopLevelModuleName -> Statistics -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Int -> Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics Int
1 Maybe TopLevelModuleName
forall a. Maybe a
Nothing (Statistics -> TCM ()) -> TCMT IO Statistics -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Lens' Statistics TCState -> TCMT IO Statistics
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' Statistics TCState
lensAccumStatistics
  where
    checkFile :: TCM (Maybe a)
checkFile = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> TCM a -> TCM (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CommandLineOptions -> Bool
optInteractive CommandLineOptions
opts) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr String
splashScreen
      TCM (Maybe Interface) -> TCM a
interaction (TCM (Maybe Interface) -> TCM a) -> TCM (Maybe Interface) -> TCM a
forall a b. (a -> b) -> a -> b
$ do
        CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts
        Bool
hasFile <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasInputFile
        -- 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
        if Bool -> Bool
not Bool
hasFile then Maybe Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Interface
forall a. Maybe a
Nothing else do
          let mode :: Mode
mode = if CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts
                     then Mode
Imp.ScopeCheck
                     else Mode
Imp.TypeCheck

          SourceFile
file    <- AbsolutePath -> SourceFile
SourceFile (AbsolutePath -> SourceFile)
-> TCMT IO AbsolutePath -> TCMT IO SourceFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO AbsolutePath
getInputFile
          (Interface
i, MaybeWarnings
mw) <- SourceFile -> Mode -> SourceInfo -> TCM (Interface, MaybeWarnings)
Imp.typeCheckMain SourceFile
file Mode
mode (SourceInfo -> TCM (Interface, MaybeWarnings))
-> TCMT IO SourceInfo -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SourceFile -> TCMT IO SourceInfo
Imp.sourceInfo SourceFile
file

          -- An interface is only generated if the mode is
          -- Imp.TypeCheck and there are no warnings.
          Maybe Interface
result <- case (Mode
mode, MaybeWarnings
mw) of
            (Mode
Imp.ScopeCheck, MaybeWarnings
_)  -> Maybe Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Interface
forall a. Maybe a
Nothing
            (Mode
_, MaybeWarnings
NoWarnings)      -> Maybe Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Interface -> TCM (Maybe Interface))
-> Maybe Interface -> TCM (Maybe Interface)
forall a b. (a -> b) -> a -> b
$ Interface -> Maybe Interface
forall a. a -> Maybe a
Just Interface
i
            (Mode
_, SomeWarnings [TCWarning]
ws) -> do
              [TCWarning]
ws' <- [TCWarning] -> TCM [TCWarning]
applyFlagsToTCWarnings [TCWarning]
ws
              case [TCWarning]
ws' of
                []   -> Maybe Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Interface
forall a. Maybe a
Nothing
                [TCWarning]
cuws -> [TCWarning] -> TCM (Maybe Interface)
forall a. [TCWarning] -> TCM a
tcWarningsToError [TCWarning]
cuws

          String -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"main" Int
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Interface -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Interface
i

          TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (CommandLineOptions -> Bool
optGenerateHTML (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TCM ()
generateHTML

          TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool)
-> (CommandLineOptions -> Maybe String)
-> CommandLineOptions
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> Maybe String
optDependencyGraph (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            Interface -> TCM ()
Dot.generateDot (Interface -> TCM ()) -> Interface -> TCM ()
forall a b. (a -> b) -> a -> b
$ Interface
i

          TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (CommandLineOptions -> Bool
optGenerateLaTeX (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            Interface -> TCM ()
LaTeX.generateLaTeX Interface
i

          -- Print accumulated warnings
          [TCWarning]
ws <- WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings (WarningsAndNonFatalErrors -> [TCWarning])
-> ([TCWarning] -> WarningsAndNonFatalErrors)
-> [TCWarning]
-> [TCWarning]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings ([TCWarning] -> [TCWarning]) -> TCM [TCWarning] -> TCM [TCWarning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WhichWarnings -> TCM [TCWarning]
Imp.getAllWarnings WhichWarnings
AllWarnings
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TCWarning]
ws) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
            let banner :: TCM Doc
banner = String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
delimiter String
"All done; warnings encountered"
            String -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"warning" Int
1 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
              [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> [m Doc]
punctuate TCM Doc
"\n" ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ TCM Doc
banner TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
: (TCWarning -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (TCWarning -> TCM Doc) -> [TCWarning] -> [TCM Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
ws)

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



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

backendUsage :: Backend -> String
backendUsage :: Backend -> String
backendUsage (Backend Backend' opts env menv mod def
b) =
  String -> [OptDescr ()] -> String
forall a. String -> [OptDescr a] -> String
usageInfo (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Backend' opts env menv mod def -> String
forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" backend options") ([OptDescr ()] -> String) -> [OptDescr ()] -> String
forall a b. (a -> b) -> a -> b
$
    (OptDescr (Flag opts) -> OptDescr ())
-> [OptDescr (Flag opts)] -> [OptDescr ()]
forall a b. (a -> b) -> [a] -> [b]
map ((Flag opts -> ()) -> OptDescr (Flag opts) -> OptDescr ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Flag opts -> ()) -> OptDescr (Flag opts) -> OptDescr ())
-> (Flag opts -> ()) -> OptDescr (Flag opts) -> OptDescr ()
forall a b. (a -> b) -> a -> b
$ () -> Flag opts -> ()
forall a b. a -> b -> a
const ()) (Backend' opts env menv mod def -> [OptDescr (Flag opts)]
forall opts env menv mod def.
Backend' opts env menv mod def -> [OptDescr (Flag opts)]
commandLineFlags Backend' opts env menv mod def
b)

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

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

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

-- | Main
main :: IO ()
main :: IO ()
main = [Backend] -> IO ()
runAgda []