TorchLean CLI Parser

Pure command-line parsers shared by examples, verification tools, and application API helpers. The definitions live directly under TorchLean.CLI.

This module stays independent of tensors and runtime modules so lightweight artifact checkers can reuse the CLI surface without importing the full public API.

def TorchLean.CLI.takeFlagValue? (arguments : List String) (key : String) : Except String (Option String × List String)

Take an optional --key value from an argument list.

Accepted forms:

• --key value
• --key=value

Duplicate occurrences are rejected. The returned argument list contains every unconsumed argument in its original order.

def TorchLean.CLI.takeFlagValue?.go (eqPrefix keyTok : String) : List String → Option String → List String → Except String (Option String × List String)

opaque TorchLean.CLI.takeFlagValue (arguments : List String) (key default : String) : Except String (String × List String)

Parse an optional string-valued flag and fall back to a provided default.

Use this when a command parser wants a concrete string immediately rather than an optional override.

opaque TorchLean.CLI.requireFlagValue (arguments : List String) (key : String) (missing? : Option String := none) : Except String (String × List String)

Parse a required string-valued flag and return the remaining arguments.

def TorchLean.CLI.flagValue? (arguments : List String) (key : String) : Except String (Option String)

Look up a string-valued flag without returning the remaining arguments.

This is useful for command shapes that support optional overrides but do not otherwise need a left-to-right consuming parser. Accepted forms are the same as takeFlagValue?: --key value and --key=value.

opaque TorchLean.CLI.takeParsedFlag {α : Type} (arguments : List String) (key default : String) (parse : String → Except String α) : Except String (α × List String)

Parse an optional string-valued flag, fall back to a provided default spelling when absent, and decode the selected spelling with a caller-supplied parser.

This is useful for enum-like CLI flags whose valid strings remain command-specific.

def TorchLean.CLI.hasFlagValue (arguments : List String) (key : String) : Bool

Return true when arguments contains --key value or --key=value.

def TorchLean.CLI.stripFlagValues (arguments keys : List String) : List String

Remove every occurrence of a string-valued flag, accepting both --key value and --key=value.

This is for wrapper commands that own a flag locally and forward the remaining arguments to another tool. It deliberately does not reject duplicates; the wrapper's local parser decides whether a duplicated flag is an error.

def TorchLean.CLI.stripFlagValues.go (keys : List String) : List String → List String

def TorchLean.CLI.takeBoolFlag (arguments : List String) (key : String) : Except String (Bool × List String)

Take a no-value boolean flag, returning whether it appeared.

def TorchLean.CLI.takeBoolFlag.go (keyTok : String) : List String → Bool → List String → Except String (Bool × List String)

def TorchLean.CLI.dropDashDash (arguments : List String) : List String

Drop the leading -- separator commonly used with lean --run.

def TorchLean.CLI.hasHelp (arguments : List String) : Bool

Return true when the argument list requests command help.

def TorchLean.CLI.checkNoArgs (arguments : List String) : Except String Unit

Fail if there are any unconsumed CLI arguments.

opaque TorchLean.CLI.takePositional? (arguments : List String) : Except String (Option String × List String)

Take at most one positional argument, leaving flags untouched.

This is useful for commands with a single optional artifact path plus named flags. A second positional argument is reported as an error instead of being silently ignored.

opaque TorchLean.CLI.takePositional (arguments : List String) (default : String) : Except String (String × List String)

Take one optional positional argument and fall back to default when it is absent.

def TorchLean.CLI.normalizePathFlag (arguments : List String) (key default : String) : List String

Normalize commands that accept either a positional path or a named path flag.

If --key / --key=... is already present, the argument list is returned unchanged. Otherwise the first positional argument is rewritten to --key=<path>. If there is no positional path, the provided default path is inserted.

opaque TorchLean.CLI.takeNatFlag? (arguments : List String) (key : String) : Except String (Option Nat × List String)

