Defines the abstract CLI interface for Lake.

# Types #

source
def Lake.ArgList :
Type
Equations

- Lake.ArgList = List String

Instances For

source
@[inline]
def Lake.ArgList.mk (args : List String) :
ArgList
Equations

- Lake.ArgList.mk args = args

Instances For

source
@[reducible, inline]
abbrev Lake.ArgsT (m : Type → Type u_1) (α : Type) :
Type u_1
Equations

- Lake.ArgsT = StateT Lake.ArgList

Instances For

source
@[inline]
def Lake.ArgsT.run {m : Type → Type u_1} {α : Type} (args : List String) (self : ArgsT m α) :
m (α × List String)
Equations

- Lake.ArgsT.run args self = StateT.run self args

Instances For

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

- Lake.ArgsT.run' args self = StateT.run' self args

Instances For

source
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`).

Instances For

# Utilities #

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

Get the remaining argument list.

Equations

- Lake.getArgs = get

Instances For

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

Replace the argument list.

Equations

- Lake.setArgs args = set (Lake.ArgList.mk args)

Instances For

source
@[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).

Equations

- Lake.takeArg? = modifyGet fun (x : Lake.ArgList) => match x with | [] => (none, []) | arg :: args => (some arg, args)

Instances For

source
@[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).

Equations

- Lake.takeArgD default = modifyGet fun (x : Lake.ArgList) => match x with | [] => (default, []) | arg :: args => (arg, args)

Instances For

source
@[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.

Equations

- Lake.takeArgs = modifyGet fun (args : List String) => (args, [])

Instances For

source
@[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.

Equations

- Lake.consArg arg = modify fun (args : List String) => arg :: args

Instances For

source
@[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`.

Equations

- Lake.shortOptionWithEq handle opt = do Lake.consArg (opt.drop 3) handle (String.Pos.Raw.get opt { byteIdx := 1 })

Instances For

source
@[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"`.

Equations

- Lake.shortOptionWithSpace handle opt = do Lake.consArg (opt.drop 2).trimLeft handle (String.Pos.Raw.get opt { byteIdx := 1 })

Instances For

source
@[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`.

Equations

- Lake.shortOptionWithArg handle opt = do Lake.consArg (opt.drop 2) handle (String.Pos.Raw.get opt { byteIdx := 1 })

Instances For

source
@[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`).

Equations

- Lake.multiShortOption handle opt = Lake.multiShortOption.loop✝ handle opt { byteIdx := 1 }

Instances For

source
@[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"`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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"`.

Equations

- Lake.longOption handle = Lake.longOptionOrEq (Lake.longOptionOrSpace handle)

Instances For

source
@[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`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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.

Equations

- Lake.option handlers opt = if (String.Pos.Raw.get opt { byteIdx := 1 } == '-') = true then Lake.longOption handlers.long opt else Lake.shortOption handlers.short handlers.longShort opt

Instances For

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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.

source
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`.

source
@[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.

Equations

- Lake.processOptions handle = do let __do_lift ← Lake.collectArgs handle Lake.setArgs __do_lift.toList

Instances For