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

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Options

Synopsis

- data CommandLineOptions = Options {
  - optProgramName :: String
  - optInputFile :: Maybe FilePath
  - optIncludePaths :: [FilePath]
  - optAbsoluteIncludePaths :: [AbsolutePath]
  - optLibraries :: [LibName]
  - optOverrideLibrariesFile :: Maybe FilePath
  - optDefaultLibs :: Bool
  - optUseLibs :: Bool
  - optShowVersion :: Bool
  - optShowHelp :: Maybe Help
  - optInteractive :: Bool
  - optGHCiInteraction :: Bool
  - optJSONInteraction :: Bool
  - optOptimSmashing :: Bool
  - optCompileDir :: Maybe FilePath
  - optGenerateVimFile :: Bool
  - optGenerateLaTeX :: Bool
  - optGenerateHTML :: Bool
  - optHTMLHighlight :: HtmlHighlight
  - optDependencyGraph :: Maybe FilePath
  - optLaTeXDir :: FilePath
  - optHTMLDir :: FilePath
  - optCSSFile :: Maybe FilePath
  - optIgnoreInterfaces :: Bool
  - optIgnoreAllInterfaces :: Bool
  - optForcing :: Bool
  - optPragmaOptions :: PragmaOptions
  - optOnlyScopeChecking :: Bool
  }
- data PragmaOptions = PragmaOptions {
  - optShowImplicit :: Bool
  - optShowIrrelevant :: Bool
  - optUseUnicode :: Bool
  - optVerbose :: Verbosity
  - optProp :: Bool
  - optAllowUnsolved :: Bool
  - optDisablePositivity :: Bool
  - optTerminationCheck :: Bool
  - optTerminationDepth :: CutOff
  - optCompletenessCheck :: Bool
  - optUniverseCheck :: Bool
  - optOmegaInOmega :: Bool
  - optSizedTypes :: WithDefault True
  - optGuardedness :: WithDefault True
  - optInjectiveTypeConstructors :: Bool
  - optUniversePolymorphism :: Bool
  - optIrrelevantProjections :: Bool
  - optExperimentalIrrelevance :: Bool
  - optWithoutK :: WithDefault False
  - optCopatterns :: Bool
  - optPatternMatching :: Bool
  - optExactSplit :: Bool
  - optEta :: Bool
  - optRewriting :: Bool
  - optCubical :: Bool
  - optPostfixProjections :: Bool
  - optInstanceSearchDepth :: Int
  - optOverlappingInstances :: Bool
  - optInversionMaxDepth :: Int
  - optSafe :: Bool
  - optDoubleCheck :: Bool
  - optSyntacticEquality :: Bool
  - optWarningMode :: WarningMode
  - optCompileNoMain :: Bool
  - optCaching :: Bool
  - optCountClusters :: Bool
  - optAutoInline :: Bool
  - optPrintPatternSynonyms :: Bool
  - optFastReduce :: Bool
  }
- type OptionsPragma = [String]
- type Flag opts = opts -> OptM opts
- type OptM = ExceptT String IO
- runOptM :: OptM a -> IO (Either String a)
- data OptDescr a = Option [Char] [String] (ArgDescr a) String
- data ArgDescr a
  - = NoArg a
  - | ReqArg (String -> a) String
  - | OptArg (Maybe String -> a) String
- type Verbosity = Trie String Int
- data HtmlHighlight
  - = HighlightAll
  - | HighlightCode
  - | HighlightAuto
- data WarningMode = WarningMode {
  - _warningSet :: Set WarningName
  - _warn2Error :: Bool
  }
- checkOpts :: Flag CommandLineOptions
- parsePragmaOptions :: [String] -> CommandLineOptions -> OptM PragmaOptions
- parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
- stripRTS :: [String] -> [String]
- defaultOptions :: CommandLineOptions
- defaultInteractionOptions :: PragmaOptions
- defaultVerbosity :: Verbosity
- defaultCutOff :: CutOff
- defaultPragmaOptions :: PragmaOptions
- standardOptions_ :: [OptDescr ()]
- unsafePragmaOptions :: PragmaOptions -> [String]
- restartOptions :: [(PragmaOptions -> RestartCodomain, String)]
- infectiveOptions :: [(PragmaOptions -> Bool, String)]
- coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
- safeFlag :: Flag PragmaOptions
- mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
- usage :: [OptDescr ()] -> String -> Help -> String
- defaultLibDir :: IO FilePath
- inputFlag :: FilePath -> Flag CommandLineOptions
- standardOptions :: [OptDescr (Flag CommandLineOptions)]
- deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
- getOptSimple :: [String] -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts

# Documentation

data CommandLineOptions Source #

