1
2{-| Agda main module.
3-}
4module Agda.Main where
5
6import Prelude hiding (null)
7
8import Control.Monad.Except
9
10import qualified Data.List as List
11import Data.Maybe
12
13import System.Environment
14import System.Console.GetOpt
15
16import Paths_Agda            ( getDataDir )
17
18import Agda.Interaction.CommandLine
19import Agda.Interaction.ExitCode (AgdaError(..), exitSuccess, exitAgdaWith)
20import Agda.Interaction.Options
21import Agda.Interaction.Options.Help (Help (..))
22import Agda.Interaction.EmacsTop (mimicGHCi)
23import Agda.Interaction.JSONTop (jsonREPL)
24import Agda.Interaction.FindFile ( SourceFile(SourceFile) )
25import qualified Agda.Interaction.Imports as Imp
26
27import Agda.TypeChecking.Monad
28import qualified Agda.TypeChecking.Monad.Benchmark as Bench
29import Agda.TypeChecking.Errors
30import Agda.TypeChecking.Warnings
31import Agda.TypeChecking.Pretty
32
33import Agda.Compiler.Backend
34import Agda.Compiler.Builtin
35
36import Agda.VersionCommit
37
38import Agda.Utils.FileName (absolute, filePath, AbsolutePath)
39import Agda.Utils.Monad
40import Agda.Utils.Null
41import Agda.Utils.String
42import qualified Agda.Utils.Benchmark as UtilsBench
43
44import Agda.Utils.Impossible
45
46-- | The main function
47runAgda :: [Backend] -> IO ()
48runAgda backends = runAgda' $ builtinBackends ++ backends
49
50-- | The main function without importing built-in backends
51runAgda' :: [Backend] -> IO ()
52runAgda' backends = do
53  progName <- getProgName
54  argv     <- getArgs
55  conf     <- runExceptT $ do
56    (bs, opts) <- ExceptT $ runOptM $ parseBackendOptions backends argv defaultOptions
57    -- The absolute path of the input file, if provided
58    inputFile <- liftIO $ mapM absolute $ optInputFile opts
59    mode      <- getMainMode bs inputFile opts
60    return (bs, opts, mode)
61
62  case conf of
63    Left err -> optionError err
64    Right (bs, opts, mode) -> case mode of
65      MainModePrintHelp hp   -> printUsage bs hp
66      MainModePrintVersion   -> printVersion bs
67      MainModePrintAgdaDir   -> printAgdaDir
68      MainModeRun interactor -> runTCMPrettyErrors $ do
69        setTCLens stBackends bs
70        runAgdaWithOptions interactor progName opts
71
72-- | Main execution mode
73data MainMode
74  = MainModeRun (Interactor ())
75  | MainModePrintHelp Help
76  | MainModePrintVersion
77  | MainModePrintAgdaDir
78
79-- | Determine the main execution mode to run, based on the configured backends and command line options.
80-- | This is pure.
81getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
82getMainMode configuredBackends maybeInputFile opts
83  | Just hp <- optPrintHelp opts = return $ MainModePrintHelp hp
84  | optPrintVersion opts         = return $ MainModePrintVersion
85  | optPrintAgdaDir opts         = return $ MainModePrintAgdaDir
86  | otherwise                    = do
87      mi <- getInteractor configuredBackends maybeInputFile opts
88      -- If there was no selection whatsoever (e.g. just invoked "agda"), we just show help and exit.
89      return $ maybe (MainModePrintHelp GeneralHelp) MainModeRun mi
90
91type Interactor a
92    -- Setup/initialization action.
93    -- This is separated so that errors can be reported in the appropriate format.
94    = TCM ()
95    -- Type-checking action
96    -> (AbsolutePath -> TCM CheckResult)
97    -- Main transformed action.
98    -> TCM a
99
100data FrontendType
101  = FrontEndEmacs
102  | FrontEndJson
103  | FrontEndRepl
104
105-- Emacs mode. Note that it ignores the "check" action because it calls typeCheck directly.
106emacsModeInteractor :: Interactor ()
107emacsModeInteractor setup _check = mimicGHCi setup
108
109-- JSON mode. Note that it ignores the "check" action because it calls typeCheck directly.
110jsonModeInteractor :: Interactor ()
111jsonModeInteractor setup _check = jsonREPL setup
112
113-- The deprecated repl mode.
114replInteractor :: Maybe AbsolutePath -> Interactor ()
115replInteractor = runInteractionLoop
116
117-- The interactor to use when there are no frontends or backends specified.
118defaultInteractor :: AbsolutePath -> Interactor ()
119defaultInteractor file setup check = do setup; void $ check file
120
121getInteractor :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m (Maybe (Interactor ()))
122getInteractor configuredBackends maybeInputFile opts =
123  case (maybeInputFile, enabledFrontends, enabledBackends) of
124    (Just inputFile, [],             _:_) -> return $ Just $ backendInteraction inputFile enabledBackends
125    (Just inputFile, [],              []) -> return $ Just $ defaultInteractor inputFile
126    (Nothing,        [],              []) -> return Nothing -- No backends, frontends, or input files specified.
127    (Nothing,        [],             _:_) -> throwError $ concat ["No input file specified for ", enabledBackendNames]
128    (_,              _:_,            _:_) -> throwError $ concat ["Cannot mix ", enabledFrontendNames, " with ", enabledBackendNames]
129    (_,              _:_:_,           []) -> throwError $ concat ["Must not specify multiple ", enabledFrontendNames]
130    (_,              [fe],            []) | optOnlyScopeChecking opts -> errorFrontendScopeChecking fe
131    (_,              [FrontEndRepl],  []) -> return $ Just $ replInteractor maybeInputFile
132    (Nothing,        [FrontEndEmacs], []) -> return $ Just $ emacsModeInteractor
133    (Nothing,        [FrontEndJson],  []) -> return $ Just $ jsonModeInteractor
134    (Just inputFile, [FrontEndEmacs], []) -> errorFrontendFileDisallowed inputFile FrontEndEmacs
135    (Just inputFile, [FrontEndJson],  []) -> errorFrontendFileDisallowed inputFile FrontEndJson
136  where
137    -- NOTE: The notion of a backend being "enabled" *just* refers to this top-level interaction mode selection. The
138    -- interaction/interactive front-ends may still invoke available backends even if they are not "enabled".
139    isBackendEnabled (Backend b) = isEnabled b (options b)
140    enabledBackends = filter isBackendEnabled configuredBackends
141    enabledFrontends = concat
142      [ [ FrontEndRepl  | optInteractive     opts ]
143      , [ FrontEndEmacs | optGHCiInteraction opts ]
144      , [ FrontEndJson  | optJSONInteraction opts ]
145      ]
146    -- Constructs messages like "(no backend)", "backend ghc", "backends (ghc, ocaml)"
147    pluralize w []  = concat ["(no ", w, ")"]
148    pluralize w [x] = concat [w, " ", x]
149    pluralize w xs  = concat [w, "s (", List.intercalate ", " xs, ")"]
150    enabledBackendNames  = pluralize "backend" [ backendName b | Backend b <- enabledBackends ]
151    enabledFrontendNames = pluralize "frontend" (frontendFlagName <$> enabledFrontends)
152    frontendFlagName = ("--" ++) . \case
153      FrontEndEmacs -> "interaction"
154      FrontEndJson -> "interaction-json"
155      FrontEndRepl -> "interactive"
156    errorFrontendScopeChecking fe = throwError $
157      concat ["The --only-scope-checking flag cannot be combined with ", frontendFlagName fe]
158    errorFrontendFileDisallowed inputFile fe = throwError $
159      concat ["Must not specify an input file (", filePath inputFile, ") with ", frontendFlagName fe]
160
161-- | Run Agda with parsed command line options
162runAgdaWithOptions
163  :: Interactor a       -- ^ Backend interaction
164  -> String             -- ^ program name
165  -> CommandLineOptions -- ^ parsed command line options
166  -> TCM a
167runAgdaWithOptions interactor progName opts = do
168          -- Main function.
169          -- Bill everything to root of Benchmark trie.
170          UtilsBench.setBenchmarking UtilsBench.BenchmarkOn
171            -- Andreas, Nisse, 2016-10-11 AIM XXIV
172            -- Turn benchmarking on provisionally, otherwise we lose track of time spent
173            -- on e.g. LaTeX-code generation.
174            -- Benchmarking might be turned off later by setCommandlineOptions
175
176          Bench.billTo [] $
177            interactor initialSetup checkFile
178          `finally_` do
179            -- Print benchmarks.
180            Bench.print
181
182            -- Print accumulated statistics.
183            printStatistics 1 Nothing =<< useTC lensAccumStatistics
184  where
185    -- Options are fleshed out here so that (most) errors like
186    -- "bad library path" are validated within the interactor,
187    -- so that they are reported with the appropriate protocol/formatting.
188    initialSetup :: TCM ()
189    initialSetup = do
190      opts <- addTrustedExecutables opts
191      setCommandLineOptions opts
192
193    checkFile :: AbsolutePath -> TCM CheckResult
194    checkFile inputFile = do
195        -- Andreas, 2013-10-30 The following 'resetState' kills the
196        -- verbosity options.  That does not make sense (see fail/Issue641).
197        -- 'resetState' here does not seem to serve any purpose,
198        -- thus, I am removing it.
199        -- resetState
200          let mode = if optOnlyScopeChecking opts
201                     then Imp.ScopeCheck
202                     else Imp.TypeCheck
203
204          result <- Imp.typeCheckMain mode =<< Imp.parseSource (SourceFile inputFile)
205
206          unless (crMode result == ModuleScopeChecked) $
207            unlessNullM (applyFlagsToTCWarnings (crWarnings result)) $ \ ws ->
208              typeError $ NonFatalErrors ws
209
210          let i = crInterface result
211          reportSDoc "main" 50 $ pretty i
212
213          -- Print accumulated warnings
214          unlessNullM (tcWarnings . classifyWarnings <$> getAllWarnings AllWarnings) $ \ ws -> do
215            let banner = text $ "\n" ++ delimiter "All done; warnings encountered"
216            reportSDoc "warning" 1 $
217              vcat $ punctuate "\n" $ banner : (prettyTCM <$> ws)
218
219          return result
220
221
222
223-- | Print usage information.
224printUsage :: [Backend] -> Help -> IO ()
225printUsage backends hp = do
226  progName <- getProgName
227  putStr $ usage standardOptions_ progName hp
228  when (hp == GeneralHelp) $ mapM_ (putStr . backendUsage) backends
229
230backendUsage :: Backend -> String
231backendUsage (Backend b) =
232  usageInfo ("\n" ++ backendName b ++ " backend options") $
233    map void (commandLineFlags b)
234
235-- | Print version information.
236printVersion :: [Backend] -> IO ()
237printVersion backends = do
238  putStrLn $ "Agda version " ++ versionWithCommitInfo
239  mapM_ putStrLn
240    [ "  - " ++ name ++ " backend version " ++ ver
241    | Backend Backend'{ backendName = name, backendVersion = Just ver } <- backends ]
242
243printAgdaDir :: IO ()
244printAgdaDir = putStrLn =<< getDataDir
245
246-- | What to do for bad options.
247optionError :: String -> IO ()
248optionError err = do
249  prog <- getProgName
250  putStrLn $ "Error: " ++ err ++ "\nRun '" ++ prog ++ " --help' for help on command line options."
251  exitAgdaWith OptionError
252
253-- | Run a TCM action in IO; catch and pretty print errors.
254runTCMPrettyErrors :: TCM () -> IO ()
255runTCMPrettyErrors tcm = do
256    r <- runTCMTop $ tcm `catchError` \err -> do
257      s2s <- prettyTCWarnings' =<< getAllWarningsOfTCErr err
258      s1  <- prettyError err
259      let ss = filter (not . null) $ s2s ++ [s1]
260      unless (null s1) (liftIO $ putStr $ unlines ss)
261      throwError err
262    case r of
263      Right _ -> exitSuccess
264      Left _  -> exitAgdaWith TCMError
265  `catchImpossible` \e -> do
266    putStr $ show e
267    exitAgdaWith ImpossibleError
268