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

import Prelude hiding (null)

import Control.Monad          ( void )
import Control.Monad.Except   ( MonadError(..), ExceptT(..), runExceptT )
import Control.Monad.IO.Class ( MonadIO(..) )

import qualified Data.List as List
import Data.Maybe

import System.Environment
import System.Console.GetOpt

import Paths_Agda            ( getDataDir )

import Agda.Interaction.CommandLine
import Agda.Interaction.ExitCode (AgdaError(..), exitSuccess, exitAgdaWith)
import Agda.Interaction.Options
import Agda.Interaction.Options.Help (Help (..))
import Agda.Interaction.EmacsTop (mimicGHCi)
import Agda.Interaction.JSONTop (jsonREPL)
import Agda.Interaction.FindFile ( SourceFile(SourceFile) )
import qualified Agda.Interaction.Imports as Imp

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.Backend
import Agda.Compiler.Builtin

import Agda.VersionCommit

import Agda.Utils.FileName (absolute, filePath, AbsolutePath)
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.String
import qualified Agda.Utils.Benchmark as UtilsBench

import Agda.Utils.Impossible

-- | The main function
runAgda :: [Backend] -> IO ()
runAgda :: [Backend] -> IO ()
runAgda [Backend]
backends = [Backend] -> IO ()
runAgda' ([Backend] -> IO ()) -> [Backend] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Backend]
builtinBackends [Backend] -> [Backend] -> [Backend]
forall a. [a] -> [a] -> [a]
++ [Backend]
backends

-- | The main function without importing built-in backends
runAgda' :: [Backend] -> IO ()
runAgda' :: [Backend] -> IO ()
runAgda' [Backend]
backends = do
  String
progName <- IO String
getProgName
  [String]
argv     <- IO [String]
getArgs
  Either String ([Backend], CommandLineOptions, MainMode)
conf     <- ExceptT String IO ([Backend], CommandLineOptions, MainMode)
-> IO (Either String ([Backend], CommandLineOptions, MainMode))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String IO ([Backend], CommandLineOptions, MainMode)
 -> IO (Either String ([Backend], CommandLineOptions, MainMode)))
-> ExceptT String IO ([Backend], CommandLineOptions, MainMode)
-> IO (Either String ([Backend], CommandLineOptions, MainMode))
forall a b. (a -> b) -> a -> b
$ do
    ([Backend]
bs, CommandLineOptions
opts) <- IO (Either String ([Backend], CommandLineOptions))
-> ExceptT String IO ([Backend], CommandLineOptions)
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (Either String ([Backend], CommandLineOptions))
 -> ExceptT String IO ([Backend], CommandLineOptions))
-> IO (Either String ([Backend], CommandLineOptions))
-> ExceptT String IO ([Backend], CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ OptM ([Backend], CommandLineOptions)
-> IO (Either String ([Backend], CommandLineOptions))
forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either String opts)
runOptM (OptM ([Backend], CommandLineOptions)
 -> IO (Either String ([Backend], CommandLineOptions)))
-> OptM ([Backend], CommandLineOptions)
-> IO (Either String ([Backend], CommandLineOptions))
forall a b. (a -> b) -> a -> b
$ [Backend]
-> [String]
-> CommandLineOptions
-> OptM ([Backend], CommandLineOptions)
parseBackendOptions [Backend]
backends [String]
argv CommandLineOptions
defaultOptions
    -- The absolute path of the input file, if provided
    Maybe AbsolutePath
inputFile <- IO (Maybe AbsolutePath) -> ExceptT String IO (Maybe AbsolutePath)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe AbsolutePath) -> ExceptT String IO (Maybe AbsolutePath))
-> IO (Maybe AbsolutePath)
-> ExceptT String IO (Maybe AbsolutePath)
forall a b. (a -> b) -> a -> b
$ (String -> IO AbsolutePath)
-> Maybe String -> IO (Maybe AbsolutePath)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> IO AbsolutePath
absolute (Maybe String -> IO (Maybe AbsolutePath))
-> Maybe String -> IO (Maybe AbsolutePath)
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> Maybe String
optInputFile CommandLineOptions
opts
    MainMode
mode      <- [Backend]
-> Maybe AbsolutePath
-> CommandLineOptions
-> ExceptT String IO MainMode
forall (m :: * -> *).
MonadError String m =>
[Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
getMainMode [Backend]
bs Maybe AbsolutePath
inputFile CommandLineOptions
opts
    ([Backend], CommandLineOptions, MainMode)
-> ExceptT String IO ([Backend], CommandLineOptions, MainMode)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Backend]
bs, CommandLineOptions
opts, MainMode
mode)

  case Either String ([Backend], CommandLineOptions, MainMode)
