data ArgOrder : Type -> Type
What to do with options following non-options
Totality: total
Visibility: public export
Constructors:
RequireOrder : ArgOrder a
no option processing after first non-option
Permute : ArgOrder a
freely intersperse options and non-options
ReturnInOrder : (String -> a) -> ArgOrder a
wrap non-options into options
Hint: Functor ArgOrder
data ArgDescr : Type -> Type
Describes whether an option takes an argument or not, and if so
how the argument is injected into a value of type `a`.
Totality: total
Visibility: public export
Constructors:
NoArg : a -> ArgDescr a
no argument expected
ReqArg : (String -> a) -> String -> ArgDescr a
option requires argument
OptArg : (Maybe String -> a) -> String -> ArgDescr a
optional argument
Hint: Functor ArgDescr
record OptDescr : Type -> Type
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
Totality: total
Visibility: public export
Constructor: MkOpt : List Char -> List String -> ArgDescr a -> String -> OptDescr a
Projections:
.argDescr : OptDescr a -> ArgDescr a
argument descriptor
.description : OptDescr a -> String
explanation of option for user
.longNames : OptDescr a -> List String
list of long option strings (without "--")
.shortNames : OptDescr a -> List Char
list of short option characters
Hint: Functor OptDescr
.shortNames : OptDescr a -> List Char
list of short option characters
Totality: total
Visibility: public exportshortNames : OptDescr a -> List Char
list of short option characters
Totality: total
Visibility: public export.longNames : OptDescr a -> List String
list of long option strings (without "--")
Totality: total
Visibility: public exportlongNames : OptDescr a -> List String
list of long option strings (without "--")
Totality: total
Visibility: public export.argDescr : OptDescr a -> ArgDescr a
argument descriptor
Totality: total
Visibility: public exportargDescr : OptDescr a -> ArgDescr a
argument descriptor
Totality: total
Visibility: public export.description : OptDescr a -> String
explanation of option for user
Totality: total
Visibility: public exportdescription : OptDescr a -> String
explanation of option for user
Totality: total
Visibility: public exportusageInfo : String -> List (OptDescr a) -> String
Return a string describing the usage of a command, derived from
the header (first argument) and the options described by the
second argument.
Totality: total
Visibility: public exportrecord Result : Type -> Type
Result of parsing the command line arguments accoring to a list
of `OptDescr`s. (see also function `getOpt`).
Totality: total
Visibility: public export
Constructor: MkResult : List a -> List String -> List String -> List String -> Result a
Projections:
.errors : Result a -> List String
Errors during option parsing. These occur, for instance, when
an option requires an additional argument but none was given.
.nonOptions : Result a -> List String
List of non-options (other command line arguments)
.options : Result a -> List a
List of successfully parsed options
.unrecognized : Result a -> List String
List of unrecognized options.
Hint: Functor Result
.options : Result a -> List a
List of successfully parsed options
Totality: total
Visibility: public exportoptions : Result a -> List a
List of successfully parsed options
Totality: total
Visibility: public export.nonOptions : Result a -> List String
List of non-options (other command line arguments)
Totality: total
Visibility: public exportnonOptions : Result a -> List String
List of non-options (other command line arguments)
Totality: total
Visibility: public export.unrecognized : Result a -> List String
List of unrecognized options.
Totality: total
Visibility: public exportunrecognized : Result a -> List String
List of unrecognized options.
Totality: total
Visibility: public export.errors : Result a -> List String
Errors during option parsing. These occur, for instance, when
an option requires an additional argument but none was given.
Totality: total
Visibility: public exporterrors : Result a -> List String
Errors during option parsing. These occur, for instance, when
an option requires an additional argument but none was given.
Totality: total
Visibility: public exportemptyRes : Result a
- Totality: total
Visibility: public export getOpt : ArgOrder a -> List (OptDescr a) -> List String -> Result a
Process the command-line, and return the list of values that matched
(and those that didn't). The arguments are:
* The order requirements (see `ArgOrder`)
* The option descriptions (see `OptDescr`)
* The actual command line arguments (presumably got from
`System.getArgs`).
Totality: total
Visibility: export