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

Safe Haskell | None
Language | Haskell2010

Agda.Main

Description

Agda main module.

Synopsis

- runAgda :: [Backend] -> IO ()
- runAgda' :: [Backend] -> IO ()
- type Interactor a = TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM a
- data FrontendType
  - = FrontEndInteraction InteractionFormat
  - | FrontEndRepl
  - | FrontEndBuildLibrary
- data InteractionFormat
  - = InteractionEmacs
  - | InteractionJson
- pattern FrontEndEmacs :: FrontendType
- pattern FrontEndJson :: FrontendType
- buildLibraryInteractor :: Interactor ()
- interactionInteractor :: InteractionFormat -> 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] -> PrintAgdaVersion -> IO ()
- printAgdaDataDir :: IO ()
- printAgdaAppDir :: IO ()
- optionError :: String -> IO ()
- runTCMPrettyErrors :: TCM () -> IO ()
- helpForLocaleError :: TCErr -> IO ()

# Documentation

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

The main function

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

The main function without importing built-in backends

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

data FrontendType Source #

Major mode of operation, not including the standard mode (checking the given main module).

Constructors

FrontEndInteraction InteractionFormat | `--interaction` or `--interaction-json`.
FrontEndRepl | `--interactive`.
FrontEndBuildLibrary | `--build-library`.

data InteractionFormat Source #

Constructors

InteractionEmacs | `--interaction`.
InteractionJson | `--interaction-json`.

pattern FrontEndEmacs :: FrontendType Source #

pattern FrontEndJson :: FrontendType Source #

buildLibraryInteractor :: Interactor () Source #

interactionInteractor :: InteractionFormat -> Interactor () Source #

Emacs/JSON mode. Note that it ignores the "check" action because it calls typeCheck directly.

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

The (deprecated) repl mode.

defaultInteractor :: AbsolutePath -> Interactor () Source #

The interactor to use when there are no frontends or backends specified.

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

Print version information.

printAgdaDataDir :: IO () Source #

printAgdaAppDir :: 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.

helpForLocaleError :: TCErr -> IO () Source #

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.