conf of
    Left String
err -> String -> IO ()
optionError String
err
    Right ([Backend]
bs, CommandLineOptions
opts, MainMode
mode) -> case MainMode
mode of
      MainModePrintHelp Help
hp   -> [Backend] -> Help -> IO ()
printUsage [Backend]
bs Help
hp
      MainMode
MainModePrintVersion   -> [Backend] -> IO ()
printVersion [Backend]
bs
      MainMode
MainModePrintAgdaDir   -> IO ()
printAgdaDir
      MainModeRun Interactor ()
interactor -> TCM () -> IO ()
runTCMPrettyErrors (TCM () -> IO ()) -> TCM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Lens' [Backend] TCState -> [Backend] -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' [Backend] TCState
stBackends [Backend]
bs
        Interactor () -> String -> CommandLineOptions -> TCM ()
forall a. Interactor a -> String -> CommandLineOptions -> TCM a
runAgdaWithOptions Interactor ()
interactor String
progName CommandLineOptions
opts

-- | Main execution mode
data MainMode
  = MainModeRun (Interactor ())
  | MainModePrintHelp Help
  | MainModePrintVersion
  | MainModePrintAgdaDir

-- | Determine the main execution mode to run, based on the configured backends and command line options.
-- | This is pure.
getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
getMainMode :: forall (m :: * -> *).
MonadError String m =>
[Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
getMainMode [Backend]
configuredBackends Maybe AbsolutePath
maybeInputFile CommandLineOptions
opts
  | Just Help
hp <- CommandLineOptions -> Maybe Help
optPrintHelp CommandLineOptions
opts = MainMode -> m MainMode
forall (m :: * -> *) a. Monad m => a -> m a
return (MainMode -> m MainMode) -> MainMode -> m MainMode
forall a b. (a -> b) -> a -> b
$ Help -> MainMode
MainModePrintHelp Help
hp
  | CommandLineOptions -> Bool
optPrintVersion CommandLineOptions
opts         = MainMode -> m MainMode
forall (m :: * -> *) a. Monad m => a -> m a
return (MainMode -> m MainMode) -> MainMode -> m MainMode
forall a b. (a -> b) -> a -> b
$ MainMode
MainModePrintVersion
  | CommandLineOptions -> Bool
optPrintAgdaDir CommandLineOptions
opts         = MainMode -> m MainMode
forall (m :: * -> *) a. Monad m => a -> m a
return (MainMode -> m MainMode) -> MainMode -> m MainMode
forall a b. (a -> b) -> a -> b
$ MainMode
MainModePrintAgdaDir
  | Bool
otherwise                    = do
      Maybe (Interactor ())
mi <- [Backend]
-> Maybe AbsolutePath
-> CommandLineOptions
-> m (Maybe (Interactor ()))
forall (m :: * -> *).
MonadError String m =>
[Backend]
-> Maybe AbsolutePath
-> CommandLineOptions
-> m (Maybe (Interactor ()))
getInteractor [Backend]
configuredBackends Maybe AbsolutePath
maybeInputFile CommandLineOptions
opts
      -- If there was no selection whatsoever (e.g. just invoked "agda"), we just show help and exit.
      MainMode -> m MainMode
forall (m :: * -> *) a. Monad m => a -> m a
return (MainMode -> m MainMode) -> MainMode -> m MainMode
forall a b. (a -> b) -> a -> b
$ MainMode
-> (Interactor () -> MainMode) -> Maybe (Interactor ()) -> MainMode
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Help -> MainMode
MainModePrintHelp Help
GeneralHelp) Interactor () -> MainMode
MainModeRun Maybe (Interactor ())
mi

type Interactor a
    -- Setup/initialization action.
    -- This is separated so that errors can be reported in the appropriate format.
    = TCM ()
    -- Type-checking action
    -> (AbsolutePath -> TCM CheckResult)
    -- Main transformed action.
    -> TCM a

data FrontendType
  = FrontEndEmacs
  | FrontEndJson
  | FrontEndRepl

-- Emacs mode. Note that it ignores the "check" action because it calls typeCheck directly.
emacsModeInteractor :: Interactor ()
emacsModeInteractor :: Interactor ()
emacsModeInteractor TCM ()
setup AbsolutePath -> TCM CheckResult
_check = TCM () -> TCM ()
mimicGHCi TCM ()
setup

