Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Options

Synopsis

Documentation

data CommandLineOptions Source #

Instances

Instances details
Show CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options

LensPersistentVerbosity CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPragmaOptions CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

data PragmaOptions Source #

Options which can be set in a pragma.

Constructors

PragmaOptions 

Fields

Instances

Instances details
Eq PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options

Show PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options

EmbPrj PragmaOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

LensPersistentVerbosity PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensVerbosity PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

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

data OptDescr a #

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

Instances details
Functor OptDescr

Since: base-4.6.0.0

Instance details

Defined in System.Console.GetOpt

Methods

fmap :: (a -> b) -> OptDescr a -> OptDescr b #

(<$) :: a -> OptDescr b -> OptDescr a #

data ArgDescr a #

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

Instances details
Functor ArgDescr

Since: base-4.6.0.0

Instance details

Defined in System.Console.GetOpt

Methods

fmap :: (a -> b) -> ArgDescr a -> ArgDescr b #

(<$) :: a -> ArgDescr b -> ArgDescr a #

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.

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.

defaultCutOff :: CutOff Source #

The default termination depth.

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.

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.

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)