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




data CommandLineOptions Source




optProgramName :: String
optInputFile :: Maybe FilePath
optIncludeDirs :: Either [FilePath] [AbsolutePath]

Left is used temporarily, before the paths have been made absolute. An empty Left list is interpreted as [.] (see Agda.TypeChecking.Monad.Options.makeIncludeDirsAbsolute).

optShowVersion :: Bool
optShowHelp :: Bool
optInteractive :: Bool
optRunTests :: Bool
optCompile :: Bool
optEpicCompile :: Bool
optJSCompile :: Bool
optCompileDir :: Maybe FilePath

In the absence of a path the project root is used.

optGenerateVimFile :: Bool
optGenerateHTML :: Bool
optDependencyGraph :: Maybe FilePath
optHTMLDir :: FilePath
optCSSFile :: Maybe FilePath
optIgnoreInterfaces :: Bool
optForcing :: Bool
optGhcFlags :: [String]
optPragmaOptions :: PragmaOptions
optEpicFlags :: [String]
optSafe :: Bool

type OptionsPragma = [String]Source

The options from an OPTIONS pragma.

In the future it might be nice to switch to a more structured representation. Note that, currently, there is not a one-to-one correspondence between list elements and options.

type Flag opts = opts -> Either String optsSource

The default output directory for HTML.

f :: Flag opts is an action on the option record that results from parsing an option. f opts produces either an error message or an updated options record

checkOpts :: Flag CommandLineOptionsSource

Checks that the given options are consistent.



:: [String]

Pragma options.

-> CommandLineOptions

Command-line options which should be updated.

-> Either String PragmaOptions 

Parse options from an options pragma.

parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag optsSource

Parse options for a plugin.

standardOptions_ :: [OptDescr ()]Source

Used for printing usage info.

isLiterate :: FilePath -> BoolSource

This should probably go somewhere else.

mapFlag :: (String -> String) -> OptDescr a -> OptDescr aSource

Map a function over the long options. Also removes the short options. Will be used to add the plugin name to the plugin options.

usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> StringSource

The usage info message. The argument is the program name (probably agda).