Collie

(source)

Collie: Command line interface for Idris2 applications

Based on Guillaume Allais's agdARGS library:

https://github.com/gallais/agdargs/

Reexports

import public Collie.Core
import public Collie.Parser
import public Collie.Usage
import public Collie.Options.Domain
import public Collie.Options.Usual
import public Collie.Modifiers
import public Data.Record
import public Data.Record.SmartConstructors
import public Data.DPair
import public Data.Magma
import public Data.SnocList
import public System

Definitions

.parseArgs : (cmd : Command nm) -> HasIO io => io (Either String (ParseTreeT Maybe Maybe cmd))

Totality: total
Visibility: public export

record Handlers : Type -> Field Command -> Type

Totality: total
Visibility: public export
Constructor:

MkHandlers : (ParsedCommand (cmd .fst) (cmd .snd) -> a) -> Checkable (Handlers a) ((cmd .snd) .subcommands) -> Handlers a cmd

Projections:

.here : Handlers a cmd -> ParsedCommand (cmd .fst) (cmd .snd) -> a
.there : Handlers a cmd -> Checkable (Handlers a) ((cmd .snd) .subcommands)

.here : Handlers a cmd -> ParsedCommand (cmd .fst) (cmd .snd) -> a

Totality: total
Visibility: public export

here : Handlers a cmd -> ParsedCommand (cmd .fst) (cmd .snd) -> a

Totality: total
Visibility: public export

.there : Handlers a cmd -> Checkable (Handlers a) ((cmd .snd) .subcommands)

Totality: total
Visibility: public export

there : Handlers a cmd -> Checkable (Handlers a) ((cmd .snd) .subcommands)

Totality: total
Visibility: public export

(::) : (ParsedCommand (cmd .fst) (cmd .snd) -> a) -> Checkable (Handlers a) ((cmd .snd) .subcommands) -> Handlers a cmd

  Givent that we already have list syntax to build records, this gives us the
  ability to use list syntax to build `Handlers`: the head will be the handler
  for the toplevel command and the tail will go towards building the record of
  handlers for the subcommands.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

0 (~~>) : Command arg -> Type -> Type

  A nicer notation for handlers

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

handle : ParseTree (cmd .snd) -> Handlers a cmd -> a

  Handling a parsetree is pretty simple: use `there` together with `(!!)` to
  select the appropriate subhandler while you're encountering  the `There`
  constructor and finish up with `here`.

Totality: total
Visibility: public export

.handleWith : (cmd : Command nm) -> cmd ~~> IO a -> IO a

  Finally we can put the various pieces together to get a toplevel command
  parsing the arguments and handling the resulting command using the
  user-provided handlers

Totality: total
Visibility: public export