Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 FilePathIn the absence of a path the project root is used.
optTerminationCheck :: Bool
optCompletenessCheck :: Bool
optUnreachableCheck :: Bool
optUniverseCheck :: Bool
optSizedTypes :: Bool
optUniversePolymorphism :: Bool
optGhcFlags :: [String]
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.
parseStandardOptions :: String -> [String] -> Either String CommandLineOptionsSource
Parse the standard options.
parsePragmaOptions :: [String] -> CommandLineOptions -> Either String CommandLineOptionsSource
Parse options from an options pragma.
parsePluginOptions :: String -> [String] -> opts -> [OptDescr (Flag opts)] -> Either String optsSource
Parse options for a plugin.
defaultOptions :: CommandLineOptionsSource
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 agdaLight).
tests :: IO BoolSource
Produced by Haddock version 2.6.0