{-# LANGUAGE CPP #-}

{-| 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.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 ]

-- | The main function
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__


-- | 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 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
          -- Main function.
          -- Bill everything to root of Benchmark trie.
          UtilsBench.setBenchmarking 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

          Bench.billTo [] checkFile `finally_` do

            -- Print benchmarks.
            Bench.print

            -- Print accumulated statistics.
            printStatistics 1 Nothing =<< use lensAccumStatistics
  where
    checkFile = Just <$> do
      when (optInteractive opts) $ liftIO $ putStr splashScreen
      interaction $ do
        setCommandLineOptions opts
        hasFile <- 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 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

          -- An interface is only generated if the mode is
          -- Imp.TypeCheck and there are no warnings.
          result <- case (mode, mw) of
            (Imp.ScopeCheck, _)  -> return Nothing
            (_, NoWarnings)      -> return $ Just i
            (_, SomeWarnings ws) -> do
              ws' <- applyFlagsToTCWarnings RespectFlags 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

          -- Print accumulated warnings
          ws <- (snd . classifyWarnings) <$> Imp.getAllWarnings' AllWarnings RespectFlags
          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



-- | Print usage information.
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)

-- | Print version information.
printVersion :: [Backend] -> IO ()
printVersion backends = do
  putStrLn $ "Agda version " ++ versionWithCommitInfo
  mapM_ putStrLn
    [ "  - " ++ name ++ " backend version " ++ ver
    | Backend Backend'{ backendName = name, backendVersion = Just ver } <- backends ]

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

-- | Run a TCM action in IO; catch and pretty print errors.
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
main :: IO ()
main = runAgda []