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