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

Safe Haskell | None

Agda.Interaction.Options

Synopsis

- data CommandLineOptions = Options {
  - optProgramName :: String
  - optInputFile :: Maybe FilePath
  - optIncludeDirs :: Either [FilePath] [AbsolutePath]
  - optShowVersion :: Bool
  - optShowHelp :: Bool
  - optInteractive :: Bool
  - optRunTests :: Bool
  - optGHCiInteraction :: Bool
  - optCompile :: Bool
  - optEpicCompile :: Bool
  - optJSCompile :: Bool
  - optCompileDir :: Maybe FilePath
  - optGenerateVimFile :: Bool
  - optGenerateLaTeX :: Bool
  - optGenerateHTML :: Bool
  - optDependencyGraph :: Maybe FilePath
  - optLaTeXDir :: FilePath
  - optHTMLDir :: FilePath
  - optCSSFile :: Maybe FilePath
  - optIgnoreInterfaces :: Bool
  - optForcing :: Bool
  - optGhcFlags :: [String]
  - optPragmaOptions :: PragmaOptions
  - optEpicFlags :: [String]
  - optSafe :: Bool
  }
- data PragmaOptions = PragmaOptions {
  - optShowImplicit :: Bool
  - optShowIrrelevant :: Bool
  - optVerbose :: Verbosity
  - optProofIrrelevance :: Bool
  - optAllowUnsolved :: Bool
  - optDisablePositivity :: Bool
  - optTerminationCheck :: Bool
  - optTerminationDepth :: Int
  - optCompletenessCheck :: Bool
  - optUniverseCheck :: Bool
  - optSizedTypes :: Bool
  - optInjectiveTypeConstructors :: Bool
  - optGuardingTypeConstructors :: Bool
  - optUniversePolymorphism :: Bool
  - optIrrelevantProjections :: Bool
  - optExperimentalIrrelevance :: Bool
  - optWithoutK :: Bool
  - optCopatterns :: 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
- defaultInteractionOptions :: PragmaOptions
- defaultVerbosity :: Verbosity
- standardOptions_ :: [OptDescr ()]
- unsafePragmaOptions :: PragmaOptions -> [String]
- isLiterate :: FilePath -> Bool
- mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
- usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> String
- tests :: IO Bool

# Documentation

data CommandLineOptions

Constructors

Options |

Fields

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 `makeIncludeDirsAbsolute`).

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

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

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

Instances

Show CommandLineOptions |

data PragmaOptions

Options which can be set in a pragma.

Constructors

PragmaOptions |

Fields

optShowImplicit :: Bool
optShowIrrelevant :: Bool
optVerbose :: Verbosity
optProofIrrelevance :: Bool
optAllowUnsolved :: Bool
optDisablePositivity :: Bool
optTerminationCheck :: Bool
optTerminationDepth :: Int
optCompletenessCheck :: Bool
optUniverseCheck :: Bool
optSizedTypes :: Bool
optInjectiveTypeConstructors :: Bool
optGuardingTypeConstructors :: Bool
optUniversePolymorphism :: Bool
optIrrelevantProjections :: Bool
optExperimentalIrrelevance :: Bool

  irrelevant levels, irrelevant data matching

optWithoutK :: Bool
optCopatterns :: Bool

  definitions by copattern matching

Instances

Show PragmaOptions |

type OptionsPragma = [String]

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 opts

`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 Int

checkOpts :: Flag CommandLineOptions

Checks that the given options are consistent.

parseStandardOptions :: [String] -> Either String CommandLineOptions

Parse the standard options.

parsePragmaOptions

Arguments

:: [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 opts

Parse options for a plugin.

defaultOptions :: CommandLineOptions

defaultInteractionOptions :: PragmaOptions

defaultVerbosity :: Verbosity

For batch usage.

standardOptions_ :: [OptDescr ()]

Used for printing usage info.

unsafePragmaOptions :: PragmaOptions -> [String]

isLiterate :: FilePath -> Bool

This should probably go somewhere else.

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

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

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

tests :: IO Bool