-- JSON mode. Note that it ignores the "check" action because it calls typeCheck directly.
jsonModeInteractor :: Interactor ()
jsonModeInteractor :: Interactor ()
jsonModeInteractor TCM ()
setup AbsolutePath -> TCM CheckResult
_check = TCM () -> TCM ()
jsonREPL TCM ()
setup

-- The deprecated repl mode.
replInteractor :: Maybe AbsolutePath -> Interactor ()
replInteractor :: Maybe AbsolutePath -> Interactor ()
replInteractor = Maybe AbsolutePath -> Interactor ()
runInteractionLoop

-- The interactor to use when there are no frontends or backends specified.
defaultInteractor :: AbsolutePath -> Interactor ()
defaultInteractor :: AbsolutePath -> Interactor ()
defaultInteractor AbsolutePath
file TCM ()
setup AbsolutePath -> TCM CheckResult
check = do TCM ()
setup; TCM CheckResult -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCM CheckResult -> TCM ()) -> TCM CheckResult -> TCM ()
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TCM CheckResult
check AbsolutePath
file

getInteractor :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m (Maybe (Interactor ()))
getInteractor :: forall (m :: * -> *).
MonadError String m =>
[Backend]
-> Maybe AbsolutePath
-> CommandLineOptions
-> m (Maybe (Interactor ()))
getInteractor [Backend]
configuredBackends Maybe AbsolutePath
maybeInputFile CommandLineOptions
opts =
  case (Maybe AbsolutePath
maybeInputFile, [FrontendType]
enabledFrontends, [Backend]
enabledBackends) of
    (Just AbsolutePath
inputFile, [],             Backend
_:[Backend]
_) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
-> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall a b. (a -> b) -> a -> b
$ Interactor () -> Maybe (Interactor ())
forall a. a -> Maybe a
Just (Interactor () -> Maybe (Interactor ()))
-> Interactor () -> Maybe (Interactor ())
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Backend] -> Interactor ()
backendInteraction AbsolutePath
inputFile [Backend]
enabledBackends
    (Just AbsolutePath
inputFile, [],              []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
-> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall a b. (a -> b) -> a -> b
$ Interactor () -> Maybe (Interactor ())
forall a. a -> Maybe a
Just (Interactor () -> Maybe (Interactor ()))
-> Interactor () -> Maybe (Interactor ())
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> Interactor ()
defaultInteractor AbsolutePath
inputFile
    (Maybe AbsolutePath
Nothing,        [],              []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Interactor ())
forall a. Maybe a
Nothing -- No backends, frontends, or input files specified.
    (Maybe AbsolutePath
Nothing,        [],             Backend
_:[Backend]
_) -> String -> m (Maybe (Interactor ()))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m (Maybe (Interactor ())))
-> String -> m (Maybe (Interactor ()))
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"No input file specified for ", String
enabledBackendNames]
    (Maybe AbsolutePath
_,              FrontendType
_:[FrontendType]
_,            Backend
_:[Backend]
_) -> String -> m (Maybe (Interactor ()))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m (Maybe (Interactor ())))
-> String -> m (Maybe (Interactor ()))
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Cannot mix ", String
enabledFrontendNames, String
" with ", String
enabledBackendNames]
    (Maybe AbsolutePath
_,              FrontendType
_:FrontendType
_:[FrontendType]
_,           []) -> String -> m (Maybe (Interactor ()))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m (Maybe (Interactor ())))
-> String -> m (Maybe (Interactor ()))
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Must not specify multiple ", String
enabledFrontendNames]
    (Maybe AbsolutePath
_,              [FrontendType
fe],            []) | CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts -> FrontendType -> m (Maybe (Interactor ()))
forall {m :: * -> *} {a}.
MonadError String m =>
FrontendType -> m a
errorFrontendScopeChecking FrontendType
fe
    (Maybe AbsolutePath
_,              [FrontendType
FrontEndRepl],  []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
-> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall a b. (a -> b) -> a -> b
$ Interactor () -> Maybe (Interactor ())
forall a. a -> Maybe a
Just (Interactor () -> Maybe (Interactor ()))
-> Interactor () -> Maybe (Interactor ())
forall a b. (a -> b) -> a -> b
$ Maybe AbsolutePath -> Interactor ()
replInteractor Maybe AbsolutePath
maybeInputFile
    (Maybe AbsolutePath
Nothing,        [FrontendType
FrontEndEmacs], []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
-> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall a b. (a -> b) -> a -> b
$ Interactor () -> Maybe (Interactor ())
forall a. a -> Maybe a
Just (Interactor () -> Maybe (Interactor ()))
-> Interactor () -> Maybe (Interactor ())
forall a b. (a -> b) -> a -> b
$ Interactor ()
emacsModeInteractor
    (Maybe AbsolutePath
Nothing,        [FrontendType
FrontEndJson],  []) -> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Interactor ()) -> m (Maybe (Interactor ())))
-> Maybe (Interactor ()) -> m (Maybe (Interactor ()))
forall a b. (a -> b) -> a -> b
$ Interactor () -> Maybe (Interactor ())
forall a. a -> Maybe a
Just (Interactor () -> Maybe (Interactor ()))
-> Interactor () -> Maybe (Interactor ())
forall a b. (a -> b) -> a -> b
$ Interactor ()
jsonModeInteractor
    (Just AbsolutePath
inputFile, [FrontendType
FrontEndEmacs], []) -> AbsolutePath -> FrontendType -> m (Maybe (Interactor ()))
forall {m :: * -> *} {a}.
MonadError String m =>
AbsolutePath -> FrontendType -> m a
errorFrontendFileDisallowed AbsolutePath
inputFile FrontendType
FrontEndEmacs
    (Just AbsolutePath
inputFile, [FrontendType
FrontEndJson],  []) -> AbsolutePath -> FrontendType -> m (Maybe (Interactor ()))
forall {m :: * -> *} {a}.
MonadError String m =>
AbsolutePath -> FrontendType -> m a
errorFrontendFileDisallowed AbsolutePath
inputFile FrontendType
FrontEndJson
  where
    -- NOTE: The notion of a backend being "enabled" *just* refers to this top-level interaction mode selection. The
    -- interaction/interactive front-ends may still invoke available backends even if they are not "enabled".
    isBackendEnabled :: Backend -> Bool