Constructors

Options |

Fields

- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludePaths :: [FilePath]
- optAbsoluteIncludePaths :: [AbsolutePath]
- optLibraries :: [LibName]
- optOverrideLibrariesFile :: Maybe FilePath

  Use this (if Just) instead of .agda/libraries

- optDefaultLibs :: Bool

  Use ~.agdadefaults

- optUseLibs :: Bool

  look for .agda-lib files

- optShowVersion :: Bool
- optShowHelp :: Maybe Help
- optInteractive :: Bool
- optGHCiInteraction :: Bool
- optJSONInteraction :: Bool
- optOptimSmashing :: Bool
- optCompileDir :: Maybe FilePath

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

- optGenerateVimFile :: Bool
- optGenerateLaTeX :: Bool
- optGenerateHTML :: Bool
- optHTMLHighlight :: HtmlHighlight
- optDependencyGraph :: Maybe FilePath
- optLaTeXDir :: FilePath
- optHTMLDir :: FilePath
- optCSSFile :: Maybe FilePath
- optIgnoreInterfaces :: Bool
- optIgnoreAllInterfaces :: Bool
- optForcing :: Bool
- optPragmaOptions :: PragmaOptions
- optOnlyScopeChecking :: Bool

  Should the top-level module only be scope-checked, and not type-checked?

Instances

Show CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options Methods showsPrec :: Int -> CommandLineOptions -> ShowS Source # show :: CommandLineOptions -> String Source # showList :: [CommandLineOptions] -> ShowS Source #
LensPersistentVerbosity CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions Source #
LensIncludePaths CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: CommandLineOptions -> [FilePath] Source #

setIncludePaths :: [FilePath] -> CommandLineOptions -> CommandLineOptions Source #

mapIncludePaths :: ([FilePath] -> [FilePath]) -> CommandLineOptions -> CommandLineOptions Source #

getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath] Source #

setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions Source #

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> CommandLineOptions -> CommandLineOptions Source #

LensSafeMode CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: CommandLineOptions -> SafeMode Source # setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions Source #
LensPragmaOptions CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPragmaOptions :: CommandLineOptions -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions Source # lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions Source #

data PragmaOptions Source #

Options which can be set in a pragma.

Constructors

PragmaOptions |

Fields

- optShowImplicit :: Bool
- optShowIrrelevant :: Bool
- optUseUnicode :: Bool
- optVerbose :: Verbosity
- optProp :: Bool
- optAllowUnsolved :: Bool
- optDisablePositivity :: Bool
- optTerminationCheck :: Bool
- optTerminationDepth :: CutOff

  Cut off structural order comparison at some depth in termination checker?

- optCompletenessCheck :: Bool
- optUniverseCheck :: Bool
- optOmegaInOmega :: Bool
- optSizedTypes :: WithDefault True
- optGuardedness :: WithDefault True
- optInjectiveTypeConstructors :: Bool
- optUniversePolymorphism :: Bool
- optIrrelevantProjections :: Bool
- optExperimentalIrrelevance :: Bool

  irrelevant levels, irrelevant data matching

- optWithoutK :: WithDefault False
- optCopatterns :: Bool

  Allow definitions by copattern matching?

- optPatternMatching :: Bool

  Is pattern matching allowed in the current file?

- optExactSplit :: Bool
- optEta :: Bool
- optRewriting :: Bool

  Can rewrite rules be added and used?

- optCubical :: Bool
- optPostfixProjections :: Bool

  Should system generated projections `ProjSystem` be printed postfix (True) or prefix (False).

- optInstanceSearchDepth :: Int
- optOverlappingInstances :: Bool
- optInversionMaxDepth :: Int
- optSafe :: Bool
- optDoubleCheck :: Bool
- optSyntacticEquality :: Bool

  Should conversion checker use syntactic equality shortcut?

- optWarningMode :: WarningMode
- optCompileNoMain :: Bool
- optCaching :: Bool
- optCountClusters :: Bool

  Count extended grapheme clusters rather than code points when generating LaTeX.

- optAutoInline :: Bool

  Automatic compile-time inlining for simple definitions (unless marked NOINLINE).

- optPrintPatternSynonyms :: Bool
- optFastReduce :: Bool

  Use the Agda abstract machine (fastReduce)?

Instances

