Agda.Main

Agda main module.

Documentation

runAgda :: [Backend] -> IO ()

The main function

runAgda' :: [Backend] -> IO ()

The main function without importing built-in backends

data MainMode

Main execution mode

Constructors

MainModeRun (Interactor ())

MainModePrintHelp Help

MainModePrintVersion

MainModePrintAgdaDir

getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode

Determine the main execution mode to run, based on the configured backends and command line options. | This is pure.

type Interactor a = TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM a

data FrontendType

Constructors

FrontEndEmacs

FrontEndJson

FrontEndRepl

emacsModeInteractor :: Interactor ()

jsonModeInteractor :: Interactor ()

replInteractor :: Maybe AbsolutePath -> Interactor ()

defaultInteractor :: AbsolutePath -> Interactor ()

getInteractor :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m (Maybe (Interactor ()))

runAgdaWithOptions

Arguments

:: Interactor a

Backend interaction

-> String

program name

-> CommandLineOptions

parsed command line options

-> TCM a

Run Agda with parsed command line options

printUsage :: [Backend] -> Help -> IO ()

Print usage information.

backendUsage :: Backend -> String

printVersion :: [Backend] -> IO ()

Print version information.

printAgdaDir :: IO ()

optionError :: String -> IO ()

What to do for bad options.

runTCMPrettyErrors :: TCM () -> IO ()

Run a TCM action in IO; catch and pretty print errors.

helpForLocaleError :: TCErr -> IO ()

If the error is an IO error, and the error message suggests that the problem is related to locales or code pages, print out some extra information.