module Agda.Main where
import Control.Monad.State
import Control.Applicative
import Data.Maybe
import System.Environment
import System.Exit
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.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.Pretty
import Agda.Compiler.Common (IsMain (..))
import Agda.Compiler.MAlonzo.Compiler as MAlonzo
import Agda.Compiler.Epic.Compiler as Epic
import Agda.Compiler.JS.Compiler as JS
import Agda.Compiler.UHC.Compiler as UHC
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
#include "undefined.h"
runAgda :: TCM ()
runAgda = do
progName <- liftIO getProgName
argv <- liftIO getArgs
opts <- liftIO $ runOptM $ parseStandardOptions argv
case opts of
Left err -> liftIO $ optionError err
Right opts -> runAgdaWithOptions generateHTML progName opts
runAgdaWithOptions
:: TCM ()
-> String
-> CommandLineOptions
-> TCM ()
runAgdaWithOptions generateHTML progName opts
| optShowHelp opts = liftIO printUsage
| optShowVersion opts = liftIO printVersion
| isNothing (optInputFile opts)
&& not (optInteractive opts)
&& not (optGHCiInteraction opts)
= liftIO printUsage
| otherwise = do
UtilsBench.setBenchmarking True
Bench.billTo [] checkFile `finally_` do
Bench.print
printStatistics 20 Nothing =<< use lensAccumStatistics
where
checkFile :: TCM ()
checkFile = do
let i = optInteractive opts
ghci = optGHCiInteraction opts
ghc = optGhcCompile opts
compileNoMain = optCompileNoMain opts
epic = optEpicCompile opts
js = optJSCompile opts
uhc = optUHCCompile opts
when i $ liftIO $ putStr splashScreen
let failIfNoInt (Just i) = return i
failIfNoInt Nothing = __IMPOSSIBLE__
failIfInt Nothing = return ()
failIfInt (Just _) = __IMPOSSIBLE__
interaction :: TCM (Maybe Interface) -> TCM ()
interaction | i = runIM . interactionLoop
| ghci = mimicGHCi . (failIfInt =<<)
| ghc && compileNoMain
= (MAlonzo.compilerMain NotMain =<<) . (failIfNoInt =<<)
| ghc = (MAlonzo.compilerMain IsMain =<<) . (failIfNoInt =<<)
| epic = (Epic.compilerMain =<<) . (failIfNoInt =<<)
| js = (JS.compilerMain =<<) . (failIfNoInt =<<)
| uhc && compileNoMain
= (UHC.compilerMain NotMain =<<) . (failIfNoInt =<<)
| uhc = (UHC.compilerMain IsMain =<<) . (failIfNoInt =<<)
| otherwise = (() <$)
interaction $ do
setCommandLineOptions opts
hasFile <- hasInputFile
if not hasFile then return Nothing else do
file <- getInputFile
(i, mw) <- Imp.typeCheckMain file
result <- case mw of
SomeWarnings ws -> do
ws' <- applyFlagsToTCWarnings RespectFlags ws
case ws' of
[] -> return Nothing
cuws -> tcWarningsToError cuws
NoWarnings -> return $ Just i
reportSDoc "main" 50 $ pretty i
whenM (optGenerateHTML <$> commandLineOptions) $
generateHTML
whenM (isJust . optDependencyGraph <$> commandLineOptions) $
Dot.generateDot $ i
whenM (optGenerateLaTeX <$> commandLineOptions) $
LaTeX.generateLaTeX i
return result
printUsage :: IO ()
printUsage = do
progName <- getProgName
putStr $ usage standardOptions_ progName
printVersion :: IO ()
printVersion = do
putStrLn $ "Agda version " ++ versionWithCommitInfo
optionError :: String -> IO ()
optionError err = do
putStrLn $ "Error: " ++ err ++ "\nRun 'agda --help' for help on command line options."
exitFailure
runTCMPrettyErrors :: TCM () -> IO ()
runTCMPrettyErrors tcm = do
r <- runTCMTop $ tcm `catchError` \err -> do
s <- prettyError err
unless (null s) (liftIO $ putStrLn s)
throwError err
case r of
Right _ -> exitSuccess
Left _ -> exitFailure
`catchImpossible` \e -> do
putStr $ show e
exitFailure
main :: IO ()
main = runTCMPrettyErrors runAgda