isBackendEnabled (Backend Backend' opts env menv mod def
b) = Backend' opts env menv mod def -> opts -> Bool
forall opts env menv mod def.
Backend' opts env menv mod def -> opts -> Bool
isEnabled Backend' opts env menv mod def
b (Backend' opts env menv mod def -> opts
forall opts env menv mod def.
Backend' opts env menv mod def -> opts
options Backend' opts env menv mod def
b)
    enabledBackends :: [Backend]
enabledBackends = (Backend -> Bool) -> [Backend] -> [Backend]
forall a. (a -> Bool) -> [a] -> [a]
filter Backend -> Bool
isBackendEnabled [Backend]
configuredBackends
    enabledFrontends :: [FrontendType]
enabledFrontends = [[FrontendType]] -> [FrontendType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ FrontendType
FrontEndRepl  | CommandLineOptions -> Bool
optInteractive     CommandLineOptions
opts ]
      , [ FrontendType
FrontEndEmacs | CommandLineOptions -> Bool
optGHCiInteraction CommandLineOptions
opts ]
      , [ FrontendType
FrontEndJson  | CommandLineOptions -> Bool
optJSONInteraction CommandLineOptions
opts ]
      ]
    -- Constructs messages like "(no backend)", "backend ghc", "backends (ghc, ocaml)"
    pluralize :: String -> [String] -> String
pluralize String
w []  = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(no ", String
w, String
")"]
    pluralize String
w [String
x] = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
w, String
" ", String
x]
    pluralize String
w [String]
xs  = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
w, String
"s (", String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " [String]
xs, String
")"]
    enabledBackendNames :: String
enabledBackendNames  = String -> [String] -> String
pluralize String
"backend" [ Backend' opts env menv mod def -> String
forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
b | Backend Backend' opts env menv mod def
b <- [Backend]
enabledBackends ]
    enabledFrontendNames :: String
enabledFrontendNames = String -> [String] -> String
pluralize String
"frontend" (FrontendType -> String
frontendFlagName (FrontendType -> String) -> [FrontendType] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FrontendType]
enabledFrontends)
    frontendFlagName :: FrontendType -> String