Eq PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options Methods (==) :: PragmaOptions -> PragmaOptions -> Bool Source # (/=) :: PragmaOptions -> PragmaOptions -> Bool Source #
Show PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options Methods showsPrec :: Int -> PragmaOptions -> ShowS Source # show :: PragmaOptions -> String Source # showList :: [PragmaOptions] -> ShowS Source #
EmbPrj PragmaOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Int32 Source # icod_ :: PragmaOptions -> S Int32 Source # value :: Int32 -> R PragmaOptions Source #
LensPersistentVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PragmaOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> PragmaOptions -> PragmaOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PragmaOptions -> PragmaOptions Source #
LensSafeMode PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PragmaOptions -> SafeMode Source # setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions Source #
LensVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: PragmaOptions -> Verbosity Source # setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions Source # mapVerbosity :: (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions Source #

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

type OptM = ExceptT String IO Source #

runOptM :: OptM a -> IO (Either String a) Source #

data OptDescr a Source #

Each `OptDescr` describes a single option.

The arguments to `Option` are:

- list of short option characters
- list of long option strings (without "--")
- argument descriptor
- explanation of option for user

Constructors

Option [Char] [String] (ArgDescr a) String |

Instances

Functor OptDescr | Since: base-4.6.0.0
Instance details Defined in System.Console.GetOpt Methods fmap :: (a -> b) -> OptDescr a -> OptDescr b Source # (<$) :: a -> OptDescr b -> OptDescr a Source #

data ArgDescr a Source #

Describes whether an option takes an argument or not, and if so how the argument is injected into a value of type `a`.

Constructors

NoArg a | no argument expected
ReqArg (String -> a) String | option requires argument
OptArg (Maybe String -> a) String | optional argument

Instances

Functor ArgDescr | Since: base-4.6.0.0
Instance details Defined in System.Console.GetOpt Methods fmap :: (a -> b) -> ArgDescr a -> ArgDescr b Source # (<$) :: a -> ArgDescr b -> ArgDescr a Source #

type Verbosity = Trie String Int Source #

data HtmlHighlight Source #

Constructors

HighlightAll |
HighlightCode |
HighlightAuto |

Instances

Eq HtmlHighlight Source # |
Instance details Defined in Agda.Interaction.Options Methods (==) :: HtmlHighlight -> HtmlHighlight -> Bool Source # (/=) :: HtmlHighlight -> HtmlHighlight -> Bool Source #
Show HtmlHighlight Source # |
Instance details Defined in Agda.Interaction.Options Methods showsPrec :: Int -> HtmlHighlight -> ShowS Source # show :: HtmlHighlight -> String Source # showList :: [HtmlHighlight] -> ShowS Source #

data WarningMode Source #

A `WarningMode` has two components: a set of warnings to be displayed and a flag stating whether warnings should be turned into fatal errors.

Constructors

WarningMode |

Fields

- _warningSet :: Set WarningName
- _warn2Error :: Bool

Instances

Eq WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningMode -> WarningMode -> Bool Source # (/=) :: WarningMode -> WarningMode -> Bool Source #
Show WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS Source # show :: WarningMode -> String Source # showList :: [WarningMode] -> ShowS Source #
EmbPrj WarningMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Int32 Source # icod_ :: WarningMode -> S Int32 Source # value :: Int32 -> R WarningMode Source #

checkOpts :: Flag CommandLineOptions Source #

Checks that the given options are consistent.

parsePragmaOptions Source #

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.

stripRTS :: [String] -> [String] Source #

Removes RTS options from a list of options.

defaultOptions :: CommandLineOptions Source #

defaultInteractionOptions :: PragmaOptions Source #

defaultVerbosity :: Verbosity Source #

defaultCutOff :: CutOff Source #

The default termination depth.

defaultPragmaOptions :: PragmaOptions Source #

standardOptions_ :: [OptDescr ()] Source #

Used for printing usage info. Does not include the dead options.

unsafePragmaOptions :: PragmaOptions -> [String] Source #

Check for unsafe pragmas. Gives a list of used unsafe flags.

restartOptions :: [(PragmaOptions -> RestartCodomain, String)] Source #

If any these options have changed, then the file will be rechecked. Boolean options are negated to mention non-default options, where possible.

infectiveOptions :: [(PragmaOptions -> Bool, String)] Source #

An infective option is an option that if used in one module, must be used in all modules that depend on this module.

coinfectiveOptions :: [(PragmaOptions -> Bool, String)] Source #

A coinfective option is an option that if used in one module, must be used in all modules that this module depends on.

safeFlag :: Flag PragmaOptions Source #

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 -> Help -> 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.

inputFlag :: FilePath -> Flag CommandLineOptions Source #

standardOptions :: [OptDescr (Flag CommandLineOptions)] Source #

deadStandardOptions :: [OptDescr (Flag CommandLineOptions)] Source #

Command line options of previous versions of Agda. Should not be listed in the usage info, put parsed by GetOpt for good error messaging.

getOptSimple Source #

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)