Agda

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.