module Agda.Main where
import Control.Monad.State
import Control.Monad.Error
import Control.Applicative
import qualified Data.List as List
import Data.Maybe
import System.Environment
import System.Exit
import qualified Text.PrettyPrint.Boxes as Boxes
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Abstract.Name (toTopLevelModuleName)
import Agda.Interaction.CommandLine.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 Agda.TypeChecking.Monad.Benchmark
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Errors
import Agda.Compiler.MAlonzo.Compiler as MAlonzo
import Agda.Compiler.Epic.Compiler as Epic
import Agda.Compiler.JS.Compiler as JS
import Agda.Utils.Monad
import qualified Agda.Utils.Trie as Trie
import Agda.Tests
import Agda.Version
#include "undefined.h"
import Agda.Utils.Impossible
runAgda :: TCM ()
runAgda = do
progName <- liftIO getProgName
argv <- liftIO getArgs
let opts = parseStandardOptions argv
case opts of
Left err -> liftIO $ optionError err
Right opts
| optShowHelp opts -> liftIO printUsage
| optShowVersion opts -> liftIO printVersion
| optRunTests opts -> liftIO $ do
ok <- testSuite
unless ok exitFailure
| isNothing (optInputFile opts)
&& not (optInteractive opts)
&& not (optGHCiInteraction opts)
-> liftIO printUsage
| otherwise -> do
setCommandLineOptions opts
billTo [] $ checkFile
whenM benchmarking $ do
(accounts, times) <- List.unzip . Trie.toList <$> getBenchmark
let showAccount [] = "Total time"
showAccount ks = List.concat . List.intersperse "." . map show $ ks
col1 = Boxes.vcat Boxes.left $
map (Boxes.text . showAccount) $
accounts
col2 = Boxes.vcat Boxes.right $
map (Boxes.text . (++ " ms") . show . (`div` 1000000000)) $
times
table = Boxes.hsep 1 Boxes.left [col1, col2]
reportBenchmarkingLn $ Boxes.render table
where
checkFile :: TCM ()
checkFile = do
i <- optInteractive <$> liftTCM commandLineOptions
ghci <- optGHCiInteraction <$> liftTCM commandLineOptions
compile <- optCompile <$> liftTCM commandLineOptions
compileNoMain <- optCompileNoMain <$> liftTCM commandLineOptions
epic <- optEpicCompile <$> liftTCM commandLineOptions
js <- optJSCompile <$> liftTCM commandLineOptions
when i $ liftIO $ putStr splashScreen
let failIfNoInt (Just i) = return i
failIfNoInt Nothing = __IMPOSSIBLE__
failIfInt x Nothing = x
failIfInt _ (Just _) = __IMPOSSIBLE__
interaction :: TCM (Maybe Interface) -> TCM ()
interaction | i = runIM . interactionLoop
| ghci = (failIfInt mimicGHCi =<<)
| compile && compileNoMain
= (MAlonzo.compilerMain False =<<) . (failIfNoInt =<<)
| compile = (MAlonzo.compilerMain True =<<) . (failIfNoInt =<<)
| epic = (Epic.compilerMain =<<) . (failIfNoInt =<<)
| js = (JS.compilerMain =<<) . (failIfNoInt =<<)
| otherwise = (() <$)
interaction $ do
hasFile <- hasInputFile
if not hasFile then return Nothing else do
file <- getInputFile
(i, mw) <- Imp.typeCheckMain file
unsolvedOK <- optAllowUnsolved <$> pragmaOptions
result <- case mw of
SomeWarnings (Warnings [] [] []) -> return Nothing
SomeWarnings (Warnings _ unsolved@(_:_) _)
| not unsolvedOK -> typeError $ UnsolvedMetas unsolved
SomeWarnings (Warnings _ _ unsolved@(_:_))
| not unsolvedOK -> typeError $ UnsolvedConstraints unsolved
SomeWarnings (Warnings termErrs@(_:_) _ _) ->
typeError $ TerminationCheckFailed termErrs
SomeWarnings _ -> return Nothing
NoWarnings -> return $ Just i
whenM (optGenerateHTML <$> commandLineOptions) $
generateHTML
whenM (isJust . optDependencyGraph <$> commandLineOptions) $
Dot.generateDot $ i
whenM (optGenerateLaTeX <$> commandLineOptions) $
LaTeX.generateLaTeX (toTopLevelModuleName $ iModuleName i) (iHighlighting i)
return result
printUsage :: IO ()
printUsage = do
progName <- getProgName
putStr $ usage standardOptions_ [] progName
printVersion :: IO ()
printVersion =
putStrLn $ "Agda version " ++ version
optionError :: String -> IO ()
optionError err = do
putStrLn $ "Error: " ++ err
printUsage
exitFailure
main :: IO ()
main = do
r <- runTCMTop $ runAgda `catchError` \err -> do
s <- prettyError err
liftIO $ putStrLn s
throwError err
case r of
Right _ -> exitSuccess
Left _ -> exitFailure
`catchImpossible` \e -> do
putStr $ show e
exitFailure