System.Console.GetOpt

This library provides facilities for parsing the command-line options
in a standalone program. It is essentially an Idris port of the GNU getopt library.
(Actually, it is an Idris port of the [corresponding Haskell module]
(http://hackage.haskell.org/package/base-4.14.1.0/docs/System-Console-GetOpt.html)).

Definitions

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

ReturnInOrder' : (String -> Either String a) -> ArgOrder a

  wrap non-options into options (or fail, if can't)

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

ReqArg' : (String -> Either String a) -> String -> ArgDescr a

  option requires argument and may fail during parsing

OptArg : (Maybe String -> a) -> String -> ArgDescr a

  optional argument

OptArg' : (Maybe String -> Either String a) -> String -> ArgDescr a

  optional argument and may fail during parsing

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 export

shortNames : 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 export

longNames : 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 export

argDescr : OptDescr a -> ArgDescr a

  argument descriptor

Totality: total
Visibility: public export

.description : OptDescr a -> String

  explanation of option for user

Totality: total
Visibility: public export

description : OptDescr a -> String

  explanation of option for user

Totality: total
Visibility: public export

usageInfo : 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 export

record Result : Type -> Type

  Result of parsing the command line arguments according 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 export

options : 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 export

nonOptions : 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 export

unrecognized : 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 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 export

emptyRes : 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

getOpt' : Applicative f => ArgOrder (f a) -> List (OptDescr (f a)) -> List String -> f (Result a)

  Parse the command-line like `getOpt`, but allow each option parser to do
  additional work in some `Applicative`.
  
  Place, notice that options parsing is done first, i.e. if you use
  applicatives that can have a failure semantics, you will lose all errors
  reported inside the `Result` type in case of any option parsing fails.

Totality: total
Visibility: export