From 839dc4509996775403005545eecd625af6ff36bb Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 2 Oct 2026 01:25:45 +0000 Subject: [PATCH 1/7] spec: env-var fallbacks and did-you-mean suggestions (SHAKE-PARSE-11, PARSE-12, HELP-3, ERR-3, ERR-4, ARGS-2 pending; TRUST-5) Co-authored-by: noah-emp --- SPEC.md | 15 ++- docs/rfc/shake-env-and-suggestions.md | 127 ++++++++++++++++++++++++++ 2 files changed, 139 insertions(+), 3 deletions(-) create mode 100644 docs/rfc/shake-env-and-suggestions.md diff --git a/SPEC.md b/SPEC.md index 0420beb..9bfc703 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,6 +1,6 @@ # shake specification -This is the list of every behavior shake guarantees, each under a stable requirement ID. Every requirement is about the interface in `main.bend`: its types, builders, `parse`, `check`, the readers, `help`, `err_text`, `help_path`, `err_path` and `argv`. Every module under `src/` is internal and carries no promise. +This is the list of every behavior shake guarantees, each under a stable requirement ID. Every requirement is about the interface in `main.bend`: its types, builders, `parse`, `parse_env`, `check`, the readers, `help`, `err_text`, `help_path`, `err_path`, `suggestion`, `argv` and `env_vars`. Every module under `src/` is internal and carries no promise. Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law (a `for` or `exs` binder) in `src/LAWS.bend` that passes the proof gate. A **Trusted** requirement is an assumption shake cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose laws have not all landed has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: the first line `bend src/PROOF.bend` prints is exactly `ALL PROOFS CHECK`. Tests and fixtures are never evidence for a requirement. @@ -8,7 +8,9 @@ A spec is **well-formed** when `check` reports nothing for it (SHAKE-SPEC-1). Th The words `parse` receives are what the program passes it. In a compiled program they come from `argv`, which drops the program name `IO.args` starts with, after the runtime has taken its own flags and the first `--` (SHAKE-TRUST-2). -The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](docs/rfc/shake-spec.md). The RFC also records the audit behind them and the rollout that proved every row. +An argument's **env var** is the name `env` gives it; an argument built without `env` has none. `parse_env` also receives **vars**, a list of name and value pairs, which in a compiled program come from `env_vars` (SHAKE-TRUST-5). An argument's **env value** is the value of the first pair in vars named by its env var, when that value is not empty; an env var no pair names, or whose first pair's value is empty, gives no env value. + +The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](docs/rfc/shake-spec.md). The RFC also records the audit behind them and the rollout that proved every row. The env and suggestion rows (SHAKE-PARSE-11, PARSE-12, HELP-3, ERR-3, ERR-4, ARGS-2, TRUST-5) are designed in [docs/rfc/shake-env-and-suggestions.md](docs/rfc/shake-env-and-suggestions.md). ## Format @@ -52,6 +54,8 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | SHAKE-PARSE-8 | Before `--` and before any positional of the current command is bound, a plain word `help`, or a word `--help` when no argument of the current command has the long spelling `help`, makes the parse fail with `NeedHelp{path}`, where `path` is the selected path followed by the remaining words, as long as each names a subcommand under the one before; the first remaining word that does not makes the parse fail with `Unexpected{word}`. A command that declares its own long `help` gets `--help` as that argument (SHAKE-TOK-1), and `help` still asks for help. | Proved | proved | src/LAWS.bend help_unknown; src/LAWS.bend help_step; src/LAWS.bend help_walk; src/LAWS.bend help_path; src/LAWS.bend dash_help_step; src/LAWS.bend dash_help_path | | SHAKE-PARSE-9 | Once a word makes the parse fail, the words after it do not change the error. | Proved | proved | src/LAWS.bend fail_stays | | SHAKE-PARSE-10 | A flag or an option built with `opt` that is given a second time while the same command is current, under any of its spellings, fails the parse with `Repeated{at, name}`; an argument of a parent command with the same name is a different argument (SHAKE-TOK-7). An option built with `many` binds every value given, in the order given, and `get_all` of its command's Matched reads them all. | Proved | proved | src/LAWS.bend repeated_long_flag; src/LAWS.bend repeated_long_opt; src/LAWS.bend letter_flag_again; src/LAWS.bend letter_opt_again; src/LAWS.bend long_binds; src/LAWS.bend letter_value; src/LAWS.bend letter_value_eq | +| SHAKE-PARSE-11 | `parse_env(spec, words, vars)` reads `words` exactly as `parse` reads them against `spec` with every argument's default, in every command, replaced by its **fallback**, and answers what that parse answers, except as SHAKE-PARSE-12 says. An argument's fallback is its env value when it has one and is not a flag; for a flag with an env value, `true` when that value, lowercased, is none of `0`, `false`, `no`, `off`, `n` and `f`, and no fallback otherwise; and for an argument with no env value, its default. So a value the words bind wins over the env value and the env value over the default (SHAKE-PARSE-6), an argument with a fallback is filled by it and needs nothing from the words to satisfy `required` (SHAKE-PARSE-7), a required positional with a fallback does not block a subcommand (SHAKE-PARSE-4), and `parse_env(spec, words, [])` is `parse(spec, words)`. | Proved | pending | | +| SHAKE-PARSE-12 | When the parse SHAKE-PARSE-11 describes succeeds and an argument other than a flag, of a command on the selected path, has an env value outside its nonempty choices that the command's Matched binds to it, `parse_env` fails instead with `BadValue{at, name, value}` of the first such argument, the root command first and each command's arguments in spec order, where `at` is the selected path. A word's value outside the choices never binds (SHAKE-PARSE-5), so only an argument filled from its env value can be bound to it. When that parse fails, `parse_env` fails with the same error. | Proved | pending | | ### Checking a spec (SHAKE-SPEC) @@ -72,6 +76,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | :---- | :---- | :---- | :---- | :---- | | SHAKE-HELP-1 | `help(spec, path)` renders the page of the command reached by following each name of `path` from the root through the subcommands, skipping a name that is not a subcommand where it stands. | Proved | proved | src/LAWS.bend help_page; src/LAWS.bend reach_child; src/LAWS.bend reach_skip | | SHAKE-HELP-2 | A page lists each subcommand of its command exactly once, in spec order, followed by `help`, and each flag and option exactly once, in spec order. Its usage line names each positional exactly once, in spec order, as `` when required and `[NAME]` otherwise, with `...` after a rest positional. | Proved | proved | src/LAWS.bend cmds_listed; src/LAWS.bend opts_listed; src/LAWS.bend usage_listed | +| SHAKE-HELP-3 | The Options line of a flag or option that has an env var `NAME` shows `[env: NAME]` after its help text, before its `[default: ...]` and `[possible values: ...]`, as clap's does; the line of one with no env var is what it would be without this row. A positional has no Options line (SHAKE-HELP-2), so its env var is not shown. | Proved | pending | | ### Errors (SHAKE-ERR) @@ -79,16 +84,19 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | :---- | :---- | :---- | :---- | :---- | | SHAKE-ERR-1 | `err_text(spec, err)` is empty exactly when `help_path(err)` is `Some`, that is, when the parse failed with a request for help. | Proved | proved | src/LAWS.bend err_text_help; src/LAWS.bend err_text_iff | | SHAKE-ERR-2 | For every error but a request for help, `err_path(err)` is the path of subcommands the parse had selected at the word that failed it, and `err_text(spec, err)` shows the usage line of the command at that path, as `help(spec, err_path(err))` does. | Proved | proved | src/LAWS.bend err_path_at; src/LAWS.bend err_text_usage; src/LAWS.bend help_page; src/LAWS.bend unknown_long; src/LAWS.bend unknown_short; src/LAWS.bend no_pos_left; src/LAWS.bend choice_refused; src/LAWS.bend flag_long_valued; src/LAWS.bend value_flag_shaped; src/LAWS.bend value_absent; src/LAWS.bend help_unknown; src/LAWS.bend long_no_name; src/LAWS.bend repeated_long_flag; src/LAWS.bend repeated_long_opt; src/LAWS.bend value_refused; src/LAWS.bend long_refused; src/LAWS.bend raw_no_pos; src/LAWS.bend raw_refused; src/LAWS.bend enter_missing; src/LAWS.bend required_missing; src/LAWS.bend letter_flag_eq; src/LAWS.bend letter_unknown; src/LAWS.bend letter_flag_again; src/LAWS.bend letter_opt_again; src/LAWS.bend letter_value_bad | +| SHAKE-ERR-3 | `suggestion(spec, err)` is `None` for every error but an `UnknownFlag{at, word}` whose word starts with `--` (SHAKE-TOK-1, TOK-7). For such a word, let `typed` be its chars after `--` up to its first `=`, and the **candidates** the long spellings of the flags and options of the command at `at`, reached as `help(spec, at)` reaches it (SHAKE-HELP-1), in spec order; a parent command's arguments, subcommands and `help` are not candidates. A candidate `c` is **close** when `0 < d` and `3 * d <= max(length(typed), length(c))`, where `d` is the optimal string alignment distance from `typed` to `c`: the fewest single-char insertions, deletions, substitutions and swaps of two adjacent chars that turn one into the other, editing no char twice. The suggestion is `Some{"--" ++ c}` for the close candidate with the least `d`, the first in spec order among equals, and `None` when no candidate is close. A short option word never gets one. | Proved | pending | | +| SHAKE-ERR-4 | When `suggestion(spec, err)` is `Some{s}`, `err_text(spec, err)` contains `s`. | Proved | pending | | ### The argument list (SHAKE-ARGS) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | | SHAKE-ARGS-1 | The copy `argv` makes of the words `IO.args` gives drops the first, the program as invoked, and keeps all the others, in order and unchanged: for every list, reading the copy back gives the list after its first word, and nothing for an empty list. | Proved | proved | src/LAWS.bend copy_keeps; src/LAWS.bend words_keeps | +| SHAKE-ARGS-2 | The names `env_vars(spec)` asks `IO.get_env` for are the env vars of the arguments that have one, the root command's arguments first and then each subcommand's, depth first, each command's arguments in spec order. | Proved | pending | | ## Left to prove -No row is pending. The RFC's Rollout and [docs/rfc/shake-walker-proofs.md](docs/rfc/shake-walker-proofs.md) say in which phase each row's laws land. Every walker law holds wherever the words before the word it is about leave the walker in the state its premise names. +SHAKE-PARSE-11, PARSE-12, HELP-3, ERR-3, ERR-4 and ARGS-2 are pending: their laws land with the code that implements them ([docs/rfc/shake-env-and-suggestions.md](docs/rfc/shake-env-and-suggestions.md), Rollout). Every other row is proved. The RFC's Rollout and [docs/rfc/shake-walker-proofs.md](docs/rfc/shake-walker-proofs.md) say in which phase each row's laws land. Every walker law holds wherever the words before the word it is about leave the walker in the state its premise names. ## Trust boundary @@ -100,3 +108,4 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | SHAKE-TRUST-2 | A program compiled by bend 2.0.34 hands `IO.args` the program as invoked (the process's `argv[0]`) followed by the process's words after it, except that at the first `--` it stops examining words, drops that `--` and passes every later word through unchanged; before that `--` it removes `--threads` and `--gpu` with the word after each (ending the process on a bad value), and ends the process before `main` on `--bend-help` and on `--gpu-build`. Every other word reaches `IO.args`, `--help` included. Run as `bend file.bend [args]`, `IO.args` is the file as given, then the arguments. | It is the C `main` bend emits (`main` in bend2/comp.ts and `IO.args` in bend2/effs/args.c), read from bend 2.0.34's source and confirmed against the demo; 2.0.29 stopped taking `--help` and 2.0.32 put the program first. It changes when bend does, so every bend bump rechecks it. | | SHAKE-TRUST-3 | The proof-gate runner fails the build unless the first line of `bend src/PROOF.bend` is `ALL PROOFS CHECK`. | It is the flake's `proofs` check, run by `nix flake check` in CI, which runs every PROOF.bend on the flake's bend and compares the first line; `ez prove` does the same once ez runs on bend 2.0.34. | | SHAKE-TRUST-4 | `argv` hands on exactly the list `IO.args` answers, through the copy SHAKE-ARGS-1 is about. | It is IO, which no law can reach: `argv` in `src/args.bend` is one `IO.bind` of `IO.args` into `words`, short enough to check by reading, and marked `# noqa: L001` for that reason. | +| SHAKE-TRUST-5 | `env_vars(spec)` answers, for each name it asks for (SHAKE-ARGS-2) and in that order, the pair of the name and the value `IO.get_env` answers for it, unchanged and empty included, and no pair for a name `IO.get_env` fails for. A program compiled by bend 2.0.34 answers `getenv`'s value for a variable that is set and fails for one that is not. | It is IO, which no law can reach: `env_vars` in `src/args.bend` is one `IO.bind` of `IO.get_env` per name, short enough to check by reading and marked `# noqa: L001`. What `IO.get_env` answers is `io_get_env_run` in bend2/effs/get_env.c, read from bend 2.0.34's source; every bend bump rechecks it, as for SHAKE-TRUST-2. | diff --git a/docs/rfc/shake-env-and-suggestions.md b/docs/rfc/shake-env-and-suggestions.md new file mode 100644 index 0000000..02d1d6b --- /dev/null +++ b/docs/rfc/shake-env-and-suggestions.md @@ -0,0 +1,127 @@ +# RFC: env-var fallbacks and "did you mean" for unknown flags + +Read at `f142895` on `main`, bend 2.0.34, bolt v1.11.0. Requested by the maintainer for bend-kit, as two clap features: `Arg::env` and the `suggestions` feature. + +## Draft Status + +**State:** Accepted; the rows are in SPEC.md as pending, and each turns proved as its laws land (see [Rollout](#rollout)). + +- [x] +- [x] +- [x] +- [x] +- [x] + +## Problem + +shake binds what the words give and fills what they leave with each argument's default (SHAKE-PARSE-6). clap also lets an argument name an environment variable: the words win, then the variable, then the default, and help shows `[env: NAME]`. And when a long option is misspelled clap says which one was meant. bend-kit wants both from shake. + +Four things in the existing system shape the answer. `parse` is pure, and every proved row is about it; the only IO is `argv`. Bend 2.0.34 can read one named variable (`IO.get_env`) but cannot list the environment. `Arg` is destructured positionally at about 250 sites in the laws and proofs. And whether a required positional blocks a subcommand is decided while the words are read (SHAKE-PARSE-4, `parse.req`), from the argument's default, so a variable that should stand in for the default has to be known before the walk starts, not only at the end. + +## Usage (caller's view) + +README: + +```bend +import shake@0.5.0.0/main.bend as Shake + +def spec() -> Shake.Cli: + Shake.app("hi", "Say hello.", None{}, + [Shake.env(Shake.opt("name", Some{"n"}, Some{"name"}, "Who to greet", False{}, + Some{"world"}, []), "HI_NAME"), + Shake.env(Shake.flag("loud", Some{"l"}, Some{"loud"}, "Shout"), "HI_LOUD")], + []) + +def main() -> IO(Unit): + do IO: + av : List<&2, String> <- Shake.argv() + ev : List<&2, String & String> <- Shake.env_vars(spec()) + IO.print(greet(Shake.parse_env(spec(), av, ev))) +``` + +`HI_NAME=Ada hi` prints `hello Ada`, `HI_NAME=Ada hi --name Bo` prints `hello Bo`, and `HI_NAME= hi` prints `hello world`. `hi --help` shows + +``` + -n, --name Who to greet [env: HI_NAME] [default: world] +``` + +and `hi --nmae Ada` fails with + +``` +error: unexpected argument '--nmae' found + + tip: a similar argument exists: '--name' + +Usage: hi [OPTIONS] +... +``` + +A program that renders its own errors reads the same tip with `Shake.suggestion(spec(), err)`. A pure test passes vars itself: `Shake.parse_env(spec(), [], [("HI_NAME", "Ada")])`. + +## Shape + +```bend +# src/cli.bend +type Fallback is Data: + Fallback{env: Maybe<&2, String>, default: Maybe<&2, String>} + +type Arg is Data: + Arg{name, short, long, kind, help, required, fallback: Fallback, choices} + +# main.bend, new +def env(+arg: S.Arg, +var: String) -> S.Arg +def parse_env(spec: S.Cli, words: List<&2, String>, vars: List<&2, String & String>) + -> Result<&2, &2, S.ParseErr, S.Matched> +def suggestion(+spec: S.Cli, err: S.ParseErr) -> Maybe<&2, String> +def env_vars(spec: S.Cli) -> IO(List<&2, String & String>) +``` + +**The env var sits beside the default.** `Arg`'s seventh field, the default, becomes `Fallback{env, default}`: both say what an argument falls back to when the words leave it unbound, and keeping them together leaves `Arg` at eight fields, so a destructuring that ignores the default (`_d`) does not change. The builders keep their signatures and build `Fallback{None{}, default}`; `env(arg, var)` sets the env var, as clap's `.env(var)` does, so no caller of a builder breaks. + +**`parse_env` resolves fallbacks, then runs the parse that exists.** `parse_env(spec, words, vars)` is `env.check(spec, vars, parse(resolve(spec, vars), words))`. `resolve` rewrites each argument's default to its fallback (SHAKE-PARSE-11); the walker, `finish`, and every proved row about `parse` are unchanged and apply to the resolved spec. This is also why a required positional whose variable is set does not block a subcommand: in the resolved spec it has a default. `env.check` passes every failure through, and turns a success into `BadValue` when an argument on the selected path is bound to an env value outside its choices (SHAKE-PARSE-12). Since a word's value outside the choices never binds (SHAKE-PARSE-5), such a binding can only have come from the variable. `parse(spec, words)` is `parse_env(spec, words, [])`, as a law, not a definition, so existing proofs do not move. + +**Policy is pure; IO is one fold.** Empty means unset, the flag literals, and the choices check all live in `resolve` and `env.check`, where laws reach them. `env_vars` asks `IO.get_env` for every env var the spec declares, in every command, since the selected path is not known until the words are read. It keeps the pairs that are set, and passes the values on unchanged (SHAKE-ARGS-2, SHAKE-TRUST-5). + +**The suggestion is derived, not stored.** `UnknownFlag{at, word}` already carries what a suggestion needs: `at` reaches the current command, as `err_text` reaches its usage line, and `word` holds the typed spelling. So `ParseErr`, the walker and every refusal law stay as they are. `suggestion` cuts the spelling at `=`, scores it against the long spellings of the flags and options of the command at `at`, and keeps the closest one that is close enough (SHAKE-ERR-3). `err_text` adds clap's tip line when there is one (SHAKE-ERR-4). SHAKE-ERR-1 still holds, because the tip only lengthens a text that was already nonempty. + +**Interface depth.** Four new defs. Each hides a policy the caller would otherwise reimplement: `env` hides where the variable is kept, `parse_env` hides precedence, emptiness, flag literals and choices, `env_vars` hides which names to read and in what order, and `suggestion` hides the candidate set, the distance and the threshold. None is a pass-through. + +**What it deliberately does not do.** It does not split an env value into several values for `many` or `rest` (one variable is one value). It does not suggest a short letter (`-x` has too little to compare), a parent command's argument, a subcommand for an unexpected word, or `--help`. `--help` is refused only after a positional is bound, so suggesting it there would suggest another refusal. It does not show env values in help, and it does not show a positional's env var, because shake's help has no Arguments block (see [Open questions](#open-questions-and-risks)). + +## Synthesis decision + +Three candidates were sketched: A (gpt-5.6), C (this author), and B (grok), which had not returned by the time of synthesis. **C is the base:** env applied by rewriting the spec in front of an unchanged `parse`, a post-check for choices, the suggestion derived from the spec and the error, and `parse` kept as it is. **From A:** the `Fallback{env, default}` pair in the default's slot, which C had as a ninth `Arg` field. It cuts the proof churn to the sites that read the default, and it groups two facts that answer one question. Also from A: excluding the synthetic `--help` from the candidates, and a strict first-in-spec-order tie break. **Rejected from A:** a third argument on `parse` (REVIEW-E1); counting an empty variable as set (REVIEW-E2); refusing env on flags in `check` (REVIEW-E3: clap supports it and it fits without changing `on`); a new Arguments block in help (scope beyond the request; an open question); and Jaro similarity. Jaro is clap's measure, but its matching window and transposition count are much harder to state in a row than an edit distance, and the maintainer asked for "edit distance / clap-like". A also checked the fallback against the choices inside `fill`, which changes `finish` and with it the proofs of SHAKE-PARSE-1, PARSE-6 and PARSE-7; C's post-check leaves them untouched. + +## Tradeoffs accepted + +- We accept two parse entry points, `parse` and `parse_env`, in exchange for no breaking change and every existing row applying unchanged. +- We accept `env_vars` reading the variables of commands that end up unselected in exchange for resolving fallbacks before the walk, which is what lets a set variable unblock a required positional. +- We accept that an env value outside its choices is reported only when the parse would otherwise succeed, so a missing argument is reported before a bad variable, in exchange for leaving `finish` and its proofs alone. +- We accept that the distance in SHAKE-ERR-3 is defined by the code that computes it, as every rendering in SHAKE-HELP is. The laws prove which candidate is chosen given the distance, not that the dynamic program matches the textbook recurrence. +- We accept the threshold `3 * d <= max(length(typed), length(c))`, which suggests `--name` for `--nmae` or `--nam` but nothing for a two-letter spelling, in exchange for one integer rule with no floating point. + +## Alternatives considered + +- **Look up env values in `fill` at the end of the parse** (A's choices check, and the obvious first shape). It is shallow in the wrong place: the walker decides subcommand blocking from defaults before `fill` runs, so a set variable could not unblock a required positional without threading vars through the walker's nine-field state. And the error path inside `fill` rewrites the proofs of three proved rows. +- **A third argument on `parse`.** One entry point instead of two, but every caller in the family breaks to gain a feature most do not use, and `parse(spec, words)` would mean nothing different from `parse(spec, words, [])`. +- **An env parameter on each builder.** It breaks every call of `opt`, `many`, `pos`, `rest` and `flag`, and spreads one optional fact across five signatures. +- **The suggestion as a field of `UnknownFlag`.** It is information `err_text` can derive. Storing it means the walker computes presentation, and every refusal law that names `UnknownFlag` changes. +- **One IO `parse_io(spec)` that reads argv and the environment and parses.** It is the deepest interface for a program, but it hides `argv` and `env_vars` from programs that build words or vars themselves, as tests and bend-kit do. It can be added later on top of these four. + +## Open questions and risks + +- Should help grow an Arguments block, as clap's has, so a positional's `[env: NAME]` and default can be shown? It changes every help page with positionals and SHAKE-HELP-2's laws, so it is left for its own change. +- Should a missing required argument really be reported before a bad env value? clap reports the bad value first. Changing it means the check moves into `finish` (see Alternatives). +- Proof cost sits in two places: the fold that picks the closest candidate (SHAKE-ERR-3), and `resolve` over the subcommand tree, needed to show `parse_env(spec, words, [])` is `parse(spec, words)`. Both are list inductions of the kind `check_listed` and `values_given` already needed. + +## Rollout + +| Step | What lands | Rows after | +| :---- | :---- | :---- | +| 1 | this RFC; the rows in SPEC.md as pending | SHAKE-PARSE-11, PARSE-12, HELP-3, ERR-3, ERR-4, ARGS-2 pending; SHAKE-TRUST-5 trusted | +| 2 | `Fallback`, `env`, `parse_env`, `env_vars`, `resolve`, `env.check`, help's `[env: NAME]`; the laws of PARSE-11, PARSE-12, HELP-3, ARGS-2 | those rows proved | +| 3 | `suggestion`, the distance and the tip in `err_text`; the laws of ERR-3, ERR-4 | no pending rows | + +## Next implementation step + +Change `Arg`'s default to `Fallback{env, default}` through `src/` and the laws, with the gate green and no behavior change, before adding anything that reads `env`. From e75f2b4013d37c428d66cc3c8d4e22e7c6ec097f Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 2 Oct 2026 01:31:07 +0000 Subject: [PATCH 2/7] refactor: an argument's default sits in Fallback{env, default}, behavior unchanged Arg keeps eight fields; laws that named a default generalize over the env var beside it. The gate and the demo are unchanged. Co-authored-by: noah-emp --- src/LAWS.bend | 74 +++++++++++----------- src/PROOF.bend | 163 ++++++++++++++++++++++++++++--------------------- src/check.bend | 2 +- src/cli.bend | 23 ++++--- src/grow.bend | 2 +- src/walk.bend | 6 +- 6 files changed, 152 insertions(+), 118 deletions(-) diff --git a/src/LAWS.bend b/src/LAWS.bend index 7b9576a..abc2962 100644 --- a/src/LAWS.bend +++ b/src/LAWS.bend @@ -528,7 +528,7 @@ law choice_refused: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +rest: List<&2, S.Arg> for h_at: {S.parse.walk(pre, S.parse.start(spec)) @@ -586,7 +586,7 @@ law flag_long_valued: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_at: {S.parse.walk(pre, S.parse.start(spec)) == S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen} : S.St} @@ -728,7 +728,7 @@ law repeated_long_flag: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_at: {S.parse.walk(pre, S.parse.start(spec)) == S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen} : S.St} @@ -765,7 +765,7 @@ law repeated_long_opt: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_at: {S.parse.walk(pre, S.parse.start(spec)) == S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen} : S.St} @@ -902,7 +902,7 @@ law pos_next: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +rest: List<&2, S.Arg> for h_at: {S.parse.walk(pre, S.parse.start(spec)) @@ -942,7 +942,7 @@ law pos_binds: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +rest: List<&2, S.Arg> for +found: Shake.Matched @@ -1001,7 +1001,7 @@ law raw_next: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +rest: List<&2, S.Arg> for h_at: {S.parse.walk(pre, S.parse.start(spec)) @@ -1036,7 +1036,7 @@ law raw_binds: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +rest: List<&2, S.Arg> for +found: Shake.Matched @@ -1095,7 +1095,7 @@ law raw_refused: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +rest: List<&2, S.Arg> for h_at: {S.parse.walk(pre, S.parse.start(spec)) @@ -1144,7 +1144,7 @@ law long_binds: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +found: Shake.Matched for h_at: {S.parse.walk(pre, S.parse.start(spec)) @@ -1215,7 +1215,7 @@ law long_refused: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_at: {S.parse.walk(pre, S.parse.start(spec)) == S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen} : S.St} @@ -1281,7 +1281,7 @@ law rest_next: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_at: {S.parse.walk(pre, S.parse.start(spec)) == S.St{S.Free{}, args, up, subs, path, bs, [S.Arg{nm, sh, lo, S.Rest{}, hp, req, dflt, cs}], False{}, seen} @@ -1315,7 +1315,7 @@ law rest_binds: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +found: Shake.Matched for h_at: {S.parse.walk(pre, S.parse.start(spec)) @@ -1352,7 +1352,7 @@ law rest_raw_next: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_at: {S.parse.walk(pre, S.parse.start(spec)) == S.St{S.Free{}, args, up, subs, path, bs, [S.Arg{nm, sh, lo, S.Rest{}, hp, req, dflt, cs}], True{}, seen} @@ -1384,7 +1384,7 @@ law rest_raw_binds: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +found: Shake.Matched for h_at: {S.parse.walk(pre, S.parse.start(spec)) @@ -1450,6 +1450,7 @@ law default_filled: for +kind: S.ArgKind for +hp: String for +req: Bool + for +ev: Maybe<&2, String> for +dd: String for +cs: List<&2, String> for +bs: List<&2, S.Bind> @@ -1459,7 +1460,8 @@ law default_filled: for h_done: {Shake.parse(spec, ws) == Done{found} : Result<&2, &2, Shake.ParseErr, Shake.Matched>} for h_fr: {Grow.gw.frame(S.parse.walk(ws, S.parse.start(spec))) == Grow.Frame{List.append(&2, S.Level, qs, - S.Level{List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, Some{dd}, cs} <> qa), bs} <> up), + S.Level{List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, Some{dd}}, cs} <> qa), + bs} <> up), List.append(&2, String, path, ms)} : Grow.Frame} for h_len: {List.length(&2, S.Level, up) == List.length(&2, String, path) : Nat} for h_pa: {none_named(pa, nn) == True{} : Bool} @@ -1484,7 +1486,7 @@ law bound_kept: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +bs: List<&2, S.Bind> for +up: List<&2, S.Level> @@ -1517,6 +1519,7 @@ law no_default: for +kind: S.ArgKind for +hp: String for +req: Bool + for +ev: Maybe<&2, String> for +cs: List<&2, String> for +bs: List<&2, S.Bind> for +up: List<&2, S.Level> @@ -1525,7 +1528,8 @@ law no_default: for h_done: {Shake.parse(spec, ws) == Done{found} : Result<&2, &2, Shake.ParseErr, Shake.Matched>} for h_fr: {Grow.gw.frame(S.parse.walk(ws, S.parse.start(spec))) == Grow.Frame{List.append(&2, S.Level, qs, - S.Level{List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, None{}, cs} <> qa), bs} <> up), + S.Level{List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, None{}}, cs} <> qa), + bs} <> up), List.append(&2, String, path, ms)} : Grow.Frame} for h_len: {List.length(&2, S.Level, up) == List.length(&2, String, path) : Nat} for h_pa: {none_named(pa, nn) == True{} : Bool} @@ -1569,7 +1573,7 @@ law required_present: for +lo: Maybe<&2, String> for +kind: S.ArgKind for +hp: String - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +bs: List<&2, S.Bind> for +up: List<&2, S.Level> @@ -1599,7 +1603,7 @@ law required_missing: for +lo: Maybe<&2, String> for +kind: S.ArgKind for +hp: String - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +bs: List<&2, S.Bind> for +up: List<&2, S.Level> @@ -1617,7 +1621,7 @@ law required_missing: # whether a pending positional blocks a subcommand: required, with no # default, and not a rest def blocks(aa: S.Arg) -> Bool: - S.Arg{_n, _s, _l, kind, _h, req, dflt, _c} = aa + S.Arg{_n, _s, _l, kind, _h, req, S.Fallback{_e, dflt}, _c} = aa Bool.and(Bool.not(S.rest.is.kind(kind)), Bool.and(req, Maybe.is_none(&2, String, dflt))) # whether no pending positional blocks a subcommand @@ -1646,11 +1650,13 @@ law first_blocking: for +lo: Maybe<&2, String> for +kind: S.ArgKind for +hp: String + for +ev: Maybe<&2, String> for +cs: List<&2, String> for +qa: List<&2, S.Arg> for +h_pa: {none_block(pa) == True{} : Bool} for h_kind: {S.rest.is.kind(kind) == False{} : Bool} - {S.parse.first_req(List.append(&2, S.Arg, pa, S.Arg{nm, sh, lo, kind, hp, True{}, None{}, cs} <> qa)) == Some{nm} + {S.parse.first_req(List.append(&2, S.Arg, pa, S.Arg{nm, sh, lo, kind, hp, True{}, S.Fallback{ev, None{}}, + cs} <> qa)) == Some{nm} : Maybe<&2, String>} # LAW: wherever the words before it leave the walker free before `--`, a plain @@ -1894,7 +1900,7 @@ law help_word_next: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +rest: List<&2, S.Arg> for h_at: {S.parse.walk(pre, S.parse.start(spec)) @@ -1925,7 +1931,7 @@ law help_word_binds: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for +rest: List<&2, S.Arg> for +found: Shake.Matched @@ -1999,7 +2005,7 @@ law letter_flag: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_found: {S.by_short(args, SCon{cc, SNil{}}) == Some{S.Arg{nn, sh, lo, S.Flag{}, hp, req, dflt, cs}} : Maybe<&2, S.Arg>} @@ -2030,7 +2036,7 @@ law letter_flag_eq: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_found: {S.by_short(args, SCon{cc, SNil{}}) == Some{S.Arg{nn, sh, lo, S.Flag{}, hp, req, dflt, cs}} : Maybe<&2, S.Arg>} @@ -2081,7 +2087,7 @@ law letter_flag_again: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_found: {S.by_short(args, SCon{cc, SNil{}}) == Some{S.Arg{nn, sh, lo, S.Flag{}, hp, req, dflt, cs}} : Maybe<&2, S.Arg>} @@ -2110,7 +2116,7 @@ law letter_opt_again: for +lo: Maybe<&2, String> for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_found: {S.by_short(args, SCon{cc, SNil{}}) == Some{S.Arg{nn, sh, lo, S.Opt{}, hp, req, dflt, cs}} : Maybe<&2, S.Arg>} @@ -2142,7 +2148,7 @@ law letter_value: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_found: {S.by_short(args, SCon{cc, SNil{}}) == Some{S.Arg{nn, sh, lo, kind, hp, req, dflt, cs}} : Maybe<&2, S.Arg>} @@ -2177,7 +2183,7 @@ law letter_value_eq: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_found: {S.by_short(args, SCon{cc, SNil{}}) == Some{S.Arg{nn, sh, lo, kind, hp, req, dflt, cs}} : Maybe<&2, S.Arg>} @@ -2206,7 +2212,7 @@ law letter_value_next: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_found: {S.by_short(args, SCon{cc, SNil{}}) == Some{S.Arg{nn, sh, lo, kind, hp, req, dflt, cs}} : Maybe<&2, S.Arg>} @@ -2236,7 +2242,7 @@ law letter_value_bad: for +kind: S.ArgKind for +hp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: S.Fallback for +cs: List<&2, String> for h_found: {S.by_short(args, SCon{cc, SNil{}}) == Some{S.Arg{nn, sh, lo, kind, hp, req, dflt, cs}} : Maybe<&2, S.Arg>} @@ -2510,7 +2516,7 @@ def arg_reports( aa: S.Arg, after: List<&2, K.SpecErr> ) -> List<&2, K.SpecErr>: - S.Arg{+name, +short, +long, _k, _h, _r, dflt, +cs} = aa + S.Arg{+name, +short, +long, _k, _h, _r, S.Fallback{_e, dflt}, +cs} = aa K.both(K.one(List.contains(~String, ~String.eq, arg_names(before), name), K.SameName{path, name}), K.both(K.one(K.spelled.seen(short, arg_shorts(before)), K.SameShort{path, S.text.of(short, "")}), K.both(K.one(K.spelled.seen(long, arg_longs(before)), K.SameLong{path, S.text.of(long, "")}), @@ -2646,7 +2652,7 @@ def is_default(args: List<&2, S.Arg>, +name: String, +vv: String) -> Bool: case Nil{}: False{} case Con{hh, tt}: - S.Arg{nn, _s, _l, _k, _h, _r, dd, _c} = hh + S.Arg{nn, _s, _l, _k, _h, _r, S.Fallback{_e, dd}, _c} = hh Bool.or(Bool.and(String.eq(nn, name), default_is(dd, vv)), is_default(tt, name, vv)) # whether a binding's value is `true`, which a flag binds, a piece of one of diff --git a/src/PROOF.bend b/src/PROOF.bend index 403fc86..5b2c144 100644 --- a/src/PROOF.bend +++ b/src/PROOF.bend @@ -560,7 +560,7 @@ def choice_refused.step( +kind: S.ArgKind, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +rest: List<&2, S.Arg>, h_dd: {String.eq(tok, "--") == False{} : Bool}, @@ -671,7 +671,7 @@ def flag_long_valued.step( +lo: Maybe<&2, String>, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, h_dd: {String.eq("--" ++ body, "--") == False{} : Bool}, h_cut: {S.cut_eq(body) == (name, Some{vv}) : String & Maybe<&2, String>}, @@ -905,7 +905,7 @@ def repeated_long_flag.step( +lo: Maybe<&2, String>, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, h_dd: {String.eq("--" ++ body, "--") == False{} : Bool}, h_cut: {S.cut_eq(body) == (name, val) : String & Maybe<&2, String>}, @@ -977,7 +977,7 @@ def repeated_long_opt.step( +lo: Maybe<&2, String>, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, h_dd: {String.eq("--" ++ body, "--") == False{} : Bool}, h_cut: {S.cut_eq(body) == (name, val) : String & Maybe<&2, String>}, @@ -1461,7 +1461,7 @@ def pos.take( +kind: S.ArgKind, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +rest: List<&2, S.Arg>, h_ok: {S.allowed(cs, tok) == True{} : Bool} @@ -1493,7 +1493,7 @@ def pos.step( +kind: S.ArgKind, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +rest: List<&2, S.Arg>, h_dd: {String.eq(tok, "--") == False{} : Bool}, @@ -1681,7 +1681,7 @@ def raw_refused.step( +kind: S.ArgKind, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +rest: List<&2, S.Arg>, h_bad: {S.allowed(cs, tok) == False{} : Bool} @@ -1796,7 +1796,7 @@ def long.step( +kind: S.ArgKind, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, h_dd: {String.eq("--" ++ body, "--") == False{} : Bool}, h_cut: {S.cut_eq(body) == (name, Some{vv}) : String & Maybe<&2, String>}, @@ -1960,7 +1960,7 @@ def long_refused.step( +kind: S.ArgKind, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, h_dd: {String.eq("--" ++ body, "--") == False{} : Bool}, h_cut: {S.cut_eq(body) == (name, Some{vv}) : String & Maybe<&2, String>}, @@ -2123,7 +2123,7 @@ def rest.arg( +lo: Maybe<&2, String>, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String> ) -> S.Arg: S.Arg{nm, sh, lo, S.Rest{}, hp, req, dflt, cs} @@ -2142,7 +2142,7 @@ def rest.walk( +lo: Maybe<&2, String>, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +h_plain: {Walk.all_plain(fs) == True{} : Bool}, +h_sub: {Walk.wk.unfound(subs, fs) == True{} : Bool}, @@ -2188,7 +2188,7 @@ def rest.raw( +lo: Maybe<&2, String>, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +h_ok: {Laws.all_allowed(cs, fs) == True{} : Bool} ) -> {S.parse.walk(fs, S.St{S.Free{}, args, up, subs, path, bs, [rest.arg(nm, sh, lo, hp, req, dflt, cs)], True{}, @@ -2693,7 +2693,7 @@ def fin.fill_other( {==} case Con{hh, +tt}: match hh: - case S.Arg{+mm, _s, _l, _k, _h, _r, dd, _c}: + case S.Arg{+mm, _s, _l, _k, _h, _r, S.Fallback{_e, dd}, _c}: Equal.trans(List<&2, String>, S.get_all.bind(S.fill.arg.go(dd, mm, S.fill.args(tt, bs)), nn), S.get_all.bind(S.fill.args(tt, bs), nn), S.get_all.bind(bs, nn), fin.go_other(dd, mm, S.fill.args(tt, bs), nn, fin.named_head(mm, tt, nn, h_none)), @@ -2711,7 +2711,7 @@ def fin.fill_other_b( {==} case Con{hh, +tt}: match hh: - case S.Arg{+mm, _s, _l, _k, _h, _r, dd, _c}: + case S.Arg{+mm, _s, _l, _k, _h, _r, S.Fallback{_e, dd}, _c}: Equal.trans(Bool, S.bound(S.fill.arg.go(dd, mm, S.fill.args(tt, bs)), nn), S.bound(S.fill.args(tt, bs), nn), S.bound(bs, nn), fin.go_other_b(dd, mm, S.fill.args(tt, bs), nn, fin.named_head(mm, tt, nn, h_none)), @@ -2732,7 +2732,7 @@ def fin.fill_pre( {==} case Con{hh, +tt}: match hh: - case S.Arg{+mm, _s, _l, _k, _h, _r, dd, _c}: + case S.Arg{+mm, _s, _l, _k, _h, _r, S.Fallback{_e, dd}, _c}: +ff = S.fill.args(List.append(&2, S.Arg, tt, rest), bs) Equal.trans(List<&2, String>, S.get_all.bind(S.fill.arg.go(dd, mm, ff), nn), S.get_all.bind(ff, nn), S.get_all.bind(S.fill.args(rest, bs), nn), @@ -2763,13 +2763,15 @@ def fin.fill_default( +kind: S.ArgKind, +hp: String, +req: Bool, + +ev: Maybe<&2, String>, +dd: String, +cs: List<&2, String>, +bs: List<&2, S.Bind>, h_pa: {Laws.none_named(pa, nn) == True{} : Bool}, +h_qa: {Laws.none_named(qa, nn) == True{} : Bool}, +h_free: {S.bound(bs, nn) == False{} : Bool} -) -> {S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, Some{dd}, cs} <> qa), bs), +) -> {S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, + Some{dd}}, cs} <> qa), bs), nn) == [dd] : List<&2, String>}: +ff = S.fill.args(qa, bs) e1 = Equal.sym(Bool, S.bound(ff, nn), False{}, @@ -2779,10 +2781,11 @@ def fin.fill_default( Equal.trans(List<&2, String>, S.get_all.bind(ff, nn), S.get_all.bind(bs, nn), [], fin.fill_other(qa, bs, nn, h_qa), fin.g_unbound(bs, nn, h_free))) Equal.trans(List<&2, String>, - S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, Some{dd}, cs} <> qa), + S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, Some{dd}}, + cs} <> qa), bs), nn), S.get_all.bind(S.fill.one(S.bound(ff, nn), nn, dd, ff), nn), [dd], - fin.fill_pre(pa, S.Arg{nn, sh, lo, kind, hp, req, Some{dd}, cs} <> qa, bs, nn, h_pa), + fin.fill_pre(pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, Some{dd}}, cs} <> qa, bs, nn, h_pa), fin.fill_default.go(nn, dd, ff, e1, e2, e3)) # a bound argument's values, with or without a default @@ -2812,7 +2815,7 @@ def fin.fill_kept( +kind: S.ArgKind, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +bs: List<&2, S.Bind>, h_pa: {Laws.none_named(pa, nn) == True{} : Bool}, @@ -2820,13 +2823,17 @@ def fin.fill_kept( h_bound: {S.bound(bs, nn) == True{} : Bool} ) -> {S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, dflt, cs} <> qa), bs), nn) == S.get_all.bind(bs, nn) : List<&2, String>}: - +ff = S.fill.args(qa, bs) - Equal.trans(List<&2, String>, - S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, dflt, cs} <> qa), bs), nn), - S.get_all.bind(S.fill.arg.go(dflt, nn, ff), nn), S.get_all.bind(bs, nn), - fin.fill_pre(pa, S.Arg{nn, sh, lo, kind, hp, req, dflt, cs} <> qa, bs, nn, h_pa), - fin.kept_go(dflt, nn, ff, bs, fin.fill_other(qa, bs, nn, h_qa), - Equal.trans(Bool, S.bound(ff, nn), S.bound(bs, nn), True{}, fin.fill_other_b(qa, bs, nn, h_qa), h_bound))) + match dflt: + case S.Fallback{+ev, +dm}: + +ff = S.fill.args(qa, bs) + Equal.trans(List<&2, String>, + S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dm}, + cs} <> qa), + bs), nn), + S.get_all.bind(S.fill.arg.go(dm, nn, ff), nn), S.get_all.bind(bs, nn), + fin.fill_pre(pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dm}, cs} <> qa, bs, nn, h_pa), + fin.kept_go(dm, nn, ff, bs, fin.fill_other(qa, bs, nn, h_qa), + Equal.trans(Bool, S.bound(ff, nn), S.bound(bs, nn), True{}, fin.fill_other_b(qa, bs, nn, h_qa), h_bound))) # an argument with no default keeps exactly its values def fin.fill_nodef( @@ -2838,16 +2845,20 @@ def fin.fill_nodef( +kind: S.ArgKind, +hp: String, +req: Bool, + +ev: Maybe<&2, String>, +cs: List<&2, String>, +bs: List<&2, S.Bind>, h_pa: {Laws.none_named(pa, nn) == True{} : Bool}, h_qa: {Laws.none_named(qa, nn) == True{} : Bool} -) -> {S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, None{}, cs} <> qa), bs), +) -> {S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, None{}}, + cs} <> qa), bs), nn) == S.get_all.bind(bs, nn) : List<&2, String>}: Equal.trans(List<&2, String>, - S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, None{}, cs} <> qa), bs), nn), + S.get_all.bind(S.fill.args(List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, None{}}, + cs} <> qa), bs), nn), S.get_all.bind(S.fill.args(qa, bs), nn), S.get_all.bind(bs, nn), - fin.fill_pre(pa, S.Arg{nn, sh, lo, kind, hp, req, None{}, cs} <> qa, bs, nn, h_pa), fin.fill_other(qa, bs, + fin.fill_pre(pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, None{}}, cs} <> qa, bs, nn, h_pa), + fin.fill_other(qa, bs, nn, h_qa)) # the frame of the walker the words leave: levels `qs` in front of the level @@ -2997,6 +3008,7 @@ def Laws.default_filled( kind, hp, req, + ev, dd, cs, bs, @@ -3010,10 +3022,10 @@ def Laws.default_filled( h_qa, h_free ): - +args = List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, Some{dd}, cs} <> qa) + +args = List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, Some{dd}}, cs} <> qa) fin.back(found, path, nn, S.get_all.bind(S.fill.args(args, bs), nn), [dd], fin.all(spec, ws, found, qs, args, bs, up, path, ms, nn, h_done, h_fr, h_len), - fin.fill_default(pa, qa, nn, sh, lo, kind, hp, req, dd, cs, bs, h_pa, h_qa, h_free)) + fin.fill_default(pa, qa, nn, sh, lo, kind, hp, req, ev, dd, cs, bs, h_pa, h_qa, h_free)) def Laws.bound_kept( spec, @@ -3060,6 +3072,7 @@ def Laws.no_default( kind, hp, req, + ev, cs, bs, up, @@ -3071,11 +3084,11 @@ def Laws.no_default( h_pa, h_qa ): - +args = List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, None{}, cs} <> qa) + +args = List.append(&2, S.Arg, pa, S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, None{}}, cs} <> qa) fin.back_bs(found, path, nn, bs, fin.back(found, path, nn, S.get_all.bind(S.fill.args(args, bs), nn), S.get_all.bind(bs, nn), fin.all(spec, ws, found, qs, args, bs, up, path, ms, nn, h_done, h_fr, h_len), - fin.fill_nodef(pa, qa, nn, sh, lo, kind, hp, req, cs, bs, h_pa, h_qa))) + fin.fill_nodef(pa, qa, nn, sh, lo, kind, hp, req, ev, cs, bs, h_pa, h_qa))) def Laws.no_argument(spec, ws, found, qs, args, nn, bs, up, path, ms, h_done, h_fr, h_len, h_none): fin.back_bs(found, path, nn, bs, @@ -3208,7 +3221,7 @@ def fin.req_args( +lo: Maybe<&2, String>, +kind: S.ArgKind, +hp: String, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +qa: List<&2, S.Arg> ) -> List<&2, S.Arg>: @@ -3223,7 +3236,7 @@ def fin.miss_req( +lo: Maybe<&2, String>, +kind: S.ArgKind, +hp: String, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +fb: List<&2, S.Bind>, hh: {S.miss.args(fin.req_args(pa, nn, sh, lo, kind, hp, dflt, cs, qa), fb) == None{} : Maybe<&2, String>} @@ -3360,7 +3373,7 @@ def fin.miss_args_some( +lo: Maybe<&2, String>, +kind: S.ArgKind, +hp: String, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +fb: List<&2, S.Bind>, +h_unbound: {S.bound(fb, nn) == False{} : Bool} @@ -3654,6 +3667,7 @@ def Laws.enter_missing( def blk.req( rk: Bool, req: Bool, + +ev: Maybe<&2, String>, dflt: Maybe<&2, String>, +nm: String, +sh: Maybe<&2, String>, @@ -3662,7 +3676,8 @@ def blk.req( +hp: String, +cs: List<&2, String>, hh: {Bool.not(Bool.and(Bool.not(rk), Bool.and(req, Maybe.is_none(&2, String, dflt)))) == True{} : Bool} -) -> {S.parse.first_req.skip(rk, S.Arg{nm, sh, lo, kind, hp, req, dflt, cs}) == None{} : Maybe<&2, String>}: +) -> {S.parse.first_req.skip(rk, S.Arg{nm, sh, lo, kind, hp, req, S.Fallback{ev, dflt}, cs}) == None{} : Maybe<&2, + String>}: match rk: case True{}: {==} @@ -3675,14 +3690,15 @@ def blk.req( case Some{_d}: {==} case None{}: - Empty.absurd({S.parse.first_req.skip(False{}, S.Arg{nm, sh, lo, kind, hp, True{}, None{}, cs}) == None{} + Empty.absurd({S.parse.first_req.skip(False{}, S.Arg{nm, sh, lo, kind, hp, True{}, S.Fallback{ev, + None{}}, cs}) == None{} : Maybe<&2, String>}, Walk.wk.false_true(hh)) # the same, from the argument's kind def blk.skip( +kind: S.ArgKind, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +nm: String, +sh: Maybe<&2, String>, +lo: Maybe<&2, String>, @@ -3691,13 +3707,15 @@ def blk.skip( hh: {Bool.not(Laws.blocks(S.Arg{nm, sh, lo, kind, hp, req, dflt, cs})) == True{} : Bool} ) -> {S.parse.first_req.skip(S.rest.is.kind(kind), S.Arg{nm, sh, lo, kind, hp, req, dflt, cs}) == None{} : Maybe<&2, String>}: - blk.req(S.rest.is.kind(kind), req, dflt, nm, sh, lo, kind, hp, cs, hh) + match dflt: + case S.Fallback{+ev, dm}: + blk.req(S.rest.is.kind(kind), req, ev, dm, nm, sh, lo, kind, hp, cs, hh) # past a positional that does not block, the first blocking one is the rest's def blk.past( +kind: S.ArgKind, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +nm: String, +sh: Maybe<&2, String>, +lo: Maybe<&2, String>, @@ -3725,22 +3743,23 @@ def Laws.none_blocking(pos, h_none): Walk.wk.and_l(Bool.not(Laws.blocks(ab)), Laws.none_block(tt), h_none)), Laws.none_blocking(tt, Walk.wk.and_r(Bool.not(Laws.blocks(ab)), Laws.none_block(tt), h_none))) -def Laws.first_blocking(pa, nm, sh, lo, kind, hp, cs, qa, h_pa, h_kind): +def Laws.first_blocking(pa, nm, sh, lo, kind, hp, ev, cs, qa, h_pa, h_kind): match pa: case Nil{}: ee = Equal.sym(Bool, S.rest.is.kind(kind), False{}, h_kind) - %ee : {S.parse.first_req.at(S.parse.first_req.skip(_, S.Arg{nm, sh, lo, kind, hp, True{}, None{}, cs}), + %ee : {S.parse.first_req.at(S.parse.first_req.skip(_, S.Arg{nm, sh, lo, kind, hp, True{}, S.Fallback{ev, + None{}}, cs}), S.parse.first_req(qa)) == Some{nm} : Maybe<&2, String>} {==} case Con{hd, +tt}: match hd: case S.Arg{+n2, +s2, +l2, +k2, +h2, +r2, +d2, +c2}: +ab = {S.Arg{n2, s2, l2, k2, h2, r2, d2, c2} : S.Arg} - +rest = List.append(&2, S.Arg, tt, S.Arg{nm, sh, lo, kind, hp, True{}, None{}, cs} <> qa) + +rest = List.append(&2, S.Arg, tt, S.Arg{nm, sh, lo, kind, hp, True{}, S.Fallback{ev, None{}}, cs} <> qa) Equal.trans(Maybe<&2, String>, S.parse.first_req(ab <> rest), S.parse.first_req(rest), Some{nm}, blk.past(k2, r2, d2, n2, s2, l2, h2, c2, rest, Walk.wk.and_l(Bool.not(Laws.blocks(ab)), Laws.none_block(tt), h_pa)), - Laws.first_blocking(tt, nm, sh, lo, kind, hp, cs, qa, + Laws.first_blocking(tt, nm, sh, lo, kind, hp, ev, cs, qa, Walk.wk.and_r(Bool.not(Laws.blocks(ab)), Laws.none_block(tt), h_pa), h_kind)) @@ -4032,7 +4051,7 @@ def hw.full( +kind: S.ArgKind, +hp: String, +req: Bool, - +dflt: Maybe<&2, String>, + +dflt: S.Fallback, +cs: List<&2, String>, +rest: List<&2, S.Arg>, h_sub: {S.find_sub(subs, "help") == None{} : Maybe<&2, S.Sub>}, @@ -5096,7 +5115,7 @@ def sc.args( {==} case Con{hh, +tt}: match hh: - case S.Arg{+name, +short, +long, +kind, +help, +req, +dflt, +cs}: + case S.Arg{+name, +short, +long, +kind, +help, +req, S.Fallback{+ev, +dflt}, +cs}: Equal.cong(List<&2, K.SpecErr>, List<&2, K.SpecErr>, zz => K.both( K.one(List.contains(~String, ~String.eq, Laws.arg_names(before), name), K.SameName{path, name}), @@ -5107,13 +5126,15 @@ def sc.args( K.args.dups(tt, path, name <> Laws.arg_names(before), K.spelled.add(short, Laws.arg_shorts(before)), K.spelled.add(long, Laws.arg_longs(before)))), K.both(Laws.off_choice(path, name, cs, dflt), - Laws.args_reports(tt, path, S.Arg{name, short, long, kind, help, req, dflt, cs} <> before)), + Laws.args_reports(tt, path, S.Arg{name, short, long, kind, help, req, S.Fallback{ev, dflt}, + cs} <> before)), sc.both(K.args.default(dflt, cs, path, name), Laws.off_choice(path, name, cs, dflt), K.args.dups(tt, path, name <> Laws.arg_names(before), K.spelled.add(short, Laws.arg_shorts(before)), K.spelled.add(long, Laws.arg_longs(before))), - Laws.args_reports(tt, path, S.Arg{name, short, long, kind, help, req, dflt, cs} <> before), + Laws.args_reports(tt, path, S.Arg{name, short, long, kind, help, req, S.Fallback{ev, dflt}, + cs} <> before), sc.dflt(path, name, cs, dflt), - sc.args(tt, path, S.Arg{name, short, long, kind, help, req, dflt, cs} <> before))) + sc.args(tt, path, S.Arg{name, short, long, kind, help, req, S.Fallback{ev, dflt}, cs} <> before))) # the positional reports, from the positionals before def sc.pos( @@ -6515,13 +6536,13 @@ def gv.given_mono( match hd: case S.Bind{+nn, +vv}: match aa: - case S.Arg{+an, +sh, +lo, +kind, +hp, +req, +ad, +cs}: - gv.and_tt(Laws.given(ws, S.Arg{an, sh, lo, kind, hp, req, ad, cs} <> tt, S.Bind{nn, vv}), - Laws.all_given(xt, ws, S.Arg{an, sh, lo, kind, hp, req, ad, cs} <> tt), + case S.Arg{+an, +sh, +lo, +kind, +hp, +req, S.Fallback{+ev, +ad}, +cs}: + gv.and_tt(Laws.given(ws, S.Arg{an, sh, lo, kind, hp, req, S.Fallback{ev, ad}, cs} <> tt, S.Bind{nn, vv}), + Laws.all_given(xt, ws, S.Arg{an, sh, lo, kind, hp, req, S.Fallback{ev, ad}, cs} <> tt), gv.dmono(String.eq(vv, "true"), Laws.piece(ws, vv), Bool.and(String.eq(an, nn), Laws.default_is(ad, vv)), Laws.is_default(tt, nn, vv), gv.and_l(Laws.given(ws, tt, S.Bind{nn, vv}), Laws.all_given(xt, ws, tt), hh)), - gv.given_mono(xt, ws, S.Arg{an, sh, lo, kind, hp, req, ad, cs}, tt, + gv.given_mono(xt, ws, S.Arg{an, sh, lo, kind, hp, req, S.Fallback{ev, ad}, cs}, tt, gv.and_r(Laws.given(ws, tt, S.Bind{nn, vv}), Laws.all_given(xt, ws, tt), hh))) # an argument's own default is given @@ -6569,15 +6590,16 @@ def gv.fill( gv.all_given(bs, ws, [], hh) case Con{aa, +tt}: match aa: - case S.Arg{+an, +sh, +lo, +kind, +hp, +req, ad, +cs}: + case S.Arg{+an, +sh, +lo, +kind, +hp, +req, S.Fallback{+ev, ad}, +cs}: match ad: case None{}: - gv.given_mono(S.fill.args(tt, bs), ws, S.Arg{an, sh, lo, kind, hp, req, None{}, cs}, tt, + gv.given_mono(S.fill.args(tt, bs), ws, S.Arg{an, sh, lo, kind, hp, req, S.Fallback{ev, None{}}, cs}, tt, gv.fill(tt, bs, ws, hh)) case Some{+dv}: gv.fone(S.bound(S.fill.args(tt, bs), an), an, dv, S.fill.args(tt, bs), ws, - S.Arg{an, sh, lo, kind, hp, req, Some{dv}, cs} <> tt, - gv.given_mono(S.fill.args(tt, bs), ws, S.Arg{an, sh, lo, kind, hp, req, Some{dv}, cs}, tt, + S.Arg{an, sh, lo, kind, hp, req, S.Fallback{ev, Some{dv}}, cs} <> tt, + gv.given_mono(S.fill.args(tt, bs), ws, S.Arg{an, sh, lo, kind, hp, req, S.Fallback{ev, Some{dv}}, + cs}, tt, gv.fill(tt, bs, ws, hh)), gv.dself(String.eq(dv, "true"), Laws.piece(ws, dv), an, dv, Laws.is_default(tt, an, dv))) @@ -7740,7 +7762,7 @@ def gn.dsub(tt: List<&2, S.Arg>, +args: List<&2, S.Arg>) -> Bool: case Nil{}: True{} case Con{aa, rest}: - S.Arg{+an, _s, _l, _k, _h, _r, dd, _c} = aa + S.Arg{+an, _s, _l, _k, _h, _r, S.Fallback{_e, dd}, _c} = aa Bool.and(gn.dcase(dd, an, args), gn.dsub(rest, args)) # a default of some arguments is a default of more @@ -7756,9 +7778,9 @@ def gn.dcase_mono( {==} case Some{+dv}: match aa: - case S.Arg{+bn, +bs, +bl, +bk, +bh, +br, +bd, +bc}: - gv.and_tt(Laws.has_arg(S.Arg{bn, bs, bl, bk, bh, br, bd, bc} <> tt, an), - Laws.is_default(S.Arg{bn, bs, bl, bk, bh, br, bd, bc} <> tt, an, dv), + case S.Arg{+bn, +bs, +bl, +bk, +bh, +br, S.Fallback{+ev, +bd}, +bc}: + gv.and_tt(Laws.has_arg(S.Arg{bn, bs, bl, bk, bh, br, S.Fallback{ev, bd}, bc} <> tt, an), + Laws.is_default(S.Arg{bn, bs, bl, bk, bh, br, S.Fallback{ev, bd}, bc} <> tt, an, dv), gn.or_rt(String.eq(bn, an), Laws.has_arg(tt, an), gv.and_l(Laws.has_arg(tt, an), Laws.is_default(tt, an, dv), hh)), gn.or_rt(Bool.and(String.eq(bn, an), Laws.default_is(bd, dv)), Laws.is_default(tt, an, dv), @@ -7776,13 +7798,14 @@ def gn.dsub_mono( {==} case Con{xx, +xt}: match xx: - case S.Arg{+xn, _s, _l, _k, _h, _r, +xd, _c}: + case S.Arg{+xn, _s, _l, _k, _h, _r, S.Fallback{_e, +xd}, _c}: gv.and_tt(gn.dcase(xd, xn, aa <> tt), gn.dsub(xt, aa <> tt), gn.dcase_mono(xd, xn, aa, tt, gv.and_l(gn.dcase(xd, xn, tt), gn.dsub(xt, tt), hh)), gn.dsub_mono(xt, aa, tt, gv.and_r(gn.dcase(xd, xn, tt), gn.dsub(xt, tt), hh))) # an argument's own default is a default of a list it heads def gn.dcase_self( + +ev: Maybe<&2, String>, dd: Maybe<&2, String>, +an: String, +sh: Maybe<&2, String>, @@ -7792,7 +7815,7 @@ def gn.dcase_self( +req: Bool, +cs: List<&2, String>, +tt: List<&2, S.Arg> -) -> {gn.dcase(dd, an, S.Arg{an, sh, lo, kind, hl, req, dd, cs} <> tt) == True{} : Bool}: +) -> {gn.dcase(dd, an, S.Arg{an, sh, lo, kind, hl, req, S.Fallback{ev, dd}, cs} <> tt) == True{} : Bool}: match dd: case None{}: {==} @@ -7813,11 +7836,11 @@ def gn.dsub_self(args: List<&2, S.Arg>) -> {gn.dsub(args, args) == True{} : Bool {==} case Con{aa, +tt}: match aa: - case S.Arg{+an, +sh, +lo, +kind, +hl, +req, +dd, +cs}: - gv.and_tt(gn.dcase(dd, an, S.Arg{an, sh, lo, kind, hl, req, dd, cs} <> tt), - gn.dsub(tt, S.Arg{an, sh, lo, kind, hl, req, dd, cs} <> tt), - gn.dcase_self(dd, an, sh, lo, kind, hl, req, cs, tt), - gn.dsub_mono(tt, S.Arg{an, sh, lo, kind, hl, req, dd, cs}, tt, gn.dsub_self(tt))) + case S.Arg{+an, +sh, +lo, +kind, +hl, +req, S.Fallback{+ev, +dd}, +cs}: + gv.and_tt(gn.dcase(dd, an, S.Arg{an, sh, lo, kind, hl, req, S.Fallback{ev, dd}, cs} <> tt), + gn.dsub(tt, S.Arg{an, sh, lo, kind, hl, req, S.Fallback{ev, dd}, cs} <> tt), + gn.dcase_self(ev, dd, an, sh, lo, kind, hl, req, cs, tt), + gn.dsub_mono(tt, S.Arg{an, sh, lo, kind, hl, req, S.Fallback{ev, dd}, cs}, tt, gn.dsub_self(tt))) # a default goes in front when its name is unbound, named and given def gn.fone( @@ -7883,7 +7906,7 @@ def gn.fill( hb case Con{aa, +rest}: match aa: - case S.Arg{+an, _s, _l, _k, _h, _r, +dd, _c}: + case S.Arg{+an, _s, _l, _k, _h, _r, S.Fallback{_e, +dd}, _c}: gn.fill_arg(dd, an, S.fill.args(rest, bs), ws, args, gn.fill(rest, args, bs, ws, hb, gv.and_r(gn.dcase(dd, an, args), gn.dsub(rest, args), hs)), gv.and_l(gn.dcase(dd, an, args), gn.dsub(rest, args), hs)) diff --git a/src/check.bend b/src/check.bend index 8ea3574..6ad928e 100644 --- a/src/check.bend +++ b/src/check.bend @@ -70,7 +70,7 @@ def args.dups( case Nil{}: [] case Con{hh, tt}: - C.Arg{+name, +short, +long, _k, _h, _r, dflt, +cs} = hh + C.Arg{+name, +short, +long, _k, _h, _r, C.Fallback{_e, dflt}, +cs} = hh both(one(List.contains(~String, ~String.eq, names, name), SameName{path, name}), both(one(spelled.seen(short, shorts), SameShort{path, C.text.of(short, "")}), both(one(spelled.seen(long, longs), SameLong{path, C.text.of(long, "")}), diff --git a/src/cli.bend b/src/cli.bend index 9dd2295..ab2ba86 100644 --- a/src/cli.bend +++ b/src/cli.bend @@ -14,6 +14,11 @@ type ArgKind is Data: Rest{} Many{} +# what an argument the words leave unbound falls back to: the value of its +# env var, when `parse_env` is given one, else its default +type Fallback is Data: + Fallback{env: Maybe<&2, String>, default: Maybe<&2, String>} + # one argument: name is the binding key; short/long are the CLI spellings type Arg is Data: Arg{ @@ -23,7 +28,7 @@ type Arg is Data: kind: ArgKind, help: String, required: Bool, - default: Maybe<&2, String>, + fallback: Fallback, choices: List<&2, String> } @@ -135,7 +140,7 @@ def flag( # noqa: L001 a builder: its result is the Arg or Sub it names, nothin long: Maybe<&2, String>, +help: String ) -> Arg: - Arg{name, short, long, Flag{}, help, False{}, None{}, []} + Arg{name, short, long, Flag{}, help, False{}, Fallback{None{}, None{}}, []} # a valued option def opt( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state @@ -147,7 +152,7 @@ def opt( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing default: Maybe<&2, String>, choices: List<&2, String> ) -> Arg: - Arg{name, short, long, Opt{}, help, required, default, choices} + Arg{name, short, long, Opt{}, help, required, Fallback{None{}, default}, choices} # an option that may be given more than once; `get_all` reads every value def many( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state @@ -159,7 +164,7 @@ def many( # noqa: L001 a builder: its result is the Arg or Sub it names, nothin default: Maybe<&2, String>, choices: List<&2, String> ) -> Arg: - Arg{name, short, long, Many{}, help, required, default, choices} + Arg{name, short, long, Many{}, help, required, Fallback{None{}, default}, choices} # a positional def pos( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state @@ -169,7 +174,7 @@ def pos( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing default: Maybe<&2, String>, choices: List<&2, String> ) -> Arg: - Arg{name, None{}, None{}, Pos{}, help, required, default, choices} + Arg{name, None{}, None{}, Pos{}, help, required, Fallback{None{}, default}, choices} # a rest positional: every leftover word, as one name def rest( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state @@ -179,7 +184,7 @@ def rest( # noqa: L001 a builder: its result is the Arg or Sub it names, nothin default: Maybe<&2, String>, choices: List<&2, String> ) -> Arg: - Arg{name, None{}, None{}, Rest{}, help, required, default, choices} + Arg{name, None{}, None{}, Rest{}, help, required, Fallback{None{}, default}, choices} # the larger of two Nats def help.max(+aa: Nat, +bb: Nat) -> Nat: @@ -1009,7 +1014,7 @@ def parse.req.go(req: Bool, bare: Bool, +nn: String) -> Maybe<&2, String>: # a required Arg without a default, as a missing name def parse.req(aa: Arg) -> Maybe<&2, String>: - Arg{+n, _s, _l, _k, _h, +req, default, _c} = aa + Arg{+n, _s, _l, _k, _h, +req, Fallback{_e, default}, _c} = aa parse.req.go(req, Maybe.is_none(&2, String, default), n) # this missing name, else the rest @@ -1328,7 +1333,7 @@ def fill.arg.go( # this Arg's default, when it has one and is not bound def fill.arg(aa: Arg, +binds: List<&2, Bind>) -> List<&2, Bind>: - Arg{+n, _s, _l, _k, _h, _r, default, _c} = aa + Arg{+n, _s, _l, _k, _h, _r, Fallback{_e, default}, _c} = aa fill.arg.go(default, n, binds) # defaults of every spec Arg @@ -1484,7 +1489,7 @@ def help.extra.go(+dd: String, +cs: List<&2, String>) -> String: # extras after the help string def help.extra(aa: Arg) -> String: - Arg{_n, _s, _l, _k, _h, _r, default, cs} = aa + Arg{_n, _s, _l, _k, _h, _r, Fallback{_e, default}, cs} = aa help.extra.go(text.of(default, ""), cs) # one option line, given the label width diff --git a/src/grow.bend b/src/grow.bend index 0485c0d..ba17a58 100644 --- a/src/grow.bend +++ b/src/grow.bend @@ -1291,7 +1291,7 @@ law gw.fill_arg: def gw.fill_arg(aa, binds): match aa: - case Shake.Arg{+name, _s, _l, _k, _h, _r, dflt, _c}: + case Shake.Arg{+name, _s, _l, _k, _h, _r, Shake.Fallback{_e, dflt}, _c}: gw.fill_go(dflt, name, binds) # LAW: filling defaults only puts bindings in front diff --git a/src/walk.bend b/src/walk.bend index 58aa4a3..de37c7e 100644 --- a/src/walk.bend +++ b/src/walk.bend @@ -201,7 +201,7 @@ def wk.plain_dash(ww, h): wk.nor_r(String.eq(ww, "--"), Bool.or(String.eq(ww, "help"), String.starts_with(ww, "-")), h))) # a rest positional with no choices -def wk.rest(+nm: String, +hlp: String, +req: Bool, +dflt: Maybe<&2, String>) -> Shake.Arg: +def wk.rest(+nm: String, +hlp: String, +req: Bool, +dflt: Shake.Fallback) -> Shake.Arg: Shake.Arg{nm, None{}, None{}, Shake.Rest{}, hlp, req, dflt, []} # the binds a walk pushes for a rest named `nm`, onto the ones it had, newest @@ -277,7 +277,7 @@ law wk.walk_plain: for +nm: String for +hlp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: Shake.Fallback for +seen: Bool for +hp: {all_plain(fs) == True{} : Bool} for +hu: {wk.unfound(subs, fs) == True{} : Bool} @@ -317,7 +317,7 @@ law wk.walk_raw: for +nm: String for +hlp: String for +req: Bool - for +dflt: Maybe<&2, String> + for +dflt: Shake.Fallback for seen: Bool {Shake.parse.walk(fs, Shake.St{Shake.Free{}, args, up, subs, path, bs, [wk.rest(nm, hlp, req, dflt)], True{}, seen}) From 7ae52f81dcb56ac68fb3531424f1601cc79363a0 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 2 Oct 2026 01:43:38 +0000 Subject: [PATCH 3/7] feat: env-var fallbacks (env, parse_env, env_vars, [env: NAME] in help); prove SHAKE-PARSE-11, PARSE-12, HELP-3, ARGS-2 Co-authored-by: noah-emp --- SPEC.md | 10 +- main.bend | 33 +++- src/LAWS.bend | 496 +++++++++++++++++++++++++++++++++++++++++++++++++ src/PROOF.bend | 339 +++++++++++++++++++++++++++++++++ src/args.bend | 36 +++- src/cli.bend | 275 ++++++++++++++++++++++++++- 6 files changed, 1175 insertions(+), 14 deletions(-) diff --git a/SPEC.md b/SPEC.md index 9bfc703..6119813 100644 --- a/SPEC.md +++ b/SPEC.md @@ -54,8 +54,8 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | SHAKE-PARSE-8 | Before `--` and before any positional of the current command is bound, a plain word `help`, or a word `--help` when no argument of the current command has the long spelling `help`, makes the parse fail with `NeedHelp{path}`, where `path` is the selected path followed by the remaining words, as long as each names a subcommand under the one before; the first remaining word that does not makes the parse fail with `Unexpected{word}`. A command that declares its own long `help` gets `--help` as that argument (SHAKE-TOK-1), and `help` still asks for help. | Proved | proved | src/LAWS.bend help_unknown; src/LAWS.bend help_step; src/LAWS.bend help_walk; src/LAWS.bend help_path; src/LAWS.bend dash_help_step; src/LAWS.bend dash_help_path | | SHAKE-PARSE-9 | Once a word makes the parse fail, the words after it do not change the error. | Proved | proved | src/LAWS.bend fail_stays | | SHAKE-PARSE-10 | A flag or an option built with `opt` that is given a second time while the same command is current, under any of its spellings, fails the parse with `Repeated{at, name}`; an argument of a parent command with the same name is a different argument (SHAKE-TOK-7). An option built with `many` binds every value given, in the order given, and `get_all` of its command's Matched reads them all. | Proved | proved | src/LAWS.bend repeated_long_flag; src/LAWS.bend repeated_long_opt; src/LAWS.bend letter_flag_again; src/LAWS.bend letter_opt_again; src/LAWS.bend long_binds; src/LAWS.bend letter_value; src/LAWS.bend letter_value_eq | -| SHAKE-PARSE-11 | `parse_env(spec, words, vars)` reads `words` exactly as `parse` reads them against `spec` with every argument's default, in every command, replaced by its **fallback**, and answers what that parse answers, except as SHAKE-PARSE-12 says. An argument's fallback is its env value when it has one and is not a flag; for a flag with an env value, `true` when that value, lowercased, is none of `0`, `false`, `no`, `off`, `n` and `f`, and no fallback otherwise; and for an argument with no env value, its default. So a value the words bind wins over the env value and the env value over the default (SHAKE-PARSE-6), an argument with a fallback is filled by it and needs nothing from the words to satisfy `required` (SHAKE-PARSE-7), a required positional with a fallback does not block a subcommand (SHAKE-PARSE-4), and `parse_env(spec, words, [])` is `parse(spec, words)`. | Proved | pending | | -| SHAKE-PARSE-12 | When the parse SHAKE-PARSE-11 describes succeeds and an argument other than a flag, of a command on the selected path, has an env value outside its nonempty choices that the command's Matched binds to it, `parse_env` fails instead with `BadValue{at, name, value}` of the first such argument, the root command first and each command's arguments in spec order, where `at` is the selected path. A word's value outside the choices never binds (SHAKE-PARSE-5), so only an argument filled from its env value can be bound to it. When that parse fails, `parse_env` fails with the same error. | Proved | pending | | +| SHAKE-PARSE-11 | `parse_env(spec, words, vars)` reads `words` exactly as `parse` reads them against `spec` with every argument's default, in every command, replaced by its **fallback**, and answers what that parse answers, except as SHAKE-PARSE-12 says. An argument's fallback is its env value when it has one and is not a flag; for a flag with an env value, `true` when that value, lowercased, is none of `0`, `false`, `no`, `off`, `n` and `f`, and no fallback otherwise; and for an argument with no env value, its default. So a value the words bind wins over the env value and the env value over the default (SHAKE-PARSE-6), an argument with a fallback is filled by it and needs nothing from the words to satisfy `required` (SHAKE-PARSE-7), a required positional with a fallback does not block a subcommand (SHAKE-PARSE-4), and `parse_env(spec, words, [])` is `parse(spec, words)`. | Proved | proved | src/LAWS.bend env_sets; src/LAWS.bend env_of_none; src/LAWS.bend env_of_nil; src/LAWS.bend env_of_hit; src/LAWS.bend env_of_empty; src/LAWS.bend env_of_skip; src/LAWS.bend fallback_env; src/LAWS.bend fallback_flag_on; src/LAWS.bend fallback_flag_off; src/LAWS.bend fallback_default; src/LAWS.bend resolve_spec; src/LAWS.bend resolve_args_con; src/LAWS.bend resolve_subs_con; src/LAWS.bend env_parse; src/LAWS.bend env_none | +| SHAKE-PARSE-12 | When the parse SHAKE-PARSE-11 describes succeeds and an argument other than a flag, of a command on the selected path, has an env value outside its nonempty choices that the command's Matched binds to it, `parse_env` fails instead with `BadValue{at, name, value}` of the first such argument, the root command first and each command's arguments in spec order, where `at` is the selected path. A word's value outside the choices never binds (SHAKE-PARSE-5), so only an argument filled from its env value can be bound to it. When that parse fails, `parse_env` fails with the same error. | Proved | proved | src/LAWS.bend env_check_fail; src/LAWS.bend env_check_good; src/LAWS.bend env_check_bad; src/LAWS.bend bad_go_leaf; src/LAWS.bend bad_go_root; src/LAWS.bend bad_go_down; src/LAWS.bend bad_args_here; src/LAWS.bend bad_args_next; src/LAWS.bend bad_args_nil; src/LAWS.bend bad_arg_some; src/LAWS.bend bad_arg_unset; src/LAWS.bend bad_arg_flag; src/LAWS.bend bad_arg_allowed; src/LAWS.bend bad_arg_unbound | ### Checking a spec (SHAKE-SPEC) @@ -76,7 +76,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | :---- | :---- | :---- | :---- | :---- | | SHAKE-HELP-1 | `help(spec, path)` renders the page of the command reached by following each name of `path` from the root through the subcommands, skipping a name that is not a subcommand where it stands. | Proved | proved | src/LAWS.bend help_page; src/LAWS.bend reach_child; src/LAWS.bend reach_skip | | SHAKE-HELP-2 | A page lists each subcommand of its command exactly once, in spec order, followed by `help`, and each flag and option exactly once, in spec order. Its usage line names each positional exactly once, in spec order, as `` when required and `[NAME]` otherwise, with `...` after a rest positional. | Proved | proved | src/LAWS.bend cmds_listed; src/LAWS.bend opts_listed; src/LAWS.bend usage_listed | -| SHAKE-HELP-3 | The Options line of a flag or option that has an env var `NAME` shows `[env: NAME]` after its help text, before its `[default: ...]` and `[possible values: ...]`, as clap's does; the line of one with no env var is what it would be without this row. A positional has no Options line (SHAKE-HELP-2), so its env var is not shown. | Proved | pending | | +| SHAKE-HELP-3 | The Options line of a flag or option that has an env var `NAME` shows `[env: NAME]` after its help text, before its `[default: ...]` and `[possible values: ...]`, as clap's does; the line of one with no env var is what it would be without this row. A positional has no Options line (SHAKE-HELP-2), so its env var is not shown. | Proved | proved | src/LAWS.bend help_env_shown; src/LAWS.bend help_env_none | ### Errors (SHAKE-ERR) @@ -92,11 +92,11 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | | SHAKE-ARGS-1 | The copy `argv` makes of the words `IO.args` gives drops the first, the program as invoked, and keeps all the others, in order and unchanged: for every list, reading the copy back gives the list after its first word, and nothing for an empty list. | Proved | proved | src/LAWS.bend copy_keeps; src/LAWS.bend words_keeps | -| SHAKE-ARGS-2 | The names `env_vars(spec)` asks `IO.get_env` for are the env vars of the arguments that have one, the root command's arguments first and then each subcommand's, depth first, each command's arguments in spec order. | Proved | pending | | +| SHAKE-ARGS-2 | The names `env_vars(spec)` asks `IO.get_env` for are the env vars of the arguments that have one, the root command's arguments first and then each subcommand's, depth first, each command's arguments in spec order. | Proved | proved | src/LAWS.bend env_names_root; src/LAWS.bend env_names_forest; src/LAWS.bend env_names_some; src/LAWS.bend env_names_none | ## Left to prove -SHAKE-PARSE-11, PARSE-12, HELP-3, ERR-3, ERR-4 and ARGS-2 are pending: their laws land with the code that implements them ([docs/rfc/shake-env-and-suggestions.md](docs/rfc/shake-env-and-suggestions.md), Rollout). Every other row is proved. The RFC's Rollout and [docs/rfc/shake-walker-proofs.md](docs/rfc/shake-walker-proofs.md) say in which phase each row's laws land. Every walker law holds wherever the words before the word it is about leave the walker in the state its premise names. +SHAKE-ERR-3 and ERR-4 are pending: their laws land with the code that implements them ([docs/rfc/shake-env-and-suggestions.md](docs/rfc/shake-env-and-suggestions.md), Rollout). Every other row is proved. The RFC's Rollout and [docs/rfc/shake-walker-proofs.md](docs/rfc/shake-walker-proofs.md) say in which phase each row's laws land. Every walker law holds wherever the words before the word it is about leave the walker in the state its premise names. ## Trust boundary diff --git a/main.bend b/main.bend index 78448c1..5ea44f0 100644 --- a/main.bend +++ b/main.bend @@ -1,13 +1,16 @@ # shake: a proven command-line argument parser for Bend 2, with subcommands and help. # # Describe a program with `app`, `sub`, `flag`, `opt`, `many`, `pos` and -# `rest`; `parse` binds argv against it, and +# `rest`, and give an argument an env var to fall back to with `env`; `parse` +# binds argv against it (`parse_env` also takes the values of the env vars, +# which `env_vars` reads), and # the result is read one command at a time, as clap's: `get`, `get_all` and # `on` read a command's own bindings, and `sub_name`, `sub_of`, `at` and # `path_of` reach the subcommands selected under it. `help` writes the usage # page for a command path. For a failed parse, `help_path` tells a request for help # from an error, `err_text` writes the message and `err_path` names the command -# it failed in. `check` reports a spec that contradicts itself. `argv` is the +# it failed in, and `suggestion` the long spelling a mistyped one was likely +# meant to be. `check` reports a spec that contradicts itself. `argv` is the # process's arguments. This file is the interface: everything under src/ is # internal. import Base @@ -32,6 +35,11 @@ def Arg() -> Data: # noqa: L001 a type alias of the interface def Matched() -> Data: S.Matched +# an env var's name and its value, a pair `(name, value)`: `parse_env` takes a +# list of them, and `env_vars` reads one for each env var that is set +def Var() -> Data: + S.Var + # a failed parse def ParseErr() -> Data: S.ParseErr @@ -113,6 +121,12 @@ def rest( # noqa: L001 a builder: its result is the Arg or Sub it names, nothin ) -> S.Arg: S.rest(name, help, required, default, choices) +# this argument, falling back to the env var `var` when the words leave it +# unbound, before its default, as clap's `.env(var)`: `parse_env` reads it, +# and help shows `[env: VAR]` +def env(arg: S.Arg, +var: String) -> S.Arg: + S.env(arg, var) + # every way a spec contradicts itself: a rest positional that is not the # last, a repeated argument name or spelling, a repeated subcommand name, a # subcommand named `help`, a default outside its choices, a required @@ -129,6 +143,16 @@ def spec_err_text(err: K.SpecErr) -> String: def parse(spec: S.Cli, words: List<&2, String>) -> Result<&2, &2, S.ParseErr, S.Matched>: S.parse(spec, words) +# argv against a program spec, with `vars`, name and value pairs, for the env +# vars: an argument the words leave unbound falls back to its env var's value +# when it is set and not empty, then to its default +def parse_env( + +spec: S.Cli, + words: List<&2, String>, + +vars: List<&2, S.Var> +) -> Result<&2, &2, S.ParseErr, S.Matched>: + S.parse_env(spec, words, vars) + # the value this command bound to `name` last, or None when it bound none def get(found: S.Matched, +name: String) -> Maybe<&2, String>: S.get(found, name) @@ -208,6 +232,11 @@ def help_path(err: S.ParseErr) -> Maybe<&2, List<&2, String>>: case S.Repeated{_at, _name}: None{} +# the env vars `spec` gives its arguments, each that is set with its value, +# for `parse_env` +def env_vars(spec: S.Cli) -> IO(List<&2, S.Var>): # noqa: L001 IO: reads env vars + Args.env_vars(spec) + # the process's arguments, each word reusable, without the program name # that `IO.args` starts with (bend 2.0.32 and later). A compiled program's # runtime has already acted on `--bend-help`, `--gpu-build`, `--threads N` diff --git a/src/LAWS.bend b/src/LAWS.bend index abc2962..d679e0e 100644 --- a/src/LAWS.bend +++ b/src/LAWS.bend @@ -2862,3 +2862,499 @@ law spec_err_where: for +err: K.SpecErr exs msg: String {Shake.spec_err_text(err) == K.at(spec_path(err)) ++ msg : String} + +# LAW: `env` gives an argument its env var and keeps the rest of it +# SHAKE-PARSE-11 +law env_sets: + for +nn: String + for +sh: Maybe<&2, String> + for +lo: Maybe<&2, String> + for +kind: S.ArgKind + for +hp: String + for +req: Bool + for ev: Maybe<&2, String> + for +dd: Maybe<&2, String> + for +cs: List<&2, String> + for +var: String + {Shake.env(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs}, var) + == S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{Some{var}, dd}, cs} : S.Arg} + +# LAW: an argument with no env var has no env value +# SHAKE-PARSE-11 +law env_of_none: + for vars: List<&2, Shake.Var> + {S.env.of(None{}, vars) == None{} : Maybe<&2, String>} + +# LAW: an env var no pair names has no env value +# SHAKE-PARSE-11 +law env_of_nil: + for var: String + {S.env.of(Some{var}, []) == None{} : Maybe<&2, String>} + +# LAW: the first pair an env var names gives its env value, when its value +# is not empty +# SHAKE-PARSE-11 +law env_of_hit: + for +var: String + for +nn: String + for +vv: String + for rest: List<&2, Shake.Var> + for h_eq: {String.eq(nn, var) == True{} : Bool} + for h_full: {String.is_empty(vv) == False{} : Bool} + {S.env.of(Some{var}, (nn, vv) <> rest) == Some{vv} : Maybe<&2, String>} + +# LAW: an empty value in the first pair an env var names gives no env value, +# whatever later pairs hold +# SHAKE-PARSE-11 +law env_of_empty: + for +var: String + for +nn: String + for +vv: String + for rest: List<&2, Shake.Var> + for h_eq: {String.eq(nn, var) == True{} : Bool} + for h_empty: {String.is_empty(vv) == True{} : Bool} + {S.env.of(Some{var}, (nn, vv) <> rest) == None{} : Maybe<&2, String>} + +# LAW: a pair named otherwise is passed over +# SHAKE-PARSE-11 +law env_of_skip: + for +var: String + for +nn: String + for +vv: String + for +rest: List<&2, Shake.Var> + for h_eq: {String.eq(nn, var) == False{} : Bool} + {S.env.of(Some{var}, (nn, vv) <> rest) == S.env.of(Some{var}, rest) : Maybe<&2, String>} + +# the env values that turn a flag off, lowercased +def off_words() -> List<&2, String>: + ["0", "false", "no", "off", "n", "f"] + +# LAW: an argument other than a flag that has an env value falls back to it +# SHAKE-PARSE-11 +law fallback_env: + for +nn: String + for +sh: Maybe<&2, String> + for +lo: Maybe<&2, String> + for +kind: S.ArgKind + for +hp: String + for +req: Bool + for +ev: Maybe<&2, String> + for dd: Maybe<&2, String> + for +cs: List<&2, String> + for +vars: List<&2, Shake.Var> + for +vv: String + for h_kind: {S.env.flag.is(kind) == False{} : Bool} + for h_env: {S.env.of(ev, vars) == Some{vv} : Maybe<&2, String>} + {S.resolve.arg(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs}, vars) + == S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, Some{vv}}, cs} : S.Arg} + +# LAW: a flag with an env value that, lowercased, is not an off word falls +# back to `true` +# SHAKE-PARSE-11 +law fallback_flag_on: + for +nn: String + for +sh: Maybe<&2, String> + for +lo: Maybe<&2, String> + for +hp: String + for +req: Bool + for +ev: Maybe<&2, String> + for dd: Maybe<&2, String> + for +cs: List<&2, String> + for +vars: List<&2, Shake.Var> + for +vv: String + for h_env: {S.env.of(ev, vars) == Some{vv} : Maybe<&2, String>} + for h_on: {S.allowed.ok(off_words(), String.to_lower(vv)) == False{} : Bool} + {S.resolve.arg(S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, dd}, cs}, vars) + == S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, Some{"true"}}, cs} : S.Arg} + +# LAW: a flag with an env value that, lowercased, is an off word has no +# fallback +# SHAKE-PARSE-11 +law fallback_flag_off: + for +nn: String + for +sh: Maybe<&2, String> + for +lo: Maybe<&2, String> + for +hp: String + for +req: Bool + for +ev: Maybe<&2, String> + for dd: Maybe<&2, String> + for +cs: List<&2, String> + for +vars: List<&2, Shake.Var> + for +vv: String + for h_env: {S.env.of(ev, vars) == Some{vv} : Maybe<&2, String>} + for h_off: {S.allowed.ok(off_words(), String.to_lower(vv)) == True{} : Bool} + {S.resolve.arg(S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, dd}, cs}, vars) + == S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, None{}}, cs} : S.Arg} + +# LAW: an argument with no env value falls back to its default +# SHAKE-PARSE-11 +law fallback_default: + for +nn: String + for +sh: Maybe<&2, String> + for +lo: Maybe<&2, String> + for +kind: S.ArgKind + for +hp: String + for +req: Bool + for +ev: Maybe<&2, String> + for +dd: Maybe<&2, String> + for +cs: List<&2, String> + for +vars: List<&2, Shake.Var> + for h_env: {S.env.of(ev, vars) == None{} : Maybe<&2, String>} + {S.resolve.arg(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs}, vars) + == S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs} : S.Arg} + +# LAW: a spec's arguments are resolved in the root command and below it +# SHAKE-PARSE-11 +law resolve_spec: + for +nn: String + for +ab: String + for +ver: Maybe<&2, String> + for args: List<&2, S.Arg> + for subs: List<&2, S.Sub> + for +vars: List<&2, Shake.Var> + {S.resolve(S.Cli{nn, ab, ver, args, subs}, vars) + == S.Cli{nn, ab, ver, S.resolve.args(args, vars), S.resolve.subs(subs, vars)} : S.Cli} + +# LAW: a command's arguments are resolved one by one, in order +# SHAKE-PARSE-11 +law resolve_args_con: + for aa: S.Arg + for tt: List<&2, S.Arg> + for +vars: List<&2, Shake.Var> + {S.resolve.args(aa <> tt, vars) == S.resolve.arg(aa, vars) <> S.resolve.args(tt, vars) : List<&2, S.Arg>} + +# LAW: a subcommand's arguments are resolved, and every subcommand under it +# SHAKE-PARSE-11 +law resolve_subs_con: + for +nn: String + for +ab: String + for args: List<&2, S.Arg> + for kids: List<&2, S.Sub> + for tt: List<&2, S.Sub> + for +vars: List<&2, Shake.Var> + {S.resolve.subs(S.Sub{nn, ab, args, kids} <> tt, vars) + == S.Sub{nn, ab, S.resolve.args(args, vars), S.resolve.subs(kids, vars)} <> S.resolve.subs(tt, vars) + : List<&2, S.Sub>} + +# LAW: `parse_env` is `parse` against the spec with every default replaced by +# its fallback, then the check SHAKE-PARSE-12 describes +# SHAKE-PARSE-11 +law env_parse: + for +spec: Shake.Cli + for ws: List<&2, String> + for +vars: List<&2, Shake.Var> + {Shake.parse_env(spec, ws, vars) == S.env.check(spec, vars, Shake.parse(S.resolve(spec, vars), ws)) + : Result<&2, &2, Shake.ParseErr, Shake.Matched>} + +# LAW: with no pairs, `parse_env` is `parse` +# SHAKE-PARSE-11 +law env_none: + for +spec: Shake.Cli + for ws: List<&2, String> + {Shake.parse_env(spec, ws, []) == Shake.parse(spec, ws) : Result<&2, &2, Shake.ParseErr, Shake.Matched>} + +# LAW: a failed parse fails `parse_env` with the same error +# SHAKE-PARSE-12 +law env_check_fail: + for spec: Shake.Cli + for vars: List<&2, Shake.Var> + for ee: Shake.ParseErr + {S.env.check(spec, vars, Fail{ee}) == Fail{ee} : Result<&2, &2, Shake.ParseErr, Shake.Matched>} + +# LAW: a successful parse that bound no env value outside its choices is +# what `parse_env` answers +# SHAKE-PARSE-12 +law env_check_good: + for nn: String + for ab: String + for ver: Maybe<&2, String> + for +args: List<&2, S.Arg> + for +subs: List<&2, S.Sub> + for +vars: List<&2, Shake.Var> + for +mm: Shake.Matched + for h_none: {S.env.bad.go(mm, args, subs, vars) == None{} : Maybe<&2, Shake.Var>} + {S.env.check(S.Cli{nn, ab, ver, args, subs}, vars, Done{mm}) == Done{mm} + : Result<&2, &2, Shake.ParseErr, Shake.Matched>} + +# LAW: a successful parse that bound an env value outside its choices fails +# with BadValue at the selected path +# SHAKE-PARSE-12 +law env_check_bad: + for nn: String + for ab: String + for ver: Maybe<&2, String> + for +args: List<&2, S.Arg> + for +subs: List<&2, S.Sub> + for +vars: List<&2, Shake.Var> + for +mm: Shake.Matched + for +name: String + for +vv: String + for h_bad: {S.env.bad.go(mm, args, subs, vars) == Some{(name, vv)} : Maybe<&2, Shake.Var>} + {S.env.check(S.Cli{nn, ab, ver, args, subs}, vars, Done{mm}) == Fail{S.BadValue{Shake.path_of(mm), name, vv}} + : Result<&2, &2, Shake.ParseErr, Shake.Matched>} + +# LAW: the last command on the path is checked among its own arguments and +# bindings +# SHAKE-PARSE-12 +law bad_go_leaf: + for +bs: List<&2, S.Bind> + for +args: List<&2, S.Arg> + for subs: List<&2, S.Sub> + for +vars: List<&2, Shake.Var> + {S.env.bad.go(S.Leaf{bs}, args, subs, vars) == S.env.bad.args(args, vars, bs) : Maybe<&2, Shake.Var>} + +# LAW: a command's own arguments come before the subcommand selected under it +# SHAKE-PARSE-12 +law bad_go_root: + for +bs: List<&2, S.Bind> + for +name: String + for +next: Shake.Matched + for +args: List<&2, S.Arg> + for +subs: List<&2, S.Sub> + for +vars: List<&2, Shake.Var> + for +pp: Shake.Var + for h_here: {S.env.bad.args(args, vars, bs) == Some{pp} : Maybe<&2, Shake.Var>} + {S.env.bad.go(S.Node{bs, name, next}, args, subs, vars) == Some{pp} : Maybe<&2, Shake.Var>} + +# LAW: with none among a command's own arguments, the subcommand selected +# under it is checked among its arguments and bindings +# SHAKE-PARSE-12 +law bad_go_down: + for +bs: List<&2, S.Bind> + for +name: String + for +next: Shake.Matched + for +args: List<&2, S.Arg> + for +subs: List<&2, S.Sub> + for +vars: List<&2, Shake.Var> + for h_none: {S.env.bad.args(args, vars, bs) == None{} : Maybe<&2, Shake.Var>} + {S.env.bad.go(S.Node{bs, name, next}, args, subs, vars) + == S.env.bad.go(next, S.env.sub.args(S.find_sub(subs, name)), S.env.sub.kids(S.find_sub(subs, name)), vars) + : Maybe<&2, Shake.Var>} + +# LAW: within a command, the first argument in spec order is the one reported +# SHAKE-PARSE-12 +law bad_args_here: + for +aa: S.Arg + for +tt: List<&2, S.Arg> + for +vars: List<&2, Shake.Var> + for +bs: List<&2, S.Bind> + for +pp: Shake.Var + for h_here: {S.env.bad.arg(aa, vars, bs) == Some{pp} : Maybe<&2, Shake.Var>} + {S.env.bad.args(aa <> tt, vars, bs) == Some{pp} : Maybe<&2, Shake.Var>} + +# LAW: an argument that is fine passes the check on to the next +# SHAKE-PARSE-12 +law bad_args_next: + for +aa: S.Arg + for +tt: List<&2, S.Arg> + for +vars: List<&2, Shake.Var> + for +bs: List<&2, S.Bind> + for h_none: {S.env.bad.arg(aa, vars, bs) == None{} : Maybe<&2, Shake.Var>} + {S.env.bad.args(aa <> tt, vars, bs) == S.env.bad.args(tt, vars, bs) : Maybe<&2, Shake.Var>} + +# LAW: no command has a bad argument when there are no pairs +# SHAKE-PARSE-12 +law bad_args_nil: + for args: List<&2, S.Arg> + for +bs: List<&2, S.Bind> + {S.env.bad.args(args, [], bs) == None{} : Maybe<&2, Shake.Var>} + +# LAW: an argument other than a flag whose env value is outside its choices +# and bound in its command is reported with that value +# SHAKE-PARSE-12 +law bad_arg_some: + for +nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for +kind: S.ArgKind + for hp: String + for req: Bool + for +ev: Maybe<&2, String> + for dd: Maybe<&2, String> + for +cs: List<&2, String> + for +vars: List<&2, Shake.Var> + for +bs: List<&2, S.Bind> + for +vv: String + for h_env: {S.env.of(ev, vars) == Some{vv} : Maybe<&2, String>} + for h_kind: {S.env.flag.is(kind) == False{} : Bool} + for h_out: {S.allowed(cs, vv) == False{} : Bool} + for h_bound: {List.contains(~String, ~String.eq, S.get_all.bind(bs, nn), vv) == True{} : Bool} + {S.env.bad.arg(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs}, vars, bs) == Some{(nn, vv)} + : Maybe<&2, Shake.Var>} + +# LAW: an argument with no env value is never reported +# SHAKE-PARSE-12 +law bad_arg_unset: + for nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for kind: S.ArgKind + for hp: String + for req: Bool + for +ev: Maybe<&2, String> + for dd: Maybe<&2, String> + for cs: List<&2, String> + for +vars: List<&2, Shake.Var> + for bs: List<&2, S.Bind> + for h_env: {S.env.of(ev, vars) == None{} : Maybe<&2, String>} + {S.env.bad.arg(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs}, vars, bs) == None{} + : Maybe<&2, Shake.Var>} + +# LAW: a flag is never reported +# SHAKE-PARSE-12 +law bad_arg_flag: + for nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for hp: String + for req: Bool + for ev: Maybe<&2, String> + for dd: Maybe<&2, String> + for cs: List<&2, String> + for vars: List<&2, Shake.Var> + for bs: List<&2, S.Bind> + {S.env.bad.arg(S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, dd}, cs}, vars, bs) == None{} + : Maybe<&2, Shake.Var>} + +# LAW: an env value its choices allow is never reported +# SHAKE-PARSE-12 +law bad_arg_allowed: + for +nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for +kind: S.ArgKind + for hp: String + for req: Bool + for +ev: Maybe<&2, String> + for dd: Maybe<&2, String> + for +cs: List<&2, String> + for +vars: List<&2, Shake.Var> + for +bs: List<&2, S.Bind> + for +vv: String + for h_env: {S.env.of(ev, vars) == Some{vv} : Maybe<&2, String>} + for h_in: {S.allowed(cs, vv) == True{} : Bool} + {S.env.bad.arg(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs}, vars, bs) == None{} + : Maybe<&2, Shake.Var>} + +# LAW: an env value its command does not bind is never reported +# SHAKE-PARSE-12 +law bad_arg_unbound: + for +nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for +kind: S.ArgKind + for hp: String + for req: Bool + for +ev: Maybe<&2, String> + for dd: Maybe<&2, String> + for +cs: List<&2, String> + for +vars: List<&2, Shake.Var> + for +bs: List<&2, S.Bind> + for +vv: String + for h_env: {S.env.of(ev, vars) == Some{vv} : Maybe<&2, String>} + for h_free: {List.contains(~String, ~String.eq, S.get_all.bind(bs, nn), vv) == False{} : Bool} + {S.env.bad.arg(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs}, vars, bs) == None{} + : Maybe<&2, Shake.Var>} + +# LAW: an option line shows the env var after the help text, before the +# default and the possible values +# SHAKE-HELP-3 +law help_env_shown: + for nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for kind: S.ArgKind + for hp: String + for req: Bool + for +var: String + for +dd: Maybe<&2, String> + for +cs: List<&2, String> + {S.help.extra(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{Some{var}, dd}, cs}) + == (" [env: " ++ var ++ "]") ++ S.help.extra.go(S.text.of(dd, ""), cs) : String} + +# LAW: an option line with no env var shows only the default and the possible +# values, as before +# SHAKE-HELP-3 +law help_env_none: + for nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for kind: S.ArgKind + for hp: String + for req: Bool + for +dd: Maybe<&2, String> + for +cs: List<&2, String> + {S.help.extra(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{None{}, dd}, cs}) + == S.help.extra.go(S.text.of(dd, ""), cs) : String} + +# LAW: `env_vars` asks for the root command's env vars, then its +# subcommands' +# SHAKE-ARGS-2 +law env_names_root: + for nn: String + for ab: String + for ver: Maybe<&2, String> + for args: List<&2, S.Arg> + for subs: List<&2, S.Sub> + {S.env.names(S.Cli{nn, ab, ver, args, subs}) + == List.append(&2, String, S.env.names.args(args), S.env.names.forest(subs)) : List<&2, String>} + +# LAW: a subcommand's env vars come before those of the subcommands under it, +# and those before its next sibling's +# SHAKE-ARGS-2 +law env_names_forest: + for nn: String + for ab: String + for args: List<&2, S.Arg> + for kids: List<&2, S.Sub> + for tt: List<&2, S.Sub> + {S.env.names.forest(S.Sub{nn, ab, args, kids} <> tt) + == List.append(&2, String, S.env.names.args(args), + List.append(&2, String, S.env.names.forest(kids), S.env.names.forest(tt))) : List<&2, String>} + +# LAW: an argument with an env var names it, in spec order +# SHAKE-ARGS-2 +law env_names_some: + for nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for kind: S.ArgKind + for hp: String + for req: Bool + for +var: String + for dd: Maybe<&2, String> + for cs: List<&2, String> + for tt: List<&2, S.Arg> + {S.env.names.args(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{Some{var}, dd}, cs} <> tt) + == var <> S.env.names.args(tt) : List<&2, String>} + +# LAW: an argument with no env var names none +# SHAKE-ARGS-2 +law env_names_none: + for nn: String + for sh: Maybe<&2, String> + for lo: Maybe<&2, String> + for kind: S.ArgKind + for hp: String + for req: Bool + for dd: Maybe<&2, String> + for cs: List<&2, String> + for tt: List<&2, S.Arg> + {S.env.names.args(S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{None{}, dd}, cs} <> tt) + == S.env.names.args(tt) : List<&2, String>} + +# LAW: a name `IO.get_env` found a value for is kept with that value, in front +# of the rest (a lemma for SHAKE-TRUST-5's reading) +law kept_set: + for +nn: String + for vv: String + for rest: List<&2, Shake.Var> + {Args.kept(nn, Done{vv}, rest) == (nn, vv) <> rest : List<&2, Shake.Var>} + +# LAW: a name `IO.get_env` failed for gives no pair (a lemma for +# SHAKE-TRUST-5's reading) +law kept_unset: + for nn: String + for ee: U32 & String + for rest: List<&2, Shake.Var> + {Args.kept(nn, Fail{ee}, rest) == rest : List<&2, Shake.Var>} diff --git a/src/PROOF.bend b/src/PROOF.bend index 5b2c144..6d63877 100644 --- a/src/PROOF.bend +++ b/src/PROOF.bend @@ -9949,3 +9949,342 @@ def Laws.spec_err_where(err): ("the default '" ++ value ++ "' of '" ++ name ++ "' is not one of its choices", {==}) case K.RequiredAfterOptional{+path, +name}: ("required positional '" ++ name ++ "' follows an optional one", {==}) + +def Laws.env_sets(_nn, _sh, _lo, _kind, _hp, _req, _ev, _dd, _cs, _var): + {==} + +def Laws.env_of_none(_vars): + {==} + +def Laws.env_of_nil(_var): + {==} + +def Laws.env_of_hit(var, nn, vv, rest, h_eq, h_full): + e1 = Equal.sym(Bool, String.eq(nn, var), True{}, h_eq) + %e1 : {S.env.full(S.env.get.at(_, vv, S.env.get(rest, var))) == Some{vv} : Maybe<&2, String>} + e2 = Equal.sym(Bool, String.is_empty(vv), False{}, h_full) + %e2 : {Bool.pick(Maybe<&2, String>, _, None{}, Some{vv}) == Some{vv} : Maybe<&2, String>} + {==} + +def Laws.env_of_empty(var, nn, vv, rest, h_eq, h_empty): + e1 = Equal.sym(Bool, String.eq(nn, var), True{}, h_eq) + %e1 : {S.env.full(S.env.get.at(_, vv, S.env.get(rest, var))) == None{} : Maybe<&2, String>} + e2 = Equal.sym(Bool, String.is_empty(vv), True{}, h_empty) + %e2 : {Bool.pick(Maybe<&2, String>, _, None{}, Some{vv}) == None{} : Maybe<&2, String>} + {==} + +def Laws.env_of_skip(var, nn, vv, rest, h_eq): + e1 = Equal.sym(Bool, String.eq(nn, var), False{}, h_eq) + %e1 : {S.env.full(S.env.get.at(_, vv, S.env.get(rest, var))) == S.env.of(Some{var}, rest) + : Maybe<&2, String>} + {==} + +# that a kind is not a flag +def fb.not_flag(kk: S.ArgKind) -> Type: + {S.env.flag.is(kk) == False{} : Bool} + +# what an env value gives an argument other than a flag is that value +def fb.kind( + kk: S.ArgKind, + +vv: String, + hh: fb.not_flag(kk) +) -> {S.env.kind(kk, vv) == Some{vv} : Maybe<&2, String>}: + match kk: + case S.Flag{}: + Empty.absurd({S.env.kind(S.Flag{}, vv) == Some{vv} : Maybe<&2, String>}, Walk.wk.true_false(hh)) + case S.Opt{}: + {==} + case S.Many{}: + {==} + case S.Pos{}: + {==} + case S.Rest{}: + {==} + +def Laws.fallback_env(nn, sh, lo, kind, hp, req, ev, dd, cs, vars, vv, h_kind, h_env): + e1 = Equal.sym(Maybe<&2, String>, S.env.of(ev, vars), Some{vv}, h_env) + %e1 : {S.Arg{nn, sh, lo, kind, hp, req, S.resolve.with(_, kind, ev, dd), cs} + == S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, Some{vv}}, cs} : S.Arg} + e2 = Equal.sym(Maybe<&2, String>, S.env.kind(kind, vv), Some{vv}, fb.kind(kind, vv, h_kind)) + %e2 : {S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, _}, cs} + == S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, Some{vv}}, cs} : S.Arg} + {==} + +def Laws.fallback_flag_on(nn, sh, lo, hp, req, ev, dd, cs, vars, vv, h_env, h_on): + e1 = Equal.sym(Maybe<&2, String>, S.env.of(ev, vars), Some{vv}, h_env) + %e1 : {S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.resolve.with(_, S.Flag{}, ev, dd), cs} + == S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, Some{"true"}}, cs} : S.Arg} + e2 = Equal.sym(Bool, S.allowed.ok(Laws.off_words(), String.to_lower(vv)), False{}, h_on) + %e2 : {S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, Bool.pick(Maybe<&2, String>, _, None{}, Some{"true"})}, cs} + == S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, Some{"true"}}, cs} : S.Arg} + {==} + +def Laws.fallback_flag_off(nn, sh, lo, hp, req, ev, dd, cs, vars, vv, h_env, h_off): + e1 = Equal.sym(Maybe<&2, String>, S.env.of(ev, vars), Some{vv}, h_env) + %e1 : {S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.resolve.with(_, S.Flag{}, ev, dd), cs} + == S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, None{}}, cs} : S.Arg} + e2 = Equal.sym(Bool, S.allowed.ok(Laws.off_words(), String.to_lower(vv)), True{}, h_off) + %e2 : {S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, Bool.pick(Maybe<&2, String>, _, None{}, Some{"true"})}, cs} + == S.Arg{nn, sh, lo, S.Flag{}, hp, req, S.Fallback{ev, None{}}, cs} : S.Arg} + {==} + +def Laws.fallback_default(nn, sh, lo, kind, hp, req, ev, dd, cs, vars, h_env): + e1 = Equal.sym(Maybe<&2, String>, S.env.of(ev, vars), None{}, h_env) + %e1 : {S.Arg{nn, sh, lo, kind, hp, req, S.resolve.with(_, kind, ev, dd), cs} + == S.Arg{nn, sh, lo, kind, hp, req, S.Fallback{ev, dd}, cs} : S.Arg} + {==} + +def Laws.resolve_spec(_nn, _ab, _ver, _args, _subs, _vars): + {==} + +def Laws.resolve_args_con(_aa, _tt, _vars): + {==} + +def Laws.resolve_subs_con(_nn, _ab, _args, _kids, _tt, _vars): + {==} + +def Laws.env_parse(_spec, _ws, _vars): + {==} + +# an argument resolved under no pairs is unchanged +def rs.arg_nil(aa: S.Arg) -> {S.resolve.arg(aa, []) == aa : S.Arg}: + match aa: + case S.Arg{+n, +s, +l, +kk, +h, +r, fb, +cs}: + match fb: + case S.Fallback{ev, +dd}: + match ev: + case None{}: + {==} + case Some{+var}: + {==} + +# arguments resolved under no pairs are unchanged +def rs.args_nil(args: List<&2, S.Arg>) -> {S.resolve.args(args, []) == args : List<&2, S.Arg>}: + match args: + case Nil{}: + {==} + case Con{+hh, +tt}: + e1 = Equal.sym(S.Arg, S.resolve.arg(hh, []), hh, rs.arg_nil(hh)) + %e1 : {_ <> S.resolve.args(tt, []) == hh <> tt : List<&2, S.Arg>} + e2 = Equal.sym(List<&2, S.Arg>, S.resolve.args(tt, []), tt, rs.args_nil(tt)) + %e2 : {hh <> _ == hh <> tt : List<&2, S.Arg>} + {==} + +# subcommands resolved under no pairs are unchanged +def rs.subs_nil(subs: List<&2, S.Sub>) -> {S.resolve.subs(subs, []) == subs : List<&2, S.Sub>}: + match subs: + case Nil{}: + {==} + case Con{hh, +tt}: + match hh: + case S.Sub{+n, +a, +args, +kids}: + e1 = Equal.sym(List<&2, S.Arg>, S.resolve.args(args, []), args, rs.args_nil(args)) + %e1 : {S.Sub{n, a, _, S.resolve.subs(kids, [])} <> S.resolve.subs(tt, []) + == S.Sub{n, a, args, kids} <> tt : List<&2, S.Sub>} + e2 = Equal.sym(List<&2, S.Sub>, S.resolve.subs(kids, []), kids, rs.subs_nil(kids)) + %e2 : {S.Sub{n, a, args, _} <> S.resolve.subs(tt, []) == S.Sub{n, a, args, kids} <> tt : List<&2, S.Sub>} + e3 = Equal.sym(List<&2, S.Sub>, S.resolve.subs(tt, []), tt, rs.subs_nil(tt)) + %e3 : {S.Sub{n, a, args, kids} <> _ == S.Sub{n, a, args, kids} <> tt : List<&2, S.Sub>} + {==} + +# a spec resolved under no pairs is unchanged +def rs.spec_nil(spec: S.Cli) -> {S.resolve(spec, []) == spec : S.Cli}: + match spec: + case S.Cli{+n, +a, +v, +args, +subs}: + e1 = Equal.sym(List<&2, S.Arg>, S.resolve.args(args, []), args, rs.args_nil(args)) + %e1 : {S.Cli{n, a, v, _, S.resolve.subs(subs, [])} == S.Cli{n, a, v, args, subs} : S.Cli} + e2 = Equal.sym(List<&2, S.Sub>, S.resolve.subs(subs, []), subs, rs.subs_nil(subs)) + %e2 : {S.Cli{n, a, v, args, _} == S.Cli{n, a, v, args, subs} : S.Cli} + {==} + +def Laws.bad_args_nil(args, bs): + match args: + case Nil{}: + {==} + case Con{hh, tt}: + match hh: + case S.Arg{_n, _s, _l, _k, _h, _r, fb, _c}: + match fb: + case S.Fallback{ev, _d}: + match ev: + case None{}: + Laws.bad_args_nil(tt, bs) + case Some{_var}: + Laws.bad_args_nil(tt, bs) + +# no command on the path has a bad argument under no pairs +def ck.go_nil( + mm: S.Matched, + +args: List<&2, S.Arg>, + +subs: List<&2, S.Sub> +) -> {S.env.bad.go(mm, args, subs, []) == None{} : Maybe<&2, S.Var>}: + match mm: + case S.Leaf{+bs}: + Laws.bad_args_nil(args, bs) + case S.Node{+bs, +name, next}: + e1 = Equal.sym(Maybe<&2, S.Var>, S.env.bad.args(args, [], bs), None{}, Laws.bad_args_nil(args, bs)) + %e1 : {S.env.first(_, + S.env.bad.go(next, S.env.sub.args(S.find_sub(subs, name)), S.env.sub.kids(S.find_sub(subs, name)), [])) + == None{} : Maybe<&2, S.Var>} + ck.go_nil(next, S.env.sub.args(S.find_sub(subs, name)), S.env.sub.kids(S.find_sub(subs, name))) + +# the check under no pairs leaves every result as it is +def ck.nil( + spec: S.Cli, + got: Result<&2, &2, S.ParseErr, S.Matched> +) -> {S.env.check(spec, [], got) == got : Result<&2, &2, S.ParseErr, S.Matched>}: + match spec: + case S.Cli{_n, _a, _v, +args, +subs}: + match got: + case Fail{_e}: + {==} + case Done{+mm}: + e1 = Equal.sym(Maybe<&2, S.Var>, S.env.bad.go(mm, args, subs, []), None{}, ck.go_nil(mm, args, subs)) + %e1 : {S.env.check.done(_, mm) == Done{mm} : Result<&2, &2, S.ParseErr, S.Matched>} + {==} + +def Laws.env_none(spec, ws): + e1 = Equal.sym(S.Cli, S.resolve(spec, []), spec, rs.spec_nil(spec)) + %e1 : {S.env.check(spec, [], S.parse(_, ws)) == S.parse(spec, ws) : Result<&2, &2, S.ParseErr, S.Matched>} + ck.nil(spec, S.parse(spec, ws)) + +def Laws.env_check_fail(_spec, _vars, _ee): + {==} + +def Laws.env_check_good(_nn, _ab, _ver, args, subs, vars, mm, h_none): + e1 = Equal.sym(Maybe<&2, S.Var>, S.env.bad.go(mm, args, subs, vars), None{}, h_none) + %e1 : {S.env.check.done(_, mm) == Done{mm} : Result<&2, &2, S.ParseErr, S.Matched>} + {==} + +def Laws.env_check_bad(_nn, _ab, _ver, args, subs, vars, mm, name, vv, h_bad): + e1 = Equal.sym(Maybe<&2, S.Var>, S.env.bad.go(mm, args, subs, vars), Some{(name, vv)}, h_bad) + %e1 : {S.env.check.done(_, mm) == Fail{S.BadValue{S.path_of(mm), name, vv}} + : Result<&2, &2, S.ParseErr, S.Matched>} + {==} + +def Laws.bad_go_leaf(_bs, _args, _subs, _vars): + {==} + +def Laws.bad_go_root(bs, name, next, args, subs, vars, pp, h_here): + e1 = Equal.sym(Maybe<&2, S.Var>, S.env.bad.args(args, vars, bs), Some{pp}, h_here) + %e1 : {S.env.first(_, + S.env.bad.go(next, S.env.sub.args(S.find_sub(subs, name)), S.env.sub.kids(S.find_sub(subs, name)), vars)) + == Some{pp} : Maybe<&2, S.Var>} + {==} + +def Laws.bad_go_down(bs, name, next, args, subs, vars, h_none): + e1 = Equal.sym(Maybe<&2, S.Var>, S.env.bad.args(args, vars, bs), None{}, h_none) + %e1 : {S.env.first(_, + S.env.bad.go(next, S.env.sub.args(S.find_sub(subs, name)), S.env.sub.kids(S.find_sub(subs, name)), vars)) + == S.env.bad.go(next, S.env.sub.args(S.find_sub(subs, name)), S.env.sub.kids(S.find_sub(subs, name)), vars) + : Maybe<&2, S.Var>} + {==} + +def Laws.bad_args_here(aa, tt, vars, bs, pp, h_here): + e1 = Equal.sym(Maybe<&2, S.Var>, S.env.bad.arg(aa, vars, bs), Some{pp}, h_here) + %e1 : {S.env.first(_, S.env.bad.args(tt, vars, bs)) == Some{pp} : Maybe<&2, S.Var>} + {==} + +def Laws.bad_args_next(aa, tt, vars, bs, h_none): + e1 = Equal.sym(Maybe<&2, S.Var>, S.env.bad.arg(aa, vars, bs), None{}, h_none) + %e1 : {S.env.first(_, S.env.bad.args(tt, vars, bs)) == S.env.bad.args(tt, vars, bs) : Maybe<&2, S.Var>} + {==} + +# an `and` with a false right side is false +def ba.and_false(bb: Bool) -> {Bool.and(bb, False{}) == False{} : Bool}: + match bb: + case True{}: + {==} + case False{}: + {==} + +# a flag is never reported, whatever its env value +def ba.flag( + found: Maybe<&2, String>, + +nn: String, + +cs: List<&2, String>, + +bs: List<&2, S.Bind> +) -> {S.env.bad.val(found, S.Flag{}, nn, cs, bs) == None{} : Maybe<&2, S.Var>}: + match found: + case None{}: + {==} + case Some{_vv}: + {==} + +def Laws.bad_arg_some(nn, _sh, _lo, kind, _hp, _req, ev, _dd, cs, vars, bs, vv, h_env, h_kind, h_out, h_bound): + e1 = Equal.sym(Maybe<&2, String>, S.env.of(ev, vars), Some{vv}, h_env) + %e1 : {S.env.bad.val(_, kind, nn, cs, bs) == Some{(nn, vv)} : Maybe<&2, S.Var>} + e2 = Equal.sym(Bool, S.env.flag.is(kind), False{}, h_kind) + %e2 : {Bool.pick(Maybe<&2, S.Var>, + Bool.and(Bool.not(_), Bool.and(Bool.not(S.allowed(cs, vv)), + List.contains(~String, ~String.eq, S.get_all.bind(bs, nn), vv))), + Some{(nn, vv)}, None{}) == Some{(nn, vv)} : Maybe<&2, S.Var>} + e3 = Equal.sym(Bool, S.allowed(cs, vv), False{}, h_out) + %e3 : {Bool.pick(Maybe<&2, S.Var>, + Bool.and(Bool.not(_), List.contains(~String, ~String.eq, S.get_all.bind(bs, nn), vv)), + Some{(nn, vv)}, None{}) == Some{(nn, vv)} : Maybe<&2, S.Var>} + e4 = Equal.sym(Bool, List.contains(~String, ~String.eq, S.get_all.bind(bs, nn), vv), True{}, h_bound) + %e4 : {Bool.pick(Maybe<&2, S.Var>, _, Some{(nn, vv)}, None{}) == Some{(nn, vv)} : Maybe<&2, S.Var>} + {==} + +def Laws.bad_arg_unset(nn, _sh, _lo, kind, _hp, _req, ev, _dd, cs, vars, bs, h_env): + e1 = Equal.sym(Maybe<&2, String>, S.env.of(ev, vars), None{}, h_env) + %e1 : {S.env.bad.val(_, kind, nn, cs, bs) == None{} : Maybe<&2, S.Var>} + {==} + +def Laws.bad_arg_flag(nn, _sh, _lo, _hp, _req, ev, _dd, cs, vars, bs): + ba.flag(S.env.of(ev, vars), nn, cs, bs) + +def Laws.bad_arg_allowed(nn, _sh, _lo, kind, _hp, _req, ev, _dd, cs, vars, bs, vv, h_env, h_in): + e1 = Equal.sym(Maybe<&2, String>, S.env.of(ev, vars), Some{vv}, h_env) + %e1 : {S.env.bad.val(_, kind, nn, cs, bs) == None{} : Maybe<&2, S.Var>} + e2 = Equal.sym(Bool, S.allowed(cs, vv), True{}, h_in) + %e2 : {Bool.pick(Maybe<&2, S.Var>, + Bool.and(Bool.not(S.env.flag.is(kind)), Bool.and(Bool.not(_), + List.contains(~String, ~String.eq, S.get_all.bind(bs, nn), vv))), + Some{(nn, vv)}, None{}) == None{} : Maybe<&2, S.Var>} + e3 = Equal.sym(Bool, Bool.and(Bool.not(S.env.flag.is(kind)), False{}), False{}, + ba.and_false(Bool.not(S.env.flag.is(kind)))) + %e3 : {Bool.pick(Maybe<&2, S.Var>, _, Some{(nn, vv)}, None{}) == None{} : Maybe<&2, S.Var>} + {==} + +def Laws.bad_arg_unbound(nn, _sh, _lo, kind, _hp, _req, ev, _dd, cs, vars, bs, vv, h_env, h_free): + e1 = Equal.sym(Maybe<&2, String>, S.env.of(ev, vars), Some{vv}, h_env) + %e1 : {S.env.bad.val(_, kind, nn, cs, bs) == None{} : Maybe<&2, S.Var>} + e2 = Equal.sym(Bool, List.contains(~String, ~String.eq, S.get_all.bind(bs, nn), vv), False{}, h_free) + %e2 : {Bool.pick(Maybe<&2, S.Var>, + Bool.and(Bool.not(S.env.flag.is(kind)), Bool.and(Bool.not(S.allowed(cs, vv)), _)), + Some{(nn, vv)}, None{}) == None{} : Maybe<&2, S.Var>} + e3 = Equal.sym(Bool, Bool.and(Bool.not(S.allowed(cs, vv)), False{}), False{}, + ba.and_false(Bool.not(S.allowed(cs, vv)))) + %e3 : {Bool.pick(Maybe<&2, S.Var>, + Bool.and(Bool.not(S.env.flag.is(kind)), _), + Some{(nn, vv)}, None{}) == None{} : Maybe<&2, S.Var>} + e4 = Equal.sym(Bool, Bool.and(Bool.not(S.env.flag.is(kind)), False{}), False{}, + ba.and_false(Bool.not(S.env.flag.is(kind)))) + %e4 : {Bool.pick(Maybe<&2, S.Var>, _, Some{(nn, vv)}, None{}) == None{} : Maybe<&2, S.Var>} + {==} + +def Laws.help_env_shown(_nn, _sh, _lo, _kind, _hp, _req, _var, _dd, _cs): + {==} + +def Laws.help_env_none(_nn, _sh, _lo, _kind, _hp, _req, _dd, _cs): + {==} + +def Laws.env_names_root(_nn, _ab, _ver, _args, _subs): + {==} + +def Laws.env_names_forest(_nn, _ab, _args, _kids, _tt): + {==} + +def Laws.env_names_some(_nn, _sh, _lo, _kind, _hp, _req, _var, _dd, _cs, _tt): + {==} + +def Laws.env_names_none(_nn, _sh, _lo, _kind, _hp, _req, _dd, _cs, _tt): + {==} + +def Laws.kept_set(_nn, _vv, _rest): + {==} + +def Laws.kept_unset(_nn, _ee, _rest): + {==} diff --git a/src/args.bend b/src/args.bend index 307a59b..a96a857 100644 --- a/src/args.bend +++ b/src/args.bend @@ -1,8 +1,10 @@ -# shake/args: the process's arguments, each word reusable, internal (main.bend -# exports it). `IO.args` answers a `&1` list that starts with the program as -# invoked (bend 2.0.32 and later); the rest of a program reads the line more -# than once, so `words` drops that head and copies the rest. +# shake/args: the process's arguments, each word reusable, and the values of a +# spec's env vars, internal (main.bend exports them). `IO.args` answers a `&1` +# list that starts with the program as invoked (bend 2.0.32 and later); the +# rest of a program reads the line more than once, so `words` drops that head +# and copies the rest. import Base +import ./cli.bend as C # a &1 list copied to &2 def copy(xs: List<&1, String>) -> List<&2, String>: @@ -24,3 +26,29 @@ def words(xs: List<&1, String>) -> List<&2, String>: def argv() -> IO(List<&2, String>): # noqa: L001 IO: reads argv (SHAKE-TRUST-4) IO.bind(List<&1, String>, List<&2, String>, IO.args(), xs => IO.pure(List<&2, String>, words(xs))) + +# a name and its value in front of the pairs, when `IO.get_env` found one +def kept( + +name: String, + got: Result<&1, &1, U32 & String, String>, + rest: List<&2, C.Var> +) -> List<&2, C.Var>: + match got: + case Done{vv}: + (name, vv) <> rest + case Fail{_e}: + rest + +# the names that are set, each with its value, in order +def vars(names: List<&2, String>) -> IO(List<&2, C.Var>): # noqa: L001 IO: reads env vars (SHAKE-TRUST-5) + match names: + case Nil{}: + IO.pure(List<&2, C.Var>, []) + case Con{+hh, tt}: + IO.bind(Result<&1, &1, U32 & String, String>, List<&2, C.Var>, IO.get_env(hh), + got => IO.bind(List<&2, C.Var>, List<&2, C.Var>, vars(tt), + rest => IO.pure(List<&2, C.Var>, kept(hh, got, rest)))) + +# the env vars a spec names that are set, each with its value +def env_vars(spec: C.Cli) -> IO(List<&2, C.Var>): # noqa: L001 IO: reads env vars (SHAKE-TRUST-5) + vars(C.env.names(spec)) diff --git a/src/cli.bend b/src/cli.bend index ab2ba86..2dd147f 100644 --- a/src/cli.bend +++ b/src/cli.bend @@ -51,6 +51,10 @@ type Cli is Data: subcommands: List<&2, Sub> } +# an env var's name and its value, as `parse_env` is given them +def Var() -> Data: + Sigma<&2, &2, String, _ => String> + # one bound name and its text type Bind is Data: Bind{name: String, value: String} @@ -186,6 +190,11 @@ def rest( # noqa: L001 a builder: its result is the Arg or Sub it names, nothin ) -> Arg: Arg{name, None{}, None{}, Rest{}, help, required, Fallback{None{}, default}, choices} +# this argument, falling back to the env var `var` (clap's `.env`) +def env(aa: Arg, +var: String) -> Arg: + Arg{+n, +s, +l, kk, +h, +r, Fallback{_e, dd}, cs} = aa + Arg{n, s, l, kk, h, r, Fallback{Some{var}, dd}, cs} + # the larger of two Nats def help.max(+aa: Nat, +bb: Nat) -> Nat: Bool.pick(Nat, Nat.is_le(aa, bb), bb, aa) @@ -1451,6 +1460,258 @@ def parse.finish(st: St) -> Result<&2, &2, ParseErr, Matched>: def parse(app: Cli, argv: List<&2, String>) -> Result<&2, &2, ParseErr, Matched>: parse.finish(parse.walk(argv, parse.start(app))) +# this pair's value when its name matches, else the rest +def env.get.at(hit: Bool, +vv: String, rest: Maybe<&2, String>) -> Maybe<&2, String>: + match hit: + case True{}: + Some{vv} + case False{}: + rest + +# the value of the first pair named `name` +def env.get(vars: List<&2, Var>, +name: String) -> Maybe<&2, String>: + match vars: + case Nil{}: + None{} + case Con{hh, tt}: + (+nn, +vv) = hh + env.get.at(String.eq(nn, name), vv, env.get(tt, name)) + +# a value that is not empty +def env.full(mv: Maybe<&2, String>) -> Maybe<&2, String>: + match mv: + case None{}: + None{} + case Some{+vv}: + Bool.pick(Maybe<&2, String>, String.is_empty(vv), None{}, Some{vv}) + +# the env value of an env var: its first pair's value, when that is not empty +def env.of(ev: Maybe<&2, String>, vars: List<&2, Var>) -> Maybe<&2, String>: + match ev: + case None{}: + None{} + case Some{+var}: + env.full(env.get(vars, var)) + +# whether an env value turns a flag off, as clap's `SetTrue` reads it +def env.off(+vv: String) -> Bool: + allowed.ok(["0", "false", "no", "off", "n", "f"], String.to_lower(vv)) + +# the default an env value gives an argument of this kind: a flag is set +# unless the value turns it off; every other kind takes the value +def env.kind(kk: ArgKind, +vv: String) -> Maybe<&2, String>: + match kk: + case Flag{}: + Bool.pick(Maybe<&2, String>, env.off(vv), None{}, Some{"true"}) + case Opt{}: + Some{vv} + case Many{}: + Some{vv} + case Pos{}: + Some{vv} + case Rest{}: + Some{vv} + +# a fallback with its default replaced by what the env value gives, when +# there is one +def resolve.with( + found: Maybe<&2, String>, + kk: ArgKind, + ev: Maybe<&2, String>, + dd: Maybe<&2, String> +) -> Fallback: + match found: + case None{}: + Fallback{ev, dd} + case Some{+vv}: + Fallback{ev, env.kind(kk, vv)} + +# an argument whose default is its fallback under `vars` +def resolve.arg(aa: Arg, vars: List<&2, Var>) -> Arg: + Arg{+n, +s, +l, +kk, +h, +r, Fallback{+ev, dd}, +cs} = aa + Arg{n, s, l, kk, h, r, resolve.with(env.of(ev, vars), kk, ev, dd), cs} + +# every argument's default is its fallback +def resolve.args(args: List<&2, Arg>, +vars: List<&2, Var>) -> List<&2, Arg>: + match args: + case Nil{}: + [] + case Con{hh, tt}: + resolve.arg(hh, vars) <> resolve.args(tt, vars) + +# every argument of every subcommand, its default its fallback +def resolve.subs(subs: List<&2, Sub>, +vars: List<&2, Var>) -> List<&2, Sub>: + match subs: + case Nil{}: + [] + case Con{hh, tt}: + Sub{+n, +a, args, kids} = hh + Sub{n, a, resolve.args(args, vars), resolve.subs(kids, vars)} <> resolve.subs(tt, vars) + +# the spec whose every argument's default is its fallback under `vars` +def resolve(app: Cli, +vars: List<&2, Var>) -> Cli: + Cli{+n, +a, +v, args, subs} = app + Cli{n, a, v, resolve.args(args, vars), resolve.subs(subs, vars)} + +# whether this kind is a flag +def env.flag.is(kk: ArgKind) -> Bool: + match kk: + case Flag{}: + True{} + case Opt{}: + False{} + case Many{}: + False{} + case Pos{}: + False{} + case Rest{}: + False{} + +# an argument bound to an env value outside its choices: never a flag, and +# only for a value its command's bindings hold +def env.bad.val( + found: Maybe<&2, String>, + kk: ArgKind, + +name: String, + +cs: List<&2, String>, + +binds: List<&2, Bind> +) -> Maybe<&2, Var>: + match found: + case None{}: + None{} + case Some{+vv}: + Bool.pick(Maybe<&2, Var>, + Bool.and(Bool.not(env.flag.is(kk)), Bool.and(Bool.not(allowed(cs, vv)), + List.contains(~String, ~String.eq, get_all.bind(binds, name), vv))), + Some{(name, vv)}, None{}) + +# this argument's name and env value, when its command's bindings hold that +# value and its choices do not +def env.bad.arg(aa: Arg, vars: List<&2, Var>, +binds: List<&2, Bind>) -> Maybe<&2, Var>: + Arg{+n, _s, _l, kk, _h, _r, Fallback{ev, _d}, +cs} = aa + env.bad.val(env.of(ev, vars), kk, n, cs, binds) + +# the first of two answers that is one +def env.first(here: Maybe<&2, Var>, rest: Maybe<&2, Var>) -> Maybe<&2, Var>: + match here: + case None{}: + rest + case Some{pp}: + Some{pp} + +# the first argument of a command bound to an env value outside its choices +def env.bad.args( + args: List<&2, Arg>, + +vars: List<&2, Var>, + +binds: List<&2, Bind> +) -> Maybe<&2, Var>: + match args: + case Nil{}: + None{} + case Con{hh, tt}: + env.first(env.bad.arg(hh, vars, binds), env.bad.args(tt, vars, binds)) + +# the arguments of a found subcommand, or none +def env.sub.args(found: Maybe<&2, Sub>) -> List<&2, Arg>: + match found: + case None{}: + [] + case Some{ss}: + Sub{_n, _a, args, _k} = ss + args + +# the subcommands of a found subcommand, or none +def env.sub.kids(found: Maybe<&2, Sub>) -> List<&2, Sub>: + match found: + case None{}: + [] + case Some{ss}: + Sub{_n, _a, _g, kids} = ss + kids + +# the first argument bound to an env value outside its choices, the command +# first, then down the selected path +def env.bad.go( + mm: Matched, + +args: List<&2, Arg>, + +subs: List<&2, Sub>, + +vars: List<&2, Var> +) -> Maybe<&2, Var>: + match mm: + case Leaf{+bs}: + env.bad.args(args, vars, bs) + case Node{+bs, +name, next}: + env.first(env.bad.args(args, vars, bs), + env.bad.go(next, env.sub.args(find_sub(subs, name)), env.sub.kids(find_sub(subs, name)), vars)) + +# a success, or the first env value outside its choices that it bound +def env.check.done(bad: Maybe<&2, Var>, +mm: Matched) -> Result<&2, &2, ParseErr, Matched>: + match bad: + case None{}: + Done{mm} + case Some{pp}: + (+name, +vv) = pp + Fail{BadValue{path_of(mm), name, vv}} + +# a successful parse checked for env values outside their choices +def env.check.ok(app: Cli, +vars: List<&2, Var>, +mm: Matched) -> Result<&2, &2, ParseErr, Matched>: + Cli{_n, _a, _v, +args, subs} = app + env.check.done(env.bad.go(mm, args, subs, vars), mm) + +# a failed parse as it is; a successful one checked for env values outside +# their choices +def env.check( + app: Cli, + +vars: List<&2, Var>, + got: Result<&2, &2, ParseErr, Matched> +) -> Result<&2, &2, ParseErr, Matched>: + match got: + case Fail{ee}: + Fail{ee} + case Done{+mm}: + env.check.ok(app, vars, mm) + +# argv against a Cli, every argument falling back to its env value under +# `vars`, then to its default +def parse_env( + +app: Cli, + argv: List<&2, String>, + +vars: List<&2, Var> +) -> Result<&2, &2, ParseErr, Matched>: + env.check(app, vars, parse(resolve(app, vars), argv)) + +# an env var in front of the names, when there is one +def env.names.put(ev: Maybe<&2, String>, rest: List<&2, String>) -> List<&2, String>: + match ev: + case None{}: + rest + case Some{var}: + var <> rest + +# the env vars of a command's arguments, in order +def env.names.args(args: List<&2, Arg>) -> List<&2, String>: + match args: + case Nil{}: + [] + case Con{hh, tt}: + Arg{_n, _s, _l, _k, _h, _r, Fallback{ev, _d}, _c} = hh + env.names.put(ev, env.names.args(tt)) + +# the env vars of every subcommand's arguments, depth first +def env.names.forest(subs: List<&2, Sub>) -> List<&2, String>: + match subs: + case Nil{}: + [] + case Con{hh, tt}: + Sub{_n, _a, args, kids} = hh + List.append(&2, String, env.names.args(args), + List.append(&2, String, env.names.forest(kids), env.names.forest(tt))) + +# the env vars of a spec: the root's arguments', then every subcommand's +def env.names(app: Cli) -> List<&2, String>: + Cli{_n, _a, _v, args, subs} = app + List.append(&2, String, env.names.args(args), env.names.forest(subs)) + # the short/long label of an option, plus a metavar for Opt def help.label.kind(kk: ArgKind, +name: String, +label: String) -> String: match kk: @@ -1487,10 +1748,18 @@ def help.extra.go(+dd: String, +cs: List<&2, String>) -> String: " [default: " ++ dd ++ "] [possible values: " ++ String.join(cs, ", ") ++ "]")) -# extras after the help string +# the env var after the help string, before the default +def help.env(ev: Maybe<&2, String>) -> String: + match ev: + case None{}: + "" + case Some{var}: + " [env: " ++ var ++ "]" + +# extras after the help string: env var, default and choices def help.extra(aa: Arg) -> String: - Arg{_n, _s, _l, _k, _h, _r, Fallback{_e, default}, cs} = aa - help.extra.go(text.of(default, ""), cs) + Arg{_n, _s, _l, _k, _h, _r, Fallback{ev, default}, cs} = aa + help.env(ev) ++ help.extra.go(text.of(default, ""), cs) # one option line, given the label width def help.opt_line(+aa: Arg, ww: Nat) -> String: From 9c26c59bc8277fcab0b37da29e9af3c32921d4c7 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 2 Oct 2026 01:43:38 +0000 Subject: [PATCH 4/7] docs: env fallbacks in the README; RFC types follow the Var alias Co-authored-by: noah-emp --- README.md | 30 ++++++++++++++++++++++----- docs/rfc/shake-env-and-suggestions.md | 14 +++++++------ 2 files changed, 33 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 912c889..ab8a40a 100644 --- a/README.md +++ b/README.md @@ -64,11 +64,12 @@ On bend 2.0.32 and later, `IO.args()` starts with the program as invoked does it for you. shake needs bend 2.0.32 or later for that reason. `main.bend` is the whole interface: the types (`Shake.Cli`, `Shake.Sub`, -`Shake.Arg`, `Shake.Matched`, `Shake.ParseErr`, `Shake.SpecErr`), the -builders (`app`, `sub`, `flag`, `opt`, `many`, `pos`, `rest`), `check` and -`spec_err_text`, `parse`, the readers (`get`, `get_all`, `on`, `sub_name`, -`sub_of`, `at`, `path_of`), `help`, `err_text`, `help_path`, `err_path` and -`argv`. Everything under `src/` is +`Shake.Arg`, `Shake.Matched`, `Shake.ParseErr`, `Shake.SpecErr`, +`Shake.Var`), the builders (`app`, `sub`, `flag`, `opt`, `many`, `pos`, +`rest`, `env`), `check` and `spec_err_text`, `parse` and `parse_env`, the +readers (`get`, `get_all`, `on`, `sub_name`, `sub_of`, `at`, `path_of`), +`help`, `err_text`, `help_path`, `err_path`, `argv` and `env_vars`. +Everything under `src/` is internal and may change in any release; import only `main.bend`. [SPEC.md](SPEC.md) lists what shake guarantees, and which of it is proved. @@ -93,6 +94,25 @@ positional keeps every leftover word under one name; `get_all` reads that list, and `get` still reads one value. `argv` is the process's arguments, each word reusable. +`env(arg, "NAME")` gives an argument an env var to fall back to, as clap's +`.env("NAME")`: `parse_env(spec, words, vars)` binds what the words give, +then fills an argument they left unbound from its env var, then from its +default. `env_vars(spec)` reads the env vars the spec names, as +`(name, value)` pairs; a test passes its own, as in +`parse_env(spec(), [], [("HI_NAME", "Ada")])`. An env var set to the empty +string counts as unset. A flag's env var sets it unless its value, in any +case, is `0`, `false`, `no`, `off`, `n` or `f`. An env value outside the +argument's choices fails the parse with `BadValue`. Help shows +`[env: NAME]` after the argument's help text. `parse` ignores env vars. + +```bend +def main() -> IO(Unit): + do IO: + av : List<&2, String> <- Shake.argv() + ev : List<&2, Shake.Var> <- Shake.env_vars(spec()) + IO.print(greet(Shake.parse_env(spec(), av, ev))) +``` + A compiled Bend program's runtime reads the command line before shake does (bend 2.0.34): diff --git a/docs/rfc/shake-env-and-suggestions.md b/docs/rfc/shake-env-and-suggestions.md index 02d1d6b..8dd5f57 100644 --- a/docs/rfc/shake-env-and-suggestions.md +++ b/docs/rfc/shake-env-and-suggestions.md @@ -35,7 +35,7 @@ def spec() -> Shake.Cli: def main() -> IO(Unit): do IO: av : List<&2, String> <- Shake.argv() - ev : List<&2, String & String> <- Shake.env_vars(spec()) + ev : List<&2, Shake.Var> <- Shake.env_vars(spec()) IO.print(greet(Shake.parse_env(spec(), av, ev))) ``` @@ -68,12 +68,14 @@ type Fallback is Data: type Arg is Data: Arg{name, short, long, kind, help, required, fallback: Fallback, choices} -# main.bend, new -def env(+arg: S.Arg, +var: String) -> S.Arg -def parse_env(spec: S.Cli, words: List<&2, String>, vars: List<&2, String & String>) +# main.bend, new; a pair `String & String` is a Type, not Data, so a list +# of them is a list of `Var` +def Var() -> Data: Sigma<&2, &2, String, _ => String> +def env(arg: S.Arg, +var: String) -> S.Arg +def parse_env(+spec: S.Cli, words: List<&2, String>, +vars: List<&2, S.Var>) -> Result<&2, &2, S.ParseErr, S.Matched> def suggestion(+spec: S.Cli, err: S.ParseErr) -> Maybe<&2, String> -def env_vars(spec: S.Cli) -> IO(List<&2, String & String>) +def env_vars(spec: S.Cli) -> IO(List<&2, S.Var>) ``` **The env var sits beside the default.** `Arg`'s seventh field, the default, becomes `Fallback{env, default}`: both say what an argument falls back to when the words leave it unbound, and keeping them together leaves `Arg` at eight fields, so a destructuring that ignores the default (`_d`) does not change. The builders keep their signatures and build `Fallback{None{}, default}`; `env(arg, var)` sets the env var, as clap's `.env(var)` does, so no caller of a builder breaks. @@ -124,4 +126,4 @@ Three candidates were sketched: A (gpt-5.6), C (this author), and B (grok), whic ## Next implementation step -Change `Arg`'s default to `Fallback{env, default}` through `src/` and the laws, with the gate green and no behavior change, before adding anything that reads `env`. +Step 2 has landed. Next: `suggestion` and the tip in `err_text`, with the laws of SHAKE-ERR-3 and ERR-4. From 31f8df9f91be5171a9e8e4768abf9a259e16be24 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 2 Oct 2026 01:50:43 +0000 Subject: [PATCH 5/7] feat: did-you-mean suggestion for unknown long options, shown as clap's tip in err_text; prove SHAKE-ERR-3, ERR-4 Co-authored-by: noah-emp --- SPEC.md | 6 +- main.bend | 6 ++ src/LAWS.bend | 148 ++++++++++++++++++++++++++++- src/PROOF.bend | 248 ++++++++++++++++++++++++++++++++++++++++++++++++- src/cli.bend | 227 +++++++++++++++++++++++++++++++++++++++++++- src/eq.bend | 11 +++ 6 files changed, 638 insertions(+), 8 deletions(-) diff --git a/SPEC.md b/SPEC.md index 6119813..ed20b2b 100644 --- a/SPEC.md +++ b/SPEC.md @@ -84,8 +84,8 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | :---- | :---- | :---- | :---- | :---- | | SHAKE-ERR-1 | `err_text(spec, err)` is empty exactly when `help_path(err)` is `Some`, that is, when the parse failed with a request for help. | Proved | proved | src/LAWS.bend err_text_help; src/LAWS.bend err_text_iff | | SHAKE-ERR-2 | For every error but a request for help, `err_path(err)` is the path of subcommands the parse had selected at the word that failed it, and `err_text(spec, err)` shows the usage line of the command at that path, as `help(spec, err_path(err))` does. | Proved | proved | src/LAWS.bend err_path_at; src/LAWS.bend err_text_usage; src/LAWS.bend help_page; src/LAWS.bend unknown_long; src/LAWS.bend unknown_short; src/LAWS.bend no_pos_left; src/LAWS.bend choice_refused; src/LAWS.bend flag_long_valued; src/LAWS.bend value_flag_shaped; src/LAWS.bend value_absent; src/LAWS.bend help_unknown; src/LAWS.bend long_no_name; src/LAWS.bend repeated_long_flag; src/LAWS.bend repeated_long_opt; src/LAWS.bend value_refused; src/LAWS.bend long_refused; src/LAWS.bend raw_no_pos; src/LAWS.bend raw_refused; src/LAWS.bend enter_missing; src/LAWS.bend required_missing; src/LAWS.bend letter_flag_eq; src/LAWS.bend letter_unknown; src/LAWS.bend letter_flag_again; src/LAWS.bend letter_opt_again; src/LAWS.bend letter_value_bad | -| SHAKE-ERR-3 | `suggestion(spec, err)` is `None` for every error but an `UnknownFlag{at, word}` whose word starts with `--` (SHAKE-TOK-1, TOK-7). For such a word, let `typed` be its chars after `--` up to its first `=`, and the **candidates** the long spellings of the flags and options of the command at `at`, reached as `help(spec, at)` reaches it (SHAKE-HELP-1), in spec order; a parent command's arguments, subcommands and `help` are not candidates. A candidate `c` is **close** when `0 < d` and `3 * d <= max(length(typed), length(c))`, where `d` is the optimal string alignment distance from `typed` to `c`: the fewest single-char insertions, deletions, substitutions and swaps of two adjacent chars that turn one into the other, editing no char twice. The suggestion is `Some{"--" ++ c}` for the close candidate with the least `d`, the first in spec order among equals, and `None` when no candidate is close. A short option word never gets one. | Proved | pending | | -| SHAKE-ERR-4 | When `suggestion(spec, err)` is `Some{s}`, `err_text(spec, err)` contains `s`. | Proved | pending | | +| SHAKE-ERR-3 | `suggestion(spec, err)` is `None` for every error but an `UnknownFlag{at, word}` whose word starts with `--` (SHAKE-TOK-1, TOK-7). For such a word, let `typed` be its chars after `--` up to its first `=`, and the **candidates** the long spellings of the flags and options of the command at `at`, reached as `help(spec, at)` reaches it (SHAKE-HELP-1), in spec order; a parent command's arguments, subcommands and `help` are not candidates. A candidate `c` is **close** when `0 < d` and `3 * d <= max(length(typed), length(c))`, where `d` is the optimal string alignment distance from `typed` to `c`: the fewest single-char insertions, deletions, substitutions and swaps of two adjacent chars that turn one into the other, editing no char twice. The suggestion is `Some{"--" ++ c}` for the close candidate with the least `d`, the first in spec order among equals, and `None` when no candidate is close. A short option word never gets one. | Proved | proved | src/LAWS.bend sug_other; src/LAWS.bend sug_short; src/LAWS.bend sug_long; src/LAWS.bend sug_found_some; src/LAWS.bend cands_some; src/LAWS.bend cands_none; src/LAWS.bend sug_close; src/LAWS.bend best_nil; src/LAWS.bend best_far; src/LAWS.bend best_only; src/LAWS.bend best_here; src/LAWS.bend best_there | +| SHAKE-ERR-4 | When `suggestion(spec, err)` is `Some{s}`, `err_text(spec, err)` contains `s`. | Proved | proved | src/LAWS.bend err_text_tip | ### The argument list (SHAKE-ARGS) @@ -96,7 +96,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n ## Left to prove -SHAKE-ERR-3 and ERR-4 are pending: their laws land with the code that implements them ([docs/rfc/shake-env-and-suggestions.md](docs/rfc/shake-env-and-suggestions.md), Rollout). Every other row is proved. The RFC's Rollout and [docs/rfc/shake-walker-proofs.md](docs/rfc/shake-walker-proofs.md) say in which phase each row's laws land. Every walker law holds wherever the words before the word it is about leave the walker in the state its premise names. +No row is pending. The RFC's Rollout and [docs/rfc/shake-walker-proofs.md](docs/rfc/shake-walker-proofs.md) say in which phase each row's laws land. Every walker law holds wherever the words before the word it is about leave the walker in the state its premise names. ## Trust boundary diff --git a/main.bend b/main.bend index 5ea44f0..b9bb129 100644 --- a/main.bend +++ b/main.bend @@ -193,6 +193,12 @@ def help(+spec: S.Cli, path: List<&2, String>) -> String: def err_text(+spec: S.Cli, err: S.ParseErr) -> String: S.err_text(spec, err) +# for an unknown long option, the long option word of the current command it +# was likely meant to be, as `--name` for `--nmae`, which `err_text` shows as +# clap's tip; None for every other error and when nothing is close +def suggestion(+spec: S.Cli, err: S.ParseErr) -> Maybe<&2, String>: + S.suggestion(spec, err) + # the command path where the parse failed: the path selected when it did, or # for a request for help the path it asks about def err_path(err: S.ParseErr) -> List<&2, String>: diff --git a/src/LAWS.bend b/src/LAWS.bend index d679e0e..800353f 100644 --- a/src/LAWS.bend +++ b/src/LAWS.bend @@ -2370,7 +2370,7 @@ law err_path_at: # then where to look for more # SHAKE-ERR-2 law err_text_usage: - for spec: Shake.Cli + for +spec: Shake.Cli for +err: Shake.ParseErr for h_err: {Shake.help_path(err) == None{} : Maybe<&2, List<&2, String>>} exs msg: String @@ -3358,3 +3358,149 @@ law kept_unset: for ee: U32 & String for rest: List<&2, Shake.Var> {Args.kept(nn, Fail{ee}, rest) == rest : List<&2, Shake.Var>} + +# whether an error is an unknown option +def unknown.is(err: Shake.ParseErr) -> Bool: + match err: + case S.UnknownFlag{_at, _word}: + True{} + case _other: + False{} + +# the arguments of a page's command +def how_args(how: S.How) -> List<&2, S.Arg>: + S.How{_b, _a, _v, args, _s, _u} = how + args + +# LAW: only an unknown option can get a suggestion +# SHAKE-ERR-3 +law sug_other: + for spec: Shake.Cli + for +err: Shake.ParseErr + for h_err: {unknown.is(err) == False{} : Bool} + {Shake.suggestion(spec, err) == None{} : Maybe<&2, String>} + +# LAW: a word that does not start with `--` gets no suggestion +# SHAKE-ERR-3 +law sug_short: + for +spec: Shake.Cli + for +at: List<&2, String> + for +word: String + for h_word: {String.starts_with(word, "--") == False{} : Bool} + {Shake.suggestion(spec, S.UnknownFlag{at, word}) == None{} : Maybe<&2, String>} + +# LAW: a long option word's suggestion is the closest close candidate to its +# spelling up to `=`, among the long spellings of the command at `at`, reached +# as `help` reaches it, as a long option word +# SHAKE-ERR-3 +law sug_long: + for +spec: Shake.Cli + for +at: List<&2, String> + for +body: String + for +name: String + for val: Maybe<&2, String> + for h_cut: {S.cut_eq(body) == (name, val) : String & Maybe<&2, String>} + {Shake.suggestion(spec, S.UnknownFlag{at, "--" ++ body}) + == S.sug.found(S.sug.best(S.sug.cands(how_args(reach(at, root(spec)))), name)) : Maybe<&2, String>} + +# LAW: a candidate is suggested as its long option word +# SHAKE-ERR-3 +law sug_found_some: + for cc: String + {S.sug.found(Some{cc}) == Some{"--" ++ cc} : Maybe<&2, String>} + +# LAW: an argument with a long spelling is a candidate, in spec order +# SHAKE-ERR-3 +law cands_some: + for nn: String + for sh: Maybe<&2, String> + for ll: String + for kind: S.ArgKind + for hp: String + for req: Bool + for fb: S.Fallback + for cs: List<&2, String> + for tt: List<&2, S.Arg> + {S.sug.cands(S.Arg{nn, sh, Some{ll}, kind, hp, req, fb, cs} <> tt) == ll <> S.sug.cands(tt) : List<&2, String>} + +# LAW: an argument with no long spelling is not a candidate +# SHAKE-ERR-3 +law cands_none: + for nn: String + for sh: Maybe<&2, String> + for kind: S.ArgKind + for hp: String + for req: Bool + for fb: S.Fallback + for cs: List<&2, String> + for tt: List<&2, S.Arg> + {S.sug.cands(S.Arg{nn, sh, None{}, kind, hp, req, fb, cs} <> tt) == S.sug.cands(tt) : List<&2, String>} + +# LAW: a candidate is close when it is some edits away, and three times as +# many is at most the longer length +# SHAKE-ERR-3 +law sug_close: + for +typed: String + for +cc: String + {S.sug.close(typed, cc) + == Bool.and(Nat.is_lt(0n, S.osa(typed, cc)), + Nat.is_le(Nat.mul(3n, S.osa(typed, cc)), Nat.max(String.length(typed), String.length(cc)))) : Bool} + +# LAW: no candidates, no closest one +# SHAKE-ERR-3 +law best_nil: + for typed: String + {S.sug.best([], typed) == None{} : Maybe<&2, String>} + +# LAW: a candidate that is not close is passed over +# SHAKE-ERR-3 +law best_far: + for +cc: String + for +tt: List<&2, String> + for +typed: String + for h_far: {S.sug.close(typed, cc) == False{} : Bool} + {S.sug.best(cc <> tt, typed) == S.sug.best(tt, typed) : Maybe<&2, String>} + +# LAW: a close candidate with none close after it is the closest +# SHAKE-ERR-3 +law best_only: + for +cc: String + for +tt: List<&2, String> + for +typed: String + for h_close: {S.sug.close(typed, cc) == True{} : Bool} + for h_rest: {S.sug.best(tt, typed) == None{} : Maybe<&2, String>} + {S.sug.best(cc <> tt, typed) == Some{cc} : Maybe<&2, String>} + +# LAW: a close candidate no farther than the closest after it is the closest: +# the first wins a tie +# SHAKE-ERR-3 +law best_here: + for +cc: String + for +tt: List<&2, String> + for +typed: String + for +ww: String + for h_close: {S.sug.close(typed, cc) == True{} : Bool} + for h_rest: {S.sug.best(tt, typed) == Some{ww} : Maybe<&2, String>} + for h_le: {Nat.is_le(S.osa(typed, cc), S.osa(typed, ww)) == True{} : Bool} + {S.sug.best(cc <> tt, typed) == Some{cc} : Maybe<&2, String>} + +# LAW: a close candidate farther than the closest after it is passed over +# SHAKE-ERR-3 +law best_there: + for +cc: String + for +tt: List<&2, String> + for +typed: String + for +ww: String + for h_close: {S.sug.close(typed, cc) == True{} : Bool} + for h_rest: {S.sug.best(tt, typed) == Some{ww} : Maybe<&2, String>} + for h_le: {Nat.is_le(S.osa(typed, cc), S.osa(typed, ww)) == False{} : Bool} + {S.sug.best(cc <> tt, typed) == Some{ww} : Maybe<&2, String>} + +# LAW: the error text shows the suggestion, when there is one +# SHAKE-ERR-4 +law err_text_tip: + for +spec: Shake.Cli + for +err: Shake.ParseErr + for +ss: String + for h_sug: {Shake.suggestion(spec, err) == Some{ss} : Maybe<&2, String>} + {String.contains(Shake.err_text(spec, err), ss) == True{} : Bool} diff --git a/src/PROOF.bend b/src/PROOF.bend index 6d63877..31151f3 100644 --- a/src/PROOF.bend +++ b/src/PROOF.bend @@ -4922,8 +4922,8 @@ def et.some_none(+path: List<&2, String>, hh: {Some{path} == None{} : Maybe<&2, def Laws.err_text_usage(spec, err, h_err): match err: case S.UnknownFlag{+at, +word}: - ("error: unexpected argument '" ++ word ++ "' found", - et.wrap(spec, at, "error: unexpected argument '" ++ word ++ "' found")) + ("error: unexpected argument '" ++ word ++ "' found" ++ S.sug.tip(S.sug.word(spec, at, word)), + et.wrap(spec, at, "error: unexpected argument '" ++ word ++ "' found" ++ S.sug.tip(S.sug.word(spec, at, word)))) case S.Missing{+at, +name}: ("error: the following required argument was not provided:\n " ++ name, et.wrap(spec, at, "error: the following required argument was not provided:\n " ++ name)) @@ -10288,3 +10288,247 @@ def Laws.kept_set(_nn, _vv, _rest): def Laws.kept_unset(_nn, _ee, _rest): {==} + +def Laws.sug_other(spec, err, h_err): + match err: + case S.UnknownFlag{at, word}: + Empty.absurd({S.suggestion(spec, S.UnknownFlag{at, word}) == None{} : Maybe<&2, String>}, + Walk.wk.true_false(h_err)) + case S.Missing{_at, _name}: + {==} + case S.NoValue{_at, _name}: + {==} + case S.BadValue{_at, _name, _value}: + {==} + case S.NeedHelp{_path}: + {==} + case S.Unexpected{_at, _arg}: + {==} + case S.Repeated{_at, _name}: + {==} + +def Laws.sug_short(spec, at, word, h_word): + e1 = Equal.sym(Bool, String.starts_with(word, "--"), False{}, h_word) + %e1 : {S.sug.word.go(_, spec, at, word) == None{} : Maybe<&2, String>} + {==} + +# the arguments reached down a path are those of the page `help` reaches +def sa.go( + path: List<&2, String>, + how: S.How +) -> {S.sug.args.go(path, how) == Laws.how_args(Laws.reach(path, how)) : List<&2, S.Arg>}: + match path: + case Nil{}: + match how: + case S.How{_b, _a, _v, _g, _s, _u}: + {==} + case Con{+hh, tt}: + sa.go(tt, S.help.step(how, hh)) + +# the arguments of the command at a path are those of its help page +def sa.reach( + spec: S.Cli, + path: List<&2, String> +) -> {S.sug.args(spec, path) == Laws.how_args(Laws.reach(path, Laws.root(spec))) : List<&2, S.Arg>}: + match spec: + case S.Cli{+n, a, v, args, subs}: + sa.go(path, S.How{n, a, v, args, subs, n}) + +def Laws.sug_long(spec, at, body, name, val, h_cut): + e1 = Equal.sym(Bool, String.starts_with(body, ""), True{}, Laws.prefix_empty(body)) + %e1 : {S.sug.word.go(_, spec, at, "--" ++ body) + == S.sug.found(S.sug.best(S.sug.cands(Laws.how_args(Laws.reach(at, Laws.root(spec)))), name)) + : Maybe<&2, String>} + e2 = Equal.sym(String, String.drop(body, 0n), body, Laws.drop_zero(body)) + %e2 : {S.sug.found(S.sug.best(S.sug.cands(S.sug.args(spec, at)), S.sug.typed(S.cut_eq(_)))) + == S.sug.found(S.sug.best(S.sug.cands(Laws.how_args(Laws.reach(at, Laws.root(spec)))), name)) + : Maybe<&2, String>} + e3 = Equal.sym(String & Maybe<&2, String>, S.cut_eq(body), (name, val), h_cut) + %e3 : {S.sug.found(S.sug.best(S.sug.cands(S.sug.args(spec, at)), S.sug.typed(_))) + == S.sug.found(S.sug.best(S.sug.cands(Laws.how_args(Laws.reach(at, Laws.root(spec)))), name)) + : Maybe<&2, String>} + e4 = Equal.sym(List<&2, S.Arg>, S.sug.args(spec, at), Laws.how_args(Laws.reach(at, Laws.root(spec))), + sa.reach(spec, at)) + %e4 : {S.sug.found(S.sug.best(S.sug.cands(_), name)) + == S.sug.found(S.sug.best(S.sug.cands(Laws.how_args(Laws.reach(at, Laws.root(spec)))), name)) + : Maybe<&2, String>} + {==} + +def Laws.sug_found_some(_cc): + {==} + +def Laws.cands_some(_nn, _sh, _ll, _kind, _hp, _req, _fb, _cs, _tt): + {==} + +def Laws.cands_none(_nn, _sh, _kind, _hp, _req, _fb, _cs, _tt): + {==} + +def Laws.sug_close(_typed, _cc): + {==} + +def Laws.best_nil(_typed): + {==} + +def Laws.best_far(cc, tt, typed, h_far): + e1 = Equal.sym(Bool, S.sug.close(typed, cc), False{}, h_far) + %e1 : {S.sug.keep(_, typed, cc, S.sug.best(tt, typed)) == S.sug.best(tt, typed) : Maybe<&2, String>} + {==} + +def Laws.best_only(cc, tt, typed, h_close, h_rest): + e1 = Equal.sym(Bool, S.sug.close(typed, cc), True{}, h_close) + %e1 : {S.sug.keep(_, typed, cc, S.sug.best(tt, typed)) == Some{cc} : Maybe<&2, String>} + e2 = Equal.sym(Maybe<&2, String>, S.sug.best(tt, typed), None{}, h_rest) + %e2 : {S.sug.keep(True{}, typed, cc, _) == Some{cc} : Maybe<&2, String>} + {==} + +def Laws.best_here(cc, tt, typed, ww, h_close, h_rest, h_le): + e1 = Equal.sym(Bool, S.sug.close(typed, cc), True{}, h_close) + %e1 : {S.sug.keep(_, typed, cc, S.sug.best(tt, typed)) == Some{cc} : Maybe<&2, String>} + e2 = Equal.sym(Maybe<&2, String>, S.sug.best(tt, typed), Some{ww}, h_rest) + %e2 : {S.sug.keep(True{}, typed, cc, _) == Some{cc} : Maybe<&2, String>} + e3 = Equal.sym(Bool, Nat.is_le(S.osa(typed, cc), S.osa(typed, ww)), True{}, h_le) + %e3 : {Bool.pick(Maybe<&2, String>, _, Some{cc}, Some{ww}) == Some{cc} : Maybe<&2, String>} + {==} + +def Laws.best_there(cc, tt, typed, ww, h_close, h_rest, h_le): + e1 = Equal.sym(Bool, S.sug.close(typed, cc), True{}, h_close) + %e1 : {S.sug.keep(_, typed, cc, S.sug.best(tt, typed)) == Some{ww} : Maybe<&2, String>} + e2 = Equal.sym(Maybe<&2, String>, S.sug.best(tt, typed), Some{ww}, h_rest) + %e2 : {S.sug.keep(True{}, typed, cc, _) == Some{ww} : Maybe<&2, String>} + e3 = Equal.sym(Bool, Nat.is_le(S.osa(typed, cc), S.osa(typed, ww)), False{}, h_le) + %e3 : {Bool.pick(Maybe<&2, String>, _, Some{cc}, Some{ww}) == Some{ww} : Maybe<&2, String>} + {==} + +# that `qq` contains `ss` +def ct.has(qq: String, ss: String) -> Type: + {String.contains(qq, ss) == True{} : Bool} + +# appending is associative +def ct.assoc(aa: String, +bb: String, +cc: String) -> {(aa ++ bb) ++ cc == aa ++ (bb ++ cc) : String}: + match aa: + case SNil{}: + {==} + case SCon{+hh, tt}: + Equal.cong(String, String, ys => SCon{hh, ys}, (tt ++ bb) ++ cc, tt ++ (bb ++ cc), ct.assoc(tt, bb, cc)) + +# a string starts with itself, whatever follows +def ct.starts(ss: String, +post: String) -> {String.starts_with(ss ++ post, ss) == True{} : Bool}: + match ss: + case SNil{}: + Laws.prefix_empty(post) + case SCon{+hh, tt}: + e1 = Equal.sym(Bool, Char.is_eq(hh, hh), True{}, Eq.char_eq_self(hh)) + %e1 : {String.starts_with.if(tt ++ post, tt, _) == True{} : Bool} + ct.starts(tt, post) + +# every string contains the empty one +def ct.nil(post: String) -> ct.has(post, ""): + match post: + case SNil{}: + {==} + case SCon{_h, _t}: + {==} + +# a string contains itself, whatever follows +def ct.front(ss: String, +post: String) -> ct.has(ss ++ post, ss): + match ss: + case SNil{}: + ct.nil(post) + case SCon{+hh, +tt}: + e1 = Equal.sym(Bool, String.starts_with(SCon{hh, tt ++ post}, SCon{hh, tt}), True{}, + ct.starts(SCon{hh, tt}, post)) + %e1 : {String.contains.if(tt ++ post, SCon{hh, tt}, _) == True{} : Bool} + {==} + +# a contained string stays contained, here or further on +def ct.if( + tt: String, + +ss: String, + here: Bool, + hh: ct.has(tt, ss) +) -> {String.contains.if(tt, ss, here) == True{} : Bool}: + match here: + case False{}: + hh + case True{}: + {==} + +# what a string contains, it contains after anything +def ct.after(pre: String, +qq: String, +ss: String, hh: ct.has(qq, ss)) -> ct.has(pre ++ qq, ss): + match pre: + case SNil{}: + hh + case SCon{+ch, +tt}: + ct.if(tt ++ qq, ss, String.starts_with(SCon{ch, tt ++ qq}, ss), ct.after(tt, qq, ss, hh)) + +# a string contained in the part after `pp` is contained in the whole +def ct.step( + +pp: String, + +qq: String, + +rr: String, + +ss: String, + hh: ct.has(qq ++ rr, ss) +) -> ct.has((pp ++ qq) ++ rr, ss): + e1 = Equal.sym(String, (pp ++ qq) ++ rr, pp ++ (qq ++ rr), ct.assoc(pp, qq, rr)) + %e1 : {String.contains(_, ss) == True{} : Bool} + ct.after(pp, qq ++ rr, ss, hh) + +# a string is contained where it leads +def ct.lead(+ss: String, +qq: String, +rr: String) -> ct.has((ss ++ qq) ++ rr, ss): + e1 = Equal.sym(String, (ss ++ qq) ++ rr, ss ++ (qq ++ rr), ct.assoc(ss, qq, rr)) + %e1 : {String.contains(_, ss) == True{} : Bool} + ct.front(ss, qq ++ rr) + +# the type that is empty exactly where a Maybe is Some +def mb.emp(mm: Maybe<&2, String>) -> Type: + match mm: + case None{}: + Unit + case Some{_s}: + Empty + +# that None is Some +def mb.none_some(ss: String) -> Type: + {None{} == Some{ss} : Maybe<&2, String>} + +# None is not Some +def mb.clash(+ss: String, eq: mb.none_some(ss)) -> Empty: + %eq : mb.emp(_) + Unit{} + +# an error with no suggestion proves anything about its text +def tp.none( + +spec: S.Cli, + +err: S.ParseErr, + +ss: String, + eq: mb.none_some(ss) +) -> ct.has(S.err_text(spec, err), ss): + Empty.absurd(ct.has(S.err_text(spec, err), ss), mb.clash(ss, eq)) + +def Laws.err_text_tip(spec, err, ss, h_sug): + match err: + case S.UnknownFlag{+at, +word}: + e1 = Equal.sym(Maybe<&2, String>, S.sug.word(spec, at, word), Some{ss}, h_sug) + %e1 : {String.contains(S.err.wrap(spec, at, "error: unexpected argument '" ++ word ++ "' found" ++ S.sug.tip(_)), + ss) == True{} : Bool} + ct.step("error: unexpected argument '", word ++ "' found" ++ "\n\n tip: a similar argument exists: '" ++ ss ++ "'", + "\n\n" ++ S.usage.at(spec, at) ++ "\n\n" ++ S.err.hint(at), ss, + ct.step(word, "' found" ++ "\n\n tip: a similar argument exists: '" ++ ss ++ "'", + "\n\n" ++ S.usage.at(spec, at) ++ "\n\n" ++ S.err.hint(at), ss, + ct.step("' found", "\n\n tip: a similar argument exists: '" ++ ss ++ "'", + "\n\n" ++ S.usage.at(spec, at) ++ "\n\n" ++ S.err.hint(at), ss, + ct.step("\n\n tip: a similar argument exists: '", ss ++ "'", + "\n\n" ++ S.usage.at(spec, at) ++ "\n\n" ++ S.err.hint(at), ss, + ct.lead(ss, "'", "\n\n" ++ S.usage.at(spec, at) ++ "\n\n" ++ S.err.hint(at)))))) + case S.Missing{+at, +name}: + tp.none(spec, S.Missing{at, name}, ss, h_sug) + case S.NoValue{+at, +name}: + tp.none(spec, S.NoValue{at, name}, ss, h_sug) + case S.BadValue{+at, +name, +value}: + tp.none(spec, S.BadValue{at, name, value}, ss, h_sug) + case S.NeedHelp{+path}: + tp.none(spec, S.NeedHelp{path}, ss, h_sug) + case S.Unexpected{+at, +arg}: + tp.none(spec, S.Unexpected{at, arg}, ss, h_sug) + case S.Repeated{+at, +name}: + tp.none(spec, S.Repeated{at, name}, ss, h_sug) diff --git a/src/cli.bend b/src/cli.bend index 2dd147f..ced7230 100644 --- a/src/cli.bend +++ b/src/cli.bend @@ -1979,11 +1979,234 @@ def err.hint(+path: List<&2, String>) -> String: def err.wrap(+app: Cli, +at: List<&2, String>, +msg: String) -> String: msg ++ "\n\n" ++ usage.at(app, at) ++ "\n\n" ++ err.hint(at) +# the head of a row, or 0 past its end +def osa.head(xs: List<&2, Nat>) -> Nat: + match xs: + case Nil{}: + 0n + case Con{hh, _t}: + hh + +# a row after its head +def osa.tail(xs: List<&2, Nat>) -> List<&2, Nat>: + match xs: + case Nil{}: + [] + case Con{_h, tt}: + tt + +# the last cell of a row, `dd` for an empty one +def osa.last(xs: List<&2, Nat>, dd: Nat) -> Nat: + match xs: + case Nil{}: + dd + case Con{hh, tt}: + osa.last(tt, hh) + +# the first row: `ii`, then one more for each char +def osa.first(bs: List<&2, Char>, +ii: Nat) -> List<&2, Nat>: + match bs: + case Nil{}: + [ii] + case Con{_c, tt}: + ii <> osa.first(tt, 1n+ii) + +# whether the char before `cb` is `ca`, once the char before `ca` is `xa` +def osa.swap.b(+xa: Char, pb: Maybe<&2, Char>, +ca: Char, +cb: Char) -> Bool: + match pb: + case None{}: + False{} + case Some{xb}: + Bool.and(Char.is_eq(ca, xb), Char.is_eq(xa, cb)) + +# whether the two chars before these, swapped, are these two +def osa.swap(pa: Maybe<&2, Char>, pb: Maybe<&2, Char>, +ca: Char, +cb: Char) -> Bool: + match pa: + case None{}: + False{} + case Some{xa}: + osa.swap.b(xa, pb, ca, cb) + +# the cheaper of a cell and a swap from two rows up and two cells left +def osa.cell.swap(swap: Bool, +best: Nat, +far: Nat) -> Nat: + Bool.pick(Nat, swap, Nat.min(best, 1n+far), best) + +# one cell: the cheapest of a deletion, an insertion, a substitution and a +# swap of two adjacent chars +def osa.cell( + swap: Bool, + +up: Nat, + +left: Nat, + +diag: Nat, + +cost: Nat, + +far: Nat +) -> Nat: + osa.cell.swap(swap, Nat.min(Nat.min(1n+up, 1n+left), Nat.add(diag, cost)), far) + +# the rest of a row for the char `ca`, whose char before is `pa`: `ps` is the +# row above from the cell above-left on, `qs` the row two up from two cells +# left on, `pb` the char of `bs` before its head +def osa.row( + bs: List<&2, Char>, + +ca: Char, + +pa: Maybe<&2, Char>, + pb: Maybe<&2, Char>, + left: Nat, + +ps: List<&2, Nat>, + +qs: List<&2, Nat> +) -> List<&2, Nat>: + match bs: + case Nil{}: + [] + case Con{+cb, bt}: + +rr = osa.cell(osa.swap(pa, pb, ca, cb), osa.head(osa.tail(ps)), left, osa.head(ps), + Bool.pick(Nat, Char.is_eq(ca, cb), 0n, 1n), osa.head(qs)) + rr <> osa.row(bt, ca, pa, Some{cb}, rr, osa.tail(ps), osa.tail(qs)) + +# the rows for the chars of `as`, the last row `pp` and the one before `qq`, +# down to the distance in the last row's last cell +def osa.rows( + as: List<&2, Char>, + +bs: List<&2, Char>, + pa: Maybe<&2, Char>, + +ii: Nat, + +pp: List<&2, Nat>, + qq: List<&2, Nat> +) -> Nat: + match as: + case Nil{}: + osa.last(pp, 0n) + case Con{+ca, at}: + osa.rows(at, bs, Some{ca}, 1n+ii, (1n+ii) <> osa.row(bs, ca, pa, None{}, 1n+ii, pp, 0n <> qq), pp) + +# the optimal string alignment distance from `aa` to `bb`: the fewest +# insertions, deletions, substitutions and swaps of two adjacent chars, no +# char edited twice +def osa(aa: String, bb: String) -> Nat: + +bs = String.to_list(bb) + osa.rows(String.to_list(aa), bs, None{}, 0n, osa.first(bs, 0n), osa.first(bs, 0n)) + +# whether a candidate is close to the typed spelling +def sug.close.go(+dd: Nat, +room: Nat) -> Bool: + Bool.and(Nat.is_lt(0n, dd), Nat.is_le(Nat.mul(3n, dd), room)) + +# whether `cc` is close to `typed`: some edits away, and at most a third of +# the longer as many +def sug.close(+typed: String, +cc: String) -> Bool: + sug.close.go(osa(typed, cc), Nat.max(String.length(typed), String.length(cc))) + +# a close candidate against the closest one after it: the earlier on a tie +def sug.keep.rest(+typed: String, +cc: String, rest: Maybe<&2, String>) -> Maybe<&2, String>: + match rest: + case None{}: + Some{cc} + case Some{+ww}: + Bool.pick(Maybe<&2, String>, Nat.is_le(osa(typed, cc), osa(typed, ww)), Some{cc}, Some{ww}) + +# a candidate, when it is close, against the closest one after it +def sug.keep(close: Bool, +typed: String, +cc: String, rest: Maybe<&2, String>) -> Maybe<&2, String>: + match close: + case False{}: + rest + case True{}: + sug.keep.rest(typed, cc, rest) + +# the closest close candidate, the first among equals +def sug.best(cands: List<&2, String>, +typed: String) -> Maybe<&2, String>: + match cands: + case Nil{}: + None{} + case Con{+cc, tt}: + sug.keep(sug.close(typed, cc), typed, cc, sug.best(tt, typed)) + +# a long spelling in front of the rest, when there is one +def sug.cands.put(long: Maybe<&2, String>, rest: List<&2, String>) -> List<&2, String>: + match long: + case None{}: + rest + case Some{ll}: + ll <> rest + +# the long spellings of a command's arguments, in order +def sug.cands(args: List<&2, Arg>) -> List<&2, String>: + match args: + case Nil{}: + [] + case Con{hh, tt}: + Arg{_n, _s, long, _k, _h, _r, _d, _c} = hh + sug.cands.put(long, sug.cands(tt)) + +# the arguments of the page at the end of a shrinking path +def sug.args.go(path: List<&2, String>, how: How) -> List<&2, Arg>: + match path: + case Nil{}: + How{_b, _a, _v, args, _s, _u} = how + args + case Con{+hh, tt}: + sug.args.go(tt, help.step(how, hh)) + +# the arguments of the command at `path`, reached as `help` reaches it +def sug.args(+app: Cli, path: List<&2, String>) -> List<&2, Arg>: + Cli{+name, +about, version, args, subs} = app + sug.args.go(path, How{name, about, version, args, subs, name}) + +# the spelling a long option word was typed with: its chars up to `=` +def sug.typed(cut: String & Maybe<&2, String>) -> String: + (nn, _v) = cut + nn + +# a candidate spelled as a long option word +def sug.found(mm: Maybe<&2, String>) -> Maybe<&2, String>: + match mm: + case None{}: + None{} + case Some{cc}: + Some{"--" ++ cc} + +# the suggestion for a word, when it is a long option word +def sug.word.go(long: Bool, +app: Cli, +at: List<&2, String>, +word: String) -> Maybe<&2, String>: + match long: + case False{}: + None{} + case True{}: + sug.found(sug.best(sug.cands(sug.args(app, at)), sug.typed(cut_eq(String.drop(word, 2n))))) + +# the long spelling a word refused at `at` was likely meant to be +def sug.word(+app: Cli, +at: List<&2, String>, +word: String) -> Maybe<&2, String>: + sug.word.go(String.starts_with(word, "--"), app, at, word) + +# the long spelling an unknown long option was likely meant to be, as clap's +# "a similar argument exists"; None for every other error +def suggestion(+app: Cli, ee: ParseErr) -> Maybe<&2, String>: + match ee: + case UnknownFlag{+at, +word}: + sug.word(app, at, word) + case Missing{_at, _name}: + None{} + case NoValue{_at, _name}: + None{} + case BadValue{_at, _name, _value}: + None{} + case NeedHelp{_path}: + None{} + case Unexpected{_at, _arg}: + None{} + case Repeated{_at, _name}: + None{} + +# clap's tip line for a suggestion, or nothing +def sug.tip(mm: Maybe<&2, String>) -> String: + match mm: + case None{}: + "" + case Some{ss}: + "\n\n tip: a similar argument exists: '" ++ ss ++ "'" + # error text; NeedHelp is empty (the caller prints `help`) def err_text(+app: Cli, ee: ParseErr) -> String: match ee: - case UnknownFlag{+at, word}: - err.wrap(app, at, "error: unexpected argument '" ++ word ++ "' found") + case UnknownFlag{+at, +word}: + err.wrap(app, at, "error: unexpected argument '" ++ word ++ "' found" ++ sug.tip(sug.word(app, at, word))) case Missing{+at, name}: err.wrap(app, at, "error: the following required argument was not provided:\n " ++ name) diff --git a/src/eq.bend b/src/eq.bend index b76b00a..beab4e3 100644 --- a/src/eq.bend +++ b/src/eq.bend @@ -62,6 +62,17 @@ def char_cmp_self(cc): # noqa: L001 a proof of this file's law Equal.cong(Cmp, (Char & Char) & Cmp, rr => ((Chr{xx}, Chr{xx}), rr), U32.cmp(xx, xx), EQ{}, u32_cmp_self(xx)) +# LAW: a char equals itself +law char_eq_self: + for +cc: Char + {Char.is_eq(cc, cc) == True{} : Bool} + +# a char is a code point, and equality is the comparison's verdict +def char_eq_self(cc): # noqa: L001 a proof of this file's law + match cc: + case Chr{+xx}: + Equal.cong(Cmp, Bool, rr => Cmp.is_eq(rr), U32.cmp(xx, xx), EQ{}, u32_cmp_self(xx)) + # LAW: a string compares equal to itself law string_cmp_self: for +ss: String From 864556c30fd7305f7260c1c1f08bc26cd2103394 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 2 Oct 2026 01:50:43 +0000 Subject: [PATCH 6/7] docs: suggestions in the README; RFC marked implemented Co-authored-by: noah-emp --- README.md | 9 +++++++-- docs/rfc/shake-env-and-suggestions.md | 4 ++-- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index ab8a40a..9b97097 100644 --- a/README.md +++ b/README.md @@ -68,7 +68,8 @@ does it for you. shake needs bend 2.0.32 or later for that reason. `Shake.Var`), the builders (`app`, `sub`, `flag`, `opt`, `many`, `pos`, `rest`, `env`), `check` and `spec_err_text`, `parse` and `parse_env`, the readers (`get`, `get_all`, `on`, `sub_name`, `sub_of`, `at`, `path_of`), -`help`, `err_text`, `help_path`, `err_path`, `argv` and `env_vars`. +`help`, `err_text`, `help_path`, `err_path`, `suggestion`, `argv` and +`env_vars`. Everything under `src/` is internal and may change in any release; import only `main.bend`. [SPEC.md](SPEC.md) lists what shake guarantees, and which of it is proved. @@ -83,7 +84,11 @@ passes, so check yours once, at start or in your own laws. `tool --help` or `tool --help` (a command that declares its own long `help` gets `--help` as that argument instead): `help_path` gives its command path, for `help` to print, and is `None` for every other error, -which `err_text` describes. +which `err_text` describes. For a mistyped long option, `err_text` adds +clap's tip (`tip: a similar argument exists: '--name'` for `--nmae`), and +`suggestion` gives that long option word on its own. It picks the closest +long spelling of the current command's flags and options, and nothing when +none is close. A successful parse is read one command at a time, as clap's `ArgMatches` is: `get`, `get_all` and `on` read the bindings a command made, and `sub_name(m)` and `sub_of(m, name)` give the subcommand selected under it and diff --git a/docs/rfc/shake-env-and-suggestions.md b/docs/rfc/shake-env-and-suggestions.md index 8dd5f57..46c50ad 100644 --- a/docs/rfc/shake-env-and-suggestions.md +++ b/docs/rfc/shake-env-and-suggestions.md @@ -4,7 +4,7 @@ Read at `f142895` on `main`, bend 2.0.34, bolt v1.11.0. Requested by the maintai ## Draft Status -**State:** Accepted; the rows are in SPEC.md as pending, and each turns proved as its laws land (see [Rollout](#rollout)). +**State:** Accepted and implemented; every row it adds to SPEC.md is proved (see [Rollout](#rollout)). - [x] - [x] @@ -126,4 +126,4 @@ Three candidates were sketched: A (gpt-5.6), C (this author), and B (grok), whic ## Next implementation step -Step 2 has landed. Next: `suggestion` and the tip in `err_text`, with the laws of SHAKE-ERR-3 and ERR-4. +All three steps have landed and every row is proved. Next, if wanted: an Arguments block in help (see [Open questions](#open-questions-and-risks)). From b9d0a805579fa62c3e490b40553c658bc7af08a6 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 2 Oct 2026 01:53:37 +0000 Subject: [PATCH 7/7] docs: RFC records design runner B, which returned after synthesis Co-authored-by: noah-emp --- docs/rfc/shake-env-and-suggestions.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/rfc/shake-env-and-suggestions.md b/docs/rfc/shake-env-and-suggestions.md index 46c50ad..920c7eb 100644 --- a/docs/rfc/shake-env-and-suggestions.md +++ b/docs/rfc/shake-env-and-suggestions.md @@ -92,7 +92,9 @@ def env_vars(spec: S.Cli) -> IO(List<&2, S.Var>) ## Synthesis decision -Three candidates were sketched: A (gpt-5.6), C (this author), and B (grok), which had not returned by the time of synthesis. **C is the base:** env applied by rewriting the spec in front of an unchanged `parse`, a post-check for choices, the suggestion derived from the spec and the error, and `parse` kept as it is. **From A:** the `Fallback{env, default}` pair in the default's slot, which C had as a ninth `Arg` field. It cuts the proof churn to the sites that read the default, and it groups two facts that answer one question. Also from A: excluding the synthetic `--help` from the candidates, and a strict first-in-spec-order tie break. **Rejected from A:** a third argument on `parse` (REVIEW-E1); counting an empty variable as set (REVIEW-E2); refusing env on flags in `check` (REVIEW-E3: clap supports it and it fits without changing `on`); a new Arguments block in help (scope beyond the request; an open question); and Jaro similarity. Jaro is clap's measure, but its matching window and transposition count are much harder to state in a row than an edit distance, and the maintainer asked for "edit distance / clap-like". A also checked the fallback against the choices inside `fill`, which changes `finish` and with it the proofs of SHAKE-PARSE-1, PARSE-6 and PARSE-7; C's post-check leaves them untouched. +Three candidates were sketched: A (gpt-5.6), C (this author), and B (grok), which returned only after this design was implemented (see the note below). **C is the base:** env applied by rewriting the spec in front of an unchanged `parse`, a post-check for choices, the suggestion derived from the spec and the error, and `parse` kept as it is. **From A:** the `Fallback{env, default}` pair in the default's slot, which C had as a ninth `Arg` field. It cuts the proof churn to the sites that read the default, and it groups two facts that answer one question. Also from A: excluding the synthetic `--help` from the candidates, and a strict first-in-spec-order tie break. **Rejected from A:** a third argument on `parse` (REVIEW-E1); counting an empty variable as set (REVIEW-E2); refusing env on flags in `check` (REVIEW-E3: clap supports it and it fits without changing `on`); a new Arguments block in help (scope beyond the request; an open question); and Jaro similarity. Jaro is clap's measure, but its matching window and transposition count are much harder to state in a row than an edit distance, and the maintainer asked for "edit distance / clap-like". A also checked the fallback against the choices inside `fill`, which changes `finish` and with it the proofs of SHAKE-PARSE-1, PARSE-6 and PARSE-7; C's post-check leaves them untouched. + +**B, read after the fact.** B independently reached the same core: `parse` kept as it is, a pure `parse_env` fed by an IO reader, the spec rewritten so a set variable stands in for the default (which unblocks a required positional), a root-first post-check for choices, and the suggestion derived in `err_text` from the spec and `at`. It differs where A did, and the decisions above stand: an empty variable counted as set (REVIEW-E2), no env on flags plus two new `check` errors (REVIEW-E3), Jaro similarity (REVIEW-E5), and a ninth `Arg` field instead of `Fallback`. B also put an env value outside its choices ahead of `Missing`, as clap does. That ordering is already an open question below. B also offered short spellings and a synthetic `--help` as candidates; we keep both out, for the reasons in What it deliberately does not do. Nothing in B changes a SPEC row. ## Tradeoffs accepted