frontendFlagName = (String
"--" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> (FrontendType -> String) -> FrontendType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      FrontendType
FrontEndEmacs -> String
"interaction"
      FrontendType
FrontEndJson -> String
"interaction-json"
      FrontendType
FrontEndRepl -> String
"interactive"
    errorFrontendScopeChecking :: FrontendType -> m a
errorFrontendScopeChecking FrontendType
fe = String -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$
      [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"The --only-scope-checking flag cannot be combined with ", FrontendType -> String
frontendFlagName FrontendType
fe]
    errorFrontendFileDisallowed :: AbsolutePath -> FrontendType -> m a
errorFrontendFileDisallowed AbsolutePath
inputFile FrontendType
fe = String -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$
      [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Must not specify an input file (", AbsolutePath -> String
filePath AbsolutePath
inputFile, String
") with ", FrontendType -> String
frontendFlagName FrontendType
fe]

-- | Run Agda with parsed command line options
runAgdaWithOptions
  :: Interactor a       -- ^ Backend interaction
  -> String             -- ^ program name
  -> CommandLineOptions -- ^ parsed command line options
  -> TCM a
runAgdaWithOptions :: forall a. Interactor a -> String -> CommandLineOptions -> TCM a
runAgdaWithOptions Interactor a
interactor String
progName CommandLineOptions
opts = do
          -- Main function.
          -- Bill everything to root of Benchmark trie.
          BenchmarkOn (BenchPhase (TCMT IO)) -> TCM ()
forall (m :: * -> *).
MonadBench m =>
BenchmarkOn (BenchPhase m) -> m ()
UtilsBench.setBenchmarking BenchmarkOn (BenchPhase (TCMT IO))
forall a. BenchmarkOn a
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

          Account (BenchPhase (TCMT IO)) -> TCM a -> TCM a
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [] (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
            Interactor a
interactor TCM ()
initialSetup AbsolutePath -> TCM CheckResult
checkFile
          TCM a -> TCM () -> TCM a
forall a b. TCM a -> TCM b -> TCM a
`finally_` do
            -- Print benchmarks.
            TCM ()
forall (tcm :: * -> *). MonadTCM tcm => tcm ()
Bench.print

            -- Print accumulated statistics.
            Int -> Maybe TopLevelModuleName -> Statistics -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Int -> Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics Int
1 Maybe TopLevelModuleName
forall a. Maybe a
Nothing (Statistics -> TCM ()) -> TCMT IO Statistics -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Lens' Statistics TCState -> TCMT IO Statistics
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' Statistics TCState
lensAccumStatistics
  where
    -- Options are fleshed out here so that (most) errors like
    -- "bad library path" are validated within the interactor,
    -- so that they are reported with the appropriate protocol/formatting.
    initialSetup :: TCM ()
    initialSetup :: TCM ()
initialSetup = do
      CommandLineOptions
opts <- CommandLineOptions -> TCM CommandLineOptions
addTrustedExecutables CommandLineOptions
opts
      CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts

    checkFile :: AbsolutePath -> TCM CheckResult
    checkFile :: AbsolutePath -> TCM CheckResult
checkFile AbsolutePath
inputFile = do
        -- 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
          let mode :: Mode
mode = if CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts
                     then Mode
Imp.ScopeCheck
                     else Mode
Imp.TypeCheck

          CheckResult
result <- Mode -> Source -> TCM CheckResult
Imp.typeCheckMain Mode
mode (Source -> TCM CheckResult) -> TCMT IO Source -> TCM CheckResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SourceFile -> TCMT IO Source
Imp.parseSource (AbsolutePath -> SourceFile
SourceFile AbsolutePath
inputFile)

          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (CheckResult -> ModuleCheckMode
crMode CheckResult
result ModuleCheckMode -> ModuleCheckMode -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleCheckMode
ModuleScopeChecked) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TCMT IO [TCWarning] -> ([TCWarning] -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM ([TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings (CheckResult -> [TCWarning]
crWarnings CheckResult
result)) (([TCWarning] -> TCM ()) -> TCM ())
-> ([TCWarning] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ [TCWarning]
ws ->
              TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [TCWarning]
ws

          let i :: Interface
i = CheckResult -> Interface
crInterface CheckResult
result
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"main" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Interface -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Interface
i

          -- Print accumulated warnings
          TCMT IO [TCWarning] -> ([TCWarning] -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings (WarningsAndNonFatalErrors -> [TCWarning])
-> ([TCWarning] -> WarningsAndNonFatalErrors)
-> [TCWarning]
-> [TCWarning]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings ([TCWarning] -> [TCWarning])
-> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WhichWarnings -> TCMT IO [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings) (([TCWarning] -> TCM ()) -> TCM ())
-> ([TCWarning] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ [TCWarning]
ws -> do
            let banner :: TCMT IO Doc
banner = String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
delimiter String
"All done; warnings encountered"
            String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"warning" Int
1 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
              [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
"\n" ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
banner TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
ws)

          CheckResult -> TCM CheckResult
forall (m :: * -> *) a. Monad m => a -> m a
return CheckResult
result



-- | Print usage information.
printUsage :: [Backend] -> Help -> IO ()
printUsage :: [Backend] -> Help -> IO ()
printUsage [Backend]
backends Help
hp = do
  String
progName <- IO String
getProgName
  String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [OptDescr ()] -> String -> Help -> String
usage [OptDescr ()]
standardOptions_ String
progName Help
hp
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Help
hp Help -> Help -> Bool
forall a. Eq a => a -> a -> Bool
== Help
GeneralHelp) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ (Backend -> IO ()) -> [Backend] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStr (String -> IO ()) -> (Backend -> String) -> Backend -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Backend -> String
backendUsage) [Backend]
backends

backendUsage :: Backend -> String
backendUsage :: Backend -> String
backendUsage (Backend Backend' opts env menv mod def
b) =
  String -> [OptDescr ()] -> String
forall a. String -> [OptDescr a] -> String
usageInfo (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Backend' opts env menv mod def -> String
forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName Backend' opts env menv mod def
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" backend options") ([OptDescr ()] -> String) -> [OptDescr ()] -> String
forall a b. (a -> b) -> a -> b
$
    (OptDescr (Flag opts) -> OptDescr ())
-> [OptDescr (Flag opts)] -> [OptDescr ()]
forall a b. (a -> b) -> [a] -> [b]
map OptDescr (Flag opts) -> OptDescr ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Backend' opts env menv mod def -> [OptDescr (Flag opts)]
forall opts env menv mod def.
Backend' opts env menv mod def -> [OptDescr (Flag opts)]
commandLineFlags Backend' opts env menv mod def
b)

-- | Print version information.
printVersion :: [Backend] -> IO ()
printVersion :: [Backend] -> IO ()
printVersion [Backend]
backends = do
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Agda version " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
versionWithCommitInfo
  (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn
    [ String
"  - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" backend version " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ver
    | Backend Backend'{ backendName :: forall opts env menv mod def.
Backend' opts env menv mod def -> String
backendName = String
name, backendVersion :: forall opts env menv mod def.
Backend' opts env menv mod def -> Maybe String
backendVersion = Just String
ver } <- [Backend]
backends ]

printAgdaDir :: IO ()
printAgdaDir :: IO ()
printAgdaDir = String -> IO ()
putStrLn (String -> IO ()) -> IO String -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO String
getDataDir

-- | What to do for bad options.
optionError :: String -> IO ()
optionError :: String -> IO ()
optionError String
err = do
  String
prog <- IO String
getProgName
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nRun '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
prog String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" --help' for help on command line options."
  AgdaError -> IO ()
exitAgdaWith AgdaError
OptionError

-- | Run a TCM action in IO; catch and pretty print errors.
runTCMPrettyErrors :: TCM () -> IO ()
runTCMPrettyErrors :: TCM () -> IO ()
runTCMPrettyErrors TCM ()
tcm = do
    Either TCErr ()
r <- TCM () -> IO (Either TCErr ())
forall a. TCM a -> IO (Either TCErr a)
runTCMTop (TCM () -> IO (Either TCErr ())) -> TCM () -> IO (Either TCErr ())
forall a b. (a -> b) -> a -> b
$ TCM ()
tcm TCM () -> (TCErr -> TCM ()) -> TCM ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> do
      [String]
s2s <- [TCWarning] -> TCM [String]
prettyTCWarnings' ([TCWarning] -> TCM [String])
-> TCMT IO [TCWarning] -> TCM [String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err
      String
s1  <- TCErr -> TCMT IO String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
err
      let ss :: [String]
ss = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall a. Null a => a -> Bool
null) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
s2s [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
s1]
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String -> Bool
forall a. Null a => a -> Bool
null String
s1) (IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
ss)
      TCErr -> TCM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
    case Either TCErr ()
r of
      Right ()
_ -> IO ()
forall a. IO a
exitSuccess
      Left TCErr
_  -> AgdaError -> IO ()
exitAgdaWith AgdaError
TCMError
  IO () -> (Impossible -> IO ()) -> IO ()
forall (m :: * -> *) a.
CatchImpossible m =>
m a -> (Impossible -> m a) -> m a
`catchImpossible` \Impossible
e -> do
    String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Impossible -> String
forall a. Show a => a -> String
show Impossible
e
    AgdaError -> IO ()
exitAgdaWith AgdaError
ImpossibleError