Agda-2.6.2.2: 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.