Defines the abstract CLI interface for Lake.

Types

def Lake.ArgList : Type

@[inline]

def Lake.ArgList.mk (args : List String) : ArgList

@[reducible, inline]

abbrev Lake.ArgsT (m : Type → Type u_1) (α : Type) : Type u_1

@[inline]

def Lake.ArgsT.run {m : Type → Type u_1} {α : Type} (args : List String) (self : ArgsT m α) : m (α × List String)

@[inline]

def Lake.ArgsT.run' {m : Type → Type u_1} {α : Type} [Functor m] (args : List String) (self : ArgsT m α) : m α

structure Lake.OptionHandlers (m : Type u → Type v) (α : Type u) : Type v

• long : String → m α

  Process a long option (ex. --long or "--long foo bar").

• short : Char → m α

  Process a short option (ex. -x or --).

• longShort : String → m α

  Process a long short option (ex. -long, -xarg, -xyz).

Utilities

@[inline]

def Lake.getArgs {m : Type → Type u_1} [MonadStateOf ArgList m] : m (List String)

Get the remaining argument list.

@[inline]

def Lake.setArgs {m : Type → Type u_1} [MonadStateOf ArgList m] (args : List String) : m PUnit

Replace the argument list.

@[inline]

def Lake.takeArg? {m : Type → Type u_1} [MonadStateOf ArgList m] : m (Option String)

Take the head of the remaining argument list (or none if empty).

@[inline]

def Lake.takeArgD {m : Type → Type u_1} [MonadStateOf ArgList m] (default : String) : m String

Take the head of the remaining argument list (or default if none).

@[inline]

def Lake.takeArgs {m : Type → Type u_1} [MonadStateOf ArgList m] : m (List String)

Take the remaining argument list, leaving only an empty list.

@[inline]

def Lake.consArg {m : Type → Type u_1} [MonadStateOf ArgList m] (arg : String) : m PUnit

Add a string to the head of the remaining argument list.

@[inline]

def Lake.shortOptionWithEq {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] {α : Type} (handle : Char → m α) (opt : String) : m α

Process a short option of the form -x=arg.

@[inline]

def Lake.shortOptionWithSpace {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] {α : Type} (handle : Char → m α) (opt : String) : m α

Process a short option of the form "-x arg".

@[inline]

def Lake.shortOptionWithArg {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] {α : Type} (handle : Char → m α) (opt : String) : m α

Process a short option of the form -xarg.

@[inline]

def Lake.multiShortOption {m : Type → Type u_1} [Monad m] (handle : Char → m PUnit) (opt : String) : m PUnit

Process a multiple short options grouped together (ex. -xyz as x, y, z).

@[inline]

def Lake.longOptionOrSpace {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] {α : Type} (handle : String → m α) (opt : String) : m α

Splits a long option of the form "--long foo bar" into --long and "foo bar".

@[inline]

def Lake.longOptionOrEq {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] {α : Type} (handle : String → m α) (opt : String) : m α

Splits a long option of the form --long=arg into --long and arg.

@[inline]

def Lake.longOption {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] {α : Type} (handle : String → m α) : String → m α

Process a long option of the form --long, --long=arg, "--long arg".

@[inline]

def Lake.shortOption {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] {α : Type} (shortHandle : Char → m α) (longHandle : String → m α) (opt : String) : m α

Process a short option of the form -x, -x=arg, -x arg, or -long.

@[inline]

def Lake.option {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] {α : Type} (handlers : OptionHandlers m α) (opt : String) : m α

Process an option, short or long, using the given handlers. An option is an argument of length > 1 starting with a dash (-). An option may consume additional elements of the argument list.

def Lake.processLeadingOption {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] (handle : String → m PUnit) : m PUnit

Process the head argument of the list using handle if it is an option.

partial def Lake.processLeadingOptions {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] (handle : String → m PUnit) : m PUnit

Process the leading options of the remaining argument list. Consumes empty leading arguments in the argument list.

partial def Lake.collectArgs {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] (option : String → m PUnit) (args : Array String := #[]) : m (Array String)

Process every option and collect the remaining arguments into an Array.

@[inline]

def Lake.processOptions {m : Type → Type u_1} [Monad m] [MonadStateOf ArgList m] (handle : String → m PUnit) : m PUnit

Process every option in the argument list.