| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Options
- data CommandLineOptions = Options {
- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludePaths :: [FilePath]
- optAbsoluteIncludePaths :: [AbsolutePath]
- optLibraries :: [LibName]
- optOverrideLibrariesFile :: Maybe FilePath
- optDefaultLibs :: Bool
- optUseLibs :: Bool
- optShowVersion :: Bool
- optShowHelp :: Bool
- optInteractive :: Bool
- optGHCiInteraction :: Bool
- optCompileNoMain :: Bool
- optGhcCompile :: Bool
- optGhcCallGhc :: Bool
- optGhcFlags :: [String]
- optEpicCompile :: Bool
- optJSCompile :: Bool
- optUHCCompile :: Bool
- optUHCBin :: Maybe FilePath
- optUHCTextualCore :: Bool
- optUHCCallUHC :: Bool
- optUHCTraceLevel :: Int
- optUHCFlags :: [String]
- optOptimSmashing :: Bool
- optCompileDir :: Maybe FilePath
- optGenerateVimFile :: Bool
- optGenerateLaTeX :: Bool
- optGenerateHTML :: Bool
- optDependencyGraph :: Maybe FilePath
- optLaTeXDir :: FilePath
- optHTMLDir :: FilePath
- optCSSFile :: Maybe FilePath
- optIgnoreInterfaces :: Bool
- optForcing :: Bool
- optPragmaOptions :: PragmaOptions
- optEpicFlags :: [String]
- optSafe :: Bool
- optSharing :: Bool
- optCaching :: Bool
- data IgnoreFlags
- data PragmaOptions = PragmaOptions {
- optShowImplicit :: Bool
- optShowIrrelevant :: Bool
- optVerbose :: Verbosity
- optProofIrrelevance :: Bool
- optAllowUnsolved :: Bool
- optDisablePositivity :: Bool
- optTerminationCheck :: Bool
- optTerminationDepth :: CutOff
- optCompletenessCheck :: Bool
- optUniverseCheck :: Bool
- optSizedTypes :: Bool
- optInjectiveTypeConstructors :: Bool
- optGuardingTypeConstructors :: Bool
- optUniversePolymorphism :: Bool
- optIrrelevantProjections :: Bool
- optExperimentalIrrelevance :: Bool
- optWithoutK :: Bool
- optCopatterns :: Bool
- optPatternMatching :: Bool
- optExactSplit :: Bool
- optEta :: Bool
- optRewriting :: Bool
- optPostfixProjections :: Bool
- optInstanceSearchDepth :: Int
- type OptionsPragma = [String]
- type Flag opts = opts -> OptM opts
- type OptM = ExceptT String IO
- runOptM :: OptM a -> IO (Either String a)
- type Verbosity = Trie String Int
- checkOpts :: Flag CommandLineOptions
- parseStandardOptions :: [String] -> OptM CommandLineOptions
- parseStandardOptions' :: [String] -> Flag CommandLineOptions
- parsePragmaOptions :: [String] -> CommandLineOptions -> OptM PragmaOptions
- parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
- defaultOptions :: CommandLineOptions
- defaultInteractionOptions :: PragmaOptions
- defaultVerbosity :: Verbosity
- defaultCutOff :: CutOff
- defaultPragmaOptions :: PragmaOptions
- standardOptions_ :: [OptDescr ()]
- unsafePragmaOptions :: PragmaOptions -> [String]
- isLiterate :: FilePath -> Bool
- mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
- usage :: [OptDescr ()] -> String -> String
- defaultLibDir :: IO FilePath
- inputFlag :: FilePath -> Flag CommandLineOptions
- standardOptions :: [OptDescr (Flag CommandLineOptions)]
- getOptSimple :: [String] -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
Documentation
data CommandLineOptions Source #
Constructors
data PragmaOptions Source #
Options which can be set in a pragma.
Constructors
| PragmaOptions | |
Fields
| |
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 -> OptM opts Source #
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] -> OptM CommandLineOptions Source #
Parse the standard options.
Arguments
| :: [String] | Pragma options. |
| -> CommandLineOptions | Command-line options which should be updated. |
| -> OptM PragmaOptions |
Parse options from an options pragma.
parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts Source #
Parse options for a plugin.
defaultCutOff :: CutOff Source #
The default termination depth.
standardOptions_ :: [OptDescr ()] Source #
Used for printing usage info.
unsafePragmaOptions :: PragmaOptions -> [String] Source #
Check for unsafe pramas. Gives a list of used unsafe flags.
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 Source #
The usage info message. The argument is the program name (probably agda).
defaultLibDir :: IO FilePath Source #
Returns the absolute default lib dir. This directory is used to store the Primitive.agda file.
Arguments
| :: [String] | command line argument words |
| -> [OptDescr (Flag opts)] | options handlers |
| -> (String -> Flag opts) | handler of non-options (only one is allowed) |
| -> Flag opts | combined opts data structure transformer |
Simple interface for System.Console.GetOpt Could be moved to Agda.Utils.Options (does not exist yet)