Defines the abstract CLI interface for Lake.

Types

def Lake.ArgList : Type

Equations

• Lake.ArgList = List String

@[inline]

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

Equations

• Lake.ArgList.mk args = args

@[reducible, inline]

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

Equations

• Lake.ArgsT = StateT Lake.ArgList

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

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

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.

Equations

• Lake.getArgs = get

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

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

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

@[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, [])

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

@[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 (opt.get { byteIdx := 1 })

@[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 (opt.get { byteIdx := 1 })

@[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 (opt.get { byteIdx := 1 })

@[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 }

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

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

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

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

@[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 (opt.get { byteIdx := 1 } == '-') = true then Lake.longOption handlers.long opt else Lake.shortOption handlers.short handlers.longShort opt

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.

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.

Equations

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