    {-# LANGUAGE CPP #-}

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

    import Control.Monad.State
    import Control.Monad.Error
    import Control.Applicative

    import Data.List
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Maybe

    import System.Environment
    import System.Exit
    import System.FilePath
    import qualified Agda.Utils.IO.Locale as LocIO
    import System.Time

    import Agda.Syntax.Position
    import Agda.Syntax.Parser
    import Agda.Syntax.Concrete.Pretty ()
    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Pretty
    import Agda.Syntax.Translation.ConcreteToAbstract
    import Agda.Syntax.Translation.AbstractToConcrete
    import Agda.Syntax.Translation.InternalToAbstract
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Strict
    import Agda.Syntax.Scope.Base

    import Agda.Interaction.Exceptions
    import Agda.Interaction.CommandLine.CommandLine
    import Agda.Interaction.Options
    import Agda.Interaction.Monad
    import Agda.Interaction.GhciTop ()      -- to make sure it compiles
    import qualified Agda.Interaction.Imports as Imp
    import Agda.Interaction.Highlighting.HTML

    import Agda.TypeChecker
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Errors
    import qualified Agda.TypeChecking.Serialise
    import Agda.TypeChecking.Serialise
    import Agda.TypeChecking.SizedTypes

    import Agda.Compiler.Agate.Main as Agate
    import Agda.Compiler.Alonzo.Main as Alonzo
    import Agda.Compiler.MAlonzo.Compiler as MAlonzo

    import Agda.Termination.TermCheck

    import Agda.Utils.Monad
    import Agda.Utils.FileName
    import Agda.Utils.Pretty

    import Agda.Tests
    import Agda.Version

    #include "undefined.h"
    import Agda.Utils.Impossible

    -- | The main function
    runAgda :: TCM ()
    runAgda = do
      progName <- liftIO getProgName
      argv   <- liftIO getArgs
      let opts = parseStandardOptions progName 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)
                                -> liftIO printUsage
          | otherwise           -> do
              setCommandLineOptions PersistentOptions opts
              checkFile
      where
        checkFile :: TCM ()
        checkFile = do
          i       <- optInteractive    <$> liftTCM commandLineOptions
          compile <- optCompile        <$> liftTCM commandLineOptions
          alonzo  <- optCompileAlonzo  <$> liftTCM commandLineOptions
          malonzo <- optCompileMAlonzo <$> liftTCM commandLineOptions
          when i $ liftIO $ LocIO.putStr splashScreen
          let failIfNoInt (Just i) = return i
              -- The allowed combinations of command-line
              -- options should rule out Nothing here.
              failIfNoInt Nothing  = __IMPOSSIBLE__

              interaction :: TCM (Maybe Interface) -> TCM ()
              interaction | i         = runIM . interactionLoop
                          | compile   = Agate.compilerMain         . (() <$)
                          | alonzo    = Alonzo.compilerMain        . (() <$)
                          | malonzo   = (MAlonzo.compilerMain =<<) . (failIfNoInt =<<)
                          | otherwise = (() <$)
          interaction $ do
            hasFile <- hasInputFile
            resetState
            if not hasFile then return Nothing else do
              file    <- getInputFile
              (i, mw) <- Imp.typeCheck file Imp.CurrentDir Nothing

              unsolvedOK <- optAllowUnsolved <$> commandLineOptions

              result <- case mw of
                Just (Imp.Warnings [] [] []) -> __IMPOSSIBLE__
                Just (Imp.Warnings _ unsolved@(_:_) _)
                  | not unsolvedOK -> typeError $ UnsolvedMetas unsolved
                Just (Imp.Warnings _ _ unsolved@(_:_))
                  | not unsolvedOK -> typeError $ UnsolvedConstraints unsolved
                Just (Imp.Warnings termErrs@(_:_) _ _) ->
                  typeError $ TerminationCheckFailed termErrs
                Just _  -> return Nothing
                Nothing -> return $ Just i

              -- Print stats
              stats <- Map.toList <$> getStatistics
              case stats of
                []      -> return ()
                _       -> liftIO $ do
                  LocIO.putStrLn "Statistics"
                  LocIO.putStrLn "----------"
                  mapM_ (\ (s,n) -> LocIO.putStrLn $ s ++ " : " ++ show n) $
                    sortBy (\x y -> compare (snd x) (snd y)) stats

              whenM (optGenerateHTML <$> commandLineOptions) $ do
                case mw of
                  Nothing -> generateHTML $ iModuleName i
                  Just _  -> reportSLn "" 1
                    "HTML is not generated (unsolved meta-variables)."

              return result

    -- | Print usage information.
    printUsage :: IO ()
    printUsage = do
      progName <- getProgName
      LocIO.putStr $ usage standardOptions_ [] progName

    -- | Print version information.
    printVersion :: IO ()
    printVersion =
      LocIO.putStrLn $ "Agda version " ++ version

    -- | What to do for bad options.
    optionError :: String -> IO ()
    optionError err = do
      LocIO.putStrLn $ "Error: " ++ err
      printUsage
      exitFailure

    -- | Main
    main :: IO ()
    main = do
        r <- runTCM $ runAgda `catchError` \err -> do
          s <- prettyError err
          liftIO $ LocIO.putStrLn s
          throwError err
        case r of
          Right _ -> exitSuccess
          Left _  -> exitFailure
      `catchImpossible` \e -> do
        LocIO.putStr $ show e
        exitFailure