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