Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.Options
Synopsis
data CommandLineOptions = Options {
optProgramName :: String
optInputFile :: Maybe FilePath
optIncludeDirs :: Either [FilePath] [AbsolutePath]
optShowVersion :: Bool
optShowHelp :: Bool
optInteractive :: Bool
optRunTests :: Bool
optCompile :: Bool
optEpicCompile :: Bool
optCompileDir :: Maybe FilePath
optGenerateVimFile :: Bool
optGenerateHTML :: Bool
optHTMLDir :: FilePath
optCSSFile :: Maybe FilePath
optIgnoreInterfaces :: Bool
optForcing :: Bool
optGhcFlags :: [String]
optPragmaOptions :: PragmaOptions
optEpicFlags :: [String]
}
data PragmaOptions = PragmaOptions {
optShowImplicit :: Bool
optVerbose :: Verbosity
optProofIrrelevance :: Bool
optAllowUnsolved :: Bool
optDisablePositivity :: Bool
optTerminationCheck :: Bool
optTerminationDepth :: Int
optCompletenessCheck :: Bool
optUnreachableCheck :: Bool
optUniverseCheck :: Bool
optSizedTypes :: Bool
optInjectiveTypeConstructors :: Bool
optGuardingTypeConstructors :: Bool
optUniversePolymorphism :: Bool
optIrrelevantProjections :: Bool
optWithoutK :: Bool
}
type OptionsPragma = [String]
type Flag opts = opts -> Either String opts
type Verbosity = Trie String Int
checkOpts :: Flag CommandLineOptions
parseStandardOptions :: [String] -> Either String CommandLineOptions
parsePragmaOptions :: [String] -> CommandLineOptions -> Either String PragmaOptions
parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
defaultOptions :: CommandLineOptions
defaultVerbosity :: Verbosity
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 :: 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
optCompileDir :: Maybe FilePathIn the absence of a path the project root is used.
optGenerateVimFile :: Bool
optGenerateHTML :: Bool
optHTMLDir :: FilePath
optCSSFile :: Maybe FilePath
optIgnoreInterfaces :: Bool
optForcing :: Bool
optGhcFlags :: [String]
optPragmaOptions :: PragmaOptions
optEpicFlags :: [String]
data PragmaOptions Source
Options which can be set in a pragma.
Constructors
PragmaOptions
optShowImplicit :: Bool
optVerbose :: Verbosity
optProofIrrelevance :: Bool
optAllowUnsolved :: Bool
optDisablePositivity :: Bool
optTerminationCheck :: Bool
optTerminationDepth :: Int
optCompletenessCheck :: Bool
optUnreachableCheck :: Bool
optUniverseCheck :: Bool
optSizedTypes :: Bool
optInjectiveTypeConstructors :: Bool
optGuardingTypeConstructors :: Bool
optUniversePolymorphism :: Bool
optIrrelevantProjections :: Bool
optWithoutK :: 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

type Verbosity = Trie String IntSource
checkOpts :: Flag CommandLineOptionsSource
Checks that the given options are consistent.
parseStandardOptions :: [String] -> Either String CommandLineOptionsSource
Parse the standard options.
parsePragmaOptionsSource
:: [String]Pragma options.
-> CommandLineOptionsCommand-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.
defaultOptions :: CommandLineOptionsSource
defaultVerbosity :: VerbositySource
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).
tests :: IO BoolSource
Produced by Haddock version 2.6.1