Take an optional natural-number flag.

opaque TorchLean.CLI.takeNatFlag (arguments : List String) (key : String) (default : Nat) : Except String (Nat × List String)

Parse an optional natural-number flag and fall back to the provided default.

def TorchLean.CLI.takePositiveNatFlag (arguments : List String) (exeName key : String) (default : Nat) : Except String (Nat × List String)

Parse an optional natural-number flag, fall back to a default, and require that the selected value is strictly positive.

def TorchLean.CLI.parseFloatLit? (s : String) : Option Float

Parse a signed decimal float literal.

The primary path accepts the same numeric syntax as Lean.Json, including scientific notation. The fallback accepts the CLI-friendly decimal form 1..

opaque TorchLean.CLI.takeFloatFlag? (arguments : List String) (key : String) : Except String (Option Float × List String)

Take an optional floating-point flag.

opaque TorchLean.CLI.takeFloatFlag (arguments : List String) (key : String) (default : Float) : Except String (Float × List String)

Parse an optional floating-point flag and fall back to the provided default.

opaque TorchLean.CLI.requireFloatFlag (arguments : List String) (key : String) (missing? : Option String := none) : Except String (Float × List String)

Parse a required floating-point flag and return the remaining arguments.

opaque TorchLean.CLI.takeBoolValueFlag? (arguments : List String) (key : String) : Except String (Option Bool × List String)

Take an optional explicitly valued boolean flag.

opaque TorchLean.CLI.takeBoolValueFlag (arguments : List String) (key : String) (default : Bool) : Except String (Bool × List String)

Parse an optional boolean-valued flag and fall back to the provided default.

opaque TorchLean.CLI.takeSwitch? (arguments : List String) (key : String) : Except String (Option Bool × List String)

Remove a boolean flag that may be written either as a bare switch or with an explicit value.

Accepted forms:

• --key
• --key=true
• --key=false
• --key true
• --key false

When --key is followed by a non-boolean token, the flag is treated as a bare switch and the next token is left for the caller. Duplicate occurrences are rejected.

opaque TorchLean.CLI.takeSwitch (arguments : List String) (key : String) (default : Bool) : Except String (Bool × List String)

Parse a bare-or-valued boolean flag and fall back to the provided default.

def TorchLean.CLI.takePositiveFloatFlag (arguments : List String) (exeName key : String) (default : Float) : Except String (Float × List String)

Parse an optional floating-point flag, fall back to the provided default, and require that the selected value is strictly positive.

def TorchLean.CLI.takeNonnegativeFloatFlag (arguments : List String) (exeName key : String) (default : Float) : Except String (Float × List String)

Parse an optional floating-point flag, fall back to the provided default, and require that the selected value is nonnegative.

opaque TorchLean.CLI.takePathFlag? (arguments : List String) (key : String) : Except String (Option System.FilePath × List String)

Take an optional path flag.

opaque TorchLean.CLI.takePathFlag (arguments : List String) (key : String) (default : System.FilePath) : Except String (System.FilePath × List String)

Parse an optional path flag and fall back to the provided default path.

Use this when an example parser wants a concrete path immediately instead of an optional override.

opaque TorchLean.CLI.requirePathFlag (arguments : List String) (key : String) (exeName : String := "") : Except String (System.FilePath × List String)

Parse a required path flag such as --data-file corpus.txt.

The error message includes exeName when provided.

def TorchLean.CLI.takePairedPathFlags (arguments : List String) (firstKey secondKey : String) : Except String ((Option System.FilePath × Option System.FilePath) × List String)

Parse two optional path flags that must appear together if either one is present.

This is useful for paired artifacts such as tokenizer vocab/merge files, where a single path is not meaningful on its own.

def TorchLean.CLI.takeSeed (arguments : List String) (default : Nat := 0) : Except String (Nat × List String)

Parse an optional --seed flag (defaults to the provided value).