| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Interaction.Options

Synopsis

data CommandLineOptions = Options {

optProgramName :: String
optInputFile :: Maybe FilePath
optIncludeDirs :: [FilePath]
optShowVersion :: Bool
optShowHelp :: Bool
optInteractive :: Bool
optVerbose :: Trie String Int
optProofIrrelevance :: Bool
optAllowUnsolved :: Bool
optShowImplicit :: Bool
optRunTests :: Bool
optCompile :: Bool
optGenerateVimFile :: Bool
optGenerateHTML :: Bool
optHTMLDir :: FilePath
optCSSFile :: Maybe FilePath
optIgnoreInterfaces :: Bool
optDisablePositivity :: Bool
optCompileAlonzo :: Bool
optCompileMAlonzo :: Bool
optMAlonzoDir :: Maybe FilePath
optTerminationCheck :: Bool
optCompletenessCheck :: Bool
optUnreachableCheck :: Bool
optUniverseCheck :: Bool
optSizedTypes :: Bool
optUniversePolymorphism :: Bool
optGhcFlags :: [String]

}

type Flag opts = opts -> Either String opts
checkOpts :: Flag CommandLineOptions
parseStandardOptions :: String -> [String] -> Either String CommandLineOptions
parsePragmaOptions :: [String] -> CommandLineOptions -> Either String CommandLineOptions
parsePluginOptions :: String -> [String] -> opts -> [OptDescr (Flag opts)] -> Either String opts
defaultOptions :: CommandLineOptions
standardOptions_ :: [OptDescr ()]
isLiterate :: FilePath -> Bool
mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> String
tests :: IO Bool

Documentation

data CommandLineOptions | Source

Constructors

Options |

optProgramName :: String |
optInputFile :: Maybe FilePath |
optIncludeDirs :: [FilePath] |
optShowVersion :: Bool |
optShowHelp :: Bool |
optInteractive :: Bool |
optVerbose :: Trie String Int |
optProofIrrelevance :: Bool |
optAllowUnsolved :: Bool |
optShowImplicit :: Bool |
optRunTests :: Bool |
optCompile :: Bool |
optGenerateVimFile :: Bool |
optGenerateHTML :: Bool |
optHTMLDir :: FilePath |
optCSSFile :: Maybe FilePath |
optIgnoreInterfaces :: Bool |
optDisablePositivity :: Bool |
optCompileAlonzo :: Bool |
optCompileMAlonzo :: Bool |
optMAlonzoDir :: Maybe FilePath | In the absence of a path the project root is used.
optTerminationCheck :: Bool |
optCompletenessCheck :: Bool |
optUnreachableCheck :: Bool |
optUniverseCheck :: Bool |
optSizedTypes :: Bool |
optUniversePolymorphism :: Bool |
optGhcFlags :: [String] |

Instances

Show CommandLineOptions

type Flag opts = opts -> Either String opts | Source

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

Checks that the given options are consistent.

parseStandardOptions :: String -> [String] -> Either String CommandLineOptions | Source

Parse the standard options.

parsePragmaOptions :: [String] -> CommandLineOptions -> Either String CommandLineOptions | Source

Parse options from an options pragma.

parsePluginOptions :: String -> [String] -> opts -> [OptDescr (Flag opts)] -> Either String opts | Source

Parse options for a plugin.

defaultOptions :: CommandLineOptions | Source

standardOptions_ :: [OptDescr ()] | Source

Used for printing usage info.

isLiterate :: FilePath -> Bool | Source

This should probably go somewhere else.

mapFlag :: (String -> String) -> OptDescr a -> OptDescr a | Source

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

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

tests :: IO Bool | Source

Produced by Haddock version 2.4.2