{-# LANGUAGE CPP #-}
module Agda.Main where
import Control.Monad.State
import Data.Maybe
import System.Environment
import System.Exit
import System.Console.GetOpt
import Agda.Syntax.Position (Range)
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Abstract.Name (toTopLevelModuleName)
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.Imports (MaybeWarnings'(..))
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.Common (IsMain (..))
import Agda.Compiler.MAlonzo.Compiler (ghcBackend)
import Agda.Compiler.JS.Compiler (jsBackend)
import Agda.Compiler.Backend
import Agda.Utils.Lens
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
import Agda.Utils.Lens
#include "undefined.h"
builtinBackends :: [Backend]
builtinBackends = [ ghcBackend, jsBackend ]
runAgda :: [Backend] -> IO ()
runAgda backends = runAgda' $ builtinBackends ++ backends
runAgda' :: [Backend] -> IO ()
runAgda' backends = runTCMPrettyErrors $ do
progName <- liftIO getProgName
argv <- liftIO getArgs
opts <- liftIO $ runOptM $ parseBackendOptions backends argv
case opts of
Left err -> liftIO $ optionError err
Right (bs, opts) -> do
stBackends .= bs
let enabled (Backend b) = isEnabled b (options b)
bs' = filter enabled bs
() <$ runAgdaWithOptions backends generateHTML (interaction bs') progName opts
where
interaction bs = backendInteraction bs $ defaultInteraction opts
defaultInteraction :: CommandLineOptions -> TCM (Maybe Interface) -> TCM ()
defaultInteraction opts
| i = runIM . interactionLoop
| ghci = mimicGHCi . (failIfInt =<<)
| otherwise = (() <$)
where
i = optInteractive opts
ghci = optGHCiInteraction opts
failIfInt Nothing = return ()
failIfInt (Just _) = __IMPOSSIBLE__
runAgdaWithOptions
:: [Backend]
-> TCM ()
-> (TCM (Maybe Interface) -> TCM a)
-> String
-> CommandLineOptions
-> TCM (Maybe a)
runAgdaWithOptions backends generateHTML interaction progName opts
| Just hp <- optShowHelp opts = Nothing <$ liftIO (printUsage backends hp)
| optShowVersion opts = Nothing <$ liftIO (printVersion backends)
| isNothing (optInputFile opts)
&& not (optInteractive opts)
&& not (optGHCiInteraction opts)
= Nothing <$ liftIO (printUsage backends GeneralHelp)
| otherwise = do
UtilsBench.setBenchmarking UtilsBench.BenchmarkOn
Bench.billTo [] checkFile `finally_` do
Bench.print
printStatistics 1 Nothing =<< use lensAccumStatistics
where
checkFile = Just <$> do
when (optInteractive opts) $ liftIO $ putStr splashScreen
interaction $ do
setCommandLineOptions opts
hasFile <- hasInputFile
if not hasFile then return Nothing else do
let mode = if optOnlyScopeChecking opts
then Imp.ScopeCheck
else Imp.TypeCheck
file <- getInputFile
(i, mw) <- Imp.typeCheckMain file mode
result <- case (mode, mw) of
(Imp.ScopeCheck, _) -> return Nothing
(_, NoWarnings) -> return $ Just i
(_, SomeWarnings ws) -> do
ws' <- applyFlagsToTCWarnings ws
case ws' of
[] -> return Nothing
cuws -> tcWarningsToError cuws
reportSDoc "main" 50 $ pretty i
whenM (optGenerateHTML <$> commandLineOptions) $
generateHTML
whenM (isJust . optDependencyGraph <$> commandLineOptions) $
Dot.generateDot $ i
whenM (optGenerateLaTeX <$> commandLineOptions) $
LaTeX.generateLaTeX i
ws <- (snd . classifyWarnings) <$> Imp.getAllWarnings AllWarnings
unless (null ws) $ do
let banner = text $ "\n" ++ delimiter "All done; warnings encountered"
reportSDoc "warning" 1 $
vcat $ punctuate (text "\n") $ banner : (prettyTCM <$> ws)
return result
printUsage :: [Backend] -> Help -> IO ()
printUsage backends hp = do
progName <- getProgName
putStr $ usage standardOptions_ progName hp
when (hp == GeneralHelp) $ mapM_ (putStr . backendUsage) backends
backendUsage :: Backend -> String
backendUsage (Backend b) =
usageInfo ("\n" ++ backendName b ++ " backend options") $
map (fmap $ const ()) (commandLineFlags b)
printVersion :: [Backend] -> IO ()
printVersion backends = do
putStrLn $ "Agda version " ++ versionWithCommitInfo
mapM_ putStrLn
[ " - " ++ name ++ " backend version " ++ ver
| Backend Backend'{ backendName = name, backendVersion = Just ver } <- backends ]
optionError :: String -> IO ()
optionError err = do
prog <- getProgName
putStrLn $ "Error: " ++ err ++ "\nRun '" ++ prog ++ " --help' for help on command line options."
exitFailure
runTCMPrettyErrors :: TCM () -> IO ()
runTCMPrettyErrors tcm = do
r <- runTCMTop $ tcm `catchError` \err -> do
s2s <- prettyTCWarnings' =<< Imp.errorWarningsOfTCErr err
s1 <- prettyError err
let ss = filter (not . null) $ s2s ++ [s1]
unless (null s1) (liftIO $ putStr $ unlines ss)
throwError err
case r of
Right _ -> exitSuccess
Left _ -> exitFailure
`catchImpossible` \e -> do
putStr $ show e
exitFailure
main :: IO ()
main = runAgda []