Agda-2.6.2.0.20211129: A dependently typed functional programming language and proof assistant

Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Main

Description

Agda main module.

Synopsis

runAgda :: [Backend] -> IO ()
runAgda' :: [Backend] -> IO ()
data MainMode
- = MainModeRun (Interactor ())
- | MainModePrintHelp Help
- | MainModePrintVersion
- | MainModePrintAgdaDir
getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode
type Interactor a = TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM a
data FrontendType
- = 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 :: Interactor a -> String -> CommandLineOptions -> TCM a
printUsage :: [Backend] -> Help -> IO ()
backendUsage :: Backend -> String
printVersion :: [Backend] -> IO ()
printAgdaDir :: IO ()
optionError :: String -> IO ()
runTCMPrettyErrors :: TCM () -> IO ()

Documentation

runAgda :: [Backend] -> IO () Source #

The main function

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

The main function without importing built-in backends

data MainMode Source #

Main execution mode

Constructors

MainModeRun (Interactor ())
MainModePrintHelp Help
MainModePrintVersion
MainModePrintAgdaDir

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

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 Source #

data FrontendType Source #

Constructors

FrontEndEmacs
FrontEndJson
FrontEndRepl

emacsModeInteractor :: Interactor () Source #

jsonModeInteractor :: Interactor () Source #

replInteractor :: Maybe AbsolutePath -> Interactor () Source #

defaultInteractor :: AbsolutePath -> Interactor () Source #

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

runAgdaWithOptions Source #

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 () Source #

Print usage information.

backendUsage :: Backend -> String Source #

printVersion :: [Backend] -> IO () Source #

Print version information.

printAgdaDir :: IO () Source #

optionError :: String -> IO () Source #

What to do for bad options.

runTCMPrettyErrors :: TCM () -> IO () Source #

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