From 40e73012de5f7252fec2a2bef278fb4edb65e90d Mon Sep 17 00:00:00 2001 From: Noah Gardner Date: Tue, 29 Sep 2026 19:53:22 -0400 Subject: [PATCH] feat!: bend 2.0.34, argv drops the program name, --help asks for help Bend 2.0.32 puts the program as invoked first in IO.args, so argv now drops that word (args.words) and every Shake.argv() caller still gets just the arguments; SHAKE-ARGS-1 gains words_keeps. Compiled binaries pass --help through since 2.0.29, and shake now reads a bare --help, before -- and before any positional of the current command is bound, as a request for help exactly like `help` (SHAKE-PARSE-8, laws dash_help_step and dash_help_path). A command that declares its own long `help` keeps it: the help request only takes an unknown --help, so check reports nothing new. The proofs port to the new String.eq (Cmp.is_eq of String.order), SPEC's trust rows restate bend 2.0.34's C main and the ALL PROOFS CHECK gate, and the flake pins bend 2.0.34 with a proofs check that runs PROOF.bend on it, ez pinned to its own bend 2.0.31. bolt moves to v1.9.0, since v1.8.0 does not build on that bend. BREAKING CHANGE: shake needs bend 2.0.32 or later: argv() drops the first word of IO.args, which on older bend is a real argument. A bare --help is now a request for help (help_path is Some) instead of an UnknownFlag error. Co-Authored-By: Claude Opus 5.5 --- README.md | 38 ++++-- SPEC.md | 18 +-- ez.lock.toml | 6 +- ez.toml | 6 +- flake.lock | 48 ++++++-- flake.nix | 31 ++++- main.bend | 12 +- src/LAWS.bend | 72 ++++++++++- src/PROOF.bend | 317 ++++++++++++++++++++++++++++++++++++++++++++----- src/args.bend | 19 ++- src/cli.bend | 67 +++++++++-- src/eq.bend | 6 +- src/grow.bend | 48 +++++++- 13 files changed, 594 insertions(+), 94 deletions(-) diff --git a/README.md b/README.md index 861a026..8c52b20 100644 --- a/README.md +++ b/README.md @@ -24,8 +24,9 @@ ez add Emerging-Patterns/shake ## Usage -A spec, a parse, and a read. `parse` answers `Done` with what the words -bound, or `Fail` with why they could not be bound: +A spec, a parse, and a read. `Shake.argv()` is the command line without +the program name; `parse` answers `Done` with what the words bound, or +`Fail` with why they could not be bound: ``` import 0x085b03c84ca37125e38dddede7b91e55/main.bend as Shake @@ -43,10 +44,21 @@ def greet(got: Result<&2, &2, Shake.ParseErr, Shake.Matched>) -> String: case Fail{ee}: Shake.err_text(spec(), ee) -def main() -> String: - greet(Shake.parse(spec(), ["--name", "Ada"])) +def main() -> IO(Unit): + do IO: + av : List<&2, String> <- Shake.argv() + IO.print(greet(Shake.parse(spec(), av))) ``` +`bend hi.bend -- --name Ada` prints `hello Ada`, and so does a compiled +`hi.bin --name Ada`. The same code works in an ez project, where +`ez add` has put shake in the ledger. + +On bend 2.0.32 and later, `IO.args()` starts with the program as invoked +(`hi.bin`, or `hi.bend` when interpreted), so a program that passes +`IO.args()` straight to `parse` must drop that first word; `Shake.argv()` +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 @@ -62,9 +74,11 @@ that is not the last, a repeated name or spelling, a subcommand named optional one). `parse` does not call it; the guarantees hold for a spec it passes, so check yours once, at start or in your own laws. -`parse` fails with a request for help on `tool help` or -`tool help `: `help_path` gives its command path, for `help` to -print, and is `None` for every other error, which `err_text` describes. +`parse` fails with a request for help on `tool help`, `tool help `, +`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. 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 @@ -76,10 +90,11 @@ list, and `get` still reads one value. `argv` is the process's arguments, each word reusable. A compiled Bend program's runtime reads the command line before shake does -(bend 2.0.27): +(bend 2.0.34): -- `--help` prints the runtime's own usage and exits, and `--gpu-build` - builds the GPU image and exits; neither runs `main`. +- `--bend-help` prints the runtime's own usage and exits, and `--gpu-build` + builds the GPU image and exits; neither runs `main`. `--help` reaches + the program, and shake reads it as a request for help. - `--threads N` and `--gpu X` are taken, with their value, and a bad value stops the program. - The first `--` is taken too, and every word after it is passed on @@ -94,6 +109,7 @@ cd shake mkdir -p bin bend examples/demo/main.bend -o bin/demo.bin bin/demo.bin help +bin/demo.bin greet --help bin/demo.bin greet --name Ada -v bin/demo.bin add 2 3 --times 2 ``` @@ -104,7 +120,7 @@ bin/demo.bin add 2 3 --times 2 - `main.bend`: the interface. - `src/`: the implementation, with `src/LAWS.bend` stating the parser's laws - and `src/PROOF.bend` proving them. `ez prove` is the proof gate. + and `src/PROOF.bend` proving them. `nix flake check` runs the proof gate. - `examples/demo/`: a small program that uses only `main.bend`. - `ez.toml` and `ez.lock.toml`: the ledger and lock; bolt, the linter, is pinned there as `[tools.bolt]`, and `nix flake check` runs it. diff --git a/SPEC.md b/SPEC.md index 289c612..0420beb 100644 --- a/SPEC.md +++ b/SPEC.md @@ -2,11 +2,11 @@ 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. -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 terms check.` (`ez prove`). Tests and fixtures are never evidence for a requirement. +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. A spec is **well-formed** when `check` reports nothing for it (SHAKE-SPEC-1). The parse requirements hold for well-formed specs; a spec that contradicts itself, such as two options spelled `-n`, is its author's bug and not an input a user can give. Every error a row names but `NeedHelp` also carries `at`, the command path selected where the parse failed (SHAKE-ERR-2); rows write it only where it matters. A **plain word** is `-`, or a word that does not start with `-`. The **current command** is the command whose arguments `parse` matches words against: the root, then each subcommand it selects. The **selected path** is the names of the subcommands selected, in order. A successful parse answers the root command's **Matched**, as clap answers `ArgMatches`: the bindings that command made while it was current and, when a subcommand was selected under it, that subcommand's name and its own Matched, and so on down the selected path. -The words `parse` receives are what the program passes it. In a compiled program they come from `argv`, after the runtime has taken its own flags and the first `--` (SHAKE-TRUST-2). +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. @@ -36,7 +36,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | SHAKE-TOK-4 | When a word exactly `--` reaches `parse` where an option could stand, it binds nothing and every later word is read as a plain word bound to a positional, whatever its shape. | Proved | proved | src/LAWS.bend dd_step; src/LAWS.bend raw_next; src/LAWS.bend raw_binds; src/LAWS.bend raw_no_pos; src/LAWS.bend raw_refused | | SHAKE-TOK-5 | A flag given a value (`--verbose=x`, or `-v=x` in a cluster) is refused as `Unexpected{word}`. | Proved | proved | src/LAWS.bend flag_long_valued; src/LAWS.bend letter_flag_eq | | SHAKE-TOK-6 | An option given no value in its own word takes the next word as its value, unless that word starts with `-` and is not `-`, or there is none; then the parse fails with `NoValue{name}`. | Proved | proved | src/LAWS.bend value_flag_shaped; src/LAWS.bend value_absent; src/LAWS.bend value_binds | -| SHAKE-TOK-7 | A long or short spelling that no argument of the current command has is refused as `UnknownFlag{word}`. Arguments of a parent command are not matched after a subcommand is selected. | Proved | proved | src/LAWS.bend unknown_long; src/LAWS.bend unknown_short; src/LAWS.bend enter_step; src/LAWS.bend letter_unknown | +| SHAKE-TOK-7 | A long or short spelling that no argument of the current command has is refused as `UnknownFlag{word}`, except a word `--help` that SHAKE-PARSE-8 reads as a request for help. Arguments of a parent command are not matched after a subcommand is selected. | Proved | proved | src/LAWS.bend unknown_long; src/LAWS.bend unknown_short; src/LAWS.bend enter_step; src/LAWS.bend letter_unknown | ### What a parse binds (SHAKE-PARSE) @@ -49,7 +49,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | SHAKE-PARSE-5 | A value given to an argument with a nonempty choices list binds only when it is in the list, and otherwise fails with `BadValue{name, value}`. An argument with no choices accepts every value. | Proved | proved | src/LAWS.bend choice_refused; src/LAWS.bend value_refused; src/LAWS.bend long_refused; src/LAWS.bend raw_refused; src/LAWS.bend letter_value_bad; src/LAWS.bend pos_next; src/LAWS.bend pos_binds; src/LAWS.bend raw_binds; src/LAWS.bend value_binds; src/LAWS.bend long_binds; src/LAWS.bend letter_value; src/LAWS.bend letter_value_eq | | SHAKE-PARSE-6 | After the last word, each argument of every command on the selected path that the words left unbound in that command and that has a default is bound to its default in that command's Matched. A bound argument's value is never replaced, and no argument without a default gains a binding. | Proved | proved | src/LAWS.bend default_filled; src/LAWS.bend bound_kept; src/LAWS.bend no_default; src/LAWS.bend no_argument | | SHAKE-PARSE-7 | A successful parse binds every required argument of every command on the selected path, in that command's Matched. Otherwise the parse fails with `Missing{name}`. | Proved | proved | src/LAWS.bend required_present; src/LAWS.bend required_missing | -| SHAKE-PARSE-8 | Before `--` and before any positional of the current command is bound, a plain word `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}`. | Proved | proved | src/LAWS.bend help_unknown; src/LAWS.bend help_step; src/LAWS.bend help_walk; src/LAWS.bend help_path | +| 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 | @@ -84,7 +84,7 @@ 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 keeps all of them, in order and unchanged: for every list, reading the copy back gives the list. | Proved | proved | src/LAWS.bend copy_keeps | +| 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 | ## Left to prove @@ -96,7 +96,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | ID | Assumption | Why it is trusted | | :---- | :---- | :---- | -| SHAKE-TRUST-1 | The Bend checker is sound: a proof it accepts proves its law. | It cannot be checked from inside Bend; this is EZ-TRUST-1. shake pins bend 2.0.27 through the flake. | -| SHAKE-TRUST-2 | A program compiled by bend 2.0.27 hands `IO.args` the process's words after the program name, except that it stops examining words at the first `--`, drops that `--` and passes every later word through unchanged; before that `--` it removes `--threads` and `--gpu` with the word after each, and ends the process before `main` on `--help` and on `--gpu-build`. | It is the C `main` bend emits, read from bend 2.0.26's own source (in its binary) and confirmed against the demo; rechecked for 2.0.27, whose `main` is identical. 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 terms check.` | It is ez's `mkProofs` running `ez prove`, run by `nix flake check` in CI; this is EZ-TRUST-4. | -| 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 `copy`, short enough to check by reading, and marked `# noqa: L001` for that reason. | +| SHAKE-TRUST-1 | The Bend checker is sound: a proof it accepts proves its law. | It cannot be checked from inside Bend; this is EZ-TRUST-1. shake pins bend 2.0.34 through the flake. | +| 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. | diff --git a/ez.lock.toml b/ez.lock.toml index 8ba4a79..d45c797 100644 --- a/ez.lock.toml +++ b/ez.lock.toml @@ -4,8 +4,8 @@ hub = "https://hub.bend-lang.com" [tools] [tools.bolt] git = "https://github.com/Emerging-Patterns/bolt" -rev = "02fb09377f5c0fbddb5f6b7c32c8ab4ae14240df" -tag = "v1.8.0" +rev = "d5a67600a96ba423f2212bd661a30c1fba38eb55" +tag = "v1.9.0" root = "." -narHash = "sha256-53zE+3lZ/jn9GvIeGoavvNMaFyUs5dEFWd7fwP49TlM=" +narHash = "sha256-HmJ8J1xDshBdSWXIiEp48GZ9qHsm+bmpHw06ZWwcDVE=" entry = "main.bend" diff --git a/ez.toml b/ez.toml index fb1ec10..1f46016 100644 --- a/ez.toml +++ b/ez.toml @@ -4,8 +4,8 @@ entry = "main.bend" [tools.bolt] git = "https://github.com/Emerging-Patterns/bolt" -rev = "02fb09377f5c0fbddb5f6b7c32c8ab4ae14240df" -tag = "v1.8.0" +rev = "d5a67600a96ba423f2212bd661a30c1fba38eb55" +tag = "v1.9.0" root = "." -narHash = "sha256-53zE+3lZ/jn9GvIeGoavvNMaFyUs5dEFWd7fwP49TlM=" +narHash = "sha256-HmJ8J1xDshBdSWXIiEp48GZ9qHsm+bmpHw06ZWwcDVE=" entry = "main.bend" diff --git a/flake.lock b/flake.lock index 55e5bef..01c6272 100644 --- a/flake.lock +++ b/flake.lock @@ -7,24 +7,42 @@ ] }, "locked": { - "lastModified": 1790348040, - "narHash": "sha256-6oh+6jj7kyl4xJsmq4p3BtU/BUl2f2LlC/5kH081D1M=", + "lastModified": 1790643370, + "narHash": "sha256-VYGPIHkNeccEaBHGer1B7+GNiWKQBiN/iiS7PozBXx0=", "owner": "bendlang", "repo": "bend", - "rev": "774ef644dccf9c3f8053f7276d8901ad23da006c", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", "type": "github" }, "original": { "owner": "bendlang", "repo": "bend", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", + "type": "github" + } + }, + "bend_2": { + "inputs": { + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1790482124, + "narHash": "sha256-Gv309ikt48M8cISbwSo6V0md2572iieIRiyl3noF1cA=", + "owner": "bendlang", + "repo": "bend", + "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", + "type": "github" + }, + "original": { + "owner": "bendlang", + "repo": "bend", + "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", "type": "github" } }, "ez": { "inputs": { - "bend": [ - "bend" - ], + "bend": "bend_2", "nixpkgs": [ "nixpkgs" ] @@ -44,6 +62,22 @@ } }, "nixpkgs": { + "locked": { + "lastModified": 1790578696, + "narHash": "sha256-ZoxIApko70jCdbH3l20HWXOBaT2HZd87orzd2yJ9dVE=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "7a0f122f5090cf4c2ade2a13a0e229d4e19ba71f", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_2": { "locked": { "lastModified": 1789546076, "narHash": "sha256-zVxLZiSnmaaPLwnhj7pwmqe3axBg/C6nG5JZsJMh2g4=", @@ -63,7 +97,7 @@ "inputs": { "bend": "bend", "ez": "ez", - "nixpkgs": "nixpkgs" + "nixpkgs": "nixpkgs_2" } } }, diff --git a/flake.nix b/flake.nix index 3223dbe..e14dac3 100644 --- a/flake.nix +++ b/flake.nix @@ -2,19 +2,25 @@ description = "shake: CLI argument parser for Bend 2"; inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + # bendlang/bend's flake at the commit that packages 2.0.34 (the v2.0.34 tag + # still packages 2.0.33) inputs.bend = { - url = "github:bendlang/bend"; + url = "github:bendlang/bend/777ee0b55c485afdd7e68bd917b3d23a88d77371"; inputs.nixpkgs.follows = "nixpkgs"; }; + # ez and its bolt stay on the bend ez's own flake.lock records until ez + # releases on 2.0.34, so ez's inputs.bend is pinned, not followed. shake's + # own builds and its proofs (checks.proofs) run on 2.0.34. inputs.ez = { url = "github:Emerging-Patterns/ez"; inputs.nixpkgs.follows = "nixpkgs"; - inputs.bend.follows = "bend"; + inputs.bend.url = "github:bendlang/bend/af569d4826913b2ce3557e9829ccad31fcf86f94"; }; outputs = { self, nixpkgs, ... }@inputs: let system = "x86_64-linux"; + pkgs = nixpkgs.legacyPackages.${system}; ez = inputs.ez.lib.${system}; ezBin = inputs.ez.packages.${system}.default; bend = inputs.bend.packages.${system}.default; @@ -29,12 +35,25 @@ in { packages.${system} = { inherit bend demo bend-cc; ez = ezBin; default = demo; }; apps.${system}.default = { type = "app"; program = "${demo}/bin/demo"; }; - # `proofs` is `ez prove`: every PROOF.bend must print exactly - # `All terms check.` first. `lint` is bolt at the lock's `[tools.bolt]` - # pin, graded by ./bolt.bend. + # `proofs` runs every PROOF.bend on this flake's bend: its first line + # must be `ALL PROOFS CHECK` (ez.mkProofs comes back when ez runs on + # 2.0.34). `lint` is bolt at the lock's `[tools.bolt]` pin, graded by + # ./bolt.bend. checks.${system} = { inherit demo; - proofs = ez.mkProofs { ez = ezBin; src = self; name = "shake-proofs"; }; + proofs = pkgs.runCommand "shake-proofs" { + nativeBuildInputs = [ bend ]; + BEND_LIB = ez.bendLib ./ez.lock.toml; + } '' + export HOME=$TMPDIR + cp -r ${self} src && chmod -R u+w src && cd src + for p in $(find . -name PROOF.bend -not -path './.ez/*' | sort); do + first=$(cd "$(dirname "$p")" && bend "$(basename "$p")" | head -n 1) + echo "$p: $first" + [ "$first" = "ALL PROOFS CHECK" ] || exit 1 + done + touch $out + ''; lint = ez.mkLint { src = self; }; }; # bolt, from the lock, is on PATH through `src` diff --git a/main.bend b/main.bend index 40fe17a..771e3b7 100644 --- a/main.bend +++ b/main.bend @@ -186,7 +186,8 @@ def err_path(err: S.ParseErr) -> List<&2, String>: case S.Repeated{at, _name}: at -# the command path of a request for help (`help`, `help `), or None +# the command path of a request for help (`help`, `help `, `--help`), +# or None # when the parse failed for another reason def help_path(err: S.ParseErr) -> Maybe<&2, List<&2, String>>: match err: @@ -205,9 +206,10 @@ def help_path(err: S.ParseErr) -> Maybe<&2, List<&2, String>>: case S.Repeated{_at, _name}: None{} -# the process's arguments, each word reusable. A compiled program's runtime -# has already acted on `--help`, `--gpu-build`, `--threads N` and `--gpu X` -# and taken the first `--`, passing every word after it here unexamined; so -# the `--` that `parse` sees is the user's second one +# 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` +# and `--gpu X` and taken the first `--`, passing every word after it here +# unexamined; so the `--` that `parse` sees is the user's second one def argv() -> IO(List<&2, String>): # noqa: L001 IO: reads argv Args.argv() diff --git a/src/LAWS.bend b/src/LAWS.bend index a7a70df..7b9576a 100644 --- a/src/LAWS.bend +++ b/src/LAWS.bend @@ -17,6 +17,14 @@ def down(ys: List<&2, String>) -> List<&1, String>: case Con{+hh, tt}: hh <> down(tt) +# the words of an IO.args line after its first, the program name +def after_head(xs: List<&1, String>) -> List<&1, String>: + match xs: + case Nil{}: + Nil{} + case Con{_hh, tt}: + tt + # the error a walker has failed with, or None while it is still going def dead_of(st: S.St) -> Maybe<&2, S.ParseErr>: match st: @@ -251,6 +259,14 @@ law copy_keeps: for xs: List<&1, String> {down(Args.copy(xs)) == xs : List<&1, String>} +# LAW: `words` drops the program name IO.args starts with and keeps every +# word after it, in order and unchanged; a line with no program name gives +# no arguments +# SHAKE-ARGS-1 +law words_keeps: + for xs: List<&1, String> + {down(Args.words(xs)) == after_head(xs) : List<&1, String>} + # LAW: walking two word lists is walking the first, then the second (a lemma) law walk_append: for xs: List<&2, String> @@ -324,6 +340,7 @@ law unknown_long_step: for h_cut: {S.cut_eq(body) == (name, val) : String & Maybe<&2, String>} for h_name: {String.is_empty(name) == False{} : Bool} for h_none: {S.by_long(args, name) == None{} : Maybe<&2, S.Arg>} + for h_lh: {S.long_help(name, val, seen) == False{} : Bool} {S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}) == S.St{S.Dead{S.UnknownFlag{path, "--" ++ body}}, args, up, subs, path, bs, pos, False{}, seen} : S.St} @@ -347,12 +364,14 @@ law unknown_long_dies: for h_cut: {S.cut_eq(body) == (name, val) : String & Maybe<&2, String>} for h_name: {String.is_empty(name) == False{} : Bool} for h_none: {S.by_long(args, name) == None{} : Maybe<&2, S.Arg>} + for h_lh: {S.long_help(name, val, seen) == False{} : Bool} {dead_of(S.parse.walk(List.append(&2, String, pre, ["--" ++ body]), S.parse.start(spec))) == Some{S.UnknownFlag{path, "--" ++ body}} : Maybe<&2, S.ParseErr>} # LAW: wherever the words before it leave the parse, in any command and with -# any bindings, a long option that no argument of that command spells fails -# the parse with UnknownFlag of the word, whatever follows +# any bindings, a long option that no argument of that command spells, other +# than a bare `--help` that asks for help, fails the parse with UnknownFlag of +# the word, whatever follows # SHAKE-TOK-7 # SHAKE-ERR-2 law unknown_long: @@ -375,6 +394,7 @@ law unknown_long: for h_cut: {S.cut_eq(body) == (name, val) : String & Maybe<&2, String>} for h_name: {String.is_empty(name) == False{} : Bool} for h_none: {S.by_long(args, name) == None{} : Maybe<&2, S.Arg>} + for h_lh: {S.long_help(name, val, seen) == False{} : Bool} {Shake.parse(spec, List.append(&2, String, List.append(&2, String, pre, ["--" ++ body]), more)) == Fail{S.UnknownFlag{path, "--" ++ body}} : Result<&2, &2, Shake.ParseErr, Shake.Matched>} @@ -522,7 +542,7 @@ law choice_refused: {Shake.parse(spec, List.append(&2, String, List.append(&2, String, pre, [tok]), more)) == Fail{S.BadValue{path, name, tok}} : Result<&2, &2, Shake.ParseErr, Shake.Matched>} -# LAW: a free walker hands a long option word to `take_arg`, with the +# LAW: a free walker hands a long option word to `take_long.found`, with the # argument its name spells and the value after `=` (a step lemma) law long_arg_step: for +body: String @@ -539,7 +559,7 @@ law long_arg_step: for h_cut: {S.cut_eq(body) == (name, val) : String & Maybe<&2, String>} for h_name: {String.is_empty(name) == False{} : Bool} {S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}) - == S.parse.take_arg(S.by_long(args, name), val, "--" ++ body, args, up, subs, path, bs, pos, + == S.parse.take_long.found(S.by_long(args, name), name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) : S.St} # LAW: wherever the words before it leave the walker free, a long option @@ -1778,6 +1798,50 @@ law help_path: {Shake.parse(spec, List.append(&2, String, List.append(&2, String, pre, ["help"]), ns)) == Fail{S.NeedHelp{List.append(&2, String, path, ns)}} : Result<&2, &2, Shake.ParseErr, Shake.Matched>} +# LAW: wherever the words before it leave the walker free, before `--` and +# before any positional of the current command is bound, a word `--help` +# starts a help path at the selected path, as `help` does, when no argument of +# the current command spells long `help` +# SHAKE-PARSE-8 +law dash_help_step: + for +spec: Shake.Cli + for +pre: List<&2, String> + for +args: List<&2, S.Arg> + for +up: List<&2, S.Level> + for +subs: List<&2, S.Sub> + for +path: List<&2, String> + for +bs: List<&2, S.Bind> + for +pos: List<&2, S.Arg> + for h_at: {S.parse.walk(pre, S.parse.start(spec)) + == S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, False{}} : S.St} + for h_none: {S.by_long(args, "help") == None{} : Maybe<&2, S.Arg>} + {S.parse.walk(List.append(&2, String, pre, ["--help"]), S.parse.start(spec)) + == S.St{S.Help{}, args, up, subs, path, bs, pos, False{}, False{}} : S.St} + +# LAW: wherever the words before it leave the walker free, before `--` and +# before any positional of the current command is bound, a word `--help`, +# when no argument of the current command spells long `help`, followed by +# words that each name a subcommand under the one before, until the words +# end, fails the parse with NeedHelp of the selected path followed by those +# words, as `help` does +# SHAKE-PARSE-8 +law dash_help_path: + for +spec: Shake.Cli + for +pre: List<&2, String> + for +ns: List<&2, String> + for +args: List<&2, S.Arg> + for +up: List<&2, S.Level> + for +subs: List<&2, S.Sub> + for +path: List<&2, String> + for +bs: List<&2, S.Bind> + for +pos: List<&2, S.Arg> + for h_at: {S.parse.walk(pre, S.parse.start(spec)) + == S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, False{}} : S.St} + for h_none: {S.by_long(args, "help") == None{} : Maybe<&2, S.Arg>} + for h_ns: {help_names(ns, subs) == True{} : Bool} + {Shake.parse(spec, List.append(&2, String, List.append(&2, String, pre, ["--help"]), ns)) + == Fail{S.NeedHelp{List.append(&2, String, path, ns)}} : Result<&2, &2, Shake.ParseErr, Shake.Matched>} + # LAW: the walk starts free at the root, with no path, no bindings, the root's # arguments current and its positionals pending # SHAKE-PARSE-2 diff --git a/src/PROOF.bend b/src/PROOF.bend index 3e22d1b..403fc86 100644 --- a/src/PROOF.bend +++ b/src/PROOF.bend @@ -185,6 +185,13 @@ def Laws.copy_keeps(xs): %ih : {hh <> _ == hh <> tt : List<&1, String>} {==} +def Laws.words_keeps(xs): + match xs: + case Nil{}: + {==} + case Con{_hh, tt}: + Laws.copy_keeps(tt) + def Laws.walk_append(xs, ys, st): match xs: case Nil{}: @@ -275,7 +282,23 @@ def Laws.drop_zero(ss): case SCon{_h, _t}: {==} -def Laws.unknown_long_step(body, name, val, args, up, subs, path, bs, pos, seen, h_dd, h_cut, h_name, h_none): +def Laws.unknown_long_step( + body, + name, + val, + args, + up, + subs, + path, + bs, + pos, + seen, + h_dd, + h_cut, + h_name, + h_none, + h_lh +): e1 = Equal.sym(Bool, String.eq("--" ++ body, "--"), False{}, h_dd) %e1 : {S.parse.step.end(_, "--" ++ body, args, up, subs, path, bs, pos, seen) == S.St{S.Dead{S.UnknownFlag{path, "--" ++ body}}, args, up, subs, path, bs, pos, False{}, seen} : S.St} @@ -292,7 +315,10 @@ def Laws.unknown_long_step(body, name, val, args, up, subs, path, bs, pos, seen, %e3 : {S.parse.take_long.named(_, name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) == S.St{S.Dead{S.UnknownFlag{path, "--" ++ body}}, args, up, subs, path, bs, pos, False{}, seen} : S.St} e4 = Equal.sym(Maybe<&2, S.Arg>, S.by_long(args, name), None{}, h_none) - %e4 : {S.parse.take_arg(_, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) + %e4 : {S.parse.take_long.found(_, name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) + == S.St{S.Dead{S.UnknownFlag{path, "--" ++ body}}, args, up, subs, path, bs, pos, False{}, seen} : S.St} + e5 = Equal.sym(Bool, S.long_help(name, val, seen), False{}, h_lh) + %e5 : {S.parse.take_long.help(_, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) == S.St{S.Dead{S.UnknownFlag{path, "--" ++ body}}, args, up, subs, path, bs, pos, False{}, seen} : S.St} {==} @@ -313,7 +339,8 @@ def Laws.unknown_long_dies( h_dd, h_cut, h_name, - h_none + h_none, + h_lh ): e1 = Equal.sym(S.St, S.parse.walk(List.append(&2, String, pre, ["--" ++ body]), S.parse.start(spec)), @@ -329,7 +356,7 @@ def Laws.unknown_long_dies( e3 = Equal.sym(S.St, S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}), S.St{S.Dead{S.UnknownFlag{path, "--" ++ body}}, args, up, subs, path, bs, pos, False{}, seen}, Laws.unknown_long_step(body, name, val, args, up, subs, path, bs, pos, seen, - h_dd, h_cut, h_name, h_none)) + h_dd, h_cut, h_name, h_none, h_lh)) %e3 : {Laws.dead_of(_) == Some{S.UnknownFlag{path, "--" ++ body}} : Maybe<&2, S.ParseErr>} {==} @@ -351,11 +378,12 @@ def Laws.unknown_long( h_dd, h_cut, h_name, - h_none + h_none, + h_lh ): Laws.fail_stays(spec, List.append(&2, String, pre, ["--" ++ body]), more, S.UnknownFlag{path, "--" ++ body}, Laws.unknown_long_dies(spec, pre, body, name, val, args, up, subs, path, bs, pos, seen, - h_at, h_dd, h_cut, h_name, h_none)) + h_at, h_dd, h_cut, h_name, h_none, h_lh)) def Laws.step_dies( spec, @@ -606,23 +634,23 @@ def Laws.long_arg_step( ): e1 = Equal.sym(Bool, String.eq("--" ++ body, "--"), False{}, h_dd) %e1 : {S.parse.step.end(_, "--" ++ body, args, up, subs, path, bs, pos, seen) - == S.parse.take_arg(S.by_long(args, name), val, "--" ++ body, args, up, subs, path, bs, pos, False{}, + == S.parse.take_long.found(S.by_long(args, name), name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) : S.St} e0 = Equal.sym(Bool, String.starts_with(body, ""), True{}, Laws.prefix_empty(body)) %e0 : {S.parse.step.kind.go(_, True{}, "--" ++ body, args, up, subs, path, bs, pos, seen) - == S.parse.take_arg(S.by_long(args, name), val, "--" ++ body, args, up, subs, path, bs, pos, False{}, + == S.parse.take_long.found(S.by_long(args, name), name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) : S.St} ed = Equal.sym(String, String.drop(body, 0n), body, Laws.drop_zero(body)) %ed : {S.parse.take_long(_, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) - == S.parse.take_arg(S.by_long(args, name), val, "--" ++ body, args, up, subs, path, bs, pos, False{}, + == S.parse.take_long.found(S.by_long(args, name), name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) : S.St} e2 = Equal.sym(String & Maybe<&2, String>, S.cut_eq(body), (name, val), h_cut) %e2 : {S.parse.take_long.cut(_, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) - == S.parse.take_arg(S.by_long(args, name), val, "--" ++ body, args, up, subs, path, bs, pos, False{}, + == S.parse.take_long.found(S.by_long(args, name), name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) : S.St} e3 = Equal.sym(Bool, String.is_empty(name), False{}, h_name) %e3 : {S.parse.take_long.named(_, name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) - == S.parse.take_arg(S.by_long(args, name), val, "--" ++ body, args, up, subs, path, bs, pos, False{}, + == S.parse.take_long.found(S.by_long(args, name), name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) : S.St} {==} @@ -653,11 +681,13 @@ def flag_long_valued.step( ) -> {Laws.dead_of(S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen})) == Some{S.Unexpected{path, "--" ++ body}} : Maybe<&2, S.ParseErr>}: e1 = Equal.sym(S.St, S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}), - S.parse.take_arg(S.by_long(args, name), Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen), + S.parse.take_long.found(S.by_long(args, name), name, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, + seen), Laws.long_arg_step(body, name, Some{vv}, args, up, subs, path, bs, pos, seen, h_dd, h_cut, h_name)) %e1 : {Laws.dead_of(_) == Some{S.Unexpected{path, "--" ++ body}} : Maybe<&2, S.ParseErr>} e2 = Equal.sym(Maybe<&2, S.Arg>, S.by_long(args, name), Some{S.Arg{nn, sh, lo, S.Flag{}, hp, req, dflt, cs}}, h_found) - %e2 : {Laws.dead_of(S.parse.take_arg(_, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen)) + %e2 : {Laws.dead_of(S.parse.take_long.found(_, name, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, + seen)) == Some{S.Unexpected{path, "--" ++ body}} : Maybe<&2, S.ParseErr>} e3 = Equal.sym(Bool, S.bound(bs, nn), False{}, h_once) %e3 : {Laws.dead_of(S.parse.once(_, S.St{S.Dead{S.Unexpected{path, "--" ++ body}}, args, up, subs, path, bs, pos, @@ -885,11 +915,12 @@ def repeated_long_flag.step( ) -> {Laws.dead_of(S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen})) == Some{S.Repeated{path, nn}} : Maybe<&2, S.ParseErr>}: e1 = Equal.sym(S.St, S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}), - S.parse.take_arg(S.by_long(args, name), val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen), + S.parse.take_long.found(S.by_long(args, name), name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, + seen), Laws.long_arg_step(body, name, val, args, up, subs, path, bs, pos, seen, h_dd, h_cut, h_name)) %e1 : {Laws.dead_of(_) == Some{S.Repeated{path, nn}} : Maybe<&2, S.ParseErr>} e2 = Equal.sym(Maybe<&2, S.Arg>, S.by_long(args, name), Some{S.Arg{nn, sh, lo, S.Flag{}, hp, req, dflt, cs}}, h_found) - %e2 : {Laws.dead_of(S.parse.take_arg(_, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen)) + %e2 : {Laws.dead_of(S.parse.take_long.found(_, name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen)) == Some{S.Repeated{path, nn}} : Maybe<&2, S.ParseErr>} e3 = Equal.sym(Bool, S.bound(bs, nn), True{}, h_again) %e3 : {Laws.dead_of(S.parse.once(_, S.parse.take_flag(val, nn, "--" ++ body, args, up, subs, path, bs, pos, @@ -956,11 +987,12 @@ def repeated_long_opt.step( ) -> {Laws.dead_of(S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen})) == Some{S.Repeated{path, nn}} : Maybe<&2, S.ParseErr>}: e1 = Equal.sym(S.St, S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}), - S.parse.take_arg(S.by_long(args, name), val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen), + S.parse.take_long.found(S.by_long(args, name), name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, + seen), Laws.long_arg_step(body, name, val, args, up, subs, path, bs, pos, seen, h_dd, h_cut, h_name)) %e1 : {Laws.dead_of(_) == Some{S.Repeated{path, nn}} : Maybe<&2, S.ParseErr>} e2 = Equal.sym(Maybe<&2, S.Arg>, S.by_long(args, name), Some{S.Arg{nn, sh, lo, S.Opt{}, hp, req, dflt, cs}}, h_found) - %e2 : {Laws.dead_of(S.parse.take_arg(_, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen)) + %e2 : {Laws.dead_of(S.parse.take_long.found(_, name, val, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen)) == Some{S.Repeated{path, nn}} : Maybe<&2, S.ParseErr>} e3 = Equal.sym(Bool, S.bound(bs, nn), True{}, h_again) %e3 : {Laws.dead_of(S.parse.once(_, S.parse.take_opt(val, nn, args, up, subs, path, bs, pos, False{}, @@ -1775,11 +1807,12 @@ def long.step( ) -> {S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}) == S.St{S.Free{}, args, up, subs, path, S.Bind{nn, vv} <> bs, pos, False{}, seen} : S.St}: e1 = Equal.sym(S.St, S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}), - S.parse.take_arg(S.by_long(args, name), Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen), + S.parse.take_long.found(S.by_long(args, name), name, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, + seen), Laws.long_arg_step(body, name, Some{vv}, args, up, subs, path, bs, pos, seen, h_dd, h_cut, h_name)) %e1 : {_ == S.St{S.Free{}, args, up, subs, path, S.Bind{nn, vv} <> bs, pos, False{}, seen} : S.St} e2 = Equal.sym(Maybe<&2, S.Arg>, S.by_long(args, name), Some{S.Arg{nn, sh, lo, kind, hp, req, dflt, cs}}, h_found) - %e2 : {S.parse.take_arg(_, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) + %e2 : {S.parse.take_long.found(_, name, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen) == S.St{S.Free{}, args, up, subs, path, S.Bind{nn, vv} <> bs, pos, False{}, seen} : S.St} long.kind(kind, nn, vv, "--" ++ body, args, up, subs, path, bs, pos, seen, h_kind, h_ok) @@ -1938,11 +1971,13 @@ def long_refused.step( ) -> {Laws.dead_of(S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen})) == Some{S.BadValue{path, nn, vv}} : Maybe<&2, S.ParseErr>}: e1 = Equal.sym(S.St, S.parse.step("--" ++ body, S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, seen}), - S.parse.take_arg(S.by_long(args, name), Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen), + S.parse.take_long.found(S.by_long(args, name), name, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, + seen), Laws.long_arg_step(body, name, Some{vv}, args, up, subs, path, bs, pos, seen, h_dd, h_cut, h_name)) %e1 : {Laws.dead_of(_) == Some{S.BadValue{path, nn, vv}} : Maybe<&2, S.ParseErr>} e2 = Equal.sym(Maybe<&2, S.Arg>, S.by_long(args, name), Some{S.Arg{nn, sh, lo, kind, hp, req, dflt, cs}}, h_found) - %e2 : {Laws.dead_of(S.parse.take_arg(_, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, seen)) + %e2 : {Laws.dead_of(S.parse.take_long.found(_, name, Some{vv}, "--" ++ body, args, up, subs, path, bs, pos, False{}, + seen)) == Some{S.BadValue{path, nn, vv}} : Maybe<&2, S.ParseErr>} long_refused.kind(kind, nn, vv, "--" ++ body, args, up, subs, path, bs, pos, seen, h_kind, h_bad) @@ -3899,6 +3934,35 @@ def Laws.help_path(spec, pre, ns, args, up, subs, path, bs, pos, h_at, h_ns): Laws.help_walk(spec, ph, ns, args, up, subs, path, bs, pos, False{}, False{}, Laws.help_step(spec, pre, args, up, subs, path, bs, pos, h_at), h_ns)) +# a free walker with no long `help` reads `--help` as `help` +def dash_help.step( + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +bs: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + h_none: {S.by_long(args, "help") == None{} : Maybe<&2, S.Arg>} +) -> {S.parse.step("--help", S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, False{}}) + == S.St{S.Help{}, args, up, subs, path, bs, pos, False{}, False{}} : S.St}: + ee = Equal.sym(Maybe<&2, S.Arg>, S.by_long(args, "help"), None{}, h_none) + %ee : {S.parse.take_long.found(_, "help", None{}, "--help", args, up, subs, path, bs, pos, False{}, False{}) + == S.St{S.Help{}, args, up, subs, path, bs, pos, False{}, False{}} : S.St} + {==} + +def Laws.dash_help_step(spec, pre, args, up, subs, path, bs, pos, h_at, h_none): + Equal.trans(S.St, S.parse.walk(List.append(&2, String, pre, ["--help"]), S.parse.start(spec)), + S.parse.step("--help", S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, False{}}), + S.St{S.Help{}, args, up, subs, path, bs, pos, False{}, False{}}, + kept.stepped(spec, pre, "--help", S.St{S.Free{}, args, up, subs, path, bs, pos, False{}, False{}}, h_at), + dash_help.step(args, up, subs, path, bs, pos, h_none)) + +def Laws.dash_help_path(spec, pre, ns, args, up, subs, path, bs, pos, h_at, h_none, h_ns): + +ph = List.append(&2, String, pre, ["--help"]) + hp.need(spec, List.append(&2, String, ph, ns), args, up, List.append(&2, String, path, ns), bs, pos, + Laws.help_walk(spec, ph, ns, args, up, subs, path, bs, pos, False{}, False{}, + Laws.dash_help_step(spec, pre, args, up, subs, path, bs, pos, h_at, h_none), h_ns)) + def Laws.start_state(_name, _about, _version, _args, _subs): {==} @@ -5644,6 +5708,53 @@ def gv.arg( case S.Arg{+name, _s, _l, kind, _h, _r, _d, _c}: gv.akind(kind, name, val, orig, args, up, subs, path, binds, pos, raw, seen, ws, hm, hb, hu) +# an unknown long option: a request for help, or an unknown flag +def gv.lhelp( + hit: Bool, + +orig: String, + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +binds: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + +raw: Bool, + +seen: Bool, + +ws: List<&2, String>, + hb: gv.B(binds, ws), + hu: gv.U(up, ws) +) -> gv.G(S.parse.take_long.help(hit, orig, args, up, subs, path, binds, pos, raw, seen), ws): + match hit: + case True{}: + gv.keep(binds, up, ws, hb, hu) + case False{}: + gv.keep(binds, up, ws, hb, hu) + +# a long option the current command spells, or an unknown one +def gv.found( + found: Maybe<&2, S.Arg>, + +name: String, + +val: Maybe<&2, String>, + +orig: String, + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +binds: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + +raw: Bool, + +seen: Bool, + +ws: List<&2, String>, + +hm: {gv.mok(val, ws) == True{} : Bool}, + hb: gv.B(binds, ws), + hu: gv.U(up, ws) +) -> gv.G(S.parse.take_long.found(found, name, val, orig, args, up, subs, path, binds, pos, raw, seen), ws): + match found: + case None{}: + gv.lhelp(S.long_help(name, val, seen), orig, args, up, subs, path, binds, pos, raw, seen, ws, hb, hu) + case Some{aa}: + gv.arg(Some{aa}, val, orig, args, up, subs, path, binds, pos, raw, seen, ws, hm, hb, hu) + # a long option with a name def gv.named( empty: Bool, @@ -5667,7 +5778,7 @@ def gv.named( case True{}: gv.keep(binds, up, ws, hb, hu) case False{}: - gv.arg(S.by_long(args, name), val, orig, args, up, subs, path, binds, pos, raw, seen, ws, hm, hb, hu) + gv.found(S.by_long(args, name), name, val, orig, args, up, subs, path, binds, pos, raw, seen, ws, hm, hb, hu) # a long option after the `=` cut def gv.cut( @@ -6924,6 +7035,54 @@ def gn.arg( case S.Arg{+name, _s, _l, kind, _h, _r, _d, _c}: gn.akind(kind, name, val, orig, args, up, subs, path, binds, pos, raw, seen, ws, hf, hm, hb, hp) +# an unknown long option: a request for help, or an unknown flag +def gn.lhelp( + hit: Bool, + +orig: String, + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +binds: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + +raw: Bool, + +seen: Bool, + +ws: List<&2, String>, + +hb: {gn.all(binds, args, ws) == True{} : Bool}, + +hp: {gn.pin(pos, args) == True{} : Bool} +) -> gn.G(S.parse.take_long.help(hit, orig, args, up, subs, path, binds, pos, raw, seen), ws): + match hit: + case True{}: + gn.keep(args, binds, pos, ws, hb, hp) + case False{}: + gn.keep(args, binds, pos, ws, hb, hp) + +# a long option the current command spells, or an unknown one +def gn.found( + found: Maybe<&2, S.Arg>, + +name: String, + +val: Maybe<&2, String>, + +orig: String, + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +binds: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + +raw: Bool, + +seen: Bool, + +ws: List<&2, String>, + +hf: {gn.fok(found, args) == True{} : Bool}, + +hm: {gv.mok(val, ws) == True{} : Bool}, + +hb: {gn.all(binds, args, ws) == True{} : Bool}, + +hp: {gn.pin(pos, args) == True{} : Bool} +) -> gn.G(S.parse.take_long.found(found, name, val, orig, args, up, subs, path, binds, pos, raw, seen), ws): + match found: + case None{}: + gn.lhelp(S.long_help(name, val, seen), orig, args, up, subs, path, binds, pos, raw, seen, ws, hb, hp) + case Some{aa}: + gn.arg(Some{aa}, val, orig, args, up, subs, path, binds, pos, raw, seen, ws, hf, hm, hb, hp) + # a long option with a name def gn.named( empty: Bool, @@ -6947,7 +7106,7 @@ def gn.named( case True{}: gn.keep(args, binds, pos, ws, hb, hp) case False{}: - gn.arg(S.by_long(args, name), val, orig, args, up, subs, path, binds, pos, raw, seen, ws, + gn.found(S.by_long(args, name), name, val, orig, args, up, subs, path, binds, pos, raw, seen, ws, gn.fok_long(args, name), hm, hb, hp) # a long option after the `=` cut @@ -8029,6 +8188,47 @@ def nd.arg( case S.Arg{+name, _s, _l, kind, _h, _r, _d, _c}: nd.akind(kind, name, val, orig, args, up, subs, path, binds, pos, raw, seen) +# an unknown long option: a request for help, or an unknown flag +def nd.lhelp( + hit: Bool, + +orig: String, + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +binds: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + +raw: Bool, + +seen: Bool +) -> nd.T(S.parse.take_long.help(hit, orig, args, up, subs, path, binds, pos, raw, seen), 1n+Laws.valued(binds)): + match hit: + case True{}: + nd.le_s(Laws.valued(binds)) + case False{}: + nd.le_s(Laws.valued(binds)) + +# a long option the current command spells, or an unknown one +def nd.found( + found: Maybe<&2, S.Arg>, + +name: String, + +val: Maybe<&2, String>, + +orig: String, + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +binds: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + +raw: Bool, + +seen: Bool +) -> nd.T(S.parse.take_long.found(found, name, val, orig, args, up, subs, path, binds, pos, raw, seen), + 1n+Laws.valued(binds)): + match found: + case None{}: + nd.lhelp(S.long_help(name, val, seen), orig, args, up, subs, path, binds, pos, raw, seen) + case Some{aa}: + nd.arg(Some{aa}, val, orig, args, up, subs, path, binds, pos, raw, seen) + # a long option with a name def nd.named( empty: Bool, @@ -8049,7 +8249,7 @@ def nd.named( case True{}: nd.le_s(Laws.valued(binds)) case False{}: - nd.arg(S.by_long(args, name), val, orig, args, up, subs, path, binds, pos, raw, seen) + nd.found(S.by_long(args, name), name, val, orig, args, up, subs, path, binds, pos, raw, seen) # a long option after the `=` cut def nd.cut( @@ -8895,6 +9095,57 @@ def nu.arg( case S.Arg{+name, _s, _l, kind, _h, _r, _d, _c}: nu.akind(kind, name, val, orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hn) +# an unknown long option: a request for help, or an unknown flag +def nu.lhelp( + hit: Bool, + +orig: String, + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +binds: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + +raw: Bool, + +seen: Bool, + +m0: S.Mode, + +hd: {nu.dead_m(m0) == False{} : Bool}, + +hl: {nu.help_m(m0) == False{} : Bool} +) -> nu.N(S.parse.take_long.help(hit, orig, args, up, subs, path, binds, pos, raw, seen), S.St{m0, args, up, subs, + path, binds, pos, raw, seen}): + match hit: + case True{}: + nu.apart(S.parse.take_long.help(True{}, orig, args, up, subs, path, binds, pos, raw, seen), S.St{m0, args, up, + subs, path, binds, pos, raw, seen}, ss => nu.help(ss), {==}, hl) + case False{}: + nu.apart(S.parse.take_long.help(False{}, orig, args, up, subs, path, binds, pos, raw, seen), S.St{m0, args, up, + subs, path, binds, pos, raw, seen}, ss => nu.dead(ss), {==}, hd) + +# a long option the current command spells, or an unknown one +def nu.found( + found: Maybe<&2, S.Arg>, + +name: String, + +val: Maybe<&2, String>, + +orig: String, + +args: List<&2, S.Arg>, + +up: List<&2, S.Level>, + +subs: List<&2, S.Sub>, + +path: List<&2, String>, + +binds: List<&2, S.Bind>, + +pos: List<&2, S.Arg>, + +raw: Bool, + +seen: Bool, + +m0: S.Mode, + +hd: {nu.dead_m(m0) == False{} : Bool}, + +hn: {nu.need_m(m0) == False{} : Bool}, + +hl: {nu.help_m(m0) == False{} : Bool} +) -> nu.N(S.parse.take_long.found(found, name, val, orig, args, up, subs, path, binds, pos, raw, seen), S.St{m0, + args, up, subs, path, binds, pos, raw, seen}): + match found: + case None{}: + nu.lhelp(S.long_help(name, val, seen), orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hl) + case Some{aa}: + nu.arg(Some{aa}, val, orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hn) + # a long option with a name def nu.named( empty: Bool, @@ -8911,7 +9162,8 @@ def nu.named( +seen: Bool, +m0: S.Mode, +hd: {nu.dead_m(m0) == False{} : Bool}, - +hn: {nu.need_m(m0) == False{} : Bool} + +hn: {nu.need_m(m0) == False{} : Bool}, + +hl: {nu.help_m(m0) == False{} : Bool} ) -> nu.N(S.parse.take_long.named(empty, name, val, orig, args, up, subs, path, binds, pos, raw, seen), S.St{m0, args, up, subs, path, binds, pos, raw, seen}): match empty: @@ -8919,7 +9171,7 @@ def nu.named( nu.apart(S.parse.take_long.named(True{}, name, val, orig, args, up, subs, path, binds, pos, raw, seen), S.St{m0, args, up, subs, path, binds, pos, raw, seen}, ss => nu.dead(ss), {==}, hd) case False{}: - nu.arg(S.by_long(args, name), val, orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hn) + nu.found(S.by_long(args, name), name, val, orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hn, hl) # a long option after the `=` cut def nu.cut( @@ -8935,12 +9187,14 @@ def nu.cut( +seen: Bool, +m0: S.Mode, +hd: {nu.dead_m(m0) == False{} : Bool}, - +hn: {nu.need_m(m0) == False{} : Bool} + +hn: {nu.need_m(m0) == False{} : Bool}, + +hl: {nu.help_m(m0) == False{} : Bool} ) -> nu.N(S.parse.take_long.cut(nv, orig, args, up, subs, path, binds, pos, raw, seen), S.St{m0, args, up, subs, path, binds, pos, raw, seen}): match nv: case (+name, +val): - nu.named(String.is_empty(name), name, val, orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hn) + nu.named(String.is_empty(name), name, val, orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hn, + hl) # a long option def nu.long( @@ -8956,10 +9210,11 @@ def nu.long( +seen: Bool, +m0: S.Mode, +hd: {nu.dead_m(m0) == False{} : Bool}, - +hn: {nu.need_m(m0) == False{} : Bool} + +hn: {nu.need_m(m0) == False{} : Bool}, + +hl: {nu.help_m(m0) == False{} : Bool} ) -> nu.N(S.parse.take_long(body, orig, args, up, subs, path, binds, pos, raw, seen), S.St{m0, args, up, subs, path, binds, pos, raw, seen}): - nu.cut(S.cut_eq(body), orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hn) + nu.cut(S.cut_eq(body), orig, args, up, subs, path, binds, pos, raw, seen, m0, hd, hn, hl) # a cluster walker changed from one with `l0` bindings, free: no fewer # bindings, and failed, waiting, reading a help path, or more bindings @@ -9519,7 +9774,7 @@ def nu.kind_go( path, binds, pos, False{}, seen}): match long: case True{}: - nu.long(String.drop(tok, 2n), tok, args, up, subs, path, binds, pos, False{}, seen, m0, hd, hn) + nu.long(String.drop(tok, 2n), tok, args, up, subs, path, binds, pos, False{}, seen, m0, hd, hn, hl) case False{}: nu.step_short(dash, tok, args, up, subs, path, binds, pos, seen, m0, hd, hn, hl) diff --git a/src/args.bend b/src/args.bend index 879684f..307a59b 100644 --- a/src/args.bend +++ b/src/args.bend @@ -1,6 +1,7 @@ -# shake/args: the process argv, each word reusable, internal (main.bend -# exports it). `IO.args` answers a `&1` list; the rest of a program reads the -# line more than once, so the walk copies it. +# 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. import Base # a &1 list copied to &2 @@ -11,7 +12,15 @@ def copy(xs: List<&1, String>) -> List<&2, String>: case Con{+h, t}: h <> copy(t) -# the process argv +# the arguments of an IO.args line: every word after the program name, copied +def words(xs: List<&1, String>) -> List<&2, String>: + match xs: + case Nil{}: + Nil{} + case Con{_h, t}: + copy(t) + +# the process's arguments, without the program name 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>, copy(xs))) + xs => IO.pure(List<&2, String>, words(xs))) diff --git a/src/cli.bend b/src/cli.bend index d561bc5..9dd2295 100644 --- a/src/cli.bend +++ b/src/cli.bend @@ -1,7 +1,8 @@ # shake/cli: the parser behind main.bend, internal. `parse` reads argv # against a Cli; `help` writes usage for a command path, and `help` is the -# subcommand that asks for it. A `--` that reaches `parse` ends option -# parsing; in a compiled program the runtime takes the first `--` itself. +# subcommand that asks for it (`--help` too, unless the command declares its +# own long `help`). A `--` that reaches `parse` ends option parsing; in a +# compiled program the runtime takes the first `--` itself. import Base # a flag, a valued option, an option that may repeat, a positional, or a rest @@ -61,9 +62,10 @@ type Matched is Data: Leaf{+binds: List<&2, Bind>} Node{+binds: List<&2, Bind>, +name: String, +sub: Matched} -# a failed parse. NeedHelp is `help` / `help `; NoValue is an option -# whose value never came, Missing a required argument nothing bound. Every -# error but NeedHelp carries `at`, the command path selected where it failed +# a failed parse. NeedHelp is `help` / `help ` (or `--help`); NoValue +# is an option whose value never came, Missing a required argument nothing +# bound. Every error but NeedHelp carries `at`, the command path selected +# where it failed type ParseErr is Data: UnknownFlag{at: List<&2, String>, flag: String} Missing{at: List<&2, String>, name: String} @@ -724,6 +726,57 @@ def parse.take_arg( parse.take_arg.kind(kind, name, val, orig, args, up, subs, path, binds, pos, raw, seen) +# whether an unknown long option is a request for help: a bare `--help`, +# with no `=` value, before any positional of the current command is bound +def long_help(+name: String, val: Maybe<&2, String>, seen: Bool) -> Bool: + match val: + case None{}: + Bool.and(String.eq(name, "help"), Bool.not(seen)) + case Some{_v}: + False{} + +# an unknown long option: a request for help (`--help`, as `help`), or an +# unknown flag +def parse.take_long.help( + hit: Bool, + +orig: String, + +args: List<&2, Arg>, + +up: List<&2, Level>, + +subs: List<&2, Sub>, + +path: List<&2, String>, + +binds: List<&2, Bind>, + +pos: List<&2, Arg>, + +raw: Bool, + +seen: Bool +) -> St: + match hit: + case True{}: + St{Help{}, args, up, subs, path, binds, pos, raw, seen} + case False{}: + parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen) + +# a long option the current command spells, or an unknown one +def parse.take_long.found( + found: Maybe<&2, Arg>, + +name: String, + val: Maybe<&2, String>, + +orig: String, + +args: List<&2, Arg>, + +up: List<&2, Level>, + +subs: List<&2, Sub>, + +path: List<&2, String>, + +binds: List<&2, Bind>, + +pos: List<&2, Arg>, + +raw: Bool, + +seen: Bool +) -> St: + match found: + case None{}: + parse.take_long.help(long_help(name, val, seen), orig, args, up, subs, path, + binds, pos, raw, seen) + case Some{a}: + parse.take_arg(Some{a}, val, orig, args, up, subs, path, binds, pos, raw, seen) + # a long option with a name, or `--=...` def parse.take_long.named( empty: Bool, @@ -743,8 +796,8 @@ def parse.take_long.named( case True{}: parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen) case False{}: - parse.take_arg(by_long(args, name), val, orig, args, up, subs, path, binds, - pos, raw, seen) + parse.take_long.found(by_long(args, name), name, val, orig, args, up, subs, + path, binds, pos, raw, seen) # a long option after the `=` cut def parse.take_long.cut( diff --git a/src/eq.bend b/src/eq.bend index 6336c1b..b76b00a 100644 --- a/src/eq.bend +++ b/src/eq.bend @@ -90,7 +90,9 @@ law string_eq_self: for +ss: String {String.eq(ss, ss) == True{} : Bool} -# equality is the comparison read as a bit, so the comparison's law answers +# equality is the comparison's verdict read as a bit, so the comparison's +# law answers def string_eq_self(ss): # noqa: L001 a proof of this file's law - Equal.cong((String & String) & Cmp, Bool, rr => String.eq.fin(rr), + Equal.cong((String & String) & Cmp, Bool, + rr => Cmp.is_eq(Pair.snd(String & String, Cmp, rr)), String.cmp(ss, ss), ((ss, ss), EQ{}), string_cmp_self(ss)) diff --git a/src/grow.bend b/src/grow.bend index e7827cd..0485c0d 100644 --- a/src/grow.bend +++ b/src/grow.bend @@ -355,6 +355,52 @@ def gw.arg(found, val, orig, args, up, subs, path, binds, pos, raw, seen): case Shake.Arg{+name, _s, _l, kind, _h, _r, _d, _c}: gw.kind(kind, name, val, orig, args, up, subs, path, binds, pos, raw, seen) +# an unknown long option: a request for help, or an unknown flag +law gw.lhelp: + for hit: Bool + for +orig: String + for +args: List<&2, Shake.Arg> + for +up: List<&2, Shake.Level> + for +subs: List<&2, Shake.Sub> + for +path: List<&2, String> + for +binds: List<&2, Shake.Bind> + for +pos: List<&2, Shake.Arg> + for +raw: Bool + for +seen: Bool + gw.Stay(Shake.parse.take_long.help(hit, orig, args, up, subs, path, binds, pos, raw, seen), View{args, up, + path, binds}) + +def gw.lhelp(hit, _orig, _args, _up, _subs, _path, _binds, _pos, _raw, _seen): + match hit: + case True{}: + ([], {==}) + case False{}: + ([], {==}) + +# a long option the current command spells, or an unknown one +law gw.found: + for found: Maybe<&2, Shake.Arg> + for +name: String + for +val: Maybe<&2, String> + for +orig: String + for +args: List<&2, Shake.Arg> + for +up: List<&2, Shake.Level> + for +subs: List<&2, Shake.Sub> + for +path: List<&2, String> + for +binds: List<&2, Shake.Bind> + for +pos: List<&2, Shake.Arg> + for +raw: Bool + for +seen: Bool + gw.Stay(Shake.parse.take_long.found(found, name, val, orig, args, up, subs, path, binds, pos, raw, seen), + View{args, up, path, binds}) + +def gw.found(found, name, val, orig, args, up, subs, path, binds, pos, raw, seen): + match found: + case None{}: + gw.lhelp(Shake.long_help(name, val, seen), orig, args, up, subs, path, binds, pos, raw, seen) + case Some{aa}: + gw.arg(Some{aa}, val, orig, args, up, subs, path, binds, pos, raw, seen) + # a long option with a name, or `--=...` law gw.named: for empty: Bool @@ -377,7 +423,7 @@ def gw.named(empty, name, val, orig, args, up, subs, path, binds, pos, raw, seen case True{}: ([], {==}) case False{}: - gw.arg(Shake.by_long(args, name), val, orig, args, up, subs, path, binds, pos, raw, seen) + gw.found(Shake.by_long(args, name), name, val, orig, args, up, subs, path, binds, pos, raw, seen) # a long option after the `=` cut law gw.cut: