From 030da919372e6736410eb628baa898da8ac1affd Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 13:33:07 +0000 Subject: [PATCH 1/6] feat(rules): fromrev (U016), String.from_list of a List.reverse `fromrev` reports each run of significant tokens whose texts are `String.from_list`, `(`, `List.reverse` and `(`, one finding on the first, and nothing else; a LAWS.bend or a PROOF.bend is exempt. Reversing a char buffer and reading it into a String walks it twice and builds a list only to throw it away, and String.from_list is not a tail call: fold the buffer onto a String with SCon in one pass. On in `suspicious` by default. Measured (bend 2.0.34, a 100k-char reversed buffer 200 times): native --gpu off 0.35 s against 0.17 s folded; JS at 20k chars 4.6 s against 3.1 s, and at 50k the two-pass form overflows the JS stack. BOLT-RULE-U016 is proved by fromrev_counts (a count against an independent counter, zero on a law file), fromrev_exempt (also under BOLT-RULE-EXEMPT) and inert_fromrev (also under BOLT-RULE-INERT). The code table's per-row proof arms cover 35 rows. bolt's own 9 sites now go through src/rchars.bend (Rchars.text, one pass): the lexer's word, noqa's word, word.bend's text, frame's decode.end, config's dir_of.go and home.segs, and trace's cells. The lexer and trace proofs are carried over to the fold (rword.go, trace.text). Refs #98 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B --- SPEC.md | 5 +- src/PROOF.bend | 10 +- src/README.md | 25 +++- src/codes.bend | 1 + src/config.bend | 7 +- src/lsp/frame.bend | 3 +- src/noqa.bend | 3 +- src/rchars.bend | 17 +++ src/rules.bend | 2 + src/rules/LAWS.bend | 78 +++++++++++ src/rules/PROOF.bend | 207 ++++++++++++++++++++++++++++++ src/rules/laws/trace.bend | 5 +- src/rules/suspicious/fromrev.bend | 49 +++++++ src/syntax/PROOF.bend | 23 ++-- src/syntax/lex.bend | 3 +- src/syntax/word.bend | 3 +- 16 files changed, 415 insertions(+), 26 deletions(-) create mode 100644 src/rchars.bend create mode 100644 src/rules/suspicious/fromrev.bend diff --git a/SPEC.md b/SPEC.md index 055081a..b512e17 100644 --- a/SPEC.md +++ b/SPEC.md @@ -48,14 +48,15 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-RULE-U013 | `scan` reports exactly, outside a LAWS.bend or a PROOF.bend, in a def that calls itself and is not a proof, outside a lambda's body (the rest of a chain after `=>`), a case pattern, and a case arm that does not call the def: each call, a plain or dotted name token then a `(` group, of a callee other than the def, one of whose walked arguments is exactly the lone name of a parameter that every self-call passes back as that same lone name in its own position (carried). A callee walks argument 2 of `List.contains`, `List.find`, `List.filter` and `List.length`, 3 of `List.any` and `List.all`, and 4 of `List.foldl` and `List.foldr` (the Base list searches); a def of the file walks, when it calls itself, its first live parameter that some self-call does not pass back unchanged, unless that parameter's type is `Nat` or `String`, and each parameter its body passes, anywhere, as the lone name of an argument a call of a Base search or of a def listed before it walks. One finding per call. | Proved | proved | src/rules/LAWS.bend scan_counts; src/rules/LAWS.bend scan_quiet; src/rules/LAWS.bend scan_slots | | BOLT-RULE-U014 | `argv` reports exactly one finding for each `IO.args` token with a `(` token right after it among the significant tokens, in every file (no path is exempt), and nothing else. It is opt-in: with no setting of its own it is off, whatever its group says (BOLT-CFG-6). | Proved | proved | src/rules/LAWS.bend argv_counts; src/rules/LAWS.bend inert_argv; src/LAWS.bend argv_opt_in | | BOLT-RULE-U015 | `thunk` (opt-in) reports exactly, in a def, a lambda whose body is exactly a self-call and whose parameter that call does not read: in a chain, at any depth, a leaf of a name kind (the parameter), a leaf whose text is `=>`, a leaf whose text is the def's name, and a `(` group, the chain ending right after the group or going on with a comma, and no name leaf in the group, at any depth, spelling the parameter or the parameter then a dot; one finding for each, on the def's name, and nothing else. | Proved | proved | src/rules/LAWS.bend thunk_walk_counts; src/rules/LAWS.bend thunk_counts | +| BOLT-RULE-U016 | `fromrev` reports exactly, outside a LAWS.bend or a PROOF.bend, one finding (on the first) for each run of four tokens right after one another among the significant tokens (spaces, newlines and comments dropped) whose texts are `String.from_list`, `(`, `List.reverse` and `(`, and nothing else: anything between them, another `(` included, is not the shape, and neither is `List.reverse.go`. | Proved | proved | src/rules/LAWS.bend fromrev_counts; src/rules/LAWS.bend fromrev_exempt; src/rules/LAWS.bend inert_fromrev | | BOLT-RULE-S001 | `doc` reports exactly a top-level def, type or law with no comment block right above it, with the header's exemptions. | Proved | proved | src/rules/LAWS.bend doc_walk_counts; src/rules/LAWS.bend doc_counts | | BOLT-RULE-S002 | `space` reports exactly trailing whitespace or a tab on any line, string literals and `#\|` lines included, or a line over 120 columns with string literals counted as two, comments at full width, and `#\|` lines not counted. | Proved | proved | src/rules/LAWS.bend space_counts; src/rules/LAWS.bend space_line_counts; src/rules/LAWS.bend space_width_counts | | BOLT-RULE-S003 | `wrap` reports exactly one finding for each def header that breaks its shape and none otherwise: a one-line header wider than 120 columns through its last `:` (the whole header when it has none), counted as `space` counts a line except that a comment counts zero, or a header across lines (one holding a newline token; a line break inside a string literal does not count) whose parameter list (opened by the first `(` with no bracket open, split by the commas at its own depth) holds a parameter that spans lines, starts on the `(` line, or starts on the line a later parameter starts on, or holds no parameter at all, or closes with its `)` not on a line below the last parameter's last line, or with no `->` (or, with no return type, the header's `:`) right after its `)` on the `)` line. | Proved | proved | src/rules/LAWS.bend wrap_width; src/rules/LAWS.bend wrap_shape_counts; src/rules/LAWS.bend wrap_counts | | BOLT-RULE-S004 | `param` reports exactly one finding for each parameter binder whose name is shorter than two characters, unless the name is one capital letter (a type parameter) or the parameter is bare or typed `: Quant` (a quantity), none for any other binder, and none at all in a PROOF.bend. | Proved | proved | src/rules/LAWS.bend param_counts | | BOLT-RULE-S005 | `noqa` reports exactly, at each noqa comment's line and column (BOLT-OUT-7), one finding for a bare one (`#`, any spaces, then `noqa` at the comment's end or before a space) and one for each code it names that no graded finding of its file on its line has, a code that is no rule's included, where a project rule's code (`coverage`, `unsafe`, `trace`) is judged only when the run is the whole tree and never in the editor, and nothing else. It runs after the filter, over the findings of every other rule, so its findings come last (BOLT-OUT-3) and no noqa comment silences them: a `# noqa: S005` silences nothing and is itself reported. | Proved | proved | src/LAWS.bend noqa_counts; src/LAWS.bend noqa_bare; src/LAWS.bend noqa_bare_text | | BOLT-RULE-P001 | `tail` reports exactly a non-tail self-call outside any `Bool.pick(..)` in a def whose first live parameter's type is a List or String, whether or not the call shrinks it. | Proved | proved | src/rules/LAWS.bend tail_walk_counts; src/rules/LAWS.bend tail_counts | -| BOLT-RULE-EXEMPT | For every text, a per-file rule's check on a path its header exempts returns no findings. The cost rules (`pick`, `strict`, `eager`, `tail`, `concat`, `index`, `table`, `hoist`, `ring`, `rewalk`, `unit`, `scan`, `thunk`) also skip, wherever it is, every def that is a proof: one whose signature returns a proof (`-> {a == b : T}`), or one written with no type at all (no `:` among its parameters and no `->`, as `def f(x, y):`), which is how Bend fills the law named f; their "reports exactly" rows are read with that skip. | Proved | proved | src/rules/LAWS.bend untyped_exempt; src/rules/LAWS.bend hole_exempt; src/rules/LAWS.bend doc_exempt; src/rules/LAWS.bend param_exempt; src/rules/LAWS.bend pick_exempt; src/rules/LAWS.bend tail_exempt; src/rules/LAWS.bend concat_exempt; src/rules/LAWS.bend eager_exempt; src/rules/LAWS.bend rewalk_exempt; src/rules/LAWS.bend strict_exempt; src/rules/LAWS.bend hoist_exempt; src/rules/LAWS.bend index_exempt; src/rules/LAWS.bend ring_exempt; src/rules/LAWS.bend table_exempt; src/rules/LAWS.bend unit_exempt; src/rules/LAWS.bend scan_exempt; src/rules/LAWS.bend thunk_exempt | -| BOLT-RULE-INERT | For every rule whose pattern is code (all but `escape`, `strings`, `chars`, `space`, `twice`, `foreign`, `noqa` and `rewalk`), changing the contents of a comment or string literal does not change the findings. | Proved | proved | src/rules/LAWS.bend inert_hole; src/rules/LAWS.bend inert_put; src/rules/LAWS.bend inert_tail; src/rules/LAWS.bend inert_pick; src/rules/LAWS.bend inert_strict; src/rules/LAWS.bend inert_doc; src/rules/LAWS.bend inert_param; src/rules/LAWS.bend inert_table; src/rules/LAWS.bend inert_index; src/rules/LAWS.bend inert_concat; src/rules/LAWS.bend inert_unit; src/rules/LAWS.bend inert_eager; src/rules/LAWS.bend inert_fuel; src/rules/LAWS.bend inert_ring; src/rules/LAWS.bend inert_arms; src/rules/LAWS.bend inert_unused; src/rules/LAWS.bend inert_hoist; src/rules/LAWS.bend inert_wrap; src/rules/LAWS.bend inert_scan; src/rules/LAWS.bend inert_argv; src/rules/LAWS.bend inert_thunk | +| BOLT-RULE-EXEMPT | For every text, a per-file rule's check on a path its header exempts returns no findings. The cost rules (`pick`, `strict`, `eager`, `tail`, `concat`, `index`, `table`, `hoist`, `ring`, `rewalk`, `unit`, `scan`, `thunk`) also skip, wherever it is, every def that is a proof: one whose signature returns a proof (`-> {a == b : T}`), or one written with no type at all (no `:` among its parameters and no `->`, as `def f(x, y):`), which is how Bend fills the law named f; their "reports exactly" rows are read with that skip. | Proved | proved | src/rules/LAWS.bend untyped_exempt; src/rules/LAWS.bend hole_exempt; src/rules/LAWS.bend doc_exempt; src/rules/LAWS.bend param_exempt; src/rules/LAWS.bend pick_exempt; src/rules/LAWS.bend tail_exempt; src/rules/LAWS.bend concat_exempt; src/rules/LAWS.bend eager_exempt; src/rules/LAWS.bend rewalk_exempt; src/rules/LAWS.bend strict_exempt; src/rules/LAWS.bend hoist_exempt; src/rules/LAWS.bend index_exempt; src/rules/LAWS.bend ring_exempt; src/rules/LAWS.bend table_exempt; src/rules/LAWS.bend unit_exempt; src/rules/LAWS.bend scan_exempt; src/rules/LAWS.bend thunk_exempt; src/rules/LAWS.bend fromrev_exempt | +| BOLT-RULE-INERT | For every rule whose pattern is code (all but `escape`, `strings`, `chars`, `space`, `twice`, `foreign`, `noqa` and `rewalk`), changing the contents of a comment or string literal does not change the findings. | Proved | proved | src/rules/LAWS.bend inert_hole; src/rules/LAWS.bend inert_put; src/rules/LAWS.bend inert_tail; src/rules/LAWS.bend inert_pick; src/rules/LAWS.bend inert_strict; src/rules/LAWS.bend inert_doc; src/rules/LAWS.bend inert_param; src/rules/LAWS.bend inert_table; src/rules/LAWS.bend inert_index; src/rules/LAWS.bend inert_concat; src/rules/LAWS.bend inert_unit; src/rules/LAWS.bend inert_eager; src/rules/LAWS.bend inert_fuel; src/rules/LAWS.bend inert_ring; src/rules/LAWS.bend inert_arms; src/rules/LAWS.bend inert_unused; src/rules/LAWS.bend inert_hoist; src/rules/LAWS.bend inert_wrap; src/rules/LAWS.bend inert_scan; src/rules/LAWS.bend inert_argv; src/rules/LAWS.bend inert_thunk; src/rules/LAWS.bend inert_fromrev | ### Laws rules (BOLT-LAW) diff --git a/src/PROOF.bend b/src/PROOF.bend index d68772f..60f6685 100644 --- a/src/PROOF.bend +++ b/src/PROOF.bend @@ -252,7 +252,7 @@ def Laws.unknown_exact(ss): def Laws.settings_graded(_text): {==} -# one arm per row of the code table (34), each checked by evaluation, and one +# one arm per row of the code table (35), each checked by evaluation, and one # past its end, where both sides are none: a new rule is a new arm here def Laws.slug_finds_row(n): match n: @@ -324,7 +324,9 @@ def Laws.slug_finds_row(n): {==} case 33n: {==} - case 34n+_p: + case 34n: + {==} + case 35n+_p: {==} # the same arms, looked up by code @@ -398,7 +400,9 @@ def Laws.code_finds_row(n): {==} case 33n: {==} - case 34n+_p: + case 34n: + {==} + case 35n+_p: {==} def Laws.shown(_path, _line, _col, _len, _rule, _msg, _level): diff --git a/src/README.md b/src/README.md index 358085d..312205a 100644 --- a/src/README.md +++ b/src/README.md @@ -51,7 +51,7 @@ unset group has its default. The groups: | group | rules | default | |---------------|----------------------------------------------------------------------------------|---------| | `correctness` | `hole` `pick` `put` `arms` `escape` `twice` `strings` `chars` `foreign` `setting` | error | -| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` (`scan`, `argv`, `thunk`: opt-in) | warn | +| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` `fromrev` (`scan`, `argv`, `thunk`: opt-in) | warn | | `style` | `doc` `space` `wrap` `param` `noqa` | warn | | `laws` | `coverage` `closed` `unsafe` (`trace`: opt-in) | warn | | `pedantic` | `tail` | off | @@ -75,6 +75,7 @@ The stable codes, assigned once (do not renumber): | | | U013 | `scan` | | | | | | U014 | `argv` | | | | | | U015 | `thunk` | | | +| | | U016 | `fromrev` | | | Letters: `C` correctness, `U` suspicious, `S` style, `L` laws, `P` pedantic. @@ -315,6 +316,28 @@ parameters and no `->`), which is how Bend fills the law named `f`. (`_u => Some{go(t)}`), or a continuation that reads its parameter (`a => go(f, a)`), is left alone; `_ => loop(n)` is not, since the rule reads the shape and not the type. +- `fromrev` — `String.from_list(List.reverse(..))`: among the significant + tokens, `String.from_list`, `(`, `List.reverse` and `(` right after one + another, one finding on the first. A buffer of chars consed on the front + and then reversed and read into a String walks the buffer twice and builds + a list only to throw it away; `String.from_list` is not a tail call either, + so a long buffer runs the JS lane out of stack. Fold the buffer onto a + String with `SCon` in one pass (`src/rchars.bend`, bolt's own): + + ```bend + def text.go(buf: List<&2, Char>, acc: String) -> String: + match buf: + case Nil{}: + acc + case Con{h, t}: + text.go(t, SCon{h, acc}) + ``` + + Called as `text.go(buf, SNil{})` (bend 2.0.34, a 100k-char buffer 200 + times: native 0.35 s against 0.17 s; JS at 20k chars 4.6 s against 3.1 s, + and at 50k the two-pass form overflows). Anything between the four tokens, + another `(` included, is not the shape, and neither is `List.reverse.go`. + A LAWS.bend or a PROOF.bend is exempt. - `put` — `Map.put`. It is Base's internal helper: at a leaf it keeps the old key and replaces the value without comparing, so a new key silently overwrites another entry. `Map.set` compares. A file that defines diff --git a/src/codes.bend b/src/codes.bend index dd8bdad..6626b71 100644 --- a/src/codes.bend +++ b/src/codes.bend @@ -38,6 +38,7 @@ def table() -> List<&2, Entry>: Entry{"scan", "U013", "suspicious"}, Entry{"argv", "U014", "suspicious"}, Entry{"thunk", "U015", "suspicious"}, + Entry{"fromrev", "U016", "suspicious"}, Entry{"doc", "S001", "style"}, Entry{"space", "S002", "style"}, Entry{"wrap", "S003", "style"}, diff --git a/src/config.bend b/src/config.bend index 55d9422..7fe3c48 100644 --- a/src/config.bend +++ b/src/config.bend @@ -20,6 +20,7 @@ import Base import ./lazy/lazy.bend as Lazy import ./syntax/lex.bend as Lex +import ./rchars.bend as Rchars import ./syntax/tree.bend as Tree import ./syntax/bind.bend as Bind import ./codes.bend as Codes @@ -170,7 +171,7 @@ def unknown(ss: List<&2, Setting>) -> List<&2, Setting>: def dir_of.go(cs: List<&2, Char>, +acc: List<&2, Char>, best: List<&2, Char>) -> String: match cs: case Nil{}: - String.from_list(List.reverse(&2, Char, best)) + Rchars.text(best) case Con{'/', t}: dir_of.go(t, '/' <> acc, '/' <> acc) case Con{c, t}: @@ -215,9 +216,9 @@ def home.step(+seg: String, +above: List<&2, String>) -> List<&2, String>: def home.segs(cs: List<&2, Char>, seg: List<&2, Char>, above: List<&2, String>) -> List<&2, String>: match cs: case Nil{}: - home.step(String.from_list(List.reverse(&2, Char, seg)), above) + home.step(Rchars.text(seg), above) case Con{'/', t}: - home.segs(t, [], home.step(String.from_list(List.reverse(&2, Char, seg)), above)) + home.segs(t, [], home.step(Rchars.text(seg), above)) case Con{c, t}: home.segs(t, c <> seg, above) diff --git a/src/lsp/frame.bend b/src/lsp/frame.bend index 8bdac29..6e7c6eb 100644 --- a/src/lsp/frame.bend +++ b/src/lsp/frame.bend @@ -2,6 +2,7 @@ # N bytes of UTF-8. Framing counts bytes and a read may end inside a char, so # the transport reads bytes, cuts on bytes, and only then decodes. import Base +import ../rchars.bend as Rchars # UTF-8, bytes to chars # --------------------- @@ -49,7 +50,7 @@ def decode.run(bs: List<&2, U32>, st: Dec) -> Dec: def decode.end(st: Dec) -> String: Dec{need, acc, out} = st - String.from_list(List.reverse(&2, Char, out)) + Rchars.text(out) # UTF-8 bytes as a string (a bad byte is skipped) def decode(bs: List<&2, U32>) -> String: diff --git a/src/noqa.bend b/src/noqa.bend index b7cc122..8aeb42f 100644 --- a/src/noqa.bend +++ b/src/noqa.bend @@ -15,6 +15,7 @@ import Base import ./lazy/lazy.bend as Lazy import ./syntax/lex.bend as Lex +import ./rchars.bend as Rchars import ./finding.bend as F import ./codes.bend as Codes import ./src.bend as Src @@ -60,7 +61,7 @@ type Rd is Data: # the chars read, the last first, as a code def word(buf: List<&2, Char>) -> String: - String.from_list(List.reverse(&2, Char, buf)) + Rchars.text(buf) # before a code: a space waits, a letter or digit starts one, anything else # ends the list diff --git a/src/rchars.bend b/src/rchars.bend new file mode 100644 index 0000000..e3a022a --- /dev/null +++ b/src/rchars.bend @@ -0,0 +1,17 @@ +# src/rchars: a buffer of chars read one at a time and consed on the front +# (the last read first) as the String it spells, in one pass: each char goes +# onto the String built so far, with no reversed list in between (the shape +# `fromrev`, U016, reports). Pure. +import Base + +# the buffer's chars, first read first, then acc +def onto(buf: List<&2, Char>, acc: String) -> String: + match buf: + case Nil{}: + acc + case Con{h, t}: + onto(t, SCon{h, acc}) + +# the buffer's chars, first read first +def text(buf: List<&2, Char>) -> String: + onto(buf, SNil{}) diff --git a/src/rules.bend b/src/rules.bend index a2e14ee..12a0af1 100644 --- a/src/rules.bend +++ b/src/rules.bend @@ -40,6 +40,7 @@ import ./rules/suspicious/unit.bend as Unit import ./rules/suspicious/scan.bend as Scan import ./rules/suspicious/argv.bend as Argv import ./rules/suspicious/thunk.bend as Thunk +import ./rules/suspicious/fromrev.bend as Fromrev import ./rules/correctness/put.bend as Put import ./rules/correctness/escape.bend as Escape import ./rules/correctness/strings.bend as Strings @@ -89,6 +90,7 @@ def on.rules(+ss: Src.Src) -> List<&2, F.Finding>: Scan.check(ss), Argv.check(ss), Thunk.check(ss), + Fromrev.check(ss), Put.check(ss), Escape.check(ss), Strings.check(ss), diff --git a/src/rules/LAWS.bend b/src/rules/LAWS.bend index 0fdcbdc..8716438 100644 --- a/src/rules/LAWS.bend +++ b/src/rules/LAWS.bend @@ -28,6 +28,7 @@ import ./suspicious/ring.bend as Ring import ./suspicious/table.bend as Table import ./suspicious/unit.bend as UnitRule import ./suspicious/argv.bend as Argv +import ./suspicious/fromrev.bend as Fromrev import ./suspicious/thunk.bend as Thunk import ./suspicious/scan.bend as Scan import ./correctness/chars.bend as Chars @@ -225,6 +226,47 @@ law argv_counts: {List.length(&2, F.Finding, Argv.check(Src.Src{path, text, toks, tree, bound, items})) == argv_count(T.sig(toks)) : Nat} +# True when tt is `String.from_list` and the tokens open with `(`, +# `List.reverse` and `(` +def fromrev_at(+tt: String, toks: List<&2, Lex.Tok>) -> Bool: + match toks: + case Nil{}: + False{} + case Con{Lex.Tok{k1, +a, l1, c1}, r1}: + match r1: + case Nil{}: + False{} + case Con{Lex.Tok{k2, +b, l2, c2}, r2}: + match r2: + case Nil{}: + False{} + case Con{Lex.Tok{k3, +d, l3, c3}, r3}: + Bool.and(Bool.and(String.eq(tt, "String.from_list"), String.eq(a, "(")), + Bool.and(String.eq(b, "List.reverse"), String.eq(d, "("))) + +# how many tokens start a `String.from_list`, `(`, `List.reverse`, `(` run +def fromrev_count(toks: List<&2, Lex.Tok>) -> Nat: + match toks: + case Nil{}: + 0n + case Con{Lex.Tok{k, +t, l, c}, +rest}: + +m = fromrev_count(rest) + Bool.pick(Nat, fromrev_at(t, rest), 1n+m, m) + +# LAW: fromrev reports, outside a LAWS.bend or a PROOF.bend, one finding for +# each run of significant tokens whose texts are `String.from_list`, `(`, +# `List.reverse` and `(`, and none for any other token +# BOLT-RULE-U016 +law fromrev_counts: + for +path: String + for text: String + for +toks: List<&2, Lex.Tok> + for tree: Tree.Node + for bound: Bind.Bound + for items: List<&2, Outline.Item> + {List.length(&2, F.Finding, Fromrev.check(Src.Src{path, text, toks, tree, bound, items})) + == Bool.pick(Nat, Paths.is_law_file(path), 0n, fromrev_count(T.sig(toks))) : Nat} + # True when the first token past spaces, newlines and comments is `TODO` def todo_next(toks: List<&2, Lex.Tok>) -> Bool: match toks: @@ -610,6 +652,19 @@ law scan_exempt: for e: {Paths.is_law_file(path) == True{} : Bool} {Scan.check(Src.Src{path, text, toks, tree, bound, items}) == Nil{} : List<&2, F.Finding>} +# LAW: fromrev reports nothing in a LAWS.bend or a PROOF.bend, which never run, whatever the source holds +# BOLT-RULE-EXEMPT +# BOLT-RULE-U016 +law fromrev_exempt: + for +path: String + for text: String + for toks: List<&2, Lex.Tok> + for tree: Tree.Node + for bound: Bind.Bound + for items: List<&2, Outline.Item> + for e: {Paths.is_law_file(path) == True{} : Bool} + {Fromrev.check(Src.Src{path, text, toks, tree, bound, items}) == Nil{} : List<&2, F.Finding>} + # LAW: a def written with no type (no `:` among its parameters, no `->`) fills the law of its name, so it is a # proof: every cost rule that reads Calls.exempt skips it wherever it is, as it skips one that returns a proof # BOLT-RULE-EXEMPT @@ -4510,6 +4565,29 @@ law inert_argv: {Argv.check(Src.Src{path, text, toks, tree, bound, items}) == Argv.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} +# LAW: fromrev reads what no comment or string says: two sources as the +# lexer makes them whose tokens read the same with comments and strings cut +# have the same findings +# BOLT-RULE-INERT +# BOLT-RULE-U016 +law inert_fromrev: + for +path: String + for text: String + for toks: List<&2, Lex.Tok> + for tree: Tree.Node + for bound: Bind.Bound + for items: List<&2, Outline.Item> + for text2: String + for toks2: List<&2, Lex.Tok> + for tree2: Tree.Node + for bound2: Bind.Bound + for items2: List<&2, Outline.Item> + for ok: {inert.oks(toks) == True{} : Bool} + for ok2: {inert.oks(toks2) == True{} : Bool} + for e: {inert.toks(toks) == inert.toks(toks2) : List<&2, Lex.Tok>} + {Fromrev.check(Src.Src{path, text, toks, tree, bound, items}) + == Fromrev.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} + # LAW: tail reads what no string says: two sources as the lexer makes them # whose trees read the same with strings cut have the same findings (a # string's text is only ever compared with the def's name or `Bool.pick`) diff --git a/src/rules/PROOF.bend b/src/rules/PROOF.bend index 3178a6d..d149e0f 100644 --- a/src/rules/PROOF.bend +++ b/src/rules/PROOF.bend @@ -29,6 +29,8 @@ import ./suspicious/ring.bend as Ring import ./suspicious/table.bend as Table import ./suspicious/unit.bend as UnitRule import ./suspicious/argv.bend as Argv +import ./suspicious/fromrev.bend as Fromrev +import ../rchars.bend as Rchars import ./suspicious/scan.bend as Scan import ./correctness/chars.bend as Chars import ./correctness/strings.bend as Strings @@ -898,6 +900,68 @@ def argv.calls(toks, path): def Laws.argv_counts(path, _text, toks, _tree, _bound, _items): argv.calls(T.sig(toks), path) +# fromrev +# ------- + +# an and of four, grouped either way +law fromrev.and4: + for p: Bool + for q: Bool + for r: Bool + for w: Bool + {Bool.and(p, Bool.and(q, Bool.and(r, w))) == Bool.and(Bool.and(p, q), Bool.and(r, w)) : Bool} + +def fromrev.and4(p, _q, _r, _w): + match p: + case True{}: + {==} + case False{}: + {==} + +# the rule's test of a run is the law's +law fromrev.at: + for +t: String + for toks: List<&2, Lex.Tok> + {Fromrev.at(t, toks) == Laws.fromrev_at(t, toks) : Bool} + +def fromrev.at(t, toks): + match toks: + case Nil{}: + {==} + case Con{Lex.Tok{k1, a, l1, c1}, r1}: + match r1: + case Nil{}: + {==} + case Con{Lex.Tok{k2, b, l2, c2}, r2}: + match r2: + case Nil{}: + {==} + case Con{Lex.Tok{k3, d, l3, c3}, r3}: + fromrev.and4(String.eq(t, "String.from_list"), String.eq(a, "("), String.eq(b, "List.reverse"), + String.eq(d, "(")) + +# fromrev's walk counts the runs +law fromrev.walk: + for toks: List<&2, Lex.Tok> + for +path: String + {List.length(&2, F.Finding, Fromrev.walk(toks, path)) == Laws.fromrev_count(toks) : Nat} + +def fromrev.walk(toks, path): + match toks: + case Nil{}: + {==} + case Con{Lex.Tok{k, +t, +l, +c}, +rest}: + +x = {F.Finding{path, l, c, 16, "fromrev", "String.from_list(List.reverse(..)) walks the list twice and builds one it throws away; fold it onto a String with SCon in one pass."} + : F.Finding} + %fromrev.at(t, rest) : {List.length(&2, F.Finding, Bool.pick(List<&2, F.Finding>, Fromrev.at(t, rest), + x <> Fromrev.walk(rest, path), Fromrev.walk(rest, path))) + == Bool.pick(Nat, _, 1n+Laws.fromrev_count(rest), Laws.fromrev_count(rest)) : Nat} + nat.pick(Fromrev.at(t, rest), x, Fromrev.walk(rest, path), Laws.fromrev_count(rest), fromrev.walk(rest, path)) + +def Laws.fromrev_counts(path, _text, toks, _tree, _bound, _items): + put.stop(Paths.is_law_file(path), Fromrev.walk(T.sig(toks), path), Laws.fromrev_count(T.sig(toks)), + fromrev.walk(T.sig(toks), path)) + # one token onto a list the TODO test agrees on law hole.todo.step: for kk: Lex.TokKind @@ -14334,6 +14398,19 @@ def trace.close(cut: Laws.trace.Cut, st: Trace.Cells) -> List<&2, String>: case Laws.trace.Cut{hh, tl} Trace.Cells{cur, done}: List.reverse.go(&2, String, done, trace.closed(tl, List.reverse.go(&2, Char, cur, hh))) +# a buffer folded onto a list's string spells what reversing it onto the list does +law trace.text: + for cs: List<&2, Char> + for acc: List<&2, Char> + {Rchars.onto(cs, String.from_list(acc)) == String.from_list(List.reverse.go(&2, Char, cs, acc)) : String} + +def trace.text(cs, acc): + match cs: + case Nil{}: + {==} + case Con{h, t}: + trace.text(t, h <> acc) + # one char onto the state is one piece onto the cut law trace.at: for bar: Bool @@ -14346,6 +14423,8 @@ law trace.at: def trace.at(bar, _cc, cut, st): match bar cut st: case True{} Laws.trace.Cut{hh, tl} Trace.Cells{cur, done}: + %trace.text(cur, []) : {List.reverse.go(&2, String, done, String.trim(Rchars.text(cur)) <> trace.closed(tl, hh)) + == List.reverse.go(&2, String, done, String.trim(_) <> trace.closed(tl, hh)) : List<&2, String>} {==} case False{} Laws.trace.Cut{hh, tl} Trace.Cells{cur, done}: {==} @@ -14362,6 +14441,8 @@ def trace.go(cs, esc, st): case Nil{}: match st: case Trace.Cells{cur, done}: + %trace.text(cur, []) : {List.reverse.go(&2, String, done, [Rchars.text(cur)]) + == List.reverse.go(&2, String, done, [_]) : List<&2, String>} {==} case Con{+cc, +t}: Equal.trans(List<&2, String>, @@ -19006,6 +19087,126 @@ def Laws.inert_argv(path, _text, toks, _tree, _bound, _items, _text2, toks2, _tr inert.via(List<&2, Lex.Tok>, z => Argv.calls(T.sig(z), path), toks, toks2, Laws.inert.toks(toks), Laws.inert.toks(toks2), inert.argv.on(toks, path, ok), inert.argv.on(toks2, path, ok2), e) +# fromrev +# ------- + +# four texts, each read that way: tested for the shape as they were +law inert.fromrev.shape: + for +b1: Bool + for +t: String + for +b2: Bool + for +a: String + for +b3: Bool + for +b: String + for +b4: Bool + for +d: String + for +e1: {Laws.inert.fits.go(b1, t) == True{} : Bool} + for +e2: {Laws.inert.fits.go(b2, a) == True{} : Bool} + for +e3: {Laws.inert.fits.go(b3, b) == True{} : Bool} + for +e4: {Laws.inert.fits.go(b4, d) == True{} : Bool} + {Fromrev.shape(Laws.inert.keep(b1, t), Laws.inert.keep(b2, a), Laws.inert.keep(b3, b), Laws.inert.keep(b4, d)) + == Fromrev.shape(t, a, b, d) : Bool} + +def inert.fromrev.shape(b1, t, b2, a, b3, b, b4, d, e1, e2, e3, e4): + +k1 = Laws.inert.keep(b1, t) + +k2 = Laws.inert.keep(b2, a) + +k3 = Laws.inert.keep(b3, b) + +k4 = Laws.inert.keep(b4, d) + +lhs = Fromrev.shape(k1, k2, k3, k4) + %inert.eq_keep(b1, t, "String.from_list", e1, {==}) : {lhs == Bool.and(_, + Bool.and(String.eq(a, "("), Bool.and(String.eq(b, "List.reverse"), String.eq(d, "(")))) : Bool} + %inert.eq_keep(b2, a, "(", e2, {==}) : {lhs == Bool.and(String.eq(k1, "String.from_list"), + Bool.and(_, Bool.and(String.eq(b, "List.reverse"), String.eq(d, "(")))) : Bool} + %inert.eq_keep(b3, b, "List.reverse", e3, {==}) : {lhs == Bool.and(String.eq(k1, "String.from_list"), + Bool.and(String.eq(k2, "("), Bool.and(_, String.eq(d, "(")))) : Bool} + %inert.eq_keep(b4, d, "(", e4, {==}) : {lhs == Bool.and(String.eq(k1, "String.from_list"), + Bool.and(String.eq(k2, "("), Bool.and(String.eq(k3, "List.reverse"), _))) : Bool} + {==} + +# a token's text, then tokens as the lexer makes them, each read that way: +# they open the shape as they did +law inert.fromrev.at: + for +b1: Bool + for +t: String + for ts: List<&2, Lex.Tok> + for +e1: {Laws.inert.fits.go(b1, t) == True{} : Bool} + for +e: {Laws.inert.oks(ts) == True{} : Bool} + {Fromrev.at(Laws.inert.keep(b1, t), Laws.inert.toks(ts)) == Fromrev.at(t, ts) : Bool} + +def inert.fromrev.at(b1, t, ts, e1, e): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k1, +a, +l1, +c1}, +r1}: + match r1: + case Nil{}: + {==} + case Con{Lex.Tok{+k2, +b, +l2, +c2}, +r2}: + match r2: + case Nil{}: + {==} + case Con{Lex.Tok{+k3, +d, +l3, +c3}, +r3}: + +h1 = {Lex.Tok{k1, a, l1, c1} : Lex.Tok} + +h2 = {Lex.Tok{k2, b, l2, c2} : Lex.Tok} + +h3 = {Lex.Tok{k3, d, l3, c3} : Lex.Tok} + +er1 = inert.and_r(Laws.inert.fits(h1), Laws.inert.oks(r1), e) + +er2 = inert.and_r(Laws.inert.fits(h2), Laws.inert.oks(r2), er1) + inert.fromrev.shape(b1, t, Laws.inert.blanks(k1), a, Laws.inert.blanks(k2), b, Laws.inert.blanks(k3), d, + e1, inert.and_l(Laws.inert.fits(h1), Laws.inert.oks(r1), e), + inert.and_l(Laws.inert.fits(h2), Laws.inert.oks(r2), er1), + inert.and_l(Laws.inert.fits(h3), Laws.inert.oks(r3), er2)) + +# fromrev's walk reads no comment or string: it compares texts with the shape's +law inert.fromrev.walk: + for ts: List<&2, Lex.Tok> + for +path: String + for +e: {Laws.inert.oks(ts) == True{} : Bool} + {Fromrev.walk(Laws.inert.toks(ts), path) == Fromrev.walk(ts, path) : List<&2, F.Finding>} + +def inert.fromrev.walk(ts, path, e): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k, +t, +l, +c}, +rest}: + +h = {Lex.Tok{k, t, l, c} : Lex.Tok} + +er = inert.and_r(Laws.inert.fits(h), Laws.inert.oks(rest), e) + +x = {F.Finding{path, l, c, 16, "fromrev", "String.from_list(List.reverse(..)) walks the list twice and builds one it throws away; fold it onto a String with SCon in one pass."} + : F.Finding} + +tt = Laws.inert.keep(Laws.inert.blanks(k), t) + +cr = Laws.inert.toks(rest) + +lhs = Bool.pick(List<&2, F.Finding>, Fromrev.at(tt, cr), x <> Fromrev.walk(cr, path), Fromrev.walk(cr, path)) + %inert.fromrev.walk(rest, path, er) : {lhs == Bool.pick(List<&2, F.Finding>, Fromrev.at(t, rest), + x <> _, _) : List<&2, F.Finding>} + %inert.fromrev.at(Laws.inert.blanks(k), t, rest, inert.and_l(Laws.inert.fits(h), Laws.inert.oks(rest), e), er) : + {lhs == Bool.pick(List<&2, F.Finding>, _, x <> Fromrev.walk(cr, path), Fromrev.walk(cr, path)) + : List<&2, F.Finding>} + {==} + +# fromrev's walk of the significant tokens reads no comment or string +law inert.fromrev.on: + for +ts: List<&2, Lex.Tok> + for +path: String + for +e: {Laws.inert.oks(ts) == True{} : Bool} + {Fromrev.walk(T.sig(Laws.inert.toks(ts)), path) == Fromrev.walk(T.sig(ts), path) : List<&2, F.Finding>} + +def inert.fromrev.on(ts, path, e): + +s = T.sig(ts) + +cs = Laws.inert.toks(s) + %Equal.sym(List<&2, Lex.Tok>, T.sig(Laws.inert.toks(ts)), cs, inert.put.sig(ts)) : + {Fromrev.walk(_, path) == Fromrev.walk(s, path) : List<&2, F.Finding>} + inert.fromrev.walk(s, path, inert.put.sig_ok(ts, e)) + +def Laws.inert_fromrev(path, _text, toks, _tree, _bound, _items, _text2, toks2, _tree2, _bound2, _items2, ok, ok2, e): + inert.via(List<&2, Lex.Tok>, z => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], + _u => Fromrev.walk(T.sig(z), path)), toks, toks2, Laws.inert.toks(toks), Laws.inert.toks(toks2), + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, w => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), + [], _u => w), Fromrev.walk(T.sig(Laws.inert.toks(toks)), path), Fromrev.walk(T.sig(toks), path), + inert.fromrev.on(toks, path, ok)), + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, w => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), + [], _u => w), Fromrev.walk(T.sig(Laws.inert.toks(toks2)), path), Fromrev.walk(T.sig(toks2), path), + inert.fromrev.on(toks2, path, ok2)), + e) + # the tree rules: what calls.bend gives them # ------------------------------------------ @@ -32161,6 +32362,12 @@ def Laws.scan_exempt(path, _text, _toks, tree, _bound, _items, e): : List<&2, F.Finding>} {==} +def Laws.fromrev_exempt(path, _text, toks, _tree, _bound, _items, e): + %Equal.sym(Bool, Paths.is_law_file(path), True{}, e) : {Lazy.stop(List<&2, F.Finding>, _, [], + _u => Fromrev.walk(T.sig(toks), path)) == Nil{} + : List<&2, F.Finding>} + {==} + # the file's walks of a name are the law's law scan.file_at: for ws: List<&2, Scan.Walk> diff --git a/src/rules/laws/trace.bend b/src/rules/laws/trace.bend index 613501e..5744043 100644 --- a/src/rules/laws/trace.bend +++ b/src/rules/laws/trace.bend @@ -21,6 +21,7 @@ import ../../finding.bend as F import ../digest.bend as Digest import ../imports.bend as Imports import ../../lazy/lazy.bend as Lazy +import ../../rchars.bend as Rchars # reading SPEC.md # --------------- @@ -70,7 +71,7 @@ def cells.at(bar: Bool, cc: Char, st: Cells) -> Cells: match bar: case True{}: Cells{cur, done} = st - Cells{[], trim(String.from_list(List.reverse(&2, Char, cur))) <> done} + Cells{[], trim(Rchars.text(cur)) <> done} case False{}: Cells{cur, done} = st Cells{cc <> cur, done} @@ -82,7 +83,7 @@ def cells.go(cs: List<&2, Char>, esc: Bool, st: Cells) -> List<&2, String>: match cs: case Nil{}: Cells{cur, done} = st - List.reverse(&2, String, String.from_list(List.reverse(&2, Char, cur)) <> done) + List.reverse(&2, String, Rchars.text(cur) <> done) case Con{+c, t}: cells.go(t, Char.is_eq(c, '\\'), cells.at(Bool.and(Char.is_eq(c, '|'), Bool.not(esc)), c, st)) diff --git a/src/rules/suspicious/fromrev.bend b/src/rules/suspicious/fromrev.bend new file mode 100644 index 0000000..a9e230a --- /dev/null +++ b/src/rules/suspicious/fromrev.bend @@ -0,0 +1,49 @@ +# rule fromrev: a String read off a reversed list: among the significant +# tokens (spaces, newlines and comments dropped), four tokens right after one +# another whose texts are `String.from_list`, `(`, `List.reverse` and `(`; +# one finding, on the `String.from_list` token, for each such run, and +# nothing else. Anything between them, another `(` included +# (`String.from_list((List.reverse(..)))`), is not the shape, and neither is +# `List.reverse.go`. A buffer of chars consed on the front, then reversed +# and read into a String, walks the buffer twice and builds a list only to +# throw it away (and String.from_list, not a tail call, runs the JS lane out +# of stack on a long buffer): fold the buffer onto a String with SCon in one +# pass, `go(t, SCon{h, acc})` from `SNil{}` (src/rchars.bend). A LAWS.bend +# or a PROOF.bend, which never runs, is exempt. +import Base +import ../../src.bend as Src +import ../../paths.bend as Paths +import ../../lazy/lazy.bend as Lazy +import ../../finding.bend as F +import ../../syntax/lex.bend as Lex +import ../tokens.bend as T + +# are the four texts `String.from_list`, `(`, `List.reverse` and `(`? +def shape(+tt: String, +aa: String, +bb: String, +dd: String) -> Bool: + Bool.and(String.eq(tt, "String.from_list"), + Bool.and(String.eq(aa, "("), Bool.and(String.eq(bb, "List.reverse"), String.eq(dd, "(")))) + +# a token of text tt, then these: do the four open the shape? +def at(+tt: String, toks: List<&2, Lex.Tok>) -> Bool: + match toks: + case Con{Lex.Tok{k1, +aa, l1, c1}, Con{Lex.Tok{k2, +bb, l2, c2}, Con{Lex.Tok{k3, +dd, l3, c3}, rest}}}: + shape(tt, aa, bb, dd) + case other: + False{} + +# every run of the shape among the tokens, in order +def walk(toks: List<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>: + match toks: + case Nil{}: + Nil{} + case Con{Lex.Tok{k, +t, +l, +c}, +rest}: + +more = walk(rest, path) + Bool.pick(List<&2, F.Finding>, at(t, rest), + F.Finding{path, l, c, 16, "fromrev", "String.from_list(List.reverse(..)) walks the list twice and builds one it throws away; fold it onto a String with SCon in one pass."} + <> more, + more) + +# the rule +def check(ss: Src.Src) -> List<&2, F.Finding>: + Src.Src{+path, text, toks, tree, bound, items} = ss + Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => walk(T.sig(toks), path)) diff --git a/src/syntax/PROOF.bend b/src/syntax/PROOF.bend index 26ab86c..cec47da 100644 --- a/src/syntax/PROOF.bend +++ b/src/syntax/PROOF.bend @@ -1,6 +1,7 @@ # syntax: the proofs. `bend PROOF.bend` is the gate. import Base import ./lex.bend as Lex +import ../rchars.bend as Rchars import ./tree.bend as Tree import ./outline.bend as Outline import ../lazy/lazy.bend as Lazy @@ -63,11 +64,11 @@ def rword(buf: List<&2, Char>) -> String: case Con{h, t}: String.append(rword(t), one(h)) -# reversing onto an accumulator spells the reversed list, then the accumulator +# folding a buffer onto a string spells the reversed buffer, then the string law rword.go: for +xs: List<&2, Char> - for +acc: List<&2, Char> - {String.from_list(List.reverse.go(&2, Char, xs, acc)) == String.append(rword(xs), String.from_list(acc)) : String} + for +acc: String + {Rchars.onto(xs, acc) == String.append(rword(xs), acc) : String} def rword.go(xs, acc): match xs: @@ -75,13 +76,13 @@ def rword.go(xs, acc): {==} case Con{h, t}: Equal.trans(String, - String.from_list(List.reverse.go(&2, Char, t, h <> acc)), - String.append(rword(t), SCon{h, String.from_list(acc)}), - String.append(String.append(rword(t), one(h)), String.from_list(acc)), - rword.go(t, h <> acc), - Equal.sym(String, String.append(String.append(rword(t), one(h)), String.from_list(acc)), - String.append(rword(t), SCon{h, String.from_list(acc)}), - app.assoc(rword(t), one(h), String.from_list(acc)))) + Rchars.onto(t, SCon{h, acc}), + String.append(rword(t), SCon{h, acc}), + String.append(String.append(rword(t), one(h)), acc), + rword.go(t, SCon{h, acc}), + Equal.sym(String, String.append(String.append(rword(t), one(h)), acc), + String.append(rword(t), SCon{h, acc}), + app.assoc(rword(t), one(h), acc))) # a buffer's word is its reversed chars law rword.word: @@ -90,7 +91,7 @@ law rword.word: def rword.word(buf): Equal.trans(String, Lex.word(buf), String.append(rword(buf), SNil{}), rword(buf), - rword.go(buf, []), app.nil(rword(buf))) + rword.go(buf, SNil{}), app.nil(rword(buf))) # a reversed token list's texts, in order def rspell(toks: List<&2, Lex.Tok>) -> String: diff --git a/src/syntax/lex.bend b/src/syntax/lex.bend index 75cd3ab..6554781 100644 --- a/src/syntax/lex.bend +++ b/src/syntax/lex.bend @@ -15,6 +15,7 @@ # a binder), `_` (TWild), and the operators that bind: `:` `=` `<-` `->` `=>` # `@` `&`. import Base +import ../rchars.bend as Rchars import ../lazy/lazy.bend as Lazy # the kinds; TName is a plain name (lowercase, undotted): what a pattern can @@ -224,7 +225,7 @@ def begin.kind(cls: Class) -> TokKind: # the buffered chars as a string, in order def word(buf: List<&2, Char>) -> String: - String.from_list(List.reverse(&2, Char, buf)) + Rchars.text(buf) # is the text one of Bend's keywords? def is_keyword(+tt: String) -> Bool: diff --git a/src/syntax/word.bend b/src/syntax/word.bend index 0ed3580..bfb97fd 100644 --- a/src/syntax/word.bend +++ b/src/syntax/word.bend @@ -4,6 +4,7 @@ # as on it, as editors put the cursor there. import Base import ../lazy/lazy.bend as Lazy +import ../rchars.bend as Rchars # i: the column of the next char; start: where the current run began; run: the # current name, reversed; hit: the name found @@ -16,7 +17,7 @@ def is_name(+cc: Char) -> Bool: # the run's chars (reversed) as a string def text(run: List<&2, Char>) -> String: - String.from_list(List.reverse(&2, Char, run)) + Rchars.text(run) # the run holds the column: keep it; otherwise the hit so far def close.yes(ok: Bool, run: List<&2, Char>, hit: Maybe<&2, String>) -> Maybe<&2, String>: From 5da74a277c0fb20ac80e2a057d49a506757b4b33 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 13:41:15 +0000 Subject: [PATCH 2/6] fix(rules): thunk (U015) reports only a lone thunk, not a dispatch thunk now reports a self-call thunk only when it is the one lambda among the arguments of the call it is passed to: the kids of a `(` group, split at their comma leaves, hold exactly one argument with a `=>` leaf of its own (not inside a bracket). A dispatch, a call given two or more lambdas (`Lazy.either(T, c, _u => go(a), _v => go(b))`), is left alone: carrying one Bool into the next call does not replace it. A lambda that is no call's argument (`x = _u => go(t)`) is no longer reported either. This narrows a guaranteed behavior: BOLT-RULE-U015 is reworded with the rule's header, and thunk_walk_counts' independent counter (thunk.count, now carrying whether the chain is such a call's kids, with thunk.args and thunk.lone) is restated to match and re-proved; thunk_counts, thunk_exempt and inert_thunk follow. Over the corpus (bolt, ez, ezhttp, ezjson, eztoml, snap; law, proof and test files removed): 200 -> 177 findings. bolt 77 -> 65, ez 69 -> 69, ezhttp 19 -> 17, ezjson 6 -> 6, eztoml 27 -> 18, snap 2 -> 2. Every one of the 23 dropped is a call with two or more lambdas. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B --- AGENTS.md | 3 +- SPEC.md | 2 +- src/README.md | 31 +++--- src/rules/LAWS.bend | 56 +++++++--- src/rules/PROOF.bend | 186 ++++++++++++++++++++++++-------- src/rules/suspicious/thunk.bend | 70 ++++++++---- 6 files changed, 253 insertions(+), 95 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index d6d506b..c61be60 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -162,7 +162,8 @@ Design specs and plans are not kept in this repo; they live under the loop on every miss (bend 2.0.34, 500 misses over 100k cells: JS 2.40 s against 0.28 s carried, native `--gpu off` 1.18 s against 0.76 s; bend's self-hosted compiler, PR #1207, gained 5.8 to 6.7% per site). `bolt`'s - `thunk` rule (U015, opt-in) reports that shape. The early exits of + `thunk` rule (U015, opt-in) reports that shape, a lone thunk (a dispatch + of two or more lambdas is left alone). The early exits of `src/lazy/lazy.bend` (`Lazy.stop`, `Lazy.or_else`, `Lazy.and_then`: the last argument is a `Unit -> T` thunk, applied only on the branch that needs it) stay right for expensive work that does not recurse. The same goes for diff --git a/SPEC.md b/SPEC.md index b512e17..984926e 100644 --- a/SPEC.md +++ b/SPEC.md @@ -47,7 +47,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-RULE-U012 | `unit` reports exactly a multiply or divide by one on a recursive step. | Proved | proved | src/rules/LAWS.bend unit_walk_counts; src/rules/LAWS.bend unit_counts | | BOLT-RULE-U013 | `scan` reports exactly, outside a LAWS.bend or a PROOF.bend, in a def that calls itself and is not a proof, outside a lambda's body (the rest of a chain after `=>`), a case pattern, and a case arm that does not call the def: each call, a plain or dotted name token then a `(` group, of a callee other than the def, one of whose walked arguments is exactly the lone name of a parameter that every self-call passes back as that same lone name in its own position (carried). A callee walks argument 2 of `List.contains`, `List.find`, `List.filter` and `List.length`, 3 of `List.any` and `List.all`, and 4 of `List.foldl` and `List.foldr` (the Base list searches); a def of the file walks, when it calls itself, its first live parameter that some self-call does not pass back unchanged, unless that parameter's type is `Nat` or `String`, and each parameter its body passes, anywhere, as the lone name of an argument a call of a Base search or of a def listed before it walks. One finding per call. | Proved | proved | src/rules/LAWS.bend scan_counts; src/rules/LAWS.bend scan_quiet; src/rules/LAWS.bend scan_slots | | BOLT-RULE-U014 | `argv` reports exactly one finding for each `IO.args` token with a `(` token right after it among the significant tokens, in every file (no path is exempt), and nothing else. It is opt-in: with no setting of its own it is off, whatever its group says (BOLT-CFG-6). | Proved | proved | src/rules/LAWS.bend argv_counts; src/rules/LAWS.bend inert_argv; src/LAWS.bend argv_opt_in | -| BOLT-RULE-U015 | `thunk` (opt-in) reports exactly, in a def, a lambda whose body is exactly a self-call and whose parameter that call does not read: in a chain, at any depth, a leaf of a name kind (the parameter), a leaf whose text is `=>`, a leaf whose text is the def's name, and a `(` group, the chain ending right after the group or going on with a comma, and no name leaf in the group, at any depth, spelling the parameter or the parameter then a dot; one finding for each, on the def's name, and nothing else. | Proved | proved | src/rules/LAWS.bend thunk_walk_counts; src/rules/LAWS.bend thunk_counts | +| BOLT-RULE-U015 | `thunk` (opt-in) reports exactly, in a def, a lambda whose body is exactly a self-call and whose parameter that call does not read, passed as the one lambda of a call: in the kids of a group opened by `(` (its arguments: the kids split at their comma leaves), exactly one argument holding, among its own nodes and not inside a group, a leaf whose text is `=>`, four nodes in a row of those kids, a leaf of a name kind (the parameter), a leaf whose text is `=>`, a leaf whose text is the def's name, and a `(` group, the kids ending right after the group or going on with a comma, and no name leaf in the group, at any depth, spelling the parameter or the parameter then a dot; such groups found at any depth; one finding for each, on the def's name, and nothing else. A call given two or more lambdas (a dispatch) gets none. | Proved | proved | src/rules/LAWS.bend thunk_walk_counts; src/rules/LAWS.bend thunk_counts | | BOLT-RULE-U016 | `fromrev` reports exactly, outside a LAWS.bend or a PROOF.bend, one finding (on the first) for each run of four tokens right after one another among the significant tokens (spaces, newlines and comments dropped) whose texts are `String.from_list`, `(`, `List.reverse` and `(`, and nothing else: anything between them, another `(` included, is not the shape, and neither is `List.reverse.go`. | Proved | proved | src/rules/LAWS.bend fromrev_counts; src/rules/LAWS.bend fromrev_exempt; src/rules/LAWS.bend inert_fromrev | | BOLT-RULE-S001 | `doc` reports exactly a top-level def, type or law with no comment block right above it, with the header's exemptions. | Proved | proved | src/rules/LAWS.bend doc_walk_counts; src/rules/LAWS.bend doc_counts | | BOLT-RULE-S002 | `space` reports exactly trailing whitespace or a tab on any line, string literals and `#\|` lines included, or a line over 120 columns with string literals counted as two, comments at full width, and `#\|` lines not counted. | Proved | proved | src/rules/LAWS.bend space_counts; src/rules/LAWS.bend space_line_counts; src/rules/LAWS.bend space_width_counts | diff --git a/src/README.md b/src/README.md index 312205a..bc3c3f0 100644 --- a/src/README.md +++ b/src/README.md @@ -302,19 +302,24 @@ parameters and no `->`), which is how Bend fills the law named `f`. tell the reader that drops it from one that does not: give that one reader `# noqa: U014`. No path is exempt. - `thunk` (opt-in) — a lambda whose body is exactly a self-call and whose - parameter the call does not read: a `Unit -> T` thunk such as - `Lazy.or_else(hit, _u => go(rest, k))`. The closure is allocated on every - step and the call in it is not a tail call of the def, so the search leaves - the loop each time round (bend 2.0.34, 500 misses over 100k cells: JS - 2.40 s against 0.28 s, native 1.18 s against 0.76 s). Carry the test as a - Bool into the next call, `go(rest, k, test(h))`, and match on it first: the - step is then a tail call and compiles to a loop. `Lazy.*` stays right for - guarding work that does not recurse. Exactly: a name leaf (the parameter), - `=>`, the def's name and its `(` group, with the chain ending there or - going on with a comma, and no name leaf in the group spelling the - parameter or the parameter then a dot. A body that does more than the call - (`_u => Some{go(t)}`), or a continuation that reads its parameter - (`a => go(f, a)`), is left alone; `_ => loop(n)` is not, since the rule + parameter the call does not read, passed as the one lambda of a call: a + `Unit -> T` thunk such as `Lazy.or_else(hit, _u => go(rest, k))`. The + closure is allocated on every step and the call in it is not a tail call of + the def, so the search leaves the loop each time round (bend 2.0.34, 500 + misses over 100k cells: JS 2.40 s against 0.28 s, native 1.18 s against + 0.76 s). Carry the test as a Bool into the next call, `go(rest, k, + test(h))`, and match on it first: the step is then a tail call and compiles + to a loop. `Lazy.*` stays right for guarding work that does not recurse. + A dispatch, a call given two or more lambdas (`Lazy.either(T, c, _u => + go(a), _v => go(b))`), is left alone: one carried Bool does not replace it. + Exactly: in the kids of a `(` group whose arguments (split at their commas) + hold exactly one with a `=>` leaf of its own (not inside a bracket), a name + leaf (the parameter), `=>`, the def's name and its `(` group, with the kids + ending there or going on with a comma, and no name leaf in the group + spelling the parameter or the parameter then a dot. A body that does more + than the call (`_u => Some{go(t)}`), a continuation that reads its + parameter (`a => go(f, a)`), or a lambda that is no call's argument + (`x = _u => go(t)`) is left alone; `_ => loop(n)` is not, since the rule reads the shape and not the type. - `fromrev` — `String.from_list(List.reverse(..))`: among the significant tokens, `String.from_list`, `(`, `List.reverse` and `(` right after one diff --git a/src/rules/LAWS.bend b/src/rules/LAWS.bend index 8716438..f6f570c 100644 --- a/src/rules/LAWS.bend +++ b/src/rules/LAWS.bend @@ -2388,13 +2388,16 @@ law unit_counts: {List.length(&2, F.Finding, UnitRule.check(Src.Src{path, text, toks, tree, bound, items})) == unit.defs(Calls.defs(tree), path) : Nat} -# thunk (BOLT-RULE-U015). A thunk of a self-call is read off a chain, at -# any depth: its first node a leaf of a name kind (the parameter), then a -# leaf whose text is `=>`, then a leaf whose text is the def's name, then a -# group opened by `(`, and after the group the chain's end or a comma. The -# group must not read the parameter: no name leaf under it, at any depth, -# spells the parameter, or the parameter then a dot. Each def of the file -# that is not exempt counts the thunks of its body. +# thunk (BOLT-RULE-U015). A thunk of a self-call is read off the kids of a +# call given one lambda: a group opened by `(` whose kids, split at their +# comma leaves, hold exactly one argument with a leaf whose text is `=>` +# among its own nodes. In those kids, its first node a leaf of a name kind +# (the parameter), then a leaf whose text is `=>`, then a leaf whose text is +# the def's name, then a group opened by `(`, and after the group the kids' +# end or a comma. The group must not read the parameter: no name leaf under +# it, at any depth, spells the parameter, or the parameter then a dot. Such +# calls are found at any depth. Each def of the file that is not exempt +# counts the thunks of its body. # does a name leaf under the node spell the parameter, or it then a dot? def thunk.reads(nn: Tree.Node, +pp: String) -> Bool: @@ -2452,27 +2455,46 @@ def thunk.at(nn: Tree.Node, +name: String) -> Bool: case other: False{} -# how many thunks of a self-call of the name the node holds, at any depth -def thunk.count(nn: Tree.Node, +name: String) -> Nat: +# the arguments of the chain, from here on, that hold a `=>` leaf among their +# own nodes (a comma leaf ends one); seen: the one under way does +def thunk.args(nn: Tree.Node, +seen: Bool) -> Nat: + match nn: + case Tree.NCons{Tree.Leaf{Lex.Tok{+k, t, l, c}}, rest}: + Nat.add(Bool.pick(Nat, Bool.and(Lex.is_comma(k), seen), 1n, 0n), + thunk.args(rest, Bool.and(Bool.not(Lex.is_comma(k)), Bool.or(seen, String.eq(t, "=>"))))) + case Tree.NCons{h, rest}: + thunk.args(rest, seen) + case other: + Bool.pick(Nat, seen, 1n, 0n) + +# is a group opened by oo over the kids a call given exactly one lambda? +def thunk.lone(+oo: String, +kids: Tree.Node) -> Bool: + Bool.and(String.eq(oo, "("), Nat.is_eq(thunk.args(kids, False{}), 1n)) + +# how many thunks of a self-call of the name the node holds, at any depth, +# each in the kids of a call given one lambda; lone: the node is the rest of +# such kids +def thunk.count(nn: Tree.Node, +lone: Bool, +name: String) -> Nat: match nn: case Tree.NCons{+h, +rest}: - Nat.add(Bool.pick(Nat, thunk.at(Tree.NCons{h, rest}, name), 1n, 0n), - Nat.add(thunk.count(h, name), thunk.count(rest, name))) - case Tree.Group{o, kids, cl}: - thunk.count(kids, name) + Nat.add(Bool.pick(Nat, Bool.and(lone, thunk.at(Tree.NCons{h, rest}, name)), 1n, 0n), + Nat.add(thunk.count(h, False{}, name), thunk.count(rest, lone, name))) + case Tree.Group{Lex.Tok{k, +o, l, c}, +kids, cl}: + thunk.count(kids, thunk.lone(o, kids), name) case Tree.Stmt{sk, kids, body}: - Nat.add(thunk.count(kids, name), thunk.count(body, name)) + Nat.add(thunk.count(kids, False{}, name), thunk.count(body, False{}, name)) case other: 0n # LAW: over any node, thunk reports one finding for each thunk of a -# self-call, and none for anything else +# self-call passed as the one lambda of a call, and none for anything else # BOLT-RULE-U015 law thunk_walk_counts: for nn: Tree.Node + for +lone: Bool for +name: String for +path: String - {List.length(&2, F.Finding, Thunk.walk(nn, name, path)) == thunk.count(nn, name) : Nat} + {List.length(&2, F.Finding, Thunk.walk(nn, lone, name, path)) == thunk.count(nn, lone, name) : Nat} # the thunks of a self-call in each def of the list that is not exempt def thunk.defs(ds: List<&2, Calls.Def>, +path: String) -> Nat: @@ -2480,7 +2502,7 @@ def thunk.defs(ds: List<&2, Calls.Def>, +path: String) -> Nat: case Nil{}: 0n case Con{Calls.Def{+name, +sig, +body}, rest}: - Nat.add(Bool.pick(Nat, Calls.exempt(path, sig), 0n, thunk.count(body, name)), thunk.defs(rest, path)) + Nat.add(Bool.pick(Nat, Calls.exempt(path, sig), 0n, thunk.count(body, False{}, name)), thunk.defs(rest, path)) # LAW: thunk reports exactly those, def by def, over the defs of the tree # BOLT-RULE-U015 diff --git a/src/rules/PROOF.bend b/src/rules/PROOF.bend index d149e0f..801e497 100644 --- a/src/rules/PROOF.bend +++ b/src/rules/PROOF.bend @@ -1721,7 +1721,7 @@ def ex.thunk(ds, path, n, e): ex.push( Calls.exempt(path, sig), ex.calls(path, sig, e), - _u => Thunk.walk(body, name, path), n, + _u => Thunk.walk(body, False{}, name, path), n, v => Thunk.check.go(rest, path, v), ex.thunk(rest, path, 1n+n, e)) def Laws.thunk_exempt(path, _text, _toks, tree, _bound, _items, e): @@ -10451,10 +10451,11 @@ def unit.go(ds, path, acc): def Laws.unit_counts(path, _text, _toks, tree, _bound, _items): unit.go(Calls.defs(tree), path, Nil{}) -# thunk (BOLT-RULE-U015). The rule's reads and ends agree with the law's by -# induction and by one split; each site helper agrees with the law's step of -# the same place, so a site gives one finding exactly when the law's chain -# opens a thunk; the walk and the def walk then add up as unit's do. +# thunk (BOLT-RULE-U015). The rule's reads, ends and lams agree with the +# law's by induction and by one split; each site helper agrees with the law's +# step of the same place, so a site gives one finding exactly when the law's +# chain opens a thunk, and a gated site exactly when the kids are a call's +# with one lambda; the walk and the def walk then add up as unit's do. # the rule's reads is the law's law thunk.reads: @@ -10630,19 +10631,75 @@ def thunk.site(hh, rest, name, path): case Tree.NNil{}: {==} case Tree.NCons{x, y}: {==} -def Laws.thunk_walk_counts(nn, name, path): +# the rule's count of lambda arguments is the law's +law thunk.lams: + for nn: Tree.Node + for +seen: Bool + {Thunk.lams(nn, seen) == Laws.thunk.args(nn, seen) : Nat} + +def thunk.lams(nn, seen): + match nn: + case Tree.NCons{h, +rest}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{+k, +t, l, c}: + +s2 = Bool.and(Bool.not(Lex.is_comma(k)), Bool.or(seen, String.eq(t, "=>"))) + +p = Bool.pick(Nat, Bool.and(Lex.is_comma(k), seen), 1n, 0n) + Equal.cong(Nat, Nat, x => Nat.add(p, x), Thunk.lams(rest, s2), Laws.thunk.args(rest, s2), + thunk.lams(rest, s2)) + case Tree.Group{x, y, z}: thunk.lams(rest, seen) + case Tree.Stmt{x, y, z}: thunk.lams(rest, seen) + case Tree.NNil{}: thunk.lams(rest, seen) + case Tree.NCons{x, y}: thunk.lams(rest, seen) + case Tree.Leaf{x}: {==} + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{x, y, z}: {==} + case Tree.NNil{}: {==} + +# the rule's call given one lambda is the law's +law thunk.only: + for +o: String + for +kids: Tree.Node + {Thunk.only(o, kids) == Laws.thunk.lone(o, kids) : Bool} + +def thunk.only(o, kids): + Equal.cong(Nat, Bool, x => Bool.and(String.eq(o, "("), Nat.is_eq(x, 1n)), Thunk.lams(kids, False{}), + Laws.thunk.args(kids, False{}), thunk.lams(kids, False{})) + +# a site gated by lone: the rule's finding is the law's count +law thunk.gate: + for +lone: Bool + for hh: Tree.Node + for rest: Tree.Node + for +name: String + for +path: String + {List.length(&2, F.Finding, Bool.pick(List<&2, F.Finding>, lone, Thunk.site(hh, rest, name, path), [])) + == Bool.pick(Nat, Bool.and(lone, Laws.thunk.at(Tree.NCons{hh, rest}, name)), 1n, 0n) : Nat} + +def thunk.gate(lone, hh, rest, name, path): + match lone: + case True{}: thunk.site(hh, rest, name, path) + case False{}: {==} + +def Laws.thunk_walk_counts(nn, lone, name, path): match nn: case Tree.NCons{+h, +rest}: - table.three(Thunk.site(h, rest, name, path), Thunk.walk(h, name, path), Thunk.walk(rest, name, path), - Bool.pick(Nat, Laws.thunk.at(Tree.NCons{h, rest}, name), 1n, 0n), Laws.thunk.count(h, name), - Laws.thunk.count(rest, name), thunk.site(h, rest, name, path), Laws.thunk_walk_counts(h, name, path), - Laws.thunk_walk_counts(rest, name, path)) - case Tree.Group{o, +kids, cl}: - Laws.thunk_walk_counts(kids, name, path) + table.three(Bool.pick(List<&2, F.Finding>, lone, Thunk.site(h, rest, name, path), []), + Thunk.walk(h, False{}, name, path), Thunk.walk(rest, lone, name, path), + Bool.pick(Nat, Bool.and(lone, Laws.thunk.at(Tree.NCons{h, rest}, name)), 1n, 0n), + Laws.thunk.count(h, False{}, name), Laws.thunk.count(rest, lone, name), thunk.gate(lone, h, rest, name, path), + Laws.thunk_walk_counts(h, False{}, name, path), Laws.thunk_walk_counts(rest, lone, name, path)) + case Tree.Group{open, +kids, cl}: + match open: + case Lex.Tok{k, +o, l, c}: + %thunk.only(o, kids) : {List.length(&2, F.Finding, Thunk.walk(kids, Thunk.only(o, kids), name, path)) + == Laws.thunk.count(kids, _, name) : Nat} + Laws.thunk_walk_counts(kids, Thunk.only(o, kids), name, path) case Tree.Stmt{sk, +kids, +body}: - table.two(Thunk.walk(kids, name, path), Thunk.walk(body, name, path), Laws.thunk.count(kids, name), - Laws.thunk.count(body, name), Laws.thunk_walk_counts(kids, name, path), Laws.thunk_walk_counts(body, name, - path)) + table.two(Thunk.walk(kids, False{}, name, path), Thunk.walk(body, False{}, name, path), + Laws.thunk.count(kids, False{}, name), Laws.thunk.count(body, False{}, name), + Laws.thunk_walk_counts(kids, False{}, name, path), Laws.thunk_walk_counts(body, False{}, name, path)) case Tree.Leaf{tok}: {==} case Tree.NNil{}: @@ -10654,15 +10711,15 @@ law thunk.stop: for +body: Tree.Node for +name: String for +path: String - {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, b, [], _u => Thunk.walk(body, name, path))) - == Bool.pick(Nat, b, 0n, Laws.thunk.count(body, name)) : Nat} + {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, b, [], _u => Thunk.walk(body, False{}, name, path))) + == Bool.pick(Nat, b, 0n, Laws.thunk.count(body, False{}, name)) : Nat} def thunk.stop(b, body, name, path): match b: case True{}: {==} case False{}: - Laws.thunk_walk_counts(body, name, path) + Laws.thunk_walk_counts(body, False{}, name, path) # thunk's def walk: the findings gathered so far, then each def's law thunk.go: @@ -10679,8 +10736,8 @@ def thunk.go(ds, path, acc): match d: case Calls.Def{+name, +sig, +body}: +b = Calls.exempt(path, sig) - +x = Lazy.stop(List<&2, F.Finding>, b, [], _u => Thunk.walk(body, name, path)) - +cb = Bool.pick(Nat, b, 0n, Laws.thunk.count(body, name)) + +x = Lazy.stop(List<&2, F.Finding>, b, [], _u => Thunk.walk(body, False{}, name, path)) + +cb = Bool.pick(Nat, b, 0n, Laws.thunk.count(body, False{}, name)) Equal.trans(Nat, List.length(&2, F.Finding, Thunk.check.go(rest, path, x <> acc)), pick.sum(acc, Nat.add(List.length(&2, F.Finding, x), Laws.thunk.defs(rest, path))), pick.sum(acc, Nat.add(cb, Laws.thunk.defs(rest, path))), @@ -24607,40 +24664,84 @@ def inert.thunk.site(hh, rest, name, path, en, e): case Tree.NNil{}: {==} case Tree.NCons{x, y}: {==} +# a chain read that way counts the lambda arguments it did: kinds are kept, +# and `=>` is never cut +law inert.thunk.lams: + for nn: Tree.Node + for +seen: Bool + for +e: {Laws.inert.ok(nn) == True{} : Bool} + {Thunk.lams(Laws.inert.node(nn), seen) == Thunk.lams(nn, seen) : Nat} + +def inert.thunk.lams(nn, seen, e): + match nn: + case Tree.NCons{h, +rest}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{+k, +t, l, c}: + +ef = inert.and_l(Laws.inert.fits.go(Laws.inert.blanks(k), t), Laws.inert.ok(rest), e) + +er = inert.and_r(Laws.inert.fits.go(Laws.inert.blanks(k), t), Laws.inert.ok(rest), e) + +p = Bool.pick(Nat, Bool.and(Lex.is_comma(k), seen), 1n, 0n) + +s1 = Bool.and(Bool.not(Lex.is_comma(k)), + Bool.or(seen, String.eq(Laws.inert.keep(Laws.inert.blanks(k), t), "=>"))) + %inert.eq_keep(Laws.inert.blanks(k), t, "=>", ef, {==}) : {Nat.add(p, + Thunk.lams(Laws.inert.node(rest), s1)) == Nat.add(p, Thunk.lams(rest, + Bool.and(Bool.not(Lex.is_comma(k)), Bool.or(seen, _)))) : Nat} + Equal.cong(Nat, Nat, x => Nat.add(p, x), Thunk.lams(Laws.inert.node(rest), s1), Thunk.lams(rest, s1), + inert.thunk.lams(rest, s1, er)) + case Tree.Group{x, y, z}: inert.thunk.lams(rest, seen, inert.and_r(Laws.inert.ok(h), Laws.inert.ok(rest), e)) + case Tree.Stmt{x, y, z}: inert.thunk.lams(rest, seen, inert.and_r(Laws.inert.ok(h), Laws.inert.ok(rest), e)) + case Tree.NNil{}: inert.thunk.lams(rest, seen, inert.and_r(Laws.inert.ok(h), Laws.inert.ok(rest), e)) + case Tree.NCons{x, y}: inert.thunk.lams(rest, seen, inert.and_r(Laws.inert.ok(h), Laws.inert.ok(rest), e)) + case Tree.Leaf{x}: {==} + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{x, y, z}: {==} + case Tree.NNil{}: {==} + # thunk's walk over a node read that way reports what it reports over the node law inert.thunk.walk: for nn: Tree.Node + for +lone: Bool for +name: String for +path: String for +en: {Laws.inert.marked(name) == False{} : Bool} for +e: {Laws.inert.ok(nn) == True{} : Bool} - {Thunk.walk(Laws.inert.node(nn), name, path) == Thunk.walk(nn, name, path) : List<&2, F.Finding>} + {Thunk.walk(Laws.inert.node(nn), lone, name, path) == Thunk.walk(nn, lone, name, path) : List<&2, F.Finding>} -def inert.thunk.walk(nn, name, path, en, e): +def inert.thunk.walk(nn, lone, name, path, en, e): match nn: case Tree.NCons{+h, +rest}: +eh = inert.and_l(Laws.inert.ok(h), Laws.inert.ok(rest), e) +er = inert.and_r(Laws.inert.ok(h), Laws.inert.ok(rest), e) +s1 = Thunk.site(Laws.inert.node(h), Laws.inert.node(rest), name, path) - +w1 = Thunk.walk(Laws.inert.node(h), name, path) - +w2 = Thunk.walk(Laws.inert.node(rest), name, path) - %inert.thunk.site(h, rest, name, path, en, er) : {List.concat(&2, F.Finding, [s1, w1, w2]) - == List.concat(&2, F.Finding, [_, Thunk.walk(h, name, path), Thunk.walk(rest, name, path)]) - : List<&2, F.Finding>} - %inert.thunk.walk(h, name, path, en, eh) : {List.concat(&2, F.Finding, [s1, w1, w2]) - == List.concat(&2, F.Finding, [s1, _, Thunk.walk(rest, name, path)]) : List<&2, F.Finding>} - %inert.thunk.walk(rest, name, path, en, er) : {List.concat(&2, F.Finding, [s1, w1, w2]) - == List.concat(&2, F.Finding, [s1, w1, _]) : List<&2, F.Finding>} - {==} - case Tree.Group{o, +kids, cl}: - inert.thunk.walk(kids, name, path, en, e) + +w1 = Thunk.walk(Laws.inert.node(h), False{}, name, path) + +w2 = Thunk.walk(Laws.inert.node(rest), lone, name, path) + %inert.thunk.site(h, rest, name, path, en, er) : {List.concat(&2, F.Finding, + [Bool.pick(List<&2, F.Finding>, lone, s1, []), w1, w2]) + == List.concat(&2, F.Finding, [Bool.pick(List<&2, F.Finding>, lone, _, []), Thunk.walk(h, False{}, name, path), + Thunk.walk(rest, lone, name, path)]) : List<&2, F.Finding>} + %inert.thunk.walk(h, False{}, name, path, en, eh) : {List.concat(&2, F.Finding, + [Bool.pick(List<&2, F.Finding>, lone, s1, []), w1, w2]) + == List.concat(&2, F.Finding, [Bool.pick(List<&2, F.Finding>, lone, s1, []), _, + Thunk.walk(rest, lone, name, path)]) : List<&2, F.Finding>} + %inert.thunk.walk(rest, lone, name, path, en, er) : {List.concat(&2, F.Finding, + [Bool.pick(List<&2, F.Finding>, lone, s1, []), w1, w2]) + == List.concat(&2, F.Finding, [Bool.pick(List<&2, F.Finding>, lone, s1, []), w1, _]) : List<&2, F.Finding>} + {==} + case Tree.Group{open, +kids, cl}: + match open: + case Lex.Tok{k, +o, l, c}: + +l1 = Thunk.only(o, Laws.inert.node(kids)) + %inert.thunk.lams(kids, False{}, e) : {Thunk.walk(Laws.inert.node(kids), l1, name, path) + == Thunk.walk(kids, Bool.and(String.eq(o, "("), Nat.is_eq(_, 1n)), name, path) : List<&2, F.Finding>} + inert.thunk.walk(kids, l1, name, path, en, e) case Tree.Stmt{sk, +kids, +body}: - +w1 = Thunk.walk(Laws.inert.node(kids), name, path) - +w2 = Thunk.walk(Laws.inert.node(body), name, path) - %inert.thunk.walk(kids, name, path, en, inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), e)) : - {List.concat(&2, F.Finding, [w1, w2]) == List.concat(&2, F.Finding, [_, Thunk.walk(body, name, path)]) + +w1 = Thunk.walk(Laws.inert.node(kids), False{}, name, path) + +w2 = Thunk.walk(Laws.inert.node(body), False{}, name, path) + %inert.thunk.walk(kids, False{}, name, path, en, inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), e)) : + {List.concat(&2, F.Finding, [w1, w2]) == List.concat(&2, F.Finding, [_, Thunk.walk(body, False{}, name, path)]) : List<&2, F.Finding>} - %inert.thunk.walk(body, name, path, en, inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), e)) : + %inert.thunk.walk(body, False{}, name, path, en, inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), e)) : {List.concat(&2, F.Finding, [w1, w2]) == List.concat(&2, F.Finding, [w1, _]) : List<&2, F.Finding>} {==} case Tree.Leaf{tok}: @@ -24660,10 +24761,11 @@ def inert.thunk.go(ds, path, acc, e): match ds: case Nil{}: {==} case Con{Calls.Def{+name, +sig, +body}, +rest}: - +lst = inert.pick.stop(Calls.exempt(path, Laws.inert.node(sig)), Thunk.walk(Laws.inert.node(body), name, path)) + +lst = inert.pick.stop(Calls.exempt(path, Laws.inert.node(sig)), Thunk.walk(Laws.inert.node(body), False{}, name, + path)) %inert.exempt(path, sig) : {Thunk.check.go(inert.defs(rest), path, lst <> acc) == Thunk.check.go(rest, path, - inert.pick.stop(_, Thunk.walk(body, name, path)) <> acc) : List<&2, F.Finding>} - %inert.thunk.walk(body, name, path, inert.dok.head(name, sig, body, rest, e), + inert.pick.stop(_, Thunk.walk(body, False{}, name, path)) <> acc) : List<&2, F.Finding>} + %inert.thunk.walk(body, False{}, name, path, inert.dok.head(name, sig, body, rest, e), inert.dok.body(name, sig, body, rest, e)) : {Thunk.check.go(inert.defs(rest), path, lst <> acc) == Thunk.check.go(rest, path, inert.pick.stop(Calls.exempt(path, Laws.inert.node(sig)), _) <> acc) : List<&2, F.Finding>} diff --git a/src/rules/suspicious/thunk.bend b/src/rules/suspicious/thunk.bend index 7adc10e..7dfdb9e 100644 --- a/src/rules/suspicious/thunk.bend +++ b/src/rules/suspicious/thunk.bend @@ -1,24 +1,32 @@ # rule thunk: a lambda whose body is exactly a self-call of its def, and -# whose parameter the call does not read: a `Unit -> T` thunk such as +# whose parameter the call does not read, when it is the one lambda among the +# arguments of the call it is passed to: a `Unit -> T` thunk such as # `Lazy.or_else(hit, _u => go(rest, k))`. The thunk is a closure allocated on # every step, and the call inside it is not a tail call of the def, so the # search leaves the loop each time round (bend 2.0.34, 500 misses over 100k # cells: JS 2.40 s against 0.28 s, native 1.18 s against 0.76 s). Carry the # test as a Bool into the next call instead, `go(rest, k, test(h))`, and match # on it first: the step is then a tail call and compiles to a loop. `Lazy.*` -# stays right for guarding work that does not recurse. -# Exactly: in a chain (the kids of a group or a statement, or a statement's -# body, at any depth) four nodes in a row, a leaf whose kind is a name (the -# parameter: `_`, `_u`, `u`), a leaf whose text is `=>`, a leaf whose text is -# the def's name, and a `(` group; the chain ends right after the group or -# goes on with a comma; and no name leaf in the group, at any depth, has the -# parameter's text or starts with it and a dot (`u.x`). One finding per such -# lambda, on the def's name. A body that does more than the call -# (`_u => go(t) ++ x`, `_u => Some{go(t)}`), a call of another def, or a -# lambda whose parameter the call reads (an IO continuation `a => go(f, a)`) -# is left alone; one that ignores its value (`_ => loop(n)`) is not, since -# the rule reads the shape and not the type. Laws and proofs never run: a -# law file, a proof file and a def that is a proof are exempt. +# stays right for guarding work that does not recurse. A dispatch, a call +# given two or more lambdas (`Lazy.either(T, c, _u => go(a), _v => go(b))`), +# is left alone: one Bool carried into the next call does not replace it. +# Exactly: in the kids of a group opened by `(` (its arguments: the kids split +# at their comma leaves), exactly one argument holding, among its own nodes +# and not inside a group, a leaf whose text is `=>`, four nodes in a row of +# those kids, a leaf whose kind is a name (the parameter: `_`, `_u`, `u`), a +# leaf whose text is `=>`, a leaf whose text is the def's name, and a `(` +# group; the kids end right after the group or go on with a comma; and no +# name leaf in the group, at any depth, has the parameter's text or starts +# with it and a dot (`u.x`). Groups are found at any depth, under statements +# and inside other groups, and a lambda inside another lambda's body is +# judged by the group it is passed to. One finding per such lambda, on the +# def's name. A body that does more than the call (`_u => go(t) ++ x`, +# `_u => Some{go(t)}`), a call of another def, a lambda whose parameter the +# call reads (an IO continuation `a => go(f, a)`), and a lambda that is not +# an argument of a call (`x = _u => go(t)`) are left alone; one that ignores +# its value (`_ => loop(n)`) is not, since the rule reads the shape and not +# the type. Laws and proofs never run: a law file, a proof file and a def +# that is a proof are exempt. import Base import ../../src.bend as Src import ../../finding.bend as F @@ -119,15 +127,35 @@ def site(hh: Tree.Node, rest: Tree.Node, +name: String, +path: String) -> List<& case _other: [] -# every thunk of a self-call under the node, at any depth -def walk(nn: Tree.Node, +name: String, +path: String) -> List<&2, F.Finding>: +# how many arguments of a group's kids, from here on, hold a `=>` leaf among +# their own nodes; seen: the argument under way does +def lams(nn: Tree.Node, +seen: Bool) -> Nat: + match nn: + case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, _l, _c}}, rest}: + +comma = Lex.is_comma(k) + Nat.add(Bool.pick(Nat, Bool.and(comma, seen), 1n, 0n), + lams(rest, Bool.and(Bool.not(comma), Bool.or(seen, String.eq(t, "=>"))))) + case Tree.NCons{_h, rest}: + lams(rest, seen) + case _other: + Bool.pick(Nat, seen, 1n, 0n) + +# is a group with this open and these kids a call given exactly one lambda? +def only(+oo: String, +kids: Tree.Node) -> Bool: + Bool.and(String.eq(oo, "("), Nat.is_eq(lams(kids, False{}), 1n)) + +# every thunk of a self-call under the node, at any depth; lone: the node is +# the rest of the kids of a call given exactly one lambda +def walk(nn: Tree.Node, +lone: Bool, +name: String, +path: String) -> List<&2, F.Finding>: match nn: case Tree.NCons{+h, +rest}: - List.concat(&2, F.Finding, [site(h, rest, name, path), walk(h, name, path), walk(rest, name, path)]) - case Tree.Group{_o, kids, _cl}: - walk(kids, name, path) + +here = site(h, rest, name, path) + List.concat(&2, F.Finding, [Bool.pick(List<&2, F.Finding>, lone, here, []), + walk(h, False{}, name, path), walk(rest, lone, name, path)]) + case Tree.Group{Lex.Tok{_k, +o, _l, _c}, +kids, _cl}: + walk(kids, only(o, kids), name, path) case Tree.Stmt{_k, kids, body}: - List.concat(&2, F.Finding, [walk(kids, name, path), walk(body, name, path)]) + List.concat(&2, F.Finding, [walk(kids, False{}, name, path), walk(body, False{}, name, path)]) case _other: Nil{} @@ -137,7 +165,7 @@ def check.go(ds: List<&2, Calls.Def>, +path: String, acc: List<&2, List<&2, F.Fi List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc)) case Con{Calls.Def{+name, +sig, body}, rest}: check.go(rest, path, - Lazy.stop(List<&2, F.Finding>, Calls.exempt(path, sig), [], _u => walk(body, name, path)) <> acc) + Lazy.stop(List<&2, F.Finding>, Calls.exempt(path, sig), [], _u => walk(body, False{}, name, path)) <> acc) # the rule def check(ss: Src.Src) -> List<&2, F.Finding>: From 6c6379d8cb0444006ebd0c74d48f31234d2a246d Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 13:54:30 +0000 Subject: [PATCH 3/6] fix(rules): fuel (U006) skips effect loops, index (U007) skips the get's own self-call Behavior change to two released rules, both with 0% sampled precision on real code. fuel (U006, BOLT-RULE-U006): a call to a def that returns an effect is no longer reported. A def returns an effect when its header holds a top-level `->` token with the capitalized name token `IO` right after it, or, when the `->` is the header's last token, first on the line under it (`->` then `IO(Unit):`). An effect loop's fuel bounds reads, frames or retries the outside world sets, not the size of an input. The law fuel_slots is restated (fuel.slots keeps only the defs that return no effect); fuel_walk_counts and fuel_counts follow it. bolt's own two `# noqa: U006` (src/lsp/files/disk.bend, src/lsp/transport/stdio.bend) silenced nothing now and are removed. index (U007, BOLT-RULE-U007): a List.get / String.get call whose name is the def's own (the step of a def named List.get or String.get, as Base's are) is no longer reported. index_counts is restated (index.count and index.site take the def's name as self). Counts on the sampled corpus (old -> new U006+U007): bend 6 -> 1 (the one left is Wav.walk, a pure def, still reported), bolt tree 0 -> 0 with its noqa comments gone, every other ecosystem repo 0 -> 0. bolt on this tree: 0 errors, 73 warnings, as before. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B --- SPEC.md | 4 +- src/README.md | 9 +- src/lsp/files/disk.bend | 2 +- src/lsp/transport/stdio.bend | 2 +- src/rules/LAWS.bend | 100 +++++-- src/rules/PROOF.bend | 494 +++++++++++++++++++++++++------- src/rules/suspicious/fuel.bend | 54 +++- src/rules/suspicious/index.bend | 27 +- 8 files changed, 542 insertions(+), 150 deletions(-) diff --git a/SPEC.md b/SPEC.md index 984926e..59aaf34 100644 --- a/SPEC.md +++ b/SPEC.md @@ -38,8 +38,8 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-RULE-U002 | `strict` reports exactly a self-call inside `Bool.and` or `Bool.or`, or in a comma-separated stretch holding `&&` or `\|\|` (matched by that exact text), where a `=>` ends the stretch on its left and a lambda body counts only by its own `&&` or `\|\|`. | Proved | proved | src/rules/LAWS.bend strict_walk_counts; src/rules/LAWS.bend strict_counts | | BOLT-RULE-U003 | `eager` reports exactly a looping def of the file called in a `Bool.pick` branch. | Proved | proved | src/rules/LAWS.bend eager_counts; src/rules/LAWS.bend eager_lambda; src/rules/LAWS.bend eager_comma; src/rules/LAWS.bend eager_plain | | BOLT-RULE-U004 | `concat` reports exactly a self-call argument that appends onto the parameter in its own position: the append written as the argument, inside any number of parentheses, or a lone name whose nearest `q = ..` or `+q = ..` let before the call, in its statement chain or an enclosing one, has such an append as its right side. | Proved | proved | src/rules/LAWS.bend concat_counts; src/rules/LAWS.bend concat_paren; src/rules/LAWS.bend concat_in_place; src/rules/LAWS.bend concat_via; src/rules/LAWS.bend concat_nearest; src/rules/LAWS.bend concat_other; src/rules/LAWS.bend concat_scope; src/rules/LAWS.bend concat_bound; src/rules/LAWS.bend concat_bound_plus | -| BOLT-RULE-U006 | `fuel` reports exactly an argument that is one Nat literal token alone, or the dotted name `U32.to_nat` then a `(` group holding one U32 literal token (digits) alone, in a call (not a self-call) to a def of the file, at a parameter named `fuel`, `gas`, `steps` or `budget` or starting with `fuel`. | Proved | proved | src/rules/LAWS.bend fuel_slots; src/rules/LAWS.bend fuel_walk_counts; src/rules/LAWS.bend fuel_counts | -| BOLT-RULE-U007 | `index` reports exactly a `List.get` or `String.get` at a non-literal index anywhere in a recursive def, except a `List.get` on a fixed table that `table` reports. | Proved | proved | src/rules/LAWS.bend index_counts | +| BOLT-RULE-U006 | `fuel` reports exactly an argument that is one Nat literal token alone, or the dotted name `U32.to_nat` then a `(` group holding one U32 literal token (digits) alone, in a call (not a self-call) to a def of the file that returns no effect (its header holds no top-level `->` token followed right away by the capitalized name token `IO`, nor ends in a `->` whose first statement under the def starts with that token), at a parameter named `fuel`, `gas`, `steps` or `budget` or starting with `fuel`. | Proved | proved | src/rules/LAWS.bend fuel_slots; src/rules/LAWS.bend fuel_walk_counts; src/rules/LAWS.bend fuel_counts | +| BOLT-RULE-U007 | `index` reports exactly a `List.get` or `String.get` at a non-literal index anywhere in a recursive def, except a `List.get` on a fixed table that `table` reports and a get that is the def's own self-call (the def is named `List.get` or `String.get`). | Proved | proved | src/rules/LAWS.bend index_counts | | BOLT-RULE-U008 | `table` reports exactly, in a def that calls itself, a `List.get` or `List.set` call whose index is not one number token and whose list is a fixed table: a list literal, a number-sized array, or `List.replicate` / `Array.new` / `List.range` with a number count, written inline, as a table def of the file, or held by the let of that name in scope. | Proved | proved | src/rules/LAWS.bend table_walk_counts; src/rules/LAWS.bend table_counts | | BOLT-RULE-U009 | `hoist` reports exactly, in a def that calls itself and is not a law or a proof, outside a lambda's body (the rest of a chain after `=>`), a case pattern, and a case arm that does not call the def: a `List.get`, `List.set`, `String.get`, `Array.get` or `Array.set` call whose collection is a table, and a let of one plain name to a table that a later get, set or `name[..]` in its block or the statements after it indexes; where a table is a list literal with eight or more top-level commas, an array literal of more than eight slots (`[v : T*n]` with n not a literal 0 to 8, `[v : T^d]` with d not a literal 0 to 3), a `List.replicate`, `Array.new` or `List.range` whose count is not a literal 0 to 8, a `List.map` or `Array.map`, or a call to a def of the file, other than an undotted self-call, whose body is a single statement that is a list literal, or an array literal, `List.replicate`, `Array.new` or `List.range` sized by a number literal, of more than eight cells by those measures; and every value name in the table (a callee or a `~` template aside) is a parameter that each self-call passes back unchanged in its own position. | Proved | proved | src/rules/LAWS.bend hoist_counts | | BOLT-RULE-U010 | `ring` reports exactly, in a def that calls itself, a self-call argument that appends onto a drop by a number literal, or a tail, of the parameter in its own position, when no `match` of the def has that parameter as a scrutinee. | Proved | proved | src/rules/LAWS.bend ring_walk_counts; src/rules/LAWS.bend ring_counts | diff --git a/src/README.md b/src/README.md index bc3c3f0..0fe59a4 100644 --- a/src/README.md +++ b/src/README.md @@ -245,7 +245,8 @@ parameters and no `->`), which is how Bend fills the law named `f`. (one sort phase went 39 s -> 0.9 s). A get anywhere in the def is reported, one in a base arm that runs once included. A literal index of any size is exempt. A `List.get` on a fixed table is `table`'s; a - `String.get` always stays here. + `String.get` always stays here. A get that is the def's own self-call (the + step of a def named `List.get` or `String.get`, as Base's are) is exempt. - `table` — `List.get` or `List.set` at a computed index inside a def that calls itself, when the list is a fixed table (a literal, a sized array, or `List.replicate` / `Array.new` / `List.range` with a constant count), @@ -397,7 +398,11 @@ parameters and no `->`), which is how Bend fills the law named `f`. overflows the checker's stack (bend 2.0.33/2.0.34). A literal of any size counts, `3n` included. Only an argument that is the literal alone, or `U32.to_nat(` it `)`, counts, so a let-bound literal and `(7n)` are not - seen. A def's own calls are exempt. + seen. A def's own calls are exempt, and so is a def that returns an + effect: a header with `->` then the name `IO` (`-> IO(Unit):`), or one + that ends in `->` with `IO(..):` on the next line. Its fuel bounds reads, + frames or retries the outside world sets (a drain of 256 datagrams a + tick, a read of 100000 chunks), not the size of an input it was given. - `tail` (pedantic) — a self-call that is not a tail call, in a def whose first live parameter is a `List` or a `String`. On a long one the JS lane overflows its stack (a 48 KB header crashed a server; ~4,900 entries and diff --git a/src/lsp/files/disk.bend b/src/lsp/files/disk.bend index c39e8b7..11cfb2a 100644 --- a/src/lsp/files/disk.bend +++ b/src/lsp/files/disk.bend @@ -57,7 +57,7 @@ def read.opened(rr: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>) case Fail{e}: IO.pure(Maybe<&2, String>, None{}) case Done{file}: - slurp(U32.to_nat(100000), file, []) # noqa: U006 100000 reads of 64 KiB, past any source + slurp(U32.to_nat(100000), file, []) # a file's text, or None when it cannot be opened def read(path: String) -> IO(Maybe<&2, String>): # noqa: L001 disk effect diff --git a/src/lsp/transport/stdio.bend b/src/lsp/transport/stdio.bend index c154cab..840163c 100644 --- a/src/lsp/transport/stdio.bend +++ b/src/lsp/transport/stdio.bend @@ -71,7 +71,7 @@ def recv.loop(fuel: Nat, h2: Stdio) -> IO(Stdio & Maybe<&2, String>): # the fuel bounds the reads one message may take def recv(h2: Stdio) -> IO(Stdio & Maybe<&2, String>): # noqa: L001 transport effect - recv.loop(U32.to_nat(1000000), h2) # noqa: U006 a million reads for one message + recv.loop(U32.to_nat(1000000), h2) def send.done(ww: File & Result<&1, &1, U32 & String, Unit>, inp: File, buf: List<&2, U32>) -> IO(Stdio): (out, r) = ww diff --git a/src/rules/LAWS.bend b/src/rules/LAWS.bend index f6f570c..a43a396 100644 --- a/src/rules/LAWS.bend +++ b/src/rules/LAWS.bend @@ -1589,6 +1589,8 @@ law unused_counts: # (argument 1) is not one number token is a finding. So is a `List.get(..)` # whose index (argument 3) is not one number token, unless `table` reports # that same call: its fixed-table test, over the tables it finds in that def. +# A call whose name is the def's own (a def named `List.get` or `String.get` +# stepping to itself) is neither. # is the chain exactly one number token? def index.lit(nn: Tree.Node) -> Bool: @@ -1608,27 +1610,39 @@ def index.fires(list: Bool, +ob: Bool, +sget: Bool, +as: List<&2, Tree.Node>, ta case False{}: Bool.and(ob, Bool.and(sget, Bool.not(index.lit(Calls.arg(as, 1n))))) -# one when the name token tt at (ll, cc), then the rest, is a call index reports -def index.site(+tt: String, +ll: U32, +cc: U32, rest: Tree.Node, +path: String, +fixed: List<&2, String>) -> Nat: +# one when the name token tt at (ll, cc), then the rest, is a call index +# reports in the def named self +def index.site( + +tt: String, + +ll: U32, + +cc: U32, + rest: Tree.Node, + +path: String, + +fixed: List<&2, String>, + +self: String +) -> Nat: match rest: case Tree.NCons{Tree.Group{Lex.Tok{k, +o, ol, oc}, +kids, cl}, r}: - Bool.pick(Nat, index.fires(String.eq(tt, "List.get"), String.eq(o, "("), String.eq(tt, "String.get"), + +other = Bool.not(String.eq(tt, self)) + Bool.pick(Nat, index.fires(Bool.and(String.eq(tt, "List.get"), other), String.eq(o, "("), + Bool.and(String.eq(tt, "String.get"), other), Calls.args(kids), Table.hit(String.eq(o, "("), "List.get", kids, fixed, path, ll, cc)), 1n, 0n) case other: 0n # how many calls at any depth of the node index reports, fixed the tables -# `table` sees -def index.count(nn: Tree.Node, +path: String, +fixed: List<&2, String>) -> Nat: +# `table` sees, in the def named self +def index.count(nn: Tree.Node, +path: String, +fixed: List<&2, String>, +self: String) -> Nat: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, +l, +c}}, +rest}: - Nat.add(index.site(t, l, c, rest, path, fixed), index.count(rest, path, fixed)) + Nat.add(index.site(t, l, c, rest, path, fixed, self), index.count(rest, path, fixed, self)) case Tree.NCons{Tree.Group{o, kids, cl}, rest}: - Nat.add(index.count(kids, path, fixed), index.count(rest, path, fixed)) + Nat.add(index.count(kids, path, fixed, self), index.count(rest, path, fixed, self)) case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}: - Nat.add(index.count(kids, path, fixed), Nat.add(index.count(body, path, fixed), index.count(rest, path, fixed))) + Nat.add(index.count(kids, path, fixed, self), Nat.add(index.count(body, path, fixed, self), + index.count(rest, path, fixed, self))) case Tree.NCons{h, rest}: - index.count(rest, path, fixed) + index.count(rest, path, fixed, self) case other: 0n @@ -1640,13 +1654,14 @@ def index.total(ds: List<&2, Calls.Def>, +mods: List<&2, String>, +path: String) 0n case Con{Calls.Def{+name, +sig, +body}, rest}: Nat.add(Bool.pick(Nat, Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig))), - index.count(body, path, Table.scope(body, mods)), 0n), index.total(rest, mods, path)) + index.count(body, path, Table.scope(body, mods), name), 0n), index.total(rest, mods, path)) # LAW: index reports one finding for each `List.get(..)` or `String.get(..)` # at an index that is not one number token, anywhere in a def that calls # itself (a base arm included) and is not a law or a proof, except a -# `List.get` that `table` reports as a get on a fixed table; none for -# anything else +# `List.get` that `table` reports as a get on a fixed table and a get that is +# the def's own self-call (in a def named `List.get` or `String.get`); none +# for anything else # BOLT-RULE-U007 law index_counts: for +path: String @@ -2103,11 +2118,15 @@ law ring_counts: == ring.defs(Calls.defs(tree), path) : Nat} # fuel (BOLT-RULE-U006). The rule lists the file's fuel parameters: for each -# def of the file (Calls.defs), each parameter (Calls.params) whose name, its -# first lowercase name before the colon (Calls.param_name), is `fuel`, `gas`, -# `steps` or `budget` or starts with `fuel`, with its position. Over each -# top-level statement it then reads every call at any depth, a name token -# then a `(` group, that is not a call of the statement's own name (a +# def of the file (Calls.defs) that returns no effect, each parameter +# (Calls.params) whose name, its first lowercase name before the colon +# (Calls.param_name), is `fuel`, `gas`, `steps` or `budget` or starts with +# `fuel`, with its position. A def returns an effect when its header's +# top-level tokens hold a `->` leaf followed right away by a capitalized name +# leaf `IO`, or, when that `->` is the header's last token (a header wrapped +# after its arrow), the first statement under the def starts with one. Over +# each top-level statement it then reads every call at any depth, a name +# token then a `(` group, that is not a call of the statement's own name (a # self-call): for each fuel parameter of a def of that name, one finding when # the argument in its position (Calls.args, split at top-level commas) is one # Nat literal token alone, digits then `n`, or the dotted name `U32.to_nat` @@ -2129,13 +2148,52 @@ def fuel.slots.of(ps: List<&2, Tree.Node>, +name: String, +ii: Nat) -> List<&2, +more = fuel.slots.of(rest, name, 1n+ii) Bool.pick(List<&2, FuelRule.Fuel>, fuel.named(Calls.param_name(p)), FuelRule.Fuel{name, ii} <> more, more) -# every fuel parameter of every def, in order +# is the node after an arrow a capitalized name leaf reading `IO`? +def fuel.io.next(nn: Tree.Node) -> Bool: + match nn: + case Tree.NCons{+g, rest}: + Bool.and(Calls.kind.leaf(~Calls.kind.upper, g), String.eq(Calls.leaf.text(g), "IO")) + case other: + False{} + +# the tokens of the first statement under a def, none when there is none +def fuel.under(body: Tree.Node) -> Tree.Node: + match body: + case Tree.NCons{Tree.Stmt{kind, kids, inner}, rest}: + kids + case other: + Tree.NNil{} + +# after an arrow: the rest of the header when there is one, else the tokens +# of the line under it (the header wrapped after its `->`) +def fuel.io.after(rest: Tree.Node, +below: Tree.Node) -> Bool: + match rest: + case Tree.NCons{h, t}: + fuel.io.next(Tree.NCons{h, t}) + case other: + fuel.io.next(below) + +# does the header return an effect: some top-level `->` leaf followed by a +# capitalized name leaf reading `IO`, the first of the line under it when the +# arrow ends the header? +def fuel.io(sig: Tree.Node, +below: Tree.Node) -> Bool: + match sig: + case Tree.NCons{h, +rest}: + Bool.or(Bool.and(Calls.kind.leaf(~Calls.kind.arrow, h), fuel.io.after(rest, below)), fuel.io(rest, below)) + case other: + False{} + +# the parameters of a def that returns no effect, none of one that does +def fuel.params(+sig: Tree.Node, body: Tree.Node) -> List<&2, Tree.Node>: + Bool.pick(List<&2, Tree.Node>, fuel.io(sig, fuel.under(body)), [], Calls.params(sig)) + +# every fuel parameter of every def that returns no effect, in order def fuel.slots(ds: List<&2, Calls.Def>) -> List<&2, FuelRule.Fuel>: match ds: case Nil{}: Nil{} case Con{Calls.Def{name, sig, body}, rest}: - List.append(&2, FuelRule.Fuel, fuel.slots.of(Calls.params(sig), name, 0n), fuel.slots(rest)) + List.append(&2, FuelRule.Fuel, fuel.slots.of(fuel.params(sig, body), name, 0n), fuel.slots(rest)) # does a call's group hold one number token alone, digits only (a U32 # literal), when ok says the call is `U32.to_nat(`? @@ -2207,8 +2265,8 @@ def fuel.total(root: Tree.Node, +fs: List<&2, FuelRule.Fuel>) -> Nat: case other: 0n -# LAW: the rule's fuel parameters are the file's defs' parameters with a fuel -# name, each at its position +# LAW: the rule's fuel parameters are the parameters with a fuel name of the +# file's defs that return no effect (no `-> IO`), each at its position # BOLT-RULE-U006 law fuel_slots: for ds: List<&2, Calls.Def> diff --git a/src/rules/PROOF.bend b/src/rules/PROOF.bend index 801e497..a541e05 100644 --- a/src/rules/PROOF.bend +++ b/src/rules/PROOF.bend @@ -1630,7 +1630,7 @@ def ex.index(ds, mods, path, n, e): ex.push( Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), ex.guard(Calls.calls(body, name), path, sig, e), - _u => Index.walk(body, path, Table.scope(body, mods)), n, + _u => Index.walk(body, path, Table.scope(body, mods), name), n, v => Index.check.go(rest, mods, path, v), ex.index(rest, mods, path, 1n+n, e)) def Laws.index_exempt(path, _text, _toks, tree, _bound, _items, e): @@ -8109,23 +8109,26 @@ law index.call: for +rr: Tree.Node for +path: String for +fixed: List<&2, String> - for ih1: {List.length(&2, F.Finding, Index.walk(kids, path, fixed)) == Laws.index.count(kids, path, fixed) : Nat} - for ih2: {List.length(&2, F.Finding, Index.walk(rr, path, fixed)) == Laws.index.count(rr, path, fixed) : Nat} + for +self: String + for ih1: {List.length(&2, F.Finding, Index.walk(kids, path, fixed, self)) == Laws.index.count(kids, path, fixed, self) + : Nat} + for ih2: {List.length(&2, F.Finding, Index.walk(rr, path, fixed, self)) == Laws.index.count(rr, path, fixed, self) + : Nat} {List.length(&2, F.Finding, Index.walk(Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, - Tree.NCons{Tree.Group{Lex.Tok{gk, o, gl, gc}, kids, cl}, rr}}, path, fixed)) + Tree.NCons{Tree.Group{Lex.Tok{gk, o, gl, gc}, kids, cl}, rr}}, path, fixed, self)) == Laws.index.count(Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, - Tree.NCons{Tree.Group{Lex.Tok{gk, o, gl, gc}, kids, cl}, rr}}, path, fixed) : Nat} + Tree.NCons{Tree.Group{Lex.Tok{gk, o, gl, gc}, kids, cl}, rr}}, path, fixed, self) : Nat} -def index.call(_k, t, l, c, _gk, o, _gl, _gc, kids, _cl, rr, path, fixed, ih1, ih2): - +list = String.eq(t, "List.get") +def index.call(_k, t, l, c, _gk, o, _gl, _gc, kids, _cl, rr, path, fixed, self, ih1, ih2): + +list = Index.named(t, self, "List.get") +ob = String.eq(o, "(") - +sb = String.eq(t, "String.get") + +sb = Index.named(t, self, "String.get") +as = Calls.args(kids) +fire = Bool.and(Bool.and(ob, Bool.or(list, sb)), Bool.and(Bool.not(Index.literal(Calls.arg(as, Bool.pick(Nat, list, 3n, 1n)))), Bool.not(Index.held(list, Calls.arg(as, 2n), fixed)))) - +more = List.concat(&2, F.Finding, [Index.walk(kids, path, fixed), Index.walk(rr, path, fixed)]) - +m = Nat.add(Laws.index.count(kids, path, fixed), Laws.index.count(rr, path, fixed)) + +more = List.concat(&2, F.Finding, [Index.walk(kids, path, fixed, self), Index.walk(rr, path, fixed, self)]) + +m = Nat.add(Laws.index.count(kids, path, fixed, self), Laws.index.count(rr, path, fixed, self)) +spec = Laws.index.fires(list, ob, sb, as, Table.hit(ob, "List.get", kids, fixed, path, l, c)) +x = {F.Finding{path, l, c, U32.from_nat(String.length(t)), "index", t ++ " in a recursive def walks the list from its head on every step, which is quadratic; recurse over the list itself."} @@ -8134,8 +8137,8 @@ def index.call(_k, t, l, c, _gk, o, _gl, _gc, kids, _cl, rr, path, fixed, ih1, i List.length(&2, F.Finding, Bool.pick(List<&2, F.Finding>, fire, x <> more, more)), Bool.pick(Nat, fire, 1n+m, m), Nat.add(Bool.pick(Nat, spec, 1n, 0n), m), - nat.pick(fire, x, more, m, index.two(Index.walk(kids, path, fixed), Index.walk(rr, path, fixed), - Laws.index.count(kids, path, fixed), Laws.index.count(rr, path, fixed), ih1, ih2)), + nat.pick(fire, x, more, m, index.two(Index.walk(kids, path, fixed, self), Index.walk(rr, path, fixed, self), + Laws.index.count(kids, path, fixed, self), Laws.index.count(rr, path, fixed, self), ih1, ih2)), Equal.trans(Nat, Bool.pick(Nat, fire, 1n+m, m), Nat.add(Bool.pick(Nat, fire, 1n, 0n), m), @@ -8149,9 +8152,10 @@ law index.walk: for nn: Tree.Node for +path: String for +fixed: List<&2, String> - {List.length(&2, F.Finding, Index.walk(nn, path, fixed)) == Laws.index.count(nn, path, fixed) : Nat} + for +self: String + {List.length(&2, F.Finding, Index.walk(nn, path, fixed, self)) == Laws.index.count(nn, path, fixed, self) : Nat} -def index.walk(nn, path, fixed): +def index.walk(nn, path, fixed, self): match nn: case Tree.Leaf{tok}: {==} @@ -8176,29 +8180,31 @@ def index.walk(nn, path, fixed): case Tree.NCons{rh, +rr}: match rh: case Tree.Group{Lex.Tok{gk, o, gl, gc}, +kids, cl}: - index.call(k, t, l, c, gk, o, gl, gc, kids, cl, rr, path, fixed, - index.walk(kids, path, fixed), index.walk(rr, path, fixed)) + index.call(k, t, l, c, gk, o, gl, gc, kids, cl, rr, path, fixed, self, + index.walk(kids, path, fixed, self), index.walk(rr, path, fixed, self)) case Tree.Leaf{tok}: - index.walk(rest, path, fixed) + index.walk(rest, path, fixed, self) case Tree.Stmt{kind, sk, sb}: - index.walk(rest, path, fixed) + index.walk(rest, path, fixed, self) case Tree.NNil{}: - index.walk(rest, path, fixed) + index.walk(rest, path, fixed, self) case Tree.NCons{nh, nt}: - index.walk(rest, path, fixed) + index.walk(rest, path, fixed, self) case Tree.Group{o, +kids, cl}: - index.two(Index.walk(kids, path, fixed), Index.walk(rest, path, fixed), - Laws.index.count(kids, path, fixed), Laws.index.count(rest, path, fixed), - index.walk(kids, path, fixed), index.walk(rest, path, fixed)) + index.two(Index.walk(kids, path, fixed, self), Index.walk(rest, path, fixed, self), + Laws.index.count(kids, path, fixed, self), Laws.index.count(rest, path, fixed, self), + index.walk(kids, path, fixed, self), index.walk(rest, path, fixed, self)) case Tree.Stmt{kind, +kids, +body}: - chars.sum(Index.walk(kids, path, fixed), Index.walk(body, path, fixed), Index.walk(rest, path, fixed), - Laws.index.count(kids, path, fixed), Laws.index.count(body, path, fixed), - Laws.index.count(rest, path, fixed), - index.walk(kids, path, fixed), index.walk(body, path, fixed), index.walk(rest, path, fixed)) + chars.sum(Index.walk(kids, path, fixed, self), Index.walk(body, path, fixed, self), + Index.walk(rest, path, fixed, self), + Laws.index.count(kids, path, fixed, self), Laws.index.count(body, path, fixed, self), + Laws.index.count(rest, path, fixed, self), + index.walk(kids, path, fixed, self), index.walk(body, path, fixed, self), + index.walk(rest, path, fixed, self)) case Tree.NNil{}: - index.walk(rest, path, fixed) + index.walk(rest, path, fixed, self) case Tree.NCons{nh, nt}: - index.walk(rest, path, fixed) + index.walk(rest, path, fixed, self) # the counts of gathered finding lists, the last gathered first def index.sum(acc: List<&2, List<&2, F.Finding>>) -> Nat: @@ -8259,13 +8265,15 @@ law index.def: for +body: Tree.Node for +path: String for +fixed: List<&2, String> - {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, Bool.not(g), [], _u => Index.walk(body, path, fixed))) - == Bool.pick(Nat, g, Laws.index.count(body, path, fixed), 0n) : Nat} + for +self: String + {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, Bool.not(g), [], _u => Index.walk(body, path, fixed, + self))) + == Bool.pick(Nat, g, Laws.index.count(body, path, fixed, self), 0n) : Nat} -def index.def(g, body, path, fixed): +def index.def(g, body, path, fixed, self): match g: case True{}: - index.walk(body, path, fixed) + index.walk(body, path, fixed, self) case False{}: {==} @@ -8286,8 +8294,8 @@ def index.go(ds, mods, path, acc): case Con{Calls.Def{+name, +sig, +body}, +rest}: +g = Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig))) +fixed = Table.scope(body, mods) - +x = Lazy.stop(List<&2, F.Finding>, Bool.not(g), [], _u => Index.walk(body, path, fixed)) - +n = Bool.pick(Nat, g, Laws.index.count(body, path, fixed), 0n) + +x = Lazy.stop(List<&2, F.Finding>, Bool.not(g), [], _u => Index.walk(body, path, fixed, name)) + +n = Bool.pick(Nat, g, Laws.index.count(body, path, fixed, name), 0n) +tot = Laws.index.total(rest, mods, path) Equal.trans(Nat, List.length(&2, F.Finding, Index.check.go(rest, mods, path, x <> acc)), @@ -8300,7 +8308,7 @@ def index.go(ds, mods, path, acc): Nat.add(index.sum(acc), Nat.add(n, tot)), index.assoc(index.sum(acc), List.length(&2, F.Finding, x), tot), Equal.cong(Nat, Nat, z => Nat.add(index.sum(acc), Nat.add(z, tot)), List.length(&2, F.Finding, x), n, - index.def(g, body, path, fixed)))) + index.def(g, body, path, fixed, name)))) def Laws.index_counts(path, _text, _toks, tree, _bound, _items): +ds = Calls.defs(tree) @@ -9282,21 +9290,139 @@ def fuel.of(ps, name, ii): x => Bool.pick(List<&2, FuelRule.Fuel>, FuelRule.is_fuel(Calls.param_name(p)), FuelRule.Fuel{name, ii} <> x, x), FuelRule.fuels.params(rest, name, 1n+ii), Laws.fuel.slots.of(rest, name, 1n+ii), fuel.of(rest, name, 1n+ii)) +# the rule reads the name after an arrow as the law does +law fuel.io.next: + for nn: Tree.Node + {FuelRule.effect.io(nn) == Laws.fuel.io.next(nn) : Bool} + +def fuel.io.next(nn): + match nn: + case Tree.NCons{g, r}: + match g: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, t, l, c}: + match k: + case Lex.TName{}: {==} + case Lex.TUpper{}: {==} + case Lex.TDotted{}: {==} + case Lex.TWild{}: {==} + case Lex.TKey{}: {==} + case Lex.TNum{}: {==} + case Lex.TStr{}: {==} + case Lex.TChar{}: {==} + case Lex.TComment{}: {==} + case Lex.TSpace{}: {==} + case Lex.TNewline{}: {==} + case Lex.TOp{}: {==} + case Lex.TColon{}: {==} + case Lex.TEq{}: {==} + case Lex.TBind{}: {==} + case Lex.TArrow{}: {==} + case Lex.TLam{}: {==} + case Lex.TAll{}: {==} + case Lex.TAmp{}: {==} + case Lex.TOpen{}: {==} + case Lex.TClose{}: {==} + case Lex.TComma{}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + +# the rule's first line under a def is the law's +law fuel.under: + for body: Tree.Node + {FuelRule.under(body) == Laws.fuel.under(body) : Tree.Node} + +def fuel.under(body): + match body: + case Tree.NCons{h, r}: + match h: + case Tree.Stmt{k, kids, inner}: {==} + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + +# the rule reads what follows an arrow as the law does +law fuel.after: + for rest: Tree.Node + for +below: Tree.Node + {FuelRule.effect.next(rest, below) == Laws.fuel.io.after(rest, below) : Bool} + +def fuel.after(rest, below): + match rest: + case Tree.NCons{h, t}: fuel.io.next(Tree.NCons{h, t}) + case Tree.Leaf{tok}: fuel.io.next(below) + case Tree.Group{o, gk, cl}: fuel.io.next(below) + case Tree.Stmt{sk, sks, sb}: fuel.io.next(below) + case Tree.NNil{}: fuel.io.next(below) + +# the rule's effect test on a header is the law's +law fuel.effect: + for sig: Tree.Node + for +below: Tree.Node + {FuelRule.effect(sig, below) == Laws.fuel.io(sig, below) : Bool} + +def fuel.effect(sig, below): + match sig: + case Tree.NCons{h, +rest}: + +a = Calls.kind.leaf(~Calls.kind.arrow, h) + Equal.trans(Bool, + Bool.or(Bool.and(a, FuelRule.effect.next(rest, below)), FuelRule.effect(rest, below)), + Bool.or(Bool.and(a, Laws.fuel.io.after(rest, below)), FuelRule.effect(rest, below)), + Bool.or(Bool.and(a, Laws.fuel.io.after(rest, below)), Laws.fuel.io(rest, below)), + Equal.cong(Bool, Bool, z => Bool.or(Bool.and(a, z), FuelRule.effect(rest, below)), + FuelRule.effect.next(rest, below), Laws.fuel.io.after(rest, below), fuel.after(rest, below)), + Equal.cong(Bool, Bool, z => Bool.or(Bool.and(a, Laws.fuel.io.after(rest, below)), z), + FuelRule.effect(rest, below), Laws.fuel.io(rest, below), fuel.effect(rest, below))) + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + +# a def's effect test, the rule's and the law's +law fuel.def: + for +sig: Tree.Node + for +body: Tree.Node + {FuelRule.effect(sig, FuelRule.under(body)) == Laws.fuel.io(sig, Laws.fuel.under(body)) : Bool} + +def fuel.def(sig, body): + Equal.trans(Bool, FuelRule.effect(sig, FuelRule.under(body)), Laws.fuel.io(sig, FuelRule.under(body)), + Laws.fuel.io(sig, Laws.fuel.under(body)), fuel.effect(sig, FuelRule.under(body)), + Equal.cong(Tree.Node, Bool, z => Laws.fuel.io(sig, z), FuelRule.under(body), Laws.fuel.under(body), + fuel.under(body))) + def Laws.fuel_slots(ds): match ds: case Nil{}: {==} case Con{d, +rest}: match d: - case Calls.Def{+name, +sig, body}: - +aa = FuelRule.fuels.params(Calls.params(sig), name, 0n) - +bb = Laws.fuel.slots.of(Calls.params(sig), name, 0n) + case Calls.Def{+name, +sig, +body}: + +aa = FuelRule.fuels.params(FuelRule.slots(sig, body), name, 0n) + +bb = Laws.fuel.slots.of(Laws.fuel.params(sig, body), name, 0n) Equal.trans(List<&2, FuelRule.Fuel>, List.append(&2, FuelRule.Fuel, aa, FuelRule.fuels(rest)), List.append(&2, FuelRule.Fuel, bb, FuelRule.fuels(rest)), List.append(&2, FuelRule.Fuel, bb, Laws.fuel.slots(rest)), Equal.cong(List<&2, FuelRule.Fuel>, List<&2, FuelRule.Fuel>, x => List.append(&2, FuelRule.Fuel, x, FuelRule.fuels(rest)), - aa, bb, fuel.of(Calls.params(sig), name, 0n)), + aa, bb, Equal.trans(List<&2, FuelRule.Fuel>, aa, + FuelRule.fuels.params(Laws.fuel.params(sig, body), name, 0n), bb, + Equal.cong(Bool, List<&2, FuelRule.Fuel>, + z => FuelRule.fuels.params(Bool.pick(List<&2, Tree.Node>, z, [], Calls.params(sig)), name, 0n), + FuelRule.effect(sig, FuelRule.under(body)), Laws.fuel.io(sig, Laws.fuel.under(body)), + fuel.def(sig, body)), + fuel.of(Laws.fuel.params(sig, body), name, 0n))), Equal.cong(List<&2, FuelRule.Fuel>, List<&2, FuelRule.Fuel>, x => List.append(&2, FuelRule.Fuel, bb, x), FuelRule.fuels(rest), Laws.fuel.slots(rest), Laws.fuel_slots(rest))) @@ -23043,16 +23169,18 @@ law inert.index.off2: for +c: U32 for +path: String for +more: List<&2, F.Finding> + for +self: String for eg: {String.eq(t, "List.get") == False{} : Bool} for es: {String.eq(t, "String.get") == False{} : Bool} - {inert.index.at(o, String.eq(t, "List.get"), String.eq(t, "String.get"), lit, hd, t, l, c, path, more) == more - : List<&2, F.Finding>} - -def inert.index.off2(o, lit, hd, t, l, c, path, more, eg, es): - %Equal.sym(Bool, String.eq(t, "List.get"), False{}, eg) : {inert.index.at(o, _, String.eq(t, "String.get"), lit, hd, t, - l, c, path, more) == more : List<&2, F.Finding>} - %Equal.sym(Bool, String.eq(t, "String.get"), False{}, es) : {inert.index.at(o, False{}, _, lit, hd, t, l, c, path, + {inert.index.at(o, Index.named(t, self, "List.get"), Index.named(t, self, "String.get"), lit, hd, t, l, c, path, more) == more : List<&2, F.Finding>} + +def inert.index.off2(o, lit, hd, t, l, c, path, more, self, eg, es): + +ns = Bool.not(String.eq(t, self)) + %Equal.sym(Bool, String.eq(t, "List.get"), False{}, eg) : {inert.index.at(o, Bool.and(_, ns), + Bool.and(String.eq(t, "String.get"), ns), lit, hd, t, l, c, path, more) == more : List<&2, F.Finding>} + %Equal.sym(Bool, String.eq(t, "String.get"), False{}, es) : {inert.index.at(o, Bool.and(False{}, ns), + Bool.and(_, ns), lit, hd, t, l, c, path, more) == more : List<&2, F.Finding>} inert.index.off(o, lit, hd, t, l, c, path, more) # what index reads of a call from its name, its group and what they report @@ -23064,11 +23192,12 @@ def inert.index.call( +c: U32, +path: String, +fixed: List<&2, String>, + +self: String, +more: List<&2, F.Finding> ) -> List<&2, F.Finding>: - +go = String.eq(tt, "List.get") + +go = Index.named(tt, self, "List.get") +aa = Calls.args(kids) - inert.index.at(o, go, String.eq(tt, "String.get"), Index.literal(Calls.arg(aa, Bool.pick(Nat, go, 3n, 1n))), + inert.index.at(o, go, Index.named(tt, self, "String.get"), Index.literal(Calls.arg(aa, Bool.pick(Nat, go, 3n, 1n))), Index.held(go, Calls.arg(aa, 2n), fixed), tt, l, c, path, more) # a call named no get, read either way, is no finding @@ -23081,15 +23210,16 @@ law inert.index.calloff: for +path: String for +fixed: List<&2, String> for +more: List<&2, F.Finding> + for +self: String for eg: {String.eq(tt, "List.get") == False{} : Bool} for es: {String.eq(tt, "String.get") == False{} : Bool} - {inert.index.call(o, tt, kids, l, c, path, fixed, more) == more : List<&2, F.Finding>} + {inert.index.call(o, tt, kids, l, c, path, fixed, self, more) == more : List<&2, F.Finding>} -def inert.index.calloff(o, tt, kids, l, c, path, fixed, more, eg, es): - +go = String.eq(tt, "List.get") +def inert.index.calloff(o, tt, kids, l, c, path, fixed, more, self, eg, es): + +go = Index.named(tt, self, "List.get") +aa = Calls.args(kids) inert.index.off2(o, Index.literal(Calls.arg(aa, Bool.pick(Nat, go, 3n, 1n))), Index.held(go, Calls.arg(aa, 2n), - fixed), tt, l, c, path, more, eg, es) + fixed), tt, l, c, path, more, self, eg, es) # a name then a group, read that way: the call reported as it was, the group # and the rest walked as they were @@ -23101,45 +23231,49 @@ law inert.index.lg: for +c: U32 for +path: String for +fixed: List<&2, String> + for +self: String for +kids: Tree.Node for +r2: Tree.Node for +ef: {Laws.inert.fits.go(b, t) == True{} : Bool} for +ek: {Laws.inert.ok(kids) == True{} : Bool} - for ik: {Index.walk(Laws.inert.node(kids), path, fixed) == Index.walk(kids, path, fixed) : List<&2, F.Finding>} - for ir: {Index.walk(Laws.inert.node(r2), path, fixed) == Index.walk(r2, path, fixed) : List<&2, F.Finding>} - {inert.index.call(o, Laws.inert.keep(b, t), Laws.inert.node(kids), l, c, path, fixed, - List.concat(&2, F.Finding, [Index.walk(Laws.inert.node(kids), path, fixed), Index.walk(Laws.inert.node(r2), path, - fixed)])) - == inert.index.call(o, t, kids, l, c, path, fixed, List.concat(&2, F.Finding, [Index.walk(kids, path, fixed), - Index.walk(r2, path, fixed)])) : List<&2, F.Finding>} - -def inert.index.lg(b, t, o, l, c, path, fixed, kids, r2, ef, ek, ik, ir): + for ik: {Index.walk(Laws.inert.node(kids), path, fixed, self) == Index.walk(kids, path, fixed, self) + : List<&2, F.Finding>} + for ir: {Index.walk(Laws.inert.node(r2), path, fixed, self) == Index.walk(r2, path, fixed, self) + : List<&2, F.Finding>} + {inert.index.call(o, Laws.inert.keep(b, t), Laws.inert.node(kids), l, c, path, fixed, self, + List.concat(&2, F.Finding, [Index.walk(Laws.inert.node(kids), path, fixed, self), + Index.walk(Laws.inert.node(r2), path, fixed, self)])) + == inert.index.call(o, t, kids, l, c, path, fixed, self, List.concat(&2, F.Finding, + [Index.walk(kids, path, fixed, self), Index.walk(r2, path, fixed, self)])) : List<&2, F.Finding>} + +def inert.index.lg(b, t, o, l, c, path, fixed, self, kids, r2, ef, ek, ik, ir): match b: case True{}: - +wk = Index.walk(Laws.inert.node(kids), path, fixed) - +wr = Index.walk(Laws.inert.node(r2), path, fixed) + +wk = Index.walk(Laws.inert.node(kids), path, fixed, self) + +wr = Index.walk(Laws.inert.node(r2), path, fixed, self) +mi = List.concat(&2, F.Finding, [wk, wr]) - +mo = List.concat(&2, F.Finding, [Index.walk(kids, path, fixed), Index.walk(r2, path, fixed)]) + +mo = List.concat(&2, F.Finding, [Index.walk(kids, path, fixed, self), Index.walk(r2, path, fixed, self)]) +ct = Laws.inert.cut(t) - Equal.trans(List<&2, F.Finding>, inert.index.call(o, ct, Laws.inert.node(kids), l, c, path, fixed, mi), mi, - inert.index.call(o, t, kids, l, c, path, fixed, mo), - inert.index.calloff(o, ct, Laws.inert.node(kids), l, c, path, fixed, mi, + Equal.trans(List<&2, F.Finding>, inert.index.call(o, ct, Laws.inert.node(kids), l, c, path, fixed, self, mi), mi, + inert.index.call(o, t, kids, l, c, path, fixed, self, mo), + inert.index.calloff(o, ct, Laws.inert.node(kids), l, c, path, fixed, mi, self, inert.neq(ct, "List.get", inert.cut_marked(t, ef), {==}), inert.neq(ct, "String.get", inert.cut_marked(t, ef), {==})), - Equal.trans(List<&2, F.Finding>, mi, mo, inert.index.call(o, t, kids, l, c, path, fixed, mo), - inert.cat2(wk, Index.walk(kids, path, fixed), wr, Index.walk(r2, path, fixed), ik, ir), - Equal.sym(List<&2, F.Finding>, inert.index.call(o, t, kids, l, c, path, fixed, mo), mo, - inert.index.calloff(o, t, kids, l, c, path, fixed, mo, inert.neq(t, "List.get", ef, {==}), + Equal.trans(List<&2, F.Finding>, mi, mo, inert.index.call(o, t, kids, l, c, path, fixed, self, mo), + inert.cat2(wk, Index.walk(kids, path, fixed, self), wr, Index.walk(r2, path, fixed, self), ik, ir), + Equal.sym(List<&2, F.Finding>, inert.index.call(o, t, kids, l, c, path, fixed, self, mo), mo, + inert.index.calloff(o, t, kids, l, c, path, fixed, mo, self, inert.neq(t, "List.get", ef, {==}), inert.neq(t, "String.get", ef, {==}))))) case False{}: - +wk = Index.walk(Laws.inert.node(kids), path, fixed) - +wr = Index.walk(Laws.inert.node(r2), path, fixed) - +mo = List.concat(&2, F.Finding, [Index.walk(kids, path, fixed), Index.walk(r2, path, fixed)]) - +go = String.eq(t, "List.get") - +gs = String.eq(t, "String.get") + +wk = Index.walk(Laws.inert.node(kids), path, fixed, self) + +wr = Index.walk(Laws.inert.node(r2), path, fixed, self) + +mo = List.concat(&2, F.Finding, [Index.walk(kids, path, fixed, self), Index.walk(r2, path, fixed, self)]) + +go = Index.named(t, self, "List.get") + +gs = Index.named(t, self, "String.get") +aa = Calls.args(kids) +nn = Bool.pick(Nat, go, 3n, 1n) - +lhs = inert.index.call(o, t, Laws.inert.node(kids), l, c, path, fixed, List.concat(&2, F.Finding, [wk, wr])) + +lhs = inert.index.call(o, t, Laws.inert.node(kids), l, c, path, fixed, self, + List.concat(&2, F.Finding, [wk, wr])) %inert.index.literal(Calls.arg(aa, nn)) : {lhs == inert.index.at(o, go, gs, _, Index.held(go, Calls.arg(aa, 2n), fixed), t, l, c, path, mo) : List<&2, F.Finding>} %inert.index.held(go, Calls.arg(aa, 2n), fixed, inert.ok.arg(kids, 2n, ek)) : {lhs == inert.index.at(o, go, gs, @@ -23150,7 +23284,7 @@ def inert.index.lg(b, t, o, l, c, path, fixed, kids, r2, ef, ek, ik, ir): Index.held(go, _, fixed), t, l, c, path, mo) : List<&2, F.Finding>} %inert.args(kids) : {lhs == inert.index.at(o, go, gs, Index.literal(Calls.arg(_, nn)), Index.held(go, Calls.arg(_, 2n), fixed), t, l, c, path, mo) : List<&2, F.Finding>} - %inert.cat2(wk, Index.walk(kids, path, fixed), wr, Index.walk(r2, path, fixed), ik, ir) : {lhs + %inert.cat2(wk, Index.walk(kids, path, fixed, self), wr, Index.walk(r2, path, fixed, self), ik, ir) : {lhs == inert.index.at(o, go, gs, Index.literal(Calls.arg(Calls.args(Laws.inert.node(kids)), nn)), Index.held(go, Calls.arg(Calls.args(Laws.inert.node(kids)), 2n), fixed), t, l, c, path, _) : List<&2, F.Finding>} {==} @@ -23161,10 +23295,11 @@ law inert.index.walk: for nn: Tree.Node for +path: String for +fixed: List<&2, String> + for +self: String for +e: {Laws.inert.ok(nn) == True{} : Bool} - {Index.walk(Laws.inert.node(nn), path, fixed) == Index.walk(nn, path, fixed) : List<&2, F.Finding>} + {Index.walk(Laws.inert.node(nn), path, fixed, self) == Index.walk(nn, path, fixed, self) : List<&2, F.Finding>} -def inert.index.walk(nn, path, fixed, e): +def inert.index.walk(nn, path, fixed, self, e): match nn: case Tree.NCons{h, +rest}: match h: @@ -23180,38 +23315,38 @@ def inert.index.walk(nn, path, fixed, e): +lf = {Tree.Leaf{Lex.Tok{k, t, l, c}} : Tree.Node} +eg = inert.ok_t(lf, Tree.NCons{Tree.Group{Lex.Tok{ok, ot, ol, oc}, kids, cl}, r2}, e) +ec = inert.ok_h(Tree.Group{Lex.Tok{ok, ot, ol, oc}, kids, cl}, r2, eg) - inert.index.lg(Laws.inert.blanks(k), t, ot, l, c, path, fixed, kids, r2, + inert.index.lg(Laws.inert.blanks(k), t, ot, l, c, path, fixed, self, kids, r2, inert.ok_h(lf, Tree.NCons{Tree.Group{Lex.Tok{ok, ot, ol, oc}, kids, cl}, r2}, e), ec, - inert.index.walk(kids, path, fixed, ec), - inert.index.walk(r2, path, fixed, inert.ok_t(Tree.Group{Lex.Tok{ok, ot, ol, oc}, kids, + inert.index.walk(kids, path, fixed, self, ec), + inert.index.walk(r2, path, fixed, self, inert.ok_t(Tree.Group{Lex.Tok{ok, ot, ol, oc}, kids, cl}, r2, eg))) case Tree.Leaf{x}: - inert.index.walk(rest, path, fixed, inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + inert.index.walk(rest, path, fixed, self, inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) case Tree.Stmt{x, y, z}: - inert.index.walk(rest, path, fixed, inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + inert.index.walk(rest, path, fixed, self, inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) case Tree.NNil{}: - inert.index.walk(rest, path, fixed, inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + inert.index.walk(rest, path, fixed, self, inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) case Tree.NCons{x, y}: - inert.index.walk(rest, path, fixed, inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + inert.index.walk(rest, path, fixed, self, inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) case Tree.Leaf{x}: {==} case Tree.Group{x, y, z}: {==} case Tree.Stmt{x, y, z}: {==} case Tree.NNil{}: {==} case Tree.Group{+o, +kids, +cl}: - inert.cat2(Index.walk(Laws.inert.node(kids), path, fixed), Index.walk(kids, path, fixed), - Index.walk(Laws.inert.node(rest), path, fixed), Index.walk(rest, path, fixed), - inert.index.walk(kids, path, fixed, inert.ok_h(Tree.Group{o, kids, cl}, rest, e)), - inert.index.walk(rest, path, fixed, inert.ok_t(Tree.Group{o, kids, cl}, rest, e))) + inert.cat2(Index.walk(Laws.inert.node(kids), path, fixed, self), Index.walk(kids, path, fixed, self), + Index.walk(Laws.inert.node(rest), path, fixed, self), Index.walk(rest, path, fixed, self), + inert.index.walk(kids, path, fixed, self, inert.ok_h(Tree.Group{o, kids, cl}, rest, e)), + inert.index.walk(rest, path, fixed, self, inert.ok_t(Tree.Group{o, kids, cl}, rest, e))) case Tree.Stmt{+sk, +kids, +body}: +es = inert.ok_h(Tree.Stmt{sk, kids, body}, rest, e) - inert.cat3(Index.walk(Laws.inert.node(kids), path, fixed), Index.walk(kids, path, fixed), - Index.walk(Laws.inert.node(body), path, fixed), Index.walk(body, path, fixed), - Index.walk(Laws.inert.node(rest), path, fixed), Index.walk(rest, path, fixed), - inert.index.walk(kids, path, fixed, inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es)), - inert.index.walk(body, path, fixed, inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es)), - inert.index.walk(rest, path, fixed, inert.ok_t(Tree.Stmt{sk, kids, body}, rest, e))) - case Tree.NNil{}: inert.index.walk(rest, path, fixed, e) - case Tree.NCons{x, y}: inert.index.walk(rest, path, fixed, inert.ok_t(Tree.NCons{x, y}, rest, e)) + inert.cat3(Index.walk(Laws.inert.node(kids), path, fixed, self), Index.walk(kids, path, fixed, self), + Index.walk(Laws.inert.node(body), path, fixed, self), Index.walk(body, path, fixed, self), + Index.walk(Laws.inert.node(rest), path, fixed, self), Index.walk(rest, path, fixed, self), + inert.index.walk(kids, path, fixed, self, inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es)), + inert.index.walk(body, path, fixed, self, inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es)), + inert.index.walk(rest, path, fixed, self, inert.ok_t(Tree.Stmt{sk, kids, body}, rest, e))) + case Tree.NNil{}: inert.index.walk(rest, path, fixed, self, e) + case Tree.NCons{x, y}: inert.index.walk(rest, path, fixed, self, inert.ok_t(Tree.NCons{x, y}, rest, e)) case Tree.Leaf{tok}: {==} case Tree.Group{o, gk, cl}: {==} case Tree.Stmt{sk, sks, sb}: {==} @@ -23234,14 +23369,14 @@ def inert.index.go(ds, mods, path, acc, e): +eb = inert.dok.body(name, sig, body, rest, e) +ib = Laws.inert.node(body) +lst = Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(Calls.calls(ib, name), Bool.not(Calls.exempt(path, - Laws.inert.node(sig))))), [], _u => Index.walk(ib, path, Table.scope(ib, mods))) + Laws.inert.node(sig))))), [], _u => Index.walk(ib, path, Table.scope(ib, mods), name)) %inert.table.scope(body, mods, eb) : {Index.check.go(inert.defs(rest), mods, path, lst <> acc) == Index.check.go(rest, mods, path, Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(Calls.calls(body, name), - Bool.not(Calls.exempt(path, sig)))), [], _u => Index.walk(body, path, _)) <> acc) : List<&2, F.Finding>} + Bool.not(Calls.exempt(path, sig)))), [], _u => Index.walk(body, path, _, name)) <> acc) : List<&2, F.Finding>} %inert.stop(Bool.not(Bool.and(Calls.calls(ib, name), Bool.not(Calls.exempt(path, Laws.inert.node(sig))))), Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), - Index.walk(ib, path, Table.scope(ib, mods)), Index.walk(body, path, Table.scope(ib, mods)), - inert.gate(path, name, sig, body, en, eb), inert.index.walk(body, path, Table.scope(ib, mods), eb)) : + Index.walk(ib, path, Table.scope(ib, mods), name), Index.walk(body, path, Table.scope(ib, mods), name), + inert.gate(path, name, sig, body, en, eb), inert.index.walk(body, path, Table.scope(ib, mods), name, eb)) : {Index.check.go(inert.defs(rest), mods, path, lst <> acc) == Index.check.go(rest, mods, path, _ <> acc) : List<&2, F.Finding>} inert.index.go(rest, mods, path, lst <> acc, inert.dok.rest(name, sig, body, rest, e)) @@ -25509,6 +25644,136 @@ def inert.fuel.params(ps, name, ii): FuelRule.Fuel{name, ii} <> mi, mi) : List<&2, FuelRule.Fuel>} {==} +# a capitalized name after an arrow, read that way, is the name it was +law inert.fuel.io: + for nn: Tree.Node + {FuelRule.effect.io(Laws.inert.node(nn)) == FuelRule.effect.io(nn) : Bool} + +def inert.fuel.io(nn): + match nn: + case Tree.NCons{h, r}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, t, l, c}: + match k: + case Lex.TName{}: {==} + case Lex.TUpper{}: {==} + case Lex.TDotted{}: {==} + case Lex.TWild{}: {==} + case Lex.TKey{}: {==} + case Lex.TNum{}: {==} + case Lex.TStr{}: {==} + case Lex.TChar{}: {==} + case Lex.TComment{}: {==} + case Lex.TSpace{}: {==} + case Lex.TNewline{}: {==} + case Lex.TOp{}: {==} + case Lex.TColon{}: {==} + case Lex.TEq{}: {==} + case Lex.TBind{}: {==} + case Lex.TArrow{}: {==} + case Lex.TLam{}: {==} + case Lex.TAll{}: {==} + case Lex.TAmp{}: {==} + case Lex.TOpen{}: {==} + case Lex.TClose{}: {==} + case Lex.TComma{}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + +# an arrow read that way is an arrow as it was +law inert.fuel.arrow: + for h: Tree.Node + {Calls.kind.leaf(~Calls.kind.arrow, Laws.inert.node(h)) == Calls.kind.leaf(~Calls.kind.arrow, h) : Bool} + +def inert.fuel.arrow(h): + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, t, l, c}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + +# the first line under a def, read that way, is that line read that way +law inert.fuel.under: + for body: Tree.Node + {FuelRule.under(Laws.inert.node(body)) == Laws.inert.node(FuelRule.under(body)) : Tree.Node} + +def inert.fuel.under(body): + match body: + case Tree.NCons{h, r}: + match h: + case Tree.Stmt{k, kids, inner}: {==} + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + +# what follows an arrow, read that way, is `IO` when it was +law inert.fuel.next: + for rest: Tree.Node + for +below: Tree.Node + {FuelRule.effect.next(Laws.inert.node(rest), Laws.inert.node(below)) == FuelRule.effect.next(rest, below) : Bool} + +def inert.fuel.next(rest, below): + match rest: + case Tree.NCons{h, t}: inert.fuel.io(Tree.NCons{h, t}) + case Tree.Leaf{tok}: inert.fuel.io(below) + case Tree.Group{o, gk, cl}: inert.fuel.io(below) + case Tree.Stmt{sk, sks, sb}: inert.fuel.io(below) + case Tree.NNil{}: inert.fuel.io(below) + +# a header read that way returns an effect when it did +law inert.fuel.effect: + for sig: Tree.Node + for +below: Tree.Node + {FuelRule.effect(Laws.inert.node(sig), Laws.inert.node(below)) == FuelRule.effect(sig, below) : Bool} + +def inert.fuel.effect(sig, below): + match sig: + case Tree.NCons{+h, +rest}: + +lhs = FuelRule.effect(Laws.inert.node(Tree.NCons{h, rest}), Laws.inert.node(below)) + +ir = Laws.inert.node(rest) + +ib = Laws.inert.node(below) + %inert.fuel.effect(rest, below) : {lhs == Bool.or(Bool.and(Calls.kind.leaf(~Calls.kind.arrow, h), + FuelRule.effect.next(rest, below)), _) : Bool} + %inert.fuel.next(rest, below) : {lhs == Bool.or(Bool.and(Calls.kind.leaf(~Calls.kind.arrow, h), _), + FuelRule.effect(ir, ib)) : Bool} + %inert.fuel.arrow(h) : {lhs == Bool.or(Bool.and(_, FuelRule.effect.next(ir, ib)), FuelRule.effect(ir, ib)) + : Bool} + {==} + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + +# the fuel parameters among parameters read that way, or none, are the ones +# they were +law inert.fuel.pick: + for b: Bool + for +ps: List<&2, Tree.Node> + for +name: String + {FuelRule.fuels.params(Bool.pick(List<&2, Tree.Node>, b, [], inert.nodes(ps)), name, 0n) + == FuelRule.fuels.params(Bool.pick(List<&2, Tree.Node>, b, [], ps), name, 0n) : List<&2, FuelRule.Fuel>} + +def inert.fuel.pick(b, ps, name): + match b: + case True{}: {==} + case False{}: inert.fuel.params(ps, name, 0n) + # the fuel parameters of defs read that way are the ones they were law inert.fuel.fuels: for ds: List<&2, Calls.Def> @@ -25519,12 +25784,21 @@ def inert.fuel.fuels(ds): case Nil{}: {==} case Con{Calls.Def{+name, +sig, +body}, +rest}: +lhs = FuelRule.fuels(inert.defs(Con{Calls.Def{name, sig, body}, rest})) - %inert.fuel.fuels(rest) : {lhs == List.append(&2, FuelRule.Fuel, FuelRule.fuels.params(Calls.params(sig), name, - 0n), _) : List<&2, FuelRule.Fuel>} - %inert.fuel.params(Calls.params(sig), name, 0n) : {lhs == List.append(&2, FuelRule.Fuel, _, - FuelRule.fuels(inert.defs(rest))) : List<&2, FuelRule.Fuel>} - %inert.params(sig) : {lhs == List.append(&2, FuelRule.Fuel, FuelRule.fuels.params(_, name, 0n), - FuelRule.fuels(inert.defs(rest))) : List<&2, FuelRule.Fuel>} + +isig = Laws.inert.node(sig) + +iu = FuelRule.under(Laws.inert.node(body)) + +ps = Calls.params(sig) + +more = FuelRule.fuels(inert.defs(rest)) + %inert.fuel.fuels(rest) : {lhs == List.append(&2, FuelRule.Fuel, FuelRule.fuels.params(FuelRule.slots(sig, body), + name, 0n), _) : List<&2, FuelRule.Fuel>} + %inert.fuel.effect(sig, FuelRule.under(body)) : {lhs == List.append(&2, FuelRule.Fuel, + FuelRule.fuels.params(Bool.pick(List<&2, Tree.Node>, _, [], ps), name, 0n), more) : List<&2, FuelRule.Fuel>} + %inert.fuel.under(body) : {lhs == List.append(&2, FuelRule.Fuel, + FuelRule.fuels.params(Bool.pick(List<&2, Tree.Node>, FuelRule.effect(isig, _), [], ps), name, 0n), more) + : List<&2, FuelRule.Fuel>} + %inert.fuel.pick(FuelRule.effect(isig, iu), ps, name) : {lhs == List.append(&2, FuelRule.Fuel, _, more) + : List<&2, FuelRule.Fuel>} + %inert.params(sig) : {lhs == List.append(&2, FuelRule.Fuel, FuelRule.fuels.params(Bool.pick(List<&2, Tree.Node>, + FuelRule.effect(isig, iu), [], _), name, 0n), more) : List<&2, FuelRule.Fuel>} {==} # a `U32.to_nat(..)` group read that way fixes the fuel it fixed diff --git a/src/rules/suspicious/fuel.bend b/src/rules/suspicious/fuel.bend index 216fe6b..0c0f99f 100644 --- a/src/rules/suspicious/fuel.bend +++ b/src/rules/suspicious/fuel.bend @@ -15,7 +15,14 @@ # counts, an exact repeat count such as `3n` included. Only an argument that # is the literal alone, or `U32.to_nat(` the U32 literal alone `)`, counts: a # let-bound literal and a parenthesized `(7n)` are not seen. A def's own calls -# are exempt: its step passes `fuel - 1`, not a literal. +# are exempt: its step passes `fuel - 1`, not a literal. So is a call to a +# def that returns an effect: its header holds a top-level `->` token with +# the capitalized name token `IO` right after it (`-> IO(Unit):`, parameters +# wrapped over lines or not), or, when the `->` is the header's last token, +# first on the line under it (`->` then `IO(Unit):`). An effect loop's fuel +# bounds its reads, frames or retries, a budget the outside world sets, not +# the size of an input it was handed (a netcode drain of 256 datagrams a +# tick, a read of 100000 chunks). import Base import ../../src.bend as Src import ../../lazy/lazy.bend as Lazy @@ -44,13 +51,54 @@ def fuels.params(ps: List<&2, Tree.Node>, +name: String, +ii: Nat) -> List<&2, F +more = fuels.params(rest, name, 1n+ii) Bool.pick(List<&2, Fuel>, is_fuel(Calls.param_name(p)), Fuel{name, ii} <> more, more) -# every fuel parameter of every def of the file +# is the chain's first node the capitalized name `IO`? +def effect.io(nn: Tree.Node) -> Bool: + match nn: + case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TUpper{}, +t, l, c}}, rest}: + String.eq(t, "IO") + case other: + False{} + +# the kids of the first statement under a def: the line a header wrapped +# after its `->` continues on (`->` then `IO(Unit):` on the next line) +def under(body: Tree.Node) -> Tree.Node: + match body: + case Tree.NCons{Tree.Stmt{kind, kids, inner}, rest}: + kids + case other: + Tree.NNil{} + +# what follows an arrow: the rest of the header, or the line under it (below) +# when the arrow ends the header; is it `IO`? +def effect.next(rest: Tree.Node, +below: Tree.Node) -> Bool: + match rest: + case Tree.NCons{h, tail}: + effect.io(Tree.NCons{h, tail}) + case other: + effect.io(below) + +# does a def's header return an effect: a top-level `->` with the +# capitalized name `IO` right after it, on the next line (below) when the +# arrow ends the header? +def effect(sig: Tree.Node, +below: Tree.Node) -> Bool: + match sig: + case Tree.NCons{h, +rest}: + +more = effect(rest, below) + Bool.or(Bool.and(Calls.kind.leaf(~Calls.kind.arrow, h), effect.next(rest, below)), more) + case other: + False{} + +# the parameters a def's fuel may sit in: none when it returns an effect +def slots(+sig: Tree.Node, body: Tree.Node) -> List<&2, Tree.Node>: + Bool.pick(List<&2, Tree.Node>, effect(sig, under(body)), [], Calls.params(sig)) + +# every fuel parameter of every def of the file that returns no effect def fuels(ds: List<&2, Calls.Def>) -> List<&2, Fuel>: match ds: case Nil{}: Nil{} case Con{Calls.Def{name, sig, body}, rest}: - List.append(&2, Fuel, fuels.params(Calls.params(sig), name, 0n), fuels(rest)) + List.append(&2, Fuel, fuels.params(slots(sig, body), name, 0n), fuels(rest)) # the group of a call at line ll, column cc, as a finding when it holds one # U32 literal alone (digits) and ok says the call is `U32.to_nat(` diff --git a/src/rules/suspicious/index.bend b/src/rules/suspicious/index.bend index 869d47d..4059826 100644 --- a/src/rules/suspicious/index.bend +++ b/src/rules/suspicious/index.bend @@ -8,7 +8,9 @@ # with no type at all fills a law: it is a proof). A # `List.get` on a fixed table (a literal, a sized array, a constant # `List.replicate`) is `table`'s finding instead, so the two rules do not -# both report that call. `String.get` is never `table`'s: it stays here. +# both report that call. `String.get` is never `table`'s: it stays here. A +# get that is the def's own self-call is exempt: the step of a def named +# `List.get` or `String.get` itself (Base's), which walks one cell per call. import Base import ../../src.bend as Src import ../../finding.bend as F @@ -34,26 +36,31 @@ def held(+list: Bool, coll: Tree.Node, +fixed: List<&2, String>) -> Bool: case True{}: Table.owns(coll, fixed) -# every List.get / String.get call at a computed index -def walk(nn: Tree.Node, +path: String, +fixed: List<&2, String>) -> List<&2, F.Finding>: +# is the call named get, and not the def's own (self)? +def named(+tt: String, +self: String, +get: String) -> Bool: + Bool.and(String.eq(tt, get), Bool.not(String.eq(tt, self))) + +# every List.get / String.get call at a computed index, but self's own +def walk(nn: Tree.Node, +path: String, +fixed: List<&2, String>, +self: String) -> List<&2, F.Finding>: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}: - +list = String.eq(t, "List.get") + +list = named(t, self, "List.get") +as = Calls.args(kids) - +get = Bool.and(String.eq(o, "("), Bool.or(list, String.eq(t, "String.get"))) + +get = Bool.and(String.eq(o, "("), Bool.or(list, named(t, self, "String.get"))) +fire = Bool.and(get, Bool.and(Bool.not(literal(Calls.arg(as, Bool.pick(Nat, list, 3n, 1n)))), Bool.not(held(list, Calls.arg(as, 2n), fixed)))) - +more = List.concat(&2, F.Finding, [walk(kids, path, fixed), walk(rest, path, fixed)]) + +more = List.concat(&2, F.Finding, [walk(kids, path, fixed, self), walk(rest, path, fixed, self)]) Bool.pick(List<&2, F.Finding>, fire, F.Finding{path, l, c, U32.from_nat(String.length(t)), "index", t ++ " in a recursive def walks the list from its head on every step, which is quadratic; recurse over the list itself."} <> more, more) case Tree.NCons{Tree.Group{open, +kids, close}, rest}: - List.concat(&2, F.Finding, [walk(kids, path, fixed), walk(rest, path, fixed)]) + List.concat(&2, F.Finding, [walk(kids, path, fixed, self), walk(rest, path, fixed, self)]) case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}: - List.concat(&2, F.Finding, [walk(kids, path, fixed), walk(body, path, fixed), walk(rest, path, fixed)]) + List.concat(&2, F.Finding, [walk(kids, path, fixed, self), walk(body, path, fixed, self), + walk(rest, path, fixed, self)]) case Tree.NCons{h, rest}: - walk(rest, path, fixed) + walk(rest, path, fixed, self) case other: Nil{} @@ -70,7 +77,7 @@ def check.go( check.go(rest, mods, path, Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), [], - _u => walk(body, path, Table.scope(body, mods))) <> acc) + _u => walk(body, path, Table.scope(body, mods), name)) <> acc) # the rule def check(ss: Src.Src) -> List<&2, F.Finding>: From 3c39e827c6a60b20e5020adbadac83bd7e234e44 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 14:03:11 +0000 Subject: [PATCH 4/6] fix(rules): unused (U001) and doc (S001) false positives Behavior changes to two released rules, each with its SPEC row, rule header and tagged law restated to match: - unused (BOLT-RULE-U001): a foreign def, whose parameters are exempt, is one whose body's first statement is `import`, wherever its header's `->` and return type fall. A header that does not end in `:` runs on through the body's statements up to one that does, so `def f(..) ->` then `IO(T):` on the next line then `import "./x.c"` is foreign. Law unused_counts restated (Laws unused.imported now takes the header). - unused: a name read in a dependent arrow at the start of a body (`@+x: U32 -> S`) is a use. The tree classified any `@`-led statement as a def (for `@unsafe def`), so the binder skipped the arrow; an `@` followed by a name, quantity-marked or not, and `:` now makes a term. New untagged laws in src/syntax: arrow_term, marked_arrow_term, attribute_def. - doc (BOLT-RULE-S001): the comment block may sit right above a run of `@` lines (`@unsafe`) right above the item. Laws doc_walk_counts and doc_counts restated (Laws doc.lead replaces doc.hash); inert_doc (BOLT-RULE-INERT) now takes lines that start with `#` alike and with `@` alike. Corpus (every group on at warn), old -> new: - bend: U001 150 -> 98 (46 wrapped foreign params in bend2/base.bend, 6 dependent-arrow params in bend3d.bend); S001 300 -> 298 (@unsafe) - selfhost: U001 3815 -> 3815; S001 2592 -> 2508 (84, all @unsafe) - bolt, ez, ezaudio, ezhttp, ezimg, ezjson, eztoml, shake, snap: 0 -> 0 No finding added anywhere, no other rule's findings changed. bolt on its own tree: 0 errors, 73 warnings, as before. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B --- SPEC.md | 4 +- src/README.md | 12 +- src/rules/LAWS.bend | 106 ++++++-- src/rules/PROOF.bend | 437 ++++++++++++++++++++++--------- src/rules/style/doc.bend | 32 ++- src/rules/suspicious/unused.bend | 72 ++++- src/syntax/LAWS.bend | 52 ++++ src/syntax/PROOF.bend | 9 + src/syntax/tree.bend | 24 +- 9 files changed, 561 insertions(+), 187 deletions(-) diff --git a/SPEC.md b/SPEC.md index 59aaf34..44318a7 100644 --- a/SPEC.md +++ b/SPEC.md @@ -34,7 +34,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-RULE-C009 | `chars` reports exactly a match with more than eight arms whose first match column opens with a char literal. | Proved | proved | src/rules/LAWS.bend chars_counts | | BOLT-RULE-C010 | `foreign` reports exactly a foreign def with a `.c` body and no `.js` or the reverse, where a file whose leading comment lines include the exact line `# lanes: native` needs no `.js`. | Proved | proved | src/rules/LAWS.bend foreign_native; src/rules/LAWS.bend foreign_walk_counts; src/rules/LAWS.bend foreign_counts | | BOLT-RULE-C011 | `setting` reports exactly, for each bolt.bend that grades a directory the run grades (a source's or SPEC.md's; the first of its candidates the World read, BOLT-CFG-4), each bolt.bend once in the order its directories come, one finding for each setting `unknown` holds (BOLT-CFG-7), at that bolt.bend's path and the line of the setting's `def`, in file order, and nothing else. It runs in the CLI lint only. | Proved | proved | src/LAWS.bend unknown_exact; src/LAWS.bend setting_reports | -| BOLT-RULE-U001 | `unused` reports exactly an unused let, do-bind, lambda binder or parameter, with the header's exemptions. | Proved | proved | src/rules/LAWS.bend unused_counts | +| BOLT-RULE-U001 | `unused` reports exactly an unused let, do-bind, lambda binder or parameter, with the header's exemptions: a foreign def, whose parameters are exempt, is one whose body's first statement is `import`, wherever its header's `->` and return type fall. | Proved | proved | src/rules/LAWS.bend unused_counts | | BOLT-RULE-U002 | `strict` reports exactly a self-call inside `Bool.and` or `Bool.or`, or in a comma-separated stretch holding `&&` or `\|\|` (matched by that exact text), where a `=>` ends the stretch on its left and a lambda body counts only by its own `&&` or `\|\|`. | Proved | proved | src/rules/LAWS.bend strict_walk_counts; src/rules/LAWS.bend strict_counts | | BOLT-RULE-U003 | `eager` reports exactly a looping def of the file called in a `Bool.pick` branch. | Proved | proved | src/rules/LAWS.bend eager_counts; src/rules/LAWS.bend eager_lambda; src/rules/LAWS.bend eager_comma; src/rules/LAWS.bend eager_plain | | BOLT-RULE-U004 | `concat` reports exactly a self-call argument that appends onto the parameter in its own position: the append written as the argument, inside any number of parentheses, or a lone name whose nearest `q = ..` or `+q = ..` let before the call, in its statement chain or an enclosing one, has such an append as its right side. | Proved | proved | src/rules/LAWS.bend concat_counts; src/rules/LAWS.bend concat_paren; src/rules/LAWS.bend concat_in_place; src/rules/LAWS.bend concat_via; src/rules/LAWS.bend concat_nearest; src/rules/LAWS.bend concat_other; src/rules/LAWS.bend concat_scope; src/rules/LAWS.bend concat_bound; src/rules/LAWS.bend concat_bound_plus | @@ -49,7 +49,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-RULE-U014 | `argv` reports exactly one finding for each `IO.args` token with a `(` token right after it among the significant tokens, in every file (no path is exempt), and nothing else. It is opt-in: with no setting of its own it is off, whatever its group says (BOLT-CFG-6). | Proved | proved | src/rules/LAWS.bend argv_counts; src/rules/LAWS.bend inert_argv; src/LAWS.bend argv_opt_in | | BOLT-RULE-U015 | `thunk` (opt-in) reports exactly, in a def, a lambda whose body is exactly a self-call and whose parameter that call does not read, passed as the one lambda of a call: in the kids of a group opened by `(` (its arguments: the kids split at their comma leaves), exactly one argument holding, among its own nodes and not inside a group, a leaf whose text is `=>`, four nodes in a row of those kids, a leaf of a name kind (the parameter), a leaf whose text is `=>`, a leaf whose text is the def's name, and a `(` group, the kids ending right after the group or going on with a comma, and no name leaf in the group, at any depth, spelling the parameter or the parameter then a dot; such groups found at any depth; one finding for each, on the def's name, and nothing else. A call given two or more lambdas (a dispatch) gets none. | Proved | proved | src/rules/LAWS.bend thunk_walk_counts; src/rules/LAWS.bend thunk_counts | | BOLT-RULE-U016 | `fromrev` reports exactly, outside a LAWS.bend or a PROOF.bend, one finding (on the first) for each run of four tokens right after one another among the significant tokens (spaces, newlines and comments dropped) whose texts are `String.from_list`, `(`, `List.reverse` and `(`, and nothing else: anything between them, another `(` included, is not the shape, and neither is `List.reverse.go`. | Proved | proved | src/rules/LAWS.bend fromrev_counts; src/rules/LAWS.bend fromrev_exempt; src/rules/LAWS.bend inert_fromrev | -| BOLT-RULE-S001 | `doc` reports exactly a top-level def, type or law with no comment block right above it, with the header's exemptions. | Proved | proved | src/rules/LAWS.bend doc_walk_counts; src/rules/LAWS.bend doc_counts | +| BOLT-RULE-S001 | `doc` reports exactly a top-level def, type or law with no comment block right above it, or right above a run of `@` lines (attributes such as `@unsafe`) right above it, with the header's exemptions. | Proved | proved | src/rules/LAWS.bend doc_walk_counts; src/rules/LAWS.bend doc_counts | | BOLT-RULE-S002 | `space` reports exactly trailing whitespace or a tab on any line, string literals and `#\|` lines included, or a line over 120 columns with string literals counted as two, comments at full width, and `#\|` lines not counted. | Proved | proved | src/rules/LAWS.bend space_counts; src/rules/LAWS.bend space_line_counts; src/rules/LAWS.bend space_width_counts | | BOLT-RULE-S003 | `wrap` reports exactly one finding for each def header that breaks its shape and none otherwise: a one-line header wider than 120 columns through its last `:` (the whole header when it has none), counted as `space` counts a line except that a comment counts zero, or a header across lines (one holding a newline token; a line break inside a string literal does not count) whose parameter list (opened by the first `(` with no bracket open, split by the commas at its own depth) holds a parameter that spans lines, starts on the `(` line, or starts on the line a later parameter starts on, or holds no parameter at all, or closes with its `)` not on a line below the last parameter's last line, or with no `->` (or, with no return type, the header's `:`) right after its `)` on the `)` line. | Proved | proved | src/rules/LAWS.bend wrap_width; src/rules/LAWS.bend wrap_shape_counts; src/rules/LAWS.bend wrap_counts | | BOLT-RULE-S004 | `param` reports exactly one finding for each parameter binder whose name is shorter than two characters, unless the name is one capital letter (a type parameter) or the parameter is bare or typed `: Quant` (a quantity), none for any other binder, and none at all in a PROOF.bend. | Proved | proved | src/rules/LAWS.bend param_counts | diff --git a/src/README.md b/src/README.md index 0fe59a4..b673ad6 100644 --- a/src/README.md +++ b/src/README.md @@ -147,17 +147,19 @@ or one written with no type at all (`def f(x, y):`, no `:` among its parameters and no `->`), which is how Bend fills the law named `f`. - `doc` — every top-level def, type and law has a comment block right above - it: column-0 `#` lines with no blank line before the item. A block of bare - `#` lines counts. Helpers (dotted names like `show.go`) ride on their + it: column-0 `#` lines with no blank line before the item, or before a run + of column-0 `@` lines (`@unsafe`) right above it. A block of bare `#` lines + counts. Helpers (dotted names like `show.go`) ride on their parent's, `main` needs none, PROOF.bend fills laws that LAWS.bend documents, and a test (under `tests/`) is documented by its header and its check names. - `unused` — a name bound by a let, a do-bind, a lambda or as a parameter is never used. Exempt: pattern binders (naming every field of `Tok{k, t, l, c}` reads better than `_`), names starting with `_`, erased parameters (`-x`), - a law's `for` names, and every parameter of a foreign def, one whose body - starts with `import` (its C and JS read them), however its header is - wrapped. + a law's `for` names, and every parameter of a foreign def, one whose body's + first statement is `import` (its C and JS read them), wherever its + header's `->` and return type fall. A name read in a dependent arrow's + types (`@+x: U32 -> S`) is a use. - `hole` — a TODO hole left in code, the one bend counts in "1 TODO found." / "N TODOs found." (under `SOME PROOFS FAIL`, exit 1): `?` and then `TODO`, with spaces, newlines or comments allowed between diff --git a/src/rules/LAWS.bend b/src/rules/LAWS.bend index a43a396..db81357 100644 --- a/src/rules/LAWS.bend +++ b/src/rules/LAWS.bend @@ -1404,10 +1404,11 @@ law closed_counts: == Bool.pick(Nat, Paths.is_laws(path), closed.count(tree), 0n) : Nat} # doc (BOLT-RULE-S001). Over the outline's items the rule reports each def, -# type and law with no comment block right above it: its outline doc text is -# empty and the line right above it does not start with `#` (a block of bare -# `#` lines has an empty text). The header's exemptions: a name that is -# `main` or holds a dot (a helper), and a PROOF.bend or a file under a +# type and law with no comment block right above it: reading up from the +# item past any lines that start with `@` (attributes such as `@unsafe`), +# the first other line does not start with `#` (a block of bare `#` lines +# counts; its doc text is never read). The header's exemptions: a name that +# is `main` or holds a dot (a helper), and a PROOF.bend or a file under a # `tests` directory. # a def, a type or a law: the kinds that need a comment @@ -1426,19 +1427,25 @@ def doc.kind(kk: Outline.ItemKind) -> Bool: def doc.free(+name: String) -> Bool: Bool.or(String.eq(name, "main"), String.contains(name, ".")) -# line nn of the lines (0-based) starts with `#` -def doc.hash(lines: List<&2, String>, +nn: U32) -> Bool: +# reading down, does a comment block end right above the next line? After a +# `#` line it does; an `@` line keeps what was above it; any other line ends it +def doc.after(+line: String, ok: Bool) -> Bool: + Bool.or(String.starts_with(line, "#"), Bool.and(String.starts_with(line, "@"), ok)) + +# reading lines 0 to nn - 1 (0-based) down from ok: does a comment block end +# right above line nn, past a run of `@` lines? +def doc.lead(lines: List<&2, String>, +nn: U32, +ok: Bool) -> Bool: match lines: case Nil{}: - False{} + Bool.and(U32.is_eq(nn, 0), ok) case Con{hh, tt}: - Bool.pick(Bool, U32.is_eq(nn, 0), String.starts_with(hh, "#"), doc.hash(tt, U32.sub(nn, 1))) + Bool.pick(Bool, U32.is_eq(nn, 0), ok, doc.lead(tt, U32.sub(nn, 1), doc.after(hh, ok))) # an item that needs a comment and has none: an unexempt def, type or law -# whose line has no `#` line right above it (its doc text is never read) +# with no `#` line right above it, or right above the `@` lines right above +# it (its doc text is never read) def doc.bare(kk: Outline.ItemKind, +name: String, +line: U32, _doc: String, +lines: List<&2, String>) -> Bool: - Bool.and(Bool.and(doc.kind(kk), Bool.not(doc.free(name))), - Bool.not(Bool.and(Bool.not(U32.is_eq(line, 0)), doc.hash(lines, U32.sub(line, 1))))) + Bool.and(Bool.and(doc.kind(kk), Bool.not(doc.free(name))), Bool.not(doc.lead(lines, line, False{}))) # how many items need a comment and have none def doc.count(items: List<&2, Outline.Item>, +lines: List<&2, String>) -> Nat: @@ -1451,7 +1458,8 @@ def doc.count(items: List<&2, Outline.Item>, +lines: List<&2, String>) -> Nat: # LAW: over the outline's items, doc reports one finding for each def, type # or law not named `main` and holding no dot whose line has no `#` line -# right above it, and none for any other item +# right above it, or right above a run of `@` lines right above it, and none +# for any other item # BOLT-RULE-S001 law doc_walk_counts: for items: List<&2, Outline.Item> @@ -1478,18 +1486,44 @@ law doc_counts: # every use with what it resolves to. A binder counts when it is a let, a # do-bind or a lambda binder (KLocal), or a parameter (KParam) that is not # erased (its declaration opens with `-`) and does not sit on a header line -# of a foreign def; its name does not start with `_`; and no use resolves to +# of a foreign def (its body's first statement, once a header that does not +# end in `:` has run on through the statements up to one that does, is an +# `import`); its name does not start with `_`; and no use resolves to # its position. Pattern binders (KPat), a law's `for` names (KFor) and every # other kind never count. -# does a def's body open with an import statement? then the def is foreign -def unused.imported(body: Tree.Node) -> Bool: - match body: - case Tree.NCons{Tree.Stmt{Tree.SImport{}, kids, b}, rest}: +# is the statement an import? +def unused.is_import(sk: Tree.StmtKind) -> Bool: + match sk: + case Tree.SImport{}: True{} case other: False{} +# does a statement's own chain end in a `:` leaf (Unused.colon, the rule's +# reading of one)? last: whether the node before the chain did +def unused.ends(kids: Tree.Node, last: Bool) -> Bool: + match kids: + case Tree.NCons{h, t}: + unused.ends(t, Unused.colon(h)) + case other: + last + +# does the body open with an import once the def's header is over? While the +# header is open (its tokens so far do not end in `:`), each statement of the +# body is more of it: `-> IO(T):` on the line after `def f(..)` +def unused.opens(body: Tree.Node, +open: Bool) -> Bool: + match body: + case Tree.NCons{Tree.Stmt{sk, kids, b}, rest}: + Bool.pick(Bool, open, unused.opens(rest, Bool.not(unused.ends(kids, False{}))), unused.is_import(sk)) + case other: + False{} + +# does a def's body open with an import statement, wherever its header's `->` +# and return type fall? then the def is foreign +def unused.imported(kids: Tree.Node, body: Tree.Node) -> Bool: + unused.opens(body, Bool.not(unused.ends(kids, False{}))) + # the line of each token def unused.token_lines(ts: List<&2, Lex.Tok>) -> List<&2, U32>: match ts: @@ -1502,9 +1536,9 @@ def unused.token_lines(ts: List<&2, Lex.Tok>) -> List<&2, U32>: # of its own tokens, def by def def unused.headers(root: Tree.Node) -> List<&2, U32>: match root: - case Tree.NCons{Tree.Stmt{Tree.SDef{}, kids, body}, rest}: + case Tree.NCons{Tree.Stmt{Tree.SDef{}, +kids, body}, rest}: +more = unused.headers(rest) - Bool.pick(List<&2, U32>, unused.imported(body), + Bool.pick(List<&2, U32>, unused.imported(kids, body), List.append(&2, U32, unused.token_lines(Tree.leaves(kids)), more), more) case Tree.NCons{h, rest}: unused.headers(rest) @@ -1569,7 +1603,7 @@ def unused.count(binds: List<&2, Bind.Bind>, +uses: List<&2, Bind.Use>, +fl: Lis # parameter no use resolves to, and none for any other binder: not a pattern # binder, a name starting with `_`, an erased parameter, a law's `for` name, # or a parameter of a foreign def (one whose body opens with `import`), -# however its header is wrapped +# wherever its header's `->` and return type fall # BOLT-RULE-U001 law unused_counts: for +path: String @@ -4746,18 +4780,36 @@ def inert.items(its: List<&2, Outline.Item>) -> List<&2, Outline.Item>: case Con{h, t}: inert.item(h) <> inert.items(t) -# which lines start with `#` -def inert.hashes(ls: List<&2, String>) -> List<&2, Bool>: +# how a line starts, as doc reads it: with `#`, with `@`, or with neither +type inert.Lead is Data: + LHash{} + LAt{} + LPlain{} + +# how a line starts, from whether it starts with `#` and whether with `@` +def inert.lead(hash: Bool, at: Bool) -> inert.Lead: + match hash: + case True{}: + LHash{} + case False{}: + match at: + case True{}: + LAt{} + case False{}: + LPlain{} + +# how each line starts +def inert.leads(ls: List<&2, String>) -> List<&2, inert.Lead>: match ls: case Nil{}: Nil{} - case Con{h, t}: - String.starts_with(h, "#") <> inert.hashes(t) + case Con{+h, t}: + inert.lead(String.starts_with(h, "#"), String.starts_with(h, "@")) <> inert.leads(t) # LAW: doc reads no comment or string: two sources whose items have the same # kinds, names and lines, and whose lines (one that starts inside a string -# literal read as empty) start with `#` alike, have the same findings, what -# their comments and strings say aside +# literal read as empty) start with `#` alike and with `@` alike, have the +# same findings, what their comments and strings say aside # BOLT-RULE-INERT law inert_doc: for +path: String @@ -4772,7 +4824,7 @@ law inert_doc: for bound2: Bind.Bound for +items2: List<&2, Outline.Item> for ei: {inert.items(items) == inert.items(items2) : List<&2, Outline.Item>} - for el: {inert.hashes(Doc.lines(text, toks)) == inert.hashes(Doc.lines(text2, toks2)) : List<&2, Bool>} + for el: {inert.leads(Doc.lines(text, toks)) == inert.leads(Doc.lines(text2, toks2)) : List<&2, inert.Lead>} {Doc.check(Src.Src{path, text, toks, tree, bound, items}) == Doc.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} diff --git a/src/rules/PROOF.bend b/src/rules/PROOF.bend index a541e05..e9b2f9a 100644 --- a/src/rules/PROOF.bend +++ b/src/rules/PROOF.bend @@ -7184,29 +7184,30 @@ def doc.pick(c, _a, _x, _y, ih): case False{}: ih -# the `#` test on line nn, to the rule and to the law -law doc.hash: +# the read down from ok to line nn, to the rule and to the law +law doc.lead: for lines: List<&2, String> for +nn: U32 - {Doc.check.hash(lines, nn) == Laws.doc.hash(lines, nn) : Bool} + for +ok: Bool + {Doc.check.lead(lines, nn, ok) == Laws.doc.lead(lines, nn, ok) : Bool} -def doc.hash(lines, nn): +def doc.lead(lines, nn, ok): match lines: case Nil{}: {==} - case Con{hh, tt}: - doc.pick(U32.is_eq(nn, 0), String.starts_with(hh, "#"), Doc.check.hash(tt, U32.sub(nn, 1)), - Laws.doc.hash(tt, U32.sub(nn, 1)), doc.hash(tt, U32.sub(nn, 1))) + case Con{+hh, tt}: + doc.pick(U32.is_eq(nn, 0), ok, Doc.check.lead(tt, U32.sub(nn, 1), Doc.check.after(hh, ok)), + Laws.doc.lead(tt, U32.sub(nn, 1), Laws.doc.after(hh, ok)), + doc.lead(tt, U32.sub(nn, 1), Doc.check.after(hh, ok))) -# the `#` line right above line nn, to the rule and to the law +# the comment block above line nn, to the rule and to the law law doc.above: for +lines: List<&2, String> for +nn: U32 - {Doc.check.above(lines, nn) == Bool.and(Bool.not(U32.is_eq(nn, 0)), Laws.doc.hash(lines, U32.sub(nn, 1))) : Bool} + {Doc.check.above(lines, nn) == Laws.doc.lead(lines, nn, False{}) : Bool} def doc.above(lines, nn): - hole.and(Bool.not(U32.is_eq(nn, 0)), Doc.check.hash(lines, U32.sub(nn, 1)), Laws.doc.hash(lines, U32.sub(nn, 1)), - doc.hash(lines, U32.sub(nn, 1))) + doc.lead(lines, nn, False{}) # the kind and name test, to the rule and to the law law doc.needs: @@ -7243,12 +7244,12 @@ law doc.hit: def doc.hit(kk, name, line, _doc, lines): +ar = Bool.and(Doc.needs(kk), Bool.not(Doc.exempt(name))) +as = Bool.and(Laws.doc.kind(kk), Bool.not(Laws.doc.free(name))) - +ns = Bool.not(Bool.and(Bool.not(U32.is_eq(line, 0)), Laws.doc.hash(lines, U32.sub(line, 1)))) + +ns = Bool.not(Laws.doc.lead(lines, line, False{})) Equal.trans(Bool, Lazy.and_then(ar, _u => Bool.not(Doc.check.above(lines, line))), Bool.and(ar, ns), Bool.and(as, ns), hole.and(ar, Bool.not(Doc.check.above(lines, line)), ns, Equal.cong(Bool, Bool, z => Bool.not(z), Doc.check.above(lines, line), - Bool.and(Bool.not(U32.is_eq(line, 0)), Laws.doc.hash(lines, U32.sub(line, 1))), doc.above(lines, line))), + Laws.doc.lead(lines, line, False{}), doc.above(lines, line))), Equal.cong(Bool, Bool, z => Bool.and(z, ns), ar, as, doc.needs(kk, name))) # an item onto a rest the law holds for @@ -7328,6 +7329,133 @@ def unused.header(kids, rest, ih): Equal.cong(List<&2, U32>, List<&2, U32>, xs => List.append(&2, U32, Laws.unused.token_lines(Tree.leaves(kids)), xs), Unused.foreign(rest), Laws.unused.headers(rest), ih)) +# the rule's `:` test on a statement's chain is the law's +law unused.ends: + for kids: Tree.Node + for last: Bool + {Unused.foreign.ends(kids, last) == Laws.unused.ends(kids, last) : Bool} + +def unused.ends(kids, _last): + match kids: + case Tree.NCons{h, t}: + unused.ends(t, Unused.colon(h)) + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NNil{}: + {==} + +# the rule's import test is the law's +law unused.first: + for sk: Tree.StmtKind + {Unused.foreign.first(sk) == Laws.unused.is_import(sk) : Bool} + +def unused.first(sk): + match sk: + case Tree.SDef{}: + {==} + case Tree.SType{}: + {==} + case Tree.SLaw{}: + {==} + case Tree.SImport{}: + {==} + case Tree.SCase{}: + {==} + case Tree.SFor{}: + {==} + case Tree.SLet{}: + {==} + case Tree.STerm{}: + {==} + +# the rule's test for a body that opens with an import once the header is +# over is the law's, whether the header is still open or not +law unused.opens: + for body: Tree.Node + for open: Bool + {Unused.foreign.opens(body, open) == Laws.unused.opens(body, open) : Bool} + +def unused.opens(body, open): + match body: + case Tree.NCons{h, +rest}: + match h: + case Tree.Stmt{sk, +kids, b}: + match open: + case True{}: + Equal.trans(Bool, Unused.foreign.opens(rest, Bool.not(Unused.foreign.ends(kids, False{}))), + Laws.unused.opens(rest, Bool.not(Unused.foreign.ends(kids, False{}))), + Laws.unused.opens(rest, Bool.not(Laws.unused.ends(kids, False{}))), + unused.opens(rest, Bool.not(Unused.foreign.ends(kids, False{}))), + Equal.cong(Bool, Bool, z => Laws.unused.opens(rest, Bool.not(z)), Unused.foreign.ends(kids, False{}), + Laws.unused.ends(kids, False{}), unused.ends(kids, False{}))) + case False{}: + unused.first(sk) + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.NNil{}: + {==} + case Tree.NCons{x, y}: + {==} + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NNil{}: + {==} + +# a pick between lists equal branch by branch is equal +law unused.pick: + for c: Bool + for -a1: List<&2, U32> + for -a2: List<&2, U32> + for -b1: List<&2, U32> + for -b2: List<&2, U32> + for ea: {a1 == a2 : List<&2, U32>} + for eb: {b1 == b2 : List<&2, U32>} + {Bool.pick(List<&2, U32>, c, a1, b1) == Bool.pick(List<&2, U32>, c, a2, b2) : List<&2, U32>} + +def unused.pick(c, _a1, _a2, _b1, _b2, ea, eb): + match c: + case True{}: + ea + case False{}: + eb + +# a def's lines onto the lines after it, to the rule and to the law +law unused.def: + for +kids: Tree.Node + for +body: Tree.Node + for +rest: Tree.Node + for +ih: {Unused.foreign(rest) == Laws.unused.headers(rest) : List<&2, U32>} + {Bool.pick(List<&2, U32>, Unused.foreign.opens(body, Bool.not(Unused.foreign.ends(kids, False{}))), + Unused.lines(Tree.leaves(kids), Unused.foreign(rest)), Unused.foreign(rest)) + == Bool.pick(List<&2, U32>, Laws.unused.imported(kids, body), + List.append(&2, U32, Laws.unused.token_lines(Tree.leaves(kids)), Laws.unused.headers(rest)), + Laws.unused.headers(rest)) : List<&2, U32>} + +def unused.def(kids, body, rest, ih): + +rc = Unused.foreign.opens(body, Bool.not(Unused.foreign.ends(kids, False{}))) + +lc = Laws.unused.imported(kids, body) + +ra = Unused.lines(Tree.leaves(kids), Unused.foreign(rest)) + +la = List.append(&2, U32, Laws.unused.token_lines(Tree.leaves(kids)), Laws.unused.headers(rest)) + +ec = Equal.trans(Bool, rc, Laws.unused.opens(body, Bool.not(Unused.foreign.ends(kids, False{}))), lc, + unused.opens(body, Bool.not(Unused.foreign.ends(kids, False{}))), + Equal.cong(Bool, Bool, z => Laws.unused.opens(body, Bool.not(z)), Unused.foreign.ends(kids, False{}), + Laws.unused.ends(kids, False{}), unused.ends(kids, False{}))) + Equal.trans(List<&2, U32>, Bool.pick(List<&2, U32>, rc, ra, Unused.foreign(rest)), + Bool.pick(List<&2, U32>, lc, ra, Unused.foreign(rest)), + Bool.pick(List<&2, U32>, lc, la, Laws.unused.headers(rest)), + Equal.cong(Bool, List<&2, U32>, z => Bool.pick(List<&2, U32>, z, ra, Unused.foreign(rest)), rc, lc, ec), + unused.pick(lc, ra, la, Unused.foreign(rest), Laws.unused.headers(rest), unused.header(kids, rest, ih), ih)) + # the rule's foreign lines are the law's header lines law unused.foreign: for root: Tree.Node @@ -7349,46 +7477,10 @@ def unused.foreign(root): unused.foreign(rest) case Tree.Group{o, gk, cl}: unused.foreign(rest) - case Tree.Stmt{kind, +kids, body}: + case Tree.Stmt{kind, +kids, +body}: match kind: case Tree.SDef{}: - match body: - case Tree.Leaf{tok}: - unused.foreign(rest) - case Tree.Group{o, gk, cl}: - unused.foreign(rest) - case Tree.Stmt{bk, bs, bb}: - unused.foreign(rest) - case Tree.NNil{}: - unused.foreign(rest) - case Tree.NCons{bh, more}: - match bh: - case Tree.Leaf{tok}: - unused.foreign(rest) - case Tree.Group{o, gk, cl}: - unused.foreign(rest) - case Tree.NNil{}: - unused.foreign(rest) - case Tree.NCons{nh, nt}: - unused.foreign(rest) - case Tree.Stmt{ik, ks, ib}: - match ik: - case Tree.SDef{}: - unused.foreign(rest) - case Tree.SType{}: - unused.foreign(rest) - case Tree.SLaw{}: - unused.foreign(rest) - case Tree.SImport{}: - unused.header(kids, rest, unused.foreign(rest)) - case Tree.SCase{}: - unused.foreign(rest) - case Tree.SFor{}: - unused.foreign(rest) - case Tree.SLet{}: - unused.foreign(rest) - case Tree.STerm{}: - unused.foreign(rest) + unused.def(kids, body, rest, unused.foreign(rest)) case Tree.SType{}: unused.foreign(rest) case Tree.SLaw{}: @@ -21167,81 +21259,93 @@ def Laws.inert_pick(path, _text, tree, _toks, _bound, _items, _text2, tree2, _to # doc # --- -# a line that is a `#` line exactly when b says so -def inert.doc.line(bb: Bool) -> String: - match bb: - case True{}: "#" - case False{}: "" +# a line that starts as ll says +def inert.doc.line(ll: Laws.inert.Lead) -> String: + match ll: + case Laws.LHash{}: "#" + case Laws.LAt{}: "@" + case Laws.LPlain{}: "" -# the lines rebuilt from which of them start with `#` -def inert.doc.relines(bs: List<&2, Bool>) -> List<&2, String>: +# the lines rebuilt from how each of them starts +def inert.doc.relines(bs: List<&2, Laws.inert.Lead>) -> List<&2, String>: match bs: case Nil{}: Nil{} case Con{h, t}: inert.doc.line(h) <> inert.doc.relines(t) -# a line rebuilt from its `#` test starts with `#` as it did -law inert.doc.hash1: - for b: Bool - {String.starts_with(inert.doc.line(b), "#") == b : Bool} +# a line rebuilt from how it starts steps doc's read down as it did +law inert.doc.after1: + for b1: Bool + for b2: Bool + for +ok: Bool + {Doc.check.after(inert.doc.line(Laws.inert.lead(b1, b2)), ok) == Bool.or(b1, Bool.and(b2, ok)) : Bool} -def inert.doc.hash1(b): - match b: +def inert.doc.after1(b1, b2, _ok): + match b1: case True{}: {==} - case False{}: {==} + case False{}: + match b2: + case True{}: {==} + case False{}: {==} -# the `#` test on the lines rebuilt is the test on the lines -law inert.doc.hash: +# doc's read down the lines rebuilt is its read down the lines +law inert.doc.lead: for lines: List<&2, String> for +nn: U32 - {Doc.check.hash(inert.doc.relines(Laws.inert.hashes(lines)), nn) == Doc.check.hash(lines, nn) : Bool} + for +ok: Bool + {Doc.check.lead(inert.doc.relines(Laws.inert.leads(lines)), nn, ok) == Doc.check.lead(lines, nn, ok) : Bool} -def inert.doc.hash(lines, nn): +def inert.doc.lead(lines, nn, ok): match lines: case Nil{}: {==} - case Con{+hh, tt}: - +h1 = String.starts_with(hh, "#") - %inert.doc.hash1(h1) : {Lazy.stop(Bool, U32.is_eq(nn, 0), String.starts_with(inert.doc.line(h1), "#"), - _u => Doc.check.hash(inert.doc.relines(Laws.inert.hashes(tt)), U32.sub(nn, 1))) - == Lazy.stop(Bool, U32.is_eq(nn, 0), _, _u => Doc.check.hash(tt, U32.sub(nn, 1))) : Bool} - %inert.doc.hash(tt, U32.sub(nn, 1)) : {Lazy.stop(Bool, U32.is_eq(nn, 0), String.starts_with(inert.doc.line(h1), - "#"), - _u => Doc.check.hash(inert.doc.relines(Laws.inert.hashes(tt)), U32.sub(nn, 1))) - == Lazy.stop(Bool, U32.is_eq(nn, 0), String.starts_with(inert.doc.line(h1), "#"), _u => _) : Bool} - {==} + case Con{+hh, +tt}: + +a1 = Doc.check.after(inert.doc.line(Laws.inert.lead(String.starts_with(hh, "#"), String.starts_with(hh, "@"))), + ok) + +a2 = Doc.check.after(hh, ok) + +rt = inert.doc.relines(Laws.inert.leads(tt)) + Equal.cong(Bool, Bool, z => Lazy.stop(Bool, U32.is_eq(nn, 0), ok, _u => z), + Doc.check.lead(rt, U32.sub(nn, 1), a1), Doc.check.lead(tt, U32.sub(nn, 1), a2), + Equal.trans(Bool, Doc.check.lead(rt, U32.sub(nn, 1), a1), Doc.check.lead(rt, U32.sub(nn, 1), a2), + Doc.check.lead(tt, U32.sub(nn, 1), a2), + Equal.cong(Bool, Bool, z => Doc.check.lead(rt, U32.sub(nn, 1), z), a1, a2, + inert.doc.after1(String.starts_with(hh, "#"), String.starts_with(hh, "@"), ok)), + inert.doc.lead(tt, U32.sub(nn, 1), a2))) # doc's walk reads its items' kinds, names and lines, and of its lines only -# which start with `#` +# how each starts law inert.doc.go: for items: List<&2, Outline.Item> for +path: String for +lines: List<&2, String> - {Doc.check.go(Laws.inert.items(items), path, inert.doc.relines(Laws.inert.hashes(lines))) + {Doc.check.go(Laws.inert.items(items), path, inert.doc.relines(Laws.inert.leads(lines))) == Doc.check.go(items, path, lines) : List<&2, F.Finding>} def inert.doc.go(items, path, lines): match items: case Nil{}: {==} - case Con{Outline.Item{+k, +name, +line, +s, +d, +p}, +rest}: - +rl = inert.doc.relines(Laws.inert.hashes(lines)) - +lhs = Doc.check.go(Laws.inert.items(Outline.Item{k, name, line, s, d, p} <> rest), path, rl) - %inert.doc.hash(lines, U32.sub(line, 1)) : {lhs == Bool.pick(List<&2, F.Finding>, - Lazy.and_then(Bool.and(Doc.needs(k), - Bool.not(Doc.exempt(name))), _u => Bool.not(Lazy.and_then(Bool.not(U32.is_eq(line, 0)), _v => _))), - F.Finding{path, line, 0, 0, "doc", Doc.what(k) ++ " " ++ name ++ " has no comment above it."} - <> Doc.check.go(rest, path, lines), Doc.check.go(rest, path, lines)) : List<&2, F.Finding>} - %inert.doc.go(rest, path, lines) : {lhs == Bool.pick(List<&2, F.Finding>, Lazy.and_then(Bool.and(Doc.needs(k), - Bool.not(Doc.exempt(name))), _u => Bool.not(Lazy.and_then(Bool.not(U32.is_eq(line, 0)), - _v => Doc.check.hash(rl, U32.sub(line, 1))))), - F.Finding{path, line, 0, 0, "doc", Doc.what(k) ++ " " ++ name ++ " has no comment above it."} <> _, _) - : List<&2, F.Finding>} - {==} + case Con{Outline.Item{+k, +name, +line, s, d, p}, +rest}: + +rl = inert.doc.relines(Laws.inert.leads(lines)) + +x = {F.Finding{path, line, 0, 0, "doc", Doc.what(k) ++ " " ++ name ++ " has no comment above it."} : F.Finding} + +nd = Bool.and(Doc.needs(k), Bool.not(Doc.exempt(name))) + +m1 = Doc.check.go(Laws.inert.items(rest), path, rl) + +m2 = Doc.check.go(rest, path, lines) + Equal.trans(List<&2, F.Finding>, + Bool.pick(List<&2, F.Finding>, Lazy.and_then(nd, _u => Bool.not(Doc.check.above(rl, line))), x <> m1, m1), + Bool.pick(List<&2, F.Finding>, Lazy.and_then(nd, _u => Bool.not(Doc.check.above(lines, line))), x <> m1, m1), + Bool.pick(List<&2, F.Finding>, Lazy.and_then(nd, _u => Bool.not(Doc.check.above(lines, line))), x <> m2, m2), + Equal.cong(Bool, List<&2, F.Finding>, + z => Bool.pick(List<&2, F.Finding>, Lazy.and_then(nd, _u => Bool.not(z)), x <> m1, m1), + Doc.check.above(rl, line), Doc.check.above(lines, line), inert.doc.lead(lines, line, False{})), + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, + z => Bool.pick(List<&2, F.Finding>, Lazy.and_then(nd, _u => Bool.not(Doc.check.above(lines, line))), + x <> z, z), + m1, m2, inert.doc.go(rest, path, lines))) def Laws.inert_doc(path, text, toks, _tree, _bound, items, text2, toks2, _tree2, _bound2, items2, ei, el): +l1 = Doc.lines(text, toks) +l2 = Doc.lines(text2, toks2) - +r1 = Doc.check.go(Laws.inert.items(items), path, inert.doc.relines(Laws.inert.hashes(l1))) - +m = Doc.check.go(Laws.inert.items(items2), path, inert.doc.relines(Laws.inert.hashes(l1))) - +r2 = Doc.check.go(Laws.inert.items(items2), path, inert.doc.relines(Laws.inert.hashes(l2))) + +r1 = Doc.check.go(Laws.inert.items(items), path, inert.doc.relines(Laws.inert.leads(l1))) + +m = Doc.check.go(Laws.inert.items(items2), path, inert.doc.relines(Laws.inert.leads(l1))) + +r2 = Doc.check.go(Laws.inert.items(items2), path, inert.doc.relines(Laws.inert.leads(l2))) +w1 = Doc.check.go(items, path, l1) +w2 = Doc.check.go(items2, path, l2) Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, @@ -21249,12 +21353,12 @@ def Laws.inert_doc(path, text, toks, _tree, _bound, items, text2, toks2, _tree2, Equal.trans(List<&2, F.Finding>, w1, r1, w2, Equal.sym(List<&2, F.Finding>, r1, w1, inert.doc.go(items, path, l1)), Equal.trans(List<&2, F.Finding>, r1, m, w2, Equal.cong(List<&2, Outline.Item>, List<&2, F.Finding>, - z => Doc.check.go(z, path, inert.doc.relines(Laws.inert.hashes(l1))), Laws.inert.items(items), + z => Doc.check.go(z, path, inert.doc.relines(Laws.inert.leads(l1))), Laws.inert.items(items), Laws.inert.items(items2), ei), Equal.trans(List<&2, F.Finding>, m, r2, w2, - Equal.cong(List<&2, Bool>, List<&2, F.Finding>, - z => Doc.check.go(Laws.inert.items(items2), path, inert.doc.relines(z)), Laws.inert.hashes(l1), - Laws.inert.hashes(l2), el), + Equal.cong(List<&2, Laws.inert.Lead>, List<&2, F.Finding>, + z => Doc.check.go(Laws.inert.items(items2), path, inert.doc.relines(z)), Laws.inert.leads(l1), + Laws.inert.leads(l2), el), inert.doc.go(items2, path, l2))))) # param @@ -28889,6 +28993,106 @@ def inert.unused.lines(kids, acc): Unused.lines(inert.canons(List.reverse.go(&2, Lex.Tok, lo, [])), acc), inert.canon_lines(List.reverse.go(&2, Lex.Tok, lo, []), acc)))) +# a node's `:` test, the node read that way, is the one it was +law inert.unused.colon: + for nn: Tree.Node + {Unused.colon(Laws.inert.node(nn)) == Unused.colon(nn) : Bool} + +def inert.unused.colon(nn): + match nn: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, t, l, c}: {==} + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{x, y, z}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + +# a statement's `:` ending, its chain read that way, is the one it was +law inert.unused.ends: + for kids: Tree.Node + for last: Bool + {Unused.foreign.ends(Laws.inert.node(kids), last) == Unused.foreign.ends(kids, last) : Bool} + +def inert.unused.ends(kids, _last): + match kids: + case Tree.NCons{+h, +t}: + Equal.trans(Bool, Unused.foreign.ends(Laws.inert.node(t), Unused.colon(Laws.inert.node(h))), + Unused.foreign.ends(Laws.inert.node(t), Unused.colon(h)), Unused.foreign.ends(t, Unused.colon(h)), + Equal.cong(Bool, Bool, z => Unused.foreign.ends(Laws.inert.node(t), z), Unused.colon(Laws.inert.node(h)), + Unused.colon(h), inert.unused.colon(h)), + inert.unused.ends(t, Unused.colon(h))) + case Tree.Leaf{x}: {==} + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{x, y, z}: {==} + case Tree.NNil{}: {==} + +# a body's opening import, the body read that way, is the one it was +law inert.unused.opens: + for body: Tree.Node + for open: Bool + {Unused.foreign.opens(Laws.inert.node(body), open) == Unused.foreign.opens(body, open) : Bool} + +def inert.unused.opens(body, open): + match body: + case Tree.NCons{h, +rest}: + match h: + case Tree.Stmt{sk, +kids, b}: + match open: + case True{}: + Equal.trans(Bool, + Unused.foreign.opens(Laws.inert.node(rest), + Bool.not(Unused.foreign.ends(Laws.inert.node(kids), False{}))), + Unused.foreign.opens(Laws.inert.node(rest), Bool.not(Unused.foreign.ends(kids, False{}))), + Unused.foreign.opens(rest, Bool.not(Unused.foreign.ends(kids, False{}))), + Equal.cong(Bool, Bool, z => Unused.foreign.opens(Laws.inert.node(rest), Bool.not(z)), + Unused.foreign.ends(Laws.inert.node(kids), False{}), Unused.foreign.ends(kids, False{}), + inert.unused.ends(kids, False{})), + inert.unused.opens(rest, Bool.not(Unused.foreign.ends(kids, False{})))) + case False{}: {==} + case Tree.Leaf{x}: {==} + case Tree.Group{x, y, z}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + case Tree.Leaf{x}: {==} + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{x, y, z}: {==} + case Tree.NNil{}: {==} + +# a def's lines onto the lines after it, the tree read that way, are the ones +# they were +law inert.unused.def: + for +kids: Tree.Node + for +body: Tree.Node + for +rest: Tree.Node + for +ih: {Unused.foreign(Laws.inert.node(rest)) == Unused.foreign(rest) : List<&2, U32>} + {Bool.pick(List<&2, U32>, + Unused.foreign.opens(Laws.inert.node(body), Bool.not(Unused.foreign.ends(Laws.inert.node(kids), False{}))), + Unused.lines(Tree.leaves(Laws.inert.node(kids)), Unused.foreign(Laws.inert.node(rest))), + Unused.foreign(Laws.inert.node(rest))) + == Bool.pick(List<&2, U32>, Unused.foreign.opens(body, Bool.not(Unused.foreign.ends(kids, False{}))), + Unused.lines(Tree.leaves(kids), Unused.foreign(rest)), Unused.foreign(rest)) : List<&2, U32>} + +def inert.unused.def(kids, body, rest, ih): + +fi = Unused.foreign(Laws.inert.node(rest)) + +fo = Unused.foreign(rest) + +ra = Unused.lines(Tree.leaves(Laws.inert.node(kids)), fi) + +rb = Unused.lines(Tree.leaves(kids), fo) + +c1 = Unused.foreign.opens(Laws.inert.node(body), Bool.not(Unused.foreign.ends(Laws.inert.node(kids), False{}))) + +c2 = Unused.foreign.opens(body, Bool.not(Unused.foreign.ends(kids, False{}))) + +ec = Equal.trans(Bool, c1, + Unused.foreign.opens(Laws.inert.node(body), Bool.not(Unused.foreign.ends(kids, False{}))), c2, + Equal.cong(Bool, Bool, z => Unused.foreign.opens(Laws.inert.node(body), Bool.not(z)), + Unused.foreign.ends(Laws.inert.node(kids), False{}), Unused.foreign.ends(kids, False{}), + inert.unused.ends(kids, False{})), + inert.unused.opens(body, Bool.not(Unused.foreign.ends(kids, False{})))) + +ea = Equal.trans(List<&2, U32>, ra, Unused.lines(Tree.leaves(kids), fi), rb, inert.unused.lines(kids, fi), + Equal.cong(List<&2, U32>, List<&2, U32>, z => Unused.lines(Tree.leaves(kids), z), fi, fo, ih)) + Equal.trans(List<&2, U32>, Bool.pick(List<&2, U32>, c1, ra, fi), Bool.pick(List<&2, U32>, c2, ra, fi), + Bool.pick(List<&2, U32>, c2, rb, fo), + Equal.cong(Bool, List<&2, U32>, z => Bool.pick(List<&2, U32>, z, ra, fi), c1, c2, ec), + unused.pick(c2, ra, rb, fi, fo, ea, ih)) + # the foreign defs' header lines, the tree read that way, are the ones they were law inert.unused.foreign: for root: Tree.Node @@ -28898,34 +29102,9 @@ def inert.unused.foreign(root): match root: case Tree.NCons{h, +rest}: match h: - case Tree.Stmt{sk, +kids, body}: + case Tree.Stmt{sk, +kids, +body}: match sk: - case Tree.SDef{}: - match body: - case Tree.NCons{b1, more}: - match b1: - case Tree.Stmt{sk2, ik, ib}: - match sk2: - case Tree.SImport{}: - %inert.unused.foreign(rest) : {Unused.lines(Tree.leaves(Laws.inert.node(kids)), - Unused.foreign(Laws.inert.node(rest))) == Unused.lines(Tree.leaves(kids), _) - : List<&2, U32>} - inert.unused.lines(kids, Unused.foreign(Laws.inert.node(rest))) - case Tree.SDef{}: inert.unused.foreign(rest) - case Tree.SType{}: inert.unused.foreign(rest) - case Tree.SLaw{}: inert.unused.foreign(rest) - case Tree.SCase{}: inert.unused.foreign(rest) - case Tree.SFor{}: inert.unused.foreign(rest) - case Tree.SLet{}: inert.unused.foreign(rest) - case Tree.STerm{}: inert.unused.foreign(rest) - case Tree.Leaf{x}: inert.unused.foreign(rest) - case Tree.Group{x, y, z}: inert.unused.foreign(rest) - case Tree.NNil{}: inert.unused.foreign(rest) - case Tree.NCons{x, y}: inert.unused.foreign(rest) - case Tree.Leaf{x}: inert.unused.foreign(rest) - case Tree.Group{x, y, z}: inert.unused.foreign(rest) - case Tree.Stmt{x, y, z}: inert.unused.foreign(rest) - case Tree.NNil{}: inert.unused.foreign(rest) + case Tree.SDef{}: inert.unused.def(kids, body, rest, inert.unused.foreign(rest)) case Tree.SType{}: inert.unused.foreign(rest) case Tree.SLaw{}: inert.unused.foreign(rest) case Tree.SImport{}: inert.unused.foreign(rest) diff --git a/src/rules/style/doc.bend b/src/rules/style/doc.bend index 53f6591..7f087e9 100644 --- a/src/rules/style/doc.bend +++ b/src/rules/style/doc.bend @@ -1,8 +1,9 @@ # rule doc: every top-level def, type and law has a comment block right above # it: one or more column-0 `#` lines with no blank line between them and the -# item. A block of bare `#` lines counts, though its text is empty; a line -# that starts inside a multi-line string literal is text, never a comment -# line. Helpers +# item, save a run of column-0 `@` lines (attributes such as `@unsafe`) that +# may sit between the block and the item. A block of bare `#` lines counts, +# though its text is empty; a line that starts inside a multi-line string +# literal is text, never a comment line. Helpers # (dotted names like `show.go`) ride on their parent's doc, `main` needs none, # PROOF.bend fills laws that LAWS.bend already documents, and a test (under # tests/) is documented by its header and its check names. @@ -40,20 +41,27 @@ def what(kk: Outline.ItemKind) -> String: case other: "Def" -# is line nn of the lines a comment line (its first char `#`)? -def check.hash(lines: List<&2, String>, +nn: U32) -> Bool: +# reading down, does a comment block end right above the next line? After a +# comment line (its first char `#`) it does; an attribute line (`@unsafe`) +# keeps what was above it; any other line ends it +def check.after(+hh: String, ok: Bool) -> Bool: + Bool.or(String.starts_with(hh, "#"), Bool.and(String.starts_with(hh, "@"), ok)) + +# reading lines 0 to nn - 1 down from ok: does a comment block end right +# above line nn, past a run of attribute lines? +def check.lead(lines: List<&2, String>, +nn: U32, +ok: Bool) -> Bool: match lines: case Nil{}: - False{} + Bool.and(U32.is_eq(nn, 0), ok) case Con{hh, tt}: - Lazy.stop(Bool, U32.is_eq(nn, 0), String.starts_with(hh, "#"), _u => check.hash(tt, U32.sub(nn, 1))) + Lazy.stop(Bool, U32.is_eq(nn, 0), ok, _u => check.lead(tt, U32.sub(nn, 1), check.after(hh, ok))) -# is there a comment line right above line nn? A block of bare `#` lines -# counts, though its doc text is empty. An item's comment block always ends -# on the line right above it, so this test alone decides: the doc text, what -# the comments say, is never read +# is there a comment line right above line nn, or right above the attribute +# lines right above it? A block of bare `#` lines counts, though its doc text +# is empty. An item's comment block always ends there, so this test alone +# decides: the doc text, what the comments say, is never read def check.above(+lines: List<&2, String>, +nn: U32) -> Bool: - Lazy.and_then(Bool.not(U32.is_eq(nn, 0)), _u => check.hash(lines, U32.sub(nn, 1))) + check.lead(lines, nn, False{}) def check.go(items: List<&2, Outline.Item>, +path: String, +lines: List<&2, String>) -> List<&2, F.Finding>: match items: diff --git a/src/rules/suspicious/unused.bend b/src/rules/suspicious/unused.bend index d43460e..26247ce 100644 --- a/src/rules/suspicious/unused.bend +++ b/src/rules/suspicious/unused.bend @@ -1,10 +1,13 @@ # rule unused: a name bound by a let, a do-bind, a lambda, or as a parameter -# is never used. Pattern binders are exempt: naming every field of -# `Tok{k, t, l, c}` reads better than `_`. So are names starting with `_`, -# erased parameters (`-x`), which exist to be unused, a law's `for` names -# (hypotheses the proof takes by position), and every parameter of a foreign -# def (one whose body starts with `import`), which its C and JS bodies read, -# however its header is wrapped. +# is never used. A name read anywhere is a use, in a dependent arrow's types +# too (`@+x: U32 -> S` reads `S`). Pattern binders are exempt: naming every +# field of `Tok{k, t, l, c}` reads better than `_`. So are names starting +# with `_`, erased parameters (`-x`), which exist to be unused, a law's `for` +# names (hypotheses the proof takes by position), and every parameter of a +# foreign def, which its C and JS bodies read: one whose body's first +# statement is `import`, wherever its header's `->` and return type fall (a +# header that does not end in `:` runs on through the body's statements up +# to one that does, as `-> IO(T):` on the line after `def f(..) ->`). import Base import ../../src.bend as Src import ../../lazy/lazy.bend as Lazy @@ -21,12 +24,61 @@ def lines(ts: List<&2, Lex.Tok>, acc: List<&2, U32>) -> List<&2, U32>: case Con{Lex.Tok{k, t, l, c}, rest}: l <> lines(rest, acc) -# every header line of the defs whose body is `import "./x.c"`, however the -# header is wrapped +# is a token of this kind a `:`? +def colon.kind(kk: Lex.TokKind) -> Bool: + match kk: + case Lex.TColon{}: + True{} + case other: + False{} + +# is the node a `:` leaf? +def colon(nn: Tree.Node) -> Bool: + match nn: + case Tree.Leaf{Lex.Tok{k, _t, _l, _c}}: + colon.kind(k) + case other: + False{} + +# does a statement's own chain end in a `:` leaf? last: whether the node +# before the chain did +def foreign.ends(kids: Tree.Node, last: Bool) -> Bool: + match kids: + case Tree.NCons{h, t}: + foreign.ends(t, colon(h)) + case other: + last + +# is the statement an import? +def foreign.first(sk: Tree.StmtKind) -> Bool: + match sk: + case Tree.SImport{}: + True{} + case other: + False{} + +# does the body open with an import once the def's header is over? While the +# header is open (its tokens so far do not end in `:`), each statement is more +# of it: `-> IO(T):` on the line after `def f(..) ->` +def foreign.opens(body: Tree.Node, open: Bool) -> Bool: + match body: + case Tree.NCons{Tree.Stmt{sk, kids, _b}, rest}: + match open: + case True{}: + foreign.opens(rest, Bool.not(foreign.ends(kids, False{}))) + case False{}: + foreign.first(sk) + case other: + False{} + +# every header line of the defs whose body is `import "./x.c"`, wherever the +# header's `->` and return type fall def foreign(root: Tree.Node) -> List<&2, U32>: match root: - case Tree.NCons{Tree.Stmt{Tree.SDef{}, kids, Tree.NCons{Tree.Stmt{Tree.SImport{}, ik, ib}, more}}, rest}: - lines(Tree.leaves(kids), foreign(rest)) + case Tree.NCons{Tree.Stmt{Tree.SDef{}, +kids, body}, rest}: + +more = foreign(rest) + +own = lines(Tree.leaves(kids), more) + Bool.pick(List<&2, U32>, foreign.opens(body, Bool.not(foreign.ends(kids, False{}))), own, more) case Tree.NCons{other, rest}: foreign(rest) case other: diff --git a/src/syntax/LAWS.bend b/src/syntax/LAWS.bend index ca940f0..c289281 100644 --- a/src/syntax/LAWS.bend +++ b/src/syntax/LAWS.bend @@ -428,3 +428,55 @@ law groups: exs o: Bind.Out {Bind.walk(Tree.NCons{Tree.Group{open, gkids, close}, rest}, Bind.MTerm{}, env, ns, out) == Bind.walk(rest, Bind.MTerm{}, env, ns, o) : Bind.W} + +# LAW: a statement led by `@`, a name and a `:` is a dependent arrow, a term, +# never a def, whatever the name and whatever follows +law arrow_term: + for +at: String + for +al: U32 + for +ac: U32 + for +x: String + for +xl: U32 + for +xc: U32 + for +ct: String + for +cl: U32 + for +cc: U32 + for +rest: Tree.Node + {Tree.classify(Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TAll{}, at, al, ac}}, Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, x, + xl, xc}}, Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, ct, cl, cc}}, rest}}}) == Tree.STerm{} : Tree.StmtKind} + +# LAW: so is one whose name carries a quantity mark (`@+x:`, `@-x:`) +law marked_arrow_term: + for +at: String + for +al: U32 + for +ac: U32 + for +mt: String + for +ml: U32 + for +mc: U32 + for +x: String + for +xl: U32 + for +xc: U32 + for +ct: String + for +cl: U32 + for +cc: U32 + for +rest: Tree.Node + {Tree.classify(Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TAll{}, at, al, ac}}, + Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TOp{}, mt, ml, mc}}, + Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, x, xl, xc}}, + Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, ct, cl, cc}}, rest}}}}) == Tree.STerm{} : Tree.StmtKind} + +# LAW: a statement led by an attribute, `@` and a name then a keyword +# (`@unsafe def`), is a def, whatever follows +law attribute_def: + for +at: String + for +al: U32 + for +ac: U32 + for +x: String + for +xl: U32 + for +xc: U32 + for +kt: String + for +kl: U32 + for +kc: U32 + for +rest: Tree.Node + {Tree.classify(Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TAll{}, at, al, ac}}, Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, x, + xl, xc}}, Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TKey{}, kt, kl, kc}}, rest}}}) == Tree.SDef{} : Tree.StmtKind} diff --git a/src/syntax/PROOF.bend b/src/syntax/PROOF.bend index cec47da..e58dd45 100644 --- a/src/syntax/PROOF.bend +++ b/src/syntax/PROOF.bend @@ -3942,3 +3942,12 @@ def Laws.lets(kk, kids, body, rest, env, ns, out, e): Empty.absurd(rs.lets.ty(Tree.SCase{}, kids, body, rest, env, ns, out), true_false(e)) case Tree.STerm{}: Empty.absurd(rs.lets.ty(Tree.STerm{}, kids, body, rest, env, ns, out), true_false(e)) + +def Laws.arrow_term(_at, _al, _ac, _x, _xl, _xc, _ct, _cl, _cc, _rest): + {==} + +def Laws.marked_arrow_term(_at, _al, _ac, _mt, _ml, _mc, _x, _xl, _xc, _ct, _cl, _cc, _rest): + {==} + +def Laws.attribute_def(_at, _al, _ac, _x, _xl, _xc, _kt, _kl, _kc, _rest): + {==} diff --git a/src/syntax/tree.bend b/src/syntax/tree.bend index 43616ed..7c62bbe 100644 --- a/src/syntax/tree.bend +++ b/src/syntax/tree.bend @@ -18,7 +18,8 @@ import ./lex.bend as Lex # what a statement is, by its shape: SDef `def f(..)` (also `@unsafe def`), # SType, SLaw, SImport, SCase `case p:`, SFor `for x: T` / `exs x: T`, SLet # (a `=` or `<-` among its own tokens), else STerm (`match x:`, `do M:`, -# `return e`, a call) +# `return e`, a call, and a dependent arrow `@x: A -> B` or `@+x: A -> B`, +# which an `@` does not make a def) type StmtKind is Data: SDef{} SType{} @@ -305,13 +306,32 @@ def keyword_kind(+tt: String) -> StmtKind: Bool.pick(StmtKind, String.eq(tt, "case"), SCase{}, Bool.pick(StmtKind, Bool.or(String.eq(tt, "for"), String.eq(tt, "exs")), SFor{}, STerm{})))))) +# does the chain after an `@` start with a binder's name and a `:`? +def arrow.named(rest: Node) -> Bool: + match rest: + case NCons{Leaf{Lex.Tok{Lex.TName{}, _t, _l, _c}}, NCons{Leaf{Lex.Tok{Lex.TColon{}, _ct, _cl, _cc}}, _r}}: + True{} + case NCons{Leaf{Lex.Tok{Lex.TUpper{}, _t, _l, _c}}, NCons{Leaf{Lex.Tok{Lex.TColon{}, _ct, _cl, _cc}}, _r}}: + True{} + case _other: + False{} + +# does the chain after an `@` bind a name, `@x:` or with a quantity mark +# `@+x:`, as a dependent arrow does, rather than name an attribute (`@unsafe`)? +def arrow(rest: Node) -> Bool: + match rest: + case NCons{Leaf{Lex.Tok{Lex.TOp{}, _t, _l, _c}}, more}: + arrow.named(more) + case other: + arrow.named(other) + # a statement's kind from its own tokens def classify(kids: Node) -> StmtKind: match kids: case NCons{Leaf{Lex.Tok{Lex.TKey{}, t, l, c}}, rest}: keyword_kind(t) case NCons{Leaf{Lex.Tok{Lex.TAll{}, t, l, c}}, rest}: - SDef{} + Bool.pick(StmtKind, arrow(rest), STerm{}, SDef{}) case other: Bool.pick(StmtKind, binds_in(other), SLet{}, STerm{}) From ae55302c49b8f3959cfdb9545db3ee68fb7d935e Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 14:17:28 +0000 Subject: [PATCH 5/6] fix(rules): retire argv (U014) before its first release A false-positive audit of argv put its precision at 8%: every IO.args() reader in the ecosystem already drops the program name, and the rule cannot tell a correct reader from a wrong one, so nearly every finding asked for a noqa. It merged in #226 and was never released, so it goes now: the rule, its registration, its code-table row, its opt-in entry, the laws argv_counts, inert_argv and argv_opt_in with their proofs, the BOLT-RULE-U014 row, and bolt's own setting and noqa for it. U014 stays reserved: codes are append-only, and src/codes.bend and src/README.md list it as retired beside C001, U005 and L004. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B --- SPEC.md | 3 +- bolt.bend | 5 - src/LAWS.bend | 9 - src/PROOF.bend | 13 +- src/README.md | 16 +- src/args.bend | 2 +- src/codes.bend | 4 +- src/config.bend | 5 +- src/rules.bend | 2 - src/rules/LAWS.bend | 59 ------- src/rules/PROOF.bend | 295 --------------------------------- src/rules/suspicious/argv.bend | 57 ------- 12 files changed, 15 insertions(+), 455 deletions(-) delete mode 100644 src/rules/suspicious/argv.bend diff --git a/SPEC.md b/SPEC.md index 44318a7..a9ddcda 100644 --- a/SPEC.md +++ b/SPEC.md @@ -46,7 +46,6 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-RULE-U011 | `rewalk` reports exactly, in each straight piece of a def that is not a law or a proof (its body outside case arms, or one case arm's body), each call of a walk (a looping def of the file other than the def itself, or a listed Base walk) whose result is read for a single value (indexed on the spot, an accessor's collection argument, or alone the right of an `=` let of one name that is a record field or is read at least once and only indexed or as an accessor's collection argument) and follows no twin so read, when a twin keeps its result whole: another call in the piece, at another position, of the same walk on the same argument (the same text, and the same number of lets before it of each name in it). | Proved | proved | src/rules/LAWS.bend rewalk_local_counts; src/rules/LAWS.bend rewalk_visit_counts; src/rules/LAWS.bend rewalk_counts | | BOLT-RULE-U012 | `unit` reports exactly a multiply or divide by one on a recursive step. | Proved | proved | src/rules/LAWS.bend unit_walk_counts; src/rules/LAWS.bend unit_counts | | BOLT-RULE-U013 | `scan` reports exactly, outside a LAWS.bend or a PROOF.bend, in a def that calls itself and is not a proof, outside a lambda's body (the rest of a chain after `=>`), a case pattern, and a case arm that does not call the def: each call, a plain or dotted name token then a `(` group, of a callee other than the def, one of whose walked arguments is exactly the lone name of a parameter that every self-call passes back as that same lone name in its own position (carried). A callee walks argument 2 of `List.contains`, `List.find`, `List.filter` and `List.length`, 3 of `List.any` and `List.all`, and 4 of `List.foldl` and `List.foldr` (the Base list searches); a def of the file walks, when it calls itself, its first live parameter that some self-call does not pass back unchanged, unless that parameter's type is `Nat` or `String`, and each parameter its body passes, anywhere, as the lone name of an argument a call of a Base search or of a def listed before it walks. One finding per call. | Proved | proved | src/rules/LAWS.bend scan_counts; src/rules/LAWS.bend scan_quiet; src/rules/LAWS.bend scan_slots | -| BOLT-RULE-U014 | `argv` reports exactly one finding for each `IO.args` token with a `(` token right after it among the significant tokens, in every file (no path is exempt), and nothing else. It is opt-in: with no setting of its own it is off, whatever its group says (BOLT-CFG-6). | Proved | proved | src/rules/LAWS.bend argv_counts; src/rules/LAWS.bend inert_argv; src/LAWS.bend argv_opt_in | | BOLT-RULE-U015 | `thunk` (opt-in) reports exactly, in a def, a lambda whose body is exactly a self-call and whose parameter that call does not read, passed as the one lambda of a call: in the kids of a group opened by `(` (its arguments: the kids split at their comma leaves), exactly one argument holding, among its own nodes and not inside a group, a leaf whose text is `=>`, four nodes in a row of those kids, a leaf of a name kind (the parameter), a leaf whose text is `=>`, a leaf whose text is the def's name, and a `(` group, the kids ending right after the group or going on with a comma, and no name leaf in the group, at any depth, spelling the parameter or the parameter then a dot; such groups found at any depth; one finding for each, on the def's name, and nothing else. A call given two or more lambdas (a dispatch) gets none. | Proved | proved | src/rules/LAWS.bend thunk_walk_counts; src/rules/LAWS.bend thunk_counts | | BOLT-RULE-U016 | `fromrev` reports exactly, outside a LAWS.bend or a PROOF.bend, one finding (on the first) for each run of four tokens right after one another among the significant tokens (spaces, newlines and comments dropped) whose texts are `String.from_list`, `(`, `List.reverse` and `(`, and nothing else: anything between them, another `(` included, is not the shape, and neither is `List.reverse.go`. | Proved | proved | src/rules/LAWS.bend fromrev_counts; src/rules/LAWS.bend fromrev_exempt; src/rules/LAWS.bend inert_fromrev | | BOLT-RULE-S001 | `doc` reports exactly a top-level def, type or law with no comment block right above it, or right above a run of `@` lines (attributes such as `@unsafe`) right above it, with the header's exemptions. | Proved | proved | src/rules/LAWS.bend doc_walk_counts; src/rules/LAWS.bend doc_counts | @@ -56,7 +55,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-RULE-S005 | `noqa` reports exactly, at each noqa comment's line and column (BOLT-OUT-7), one finding for a bare one (`#`, any spaces, then `noqa` at the comment's end or before a space) and one for each code it names that no graded finding of its file on its line has, a code that is no rule's included, where a project rule's code (`coverage`, `unsafe`, `trace`) is judged only when the run is the whole tree and never in the editor, and nothing else. It runs after the filter, over the findings of every other rule, so its findings come last (BOLT-OUT-3) and no noqa comment silences them: a `# noqa: S005` silences nothing and is itself reported. | Proved | proved | src/LAWS.bend noqa_counts; src/LAWS.bend noqa_bare; src/LAWS.bend noqa_bare_text | | BOLT-RULE-P001 | `tail` reports exactly a non-tail self-call outside any `Bool.pick(..)` in a def whose first live parameter's type is a List or String, whether or not the call shrinks it. | Proved | proved | src/rules/LAWS.bend tail_walk_counts; src/rules/LAWS.bend tail_counts | | BOLT-RULE-EXEMPT | For every text, a per-file rule's check on a path its header exempts returns no findings. The cost rules (`pick`, `strict`, `eager`, `tail`, `concat`, `index`, `table`, `hoist`, `ring`, `rewalk`, `unit`, `scan`, `thunk`) also skip, wherever it is, every def that is a proof: one whose signature returns a proof (`-> {a == b : T}`), or one written with no type at all (no `:` among its parameters and no `->`, as `def f(x, y):`), which is how Bend fills the law named f; their "reports exactly" rows are read with that skip. | Proved | proved | src/rules/LAWS.bend untyped_exempt; src/rules/LAWS.bend hole_exempt; src/rules/LAWS.bend doc_exempt; src/rules/LAWS.bend param_exempt; src/rules/LAWS.bend pick_exempt; src/rules/LAWS.bend tail_exempt; src/rules/LAWS.bend concat_exempt; src/rules/LAWS.bend eager_exempt; src/rules/LAWS.bend rewalk_exempt; src/rules/LAWS.bend strict_exempt; src/rules/LAWS.bend hoist_exempt; src/rules/LAWS.bend index_exempt; src/rules/LAWS.bend ring_exempt; src/rules/LAWS.bend table_exempt; src/rules/LAWS.bend unit_exempt; src/rules/LAWS.bend scan_exempt; src/rules/LAWS.bend thunk_exempt; src/rules/LAWS.bend fromrev_exempt | -| BOLT-RULE-INERT | For every rule whose pattern is code (all but `escape`, `strings`, `chars`, `space`, `twice`, `foreign`, `noqa` and `rewalk`), changing the contents of a comment or string literal does not change the findings. | Proved | proved | src/rules/LAWS.bend inert_hole; src/rules/LAWS.bend inert_put; src/rules/LAWS.bend inert_tail; src/rules/LAWS.bend inert_pick; src/rules/LAWS.bend inert_strict; src/rules/LAWS.bend inert_doc; src/rules/LAWS.bend inert_param; src/rules/LAWS.bend inert_table; src/rules/LAWS.bend inert_index; src/rules/LAWS.bend inert_concat; src/rules/LAWS.bend inert_unit; src/rules/LAWS.bend inert_eager; src/rules/LAWS.bend inert_fuel; src/rules/LAWS.bend inert_ring; src/rules/LAWS.bend inert_arms; src/rules/LAWS.bend inert_unused; src/rules/LAWS.bend inert_hoist; src/rules/LAWS.bend inert_wrap; src/rules/LAWS.bend inert_scan; src/rules/LAWS.bend inert_argv; src/rules/LAWS.bend inert_thunk; src/rules/LAWS.bend inert_fromrev | +| BOLT-RULE-INERT | For every rule whose pattern is code (all but `escape`, `strings`, `chars`, `space`, `twice`, `foreign`, `noqa` and `rewalk`), changing the contents of a comment or string literal does not change the findings. | Proved | proved | src/rules/LAWS.bend inert_hole; src/rules/LAWS.bend inert_put; src/rules/LAWS.bend inert_tail; src/rules/LAWS.bend inert_pick; src/rules/LAWS.bend inert_strict; src/rules/LAWS.bend inert_doc; src/rules/LAWS.bend inert_param; src/rules/LAWS.bend inert_table; src/rules/LAWS.bend inert_index; src/rules/LAWS.bend inert_concat; src/rules/LAWS.bend inert_unit; src/rules/LAWS.bend inert_eager; src/rules/LAWS.bend inert_fuel; src/rules/LAWS.bend inert_ring; src/rules/LAWS.bend inert_arms; src/rules/LAWS.bend inert_unused; src/rules/LAWS.bend inert_hoist; src/rules/LAWS.bend inert_wrap; src/rules/LAWS.bend inert_scan; src/rules/LAWS.bend inert_thunk; src/rules/LAWS.bend inert_fromrev | ### Laws rules (BOLT-LAW) diff --git a/bolt.bend b/bolt.bend index e1fd204..c77dfc2 100644 --- a/bolt.bend +++ b/bolt.bend @@ -36,8 +36,3 @@ def trace() -> String: # a loop that walks a list it carries unchanged, on every step def scan() -> String: "error" - -# a direct IO.args() read: the one reader, src/args.bend's, drops the -# program and says so with a noqa -def argv() -> String: - "error" diff --git a/src/LAWS.bend b/src/LAWS.bend index 6e777a2..efff0e8 100644 --- a/src/LAWS.bend +++ b/src/LAWS.bend @@ -159,15 +159,6 @@ law opt_in_off: for h_rule: {Config.set_level(sets, rule) == None{} : Maybe<&2, Config.Level>} {Config.level(Config.Config{sets}, group, rule) == Config.Off{} : Config.Level} -# LAW: argv is opt-in: with no setting of its own it is off, whatever its -# group says, so it reports on no project that did not name it -# BOLT-RULE-U014 -law argv_opt_in: - for +sets: List<&2, Config.LevelSet> - for +group: String - for h_rule: {Config.set_level(sets, "argv") == None{} : Maybe<&2, Config.Level>} - {Config.level(Config.Config{sets}, group, "argv") == Config.Off{} : Config.Level} - # Unknown names (BOLT-CFG-7). The specs below are strict folds over the code # table, written apart from config.bend's lookups. diff --git a/src/PROOF.bend b/src/PROOF.bend index 60f6685..c32a33f 100644 --- a/src/PROOF.bend +++ b/src/PROOF.bend @@ -148,9 +148,6 @@ def Laws.opt_in_off(sets, group, rule, h_opt, h_rule): == Config.Off{} : Config.Level} {==} -def Laws.argv_opt_in(sets, group, h_rule): - Laws.opt_in_off(sets, group, "argv", {==}, h_rule) - # Unknown names (BOLT-CFG-7). config.bend looks a slug up with Codes.find and # a group with an early-exit fold; the spec folds both strictly. Each step # lemma takes the comparison it branches on as a variable and cases on it. @@ -252,7 +249,7 @@ def Laws.unknown_exact(ss): def Laws.settings_graded(_text): {==} -# one arm per row of the code table (35), each checked by evaluation, and one +# one arm per row of the code table (34), each checked by evaluation, and one # past its end, where both sides are none: a new rule is a new arm here def Laws.slug_finds_row(n): match n: @@ -324,9 +321,7 @@ def Laws.slug_finds_row(n): {==} case 33n: {==} - case 34n: - {==} - case 35n+_p: + case 34n+_p: {==} # the same arms, looked up by code @@ -400,9 +395,7 @@ def Laws.code_finds_row(n): {==} case 33n: {==} - case 34n: - {==} - case 35n+_p: + case 34n+_p: {==} def Laws.shown(_path, _line, _col, _len, _rule, _msg, _level): diff --git a/src/README.md b/src/README.md index b673ad6..56d62e8 100644 --- a/src/README.md +++ b/src/README.md @@ -51,7 +51,7 @@ unset group has its default. The groups: | group | rules | default | |---------------|----------------------------------------------------------------------------------|---------| | `correctness` | `hole` `pick` `put` `arms` `escape` `twice` `strings` `chars` `foreign` `setting` | error | -| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` `fromrev` (`scan`, `argv`, `thunk`: opt-in) | warn | +| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` `fromrev` (`scan`, `thunk`: opt-in) | warn | | `style` | `doc` `space` `wrap` `param` `noqa` | warn | | `laws` | `coverage` `closed` `unsafe` (`trace`: opt-in) | warn | | `pedantic` | `tail` | off | @@ -73,7 +73,7 @@ The stable codes, assigned once (do not renumber): | C011 | `setting` | U011 | `rewalk` | P001 | `tail` | | | | U012 | `unit` | | | | | | U013 | `scan` | | | -| | | U014 | `argv` | | | +| | | U014 | retired | | | | | | U015 | `thunk` | | | | | | U016 | `fromrev` | | | @@ -81,7 +81,10 @@ Letters: `C` correctness, `U` suspicious, `S` style, `L` laws, `P` pedantic. `pedantic` is advice that is noisy on idiomatic code: off until a project asks for it. L004 was `quantify`, the opt-in strict mode of `closed`; -`closed` is strict itself now, and L004 is never reused. `trace` is opt-in: +`closed` is strict itself now, and L004 is never reused. U014 was `argv`, +a check on `IO.args()` readers, retired before its first release: every +reader already drops the program, and it could not tell one that does from +one that does not. U014 is never reused either. `trace` is opt-in: it is in `laws`, but no group setting reaches it; only `def trace()` in a bolt.bend turns it on. `scan` and `thunk` are opt-in the same way, in `suspicious`: only `def scan()` or `def thunk()` turns each on. An unknown level word grades as an error, so a typo shows. A `bolt.bend` is @@ -297,13 +300,6 @@ parameters and no `->`), which is how Bend fills the law named `f`. recurse, a Base walk that rebuilds the list (`List.map`, `List.append`), and a def of another module are left alone. One finding per call, on its callee. -- `argv` (opt-in) — a call `IO.args(`: an `IO.args` token with a `(` right - after it. Since bend 2.0.32 `IO.args()` starts with the program as - invoked, as C's argv does, so a program that parses it as it comes takes - its own path for its first argument. Read the arguments through shake's - `Shake.argv()`, or drop the first word before parsing. The rule cannot - tell the reader that drops it from one that does not: give that one - reader `# noqa: U014`. No path is exempt. - `thunk` (opt-in) — a lambda whose body is exactly a self-call and whose parameter the call does not read, passed as the one lambda of a call: a `Unit -> T` thunk such as `Lazy.or_else(hit, _u => go(rest, k))`. The diff --git a/src/args.bend b/src/args.bend index e33e566..dd9ce52 100644 --- a/src/args.bend +++ b/src/args.bend @@ -39,7 +39,7 @@ def args_of(ss: List<&1, String>) -> List<&2, String>: # bolt's command line: its arguments, without the program def argv() -> IO(List<&2, String>): # noqa: L001 IO: reads argv do IO>: - ss : List<&1, String> <- IO.args() # noqa: U014 the one reader: args_of drops the program + ss : List<&1, String> <- IO.args() return args_of(ss) # whether a word names a subcommand diff --git a/src/codes.bend b/src/codes.bend index 6626b71..6c0a1ac 100644 --- a/src/codes.bend +++ b/src/codes.bend @@ -3,7 +3,8 @@ # source `bolt(group:slug)`. Numbers are assigned once, in the group order # of src/README.md: do not renumber a rule, and do not reuse a retired code # (L004 was `quantify`, now `closed` itself; C001 was `shadow` and U005 was -# `nat`, whose failures bend 2.0.25 no longer has). +# `nat`, whose failures bend 2.0.25 no longer has; U014 was `argv`, retired +# before its first release, since every reader already drops the program). import Base import ./lazy/lazy.bend as Lazy @@ -36,7 +37,6 @@ def table() -> List<&2, Entry>: Entry{"rewalk", "U011", "suspicious"}, Entry{"unit", "U012", "suspicious"}, Entry{"scan", "U013", "suspicious"}, - Entry{"argv", "U014", "suspicious"}, Entry{"thunk", "U015", "suspicious"}, Entry{"fromrev", "U016", "suspicious"}, Entry{"doc", "S001", "style"}, diff --git a/src/config.bend b/src/config.bend index 7fe3c48..a643f50 100644 --- a/src/config.bend +++ b/src/config.bend @@ -275,10 +275,9 @@ def default(+group: String) -> Level: # a rule only its own setting turns on: a group setting, or the group's # default, would put new findings on projects that never asked for it -# (`trace`, and `argv`, which cannot tell the one reader that drops the -# program from the rest) +# (`trace`, `thunk` and `scan`) def opt_in(+rule: String) -> Bool: - List.contains(~String, ~String.eq, ["trace", "argv", "thunk", "scan"], rule) + List.contains(~String, ~String.eq, ["trace", "thunk", "scan"], rule) # the rule's own setting, else its group's, else the group's default; an # opt-in rule's own setting, else off diff --git a/src/rules.bend b/src/rules.bend index 12a0af1..05b7513 100644 --- a/src/rules.bend +++ b/src/rules.bend @@ -38,7 +38,6 @@ import ./rules/suspicious/ring.bend as Ring import ./rules/suspicious/rewalk.bend as Rewalk import ./rules/suspicious/unit.bend as Unit import ./rules/suspicious/scan.bend as Scan -import ./rules/suspicious/argv.bend as Argv import ./rules/suspicious/thunk.bend as Thunk import ./rules/suspicious/fromrev.bend as Fromrev import ./rules/correctness/put.bend as Put @@ -88,7 +87,6 @@ def on.rules(+ss: Src.Src) -> List<&2, F.Finding>: Rewalk.check(ss), Unit.check(ss), Scan.check(ss), - Argv.check(ss), Thunk.check(ss), Fromrev.check(ss), Put.check(ss), diff --git a/src/rules/LAWS.bend b/src/rules/LAWS.bend index db81357..c7863cc 100644 --- a/src/rules/LAWS.bend +++ b/src/rules/LAWS.bend @@ -27,7 +27,6 @@ import ./suspicious/index.bend as Index import ./suspicious/ring.bend as Ring import ./suspicious/table.bend as Table import ./suspicious/unit.bend as UnitRule -import ./suspicious/argv.bend as Argv import ./suspicious/fromrev.bend as Fromrev import ./suspicious/thunk.bend as Thunk import ./suspicious/scan.bend as Scan @@ -191,41 +190,6 @@ law put_counts: {List.length(&2, F.Finding, Put.check.on(toks, path)) == Bool.pick(Nat, put_defined(toks), 0n, put_count(toks)) : Nat} -# True when tt is `IO.args` and the tokens open with a `(` token -def argv_open(+tt: String, toks: List<&2, Lex.Tok>) -> Bool: - match toks: - case Con{Lex.Tok{Lex.TOpen{}, +o, l, c}, rest}: - Bool.and(String.eq(tt, "IO.args"), String.eq(o, "(")) - case Con{h, rest}: - False{} - case Nil{}: - False{} - -# how many `IO.args` tokens have a `(` token right after them -def argv_count(toks: List<&2, Lex.Tok>) -> Nat: - match toks: - case Nil{}: - 0n - case Con{Lex.Tok{Lex.TDotted{}, +t, l, c}, +rest}: - +m = argv_count(rest) - Bool.pick(Nat, argv_open(t, rest), 1n+m, m) - case Con{h, rest}: - argv_count(rest) - -# LAW: argv reports one finding for each `IO.args` token with a `(` token -# right after it among the significant tokens, at any path, and none for -# any other token -# BOLT-RULE-U014 -law argv_counts: - for +path: String - for text: String - for +toks: List<&2, Lex.Tok> - for tree: Tree.Node - for bound: Bind.Bound - for items: List<&2, Outline.Item> - {List.length(&2, F.Finding, Argv.check(Src.Src{path, text, toks, tree, bound, items})) - == argv_count(T.sig(toks)) : Nat} - # True when tt is `String.from_list` and the tokens open with `(`, # `List.reverse` and `(` def fromrev_at(+tt: String, toks: List<&2, Lex.Tok>) -> Bool: @@ -4656,29 +4620,6 @@ law inert_put: {Put.check(Src.Src{path, text, toks, tree, bound, items}) == Put.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} -# LAW: argv reads what no comment or string says: two sources as the lexer -# makes them whose tokens read the same with comments and strings cut have -# the same findings -# BOLT-RULE-INERT -# BOLT-RULE-U014 -law inert_argv: - for +path: String - for text: String - for toks: List<&2, Lex.Tok> - for tree: Tree.Node - for bound: Bind.Bound - for items: List<&2, Outline.Item> - for text2: String - for toks2: List<&2, Lex.Tok> - for tree2: Tree.Node - for bound2: Bind.Bound - for items2: List<&2, Outline.Item> - for ok: {inert.oks(toks) == True{} : Bool} - for ok2: {inert.oks(toks2) == True{} : Bool} - for e: {inert.toks(toks) == inert.toks(toks2) : List<&2, Lex.Tok>} - {Argv.check(Src.Src{path, text, toks, tree, bound, items}) - == Argv.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} - # LAW: fromrev reads what no comment or string says: two sources as the # lexer makes them whose tokens read the same with comments and strings cut # have the same findings diff --git a/src/rules/PROOF.bend b/src/rules/PROOF.bend index e9b2f9a..57c0c23 100644 --- a/src/rules/PROOF.bend +++ b/src/rules/PROOF.bend @@ -28,7 +28,6 @@ import ./suspicious/index.bend as Index import ./suspicious/ring.bend as Ring import ./suspicious/table.bend as Table import ./suspicious/unit.bend as UnitRule -import ./suspicious/argv.bend as Argv import ./suspicious/fromrev.bend as Fromrev import ../rchars.bend as Rchars import ./suspicious/scan.bend as Scan @@ -689,217 +688,6 @@ def Laws.put_counts(toks, path): Equal.cong(Bool, Nat, z => Bool.pick(Nat, z, 0n, Laws.put_count(toks)), Put.defines(toks), Laws.put_defined(toks), put.defines(toks))) -# argv -# ---- - -# a lone token: no call follows it -law argv.one: - for kk: Lex.TokKind - for t: String - for l: U32 - for c: U32 - for +path: String - {List.length(&2, F.Finding, Argv.calls(Lex.Tok{kk, t, l, c} <> [], path)) - == Laws.argv_count(Lex.Tok{kk, t, l, c} <> []) : Nat} - -def argv.one(kk, _t, _l, _c, _path): - match kk: - case Lex.TName{}: - {==} - case Lex.TUpper{}: - {==} - case Lex.TDotted{}: - {==} - case Lex.TWild{}: - {==} - case Lex.TKey{}: - {==} - case Lex.TNum{}: - {==} - case Lex.TStr{}: - {==} - case Lex.TChar{}: - {==} - case Lex.TComment{}: - {==} - case Lex.TSpace{}: - {==} - case Lex.TNewline{}: - {==} - case Lex.TOp{}: - {==} - case Lex.TColon{}: - {==} - case Lex.TEq{}: - {==} - case Lex.TBind{}: - {==} - case Lex.TArrow{}: - {==} - case Lex.TLam{}: - {==} - case Lex.TAll{}: - {==} - case Lex.TAmp{}: - {==} - case Lex.TOpen{}: - {==} - case Lex.TClose{}: - {==} - case Lex.TComma{}: - {==} - -# an `IO.args` token, then any token, onto a list the law holds for -law argv.dot: - for kk: Lex.TokKind - for +t: String - for +o: String - for +l: U32 - for +c: U32 - for l2: U32 - for c2: U32 - for +r: List<&2, Lex.Tok> - for +path: String - for ih1: {List.length(&2, F.Finding, Argv.calls(Lex.Tok{kk, o, l2, c2} <> r, path)) - == Laws.argv_count(Lex.Tok{kk, o, l2, c2} <> r) : Nat} - for ih2: {List.length(&2, F.Finding, Argv.calls(r, path)) == Laws.argv_count(r) : Nat} - {List.length(&2, F.Finding, Argv.calls(Lex.Tok{Lex.TDotted{}, t, l, c} <> Lex.Tok{kk, o, l2, c2} <> r, path)) - == Laws.argv_count(Lex.Tok{Lex.TDotted{}, t, l, c} <> Lex.Tok{kk, o, l2, c2} <> r) : Nat} - -def argv.dot(kk, t, o, l, c, _l2, _c2, r, path, ih1, ih2): - match kk: - case Lex.TName{}: - ih1 - case Lex.TUpper{}: - ih1 - case Lex.TDotted{}: - ih1 - case Lex.TWild{}: - ih1 - case Lex.TKey{}: - ih1 - case Lex.TNum{}: - ih1 - case Lex.TStr{}: - ih1 - case Lex.TChar{}: - ih1 - case Lex.TComment{}: - ih1 - case Lex.TSpace{}: - ih1 - case Lex.TNewline{}: - ih1 - case Lex.TOp{}: - ih1 - case Lex.TColon{}: - ih1 - case Lex.TEq{}: - ih1 - case Lex.TBind{}: - ih1 - case Lex.TArrow{}: - ih1 - case Lex.TLam{}: - ih1 - case Lex.TAll{}: - ih1 - case Lex.TAmp{}: - ih1 - case Lex.TOpen{}: - nat.pick(Bool.and(String.eq(t, "IO.args"), String.eq(o, "(")), - F.Finding{path, l, c, 7, "argv", "IO.args() starts with the program as invoked (bend 2.0.32); use Shake.argv(), or drop the first word before parsing."}, - Argv.calls(r, path), Laws.argv_count(r), ih2) - case Lex.TClose{}: - ih1 - case Lex.TComma{}: - ih1 - -# two tokens onto a list the law holds for -law argv.pair: - for kk: Lex.TokKind - for +t: String - for +l: U32 - for +c: U32 - for k2: Lex.TokKind - for +o: String - for +l2: U32 - for +c2: U32 - for +r: List<&2, Lex.Tok> - for +path: String - for ih1: {List.length(&2, F.Finding, Argv.calls(Lex.Tok{k2, o, l2, c2} <> r, path)) - == Laws.argv_count(Lex.Tok{k2, o, l2, c2} <> r) : Nat} - for ih2: {List.length(&2, F.Finding, Argv.calls(r, path)) == Laws.argv_count(r) : Nat} - {List.length(&2, F.Finding, Argv.calls(Lex.Tok{kk, t, l, c} <> Lex.Tok{k2, o, l2, c2} <> r, path)) - == Laws.argv_count(Lex.Tok{kk, t, l, c} <> Lex.Tok{k2, o, l2, c2} <> r) : Nat} - -def argv.pair(kk, t, l, c, k2, o, l2, c2, r, path, ih1, ih2): - match kk: - case Lex.TName{}: - ih1 - case Lex.TUpper{}: - ih1 - case Lex.TDotted{}: - argv.dot(k2, t, o, l, c, l2, c2, r, path, ih1, ih2) - case Lex.TWild{}: - ih1 - case Lex.TKey{}: - ih1 - case Lex.TNum{}: - ih1 - case Lex.TStr{}: - ih1 - case Lex.TChar{}: - ih1 - case Lex.TComment{}: - ih1 - case Lex.TSpace{}: - ih1 - case Lex.TNewline{}: - ih1 - case Lex.TOp{}: - ih1 - case Lex.TColon{}: - ih1 - case Lex.TEq{}: - ih1 - case Lex.TBind{}: - ih1 - case Lex.TArrow{}: - ih1 - case Lex.TLam{}: - ih1 - case Lex.TAll{}: - ih1 - case Lex.TAmp{}: - ih1 - case Lex.TOpen{}: - ih1 - case Lex.TClose{}: - ih1 - case Lex.TComma{}: - ih1 - -# argv's calls count the `IO.args(` sites -law argv.calls: - for toks: List<&2, Lex.Tok> - for +path: String - {List.length(&2, F.Finding, Argv.calls(toks, path)) == Laws.argv_count(toks) : Nat} - -def argv.calls(toks, path): - match toks: - case Nil{}: - {==} - case Con{Lex.Tok{kk, t, l, c}, +rest}: - match rest: - case Nil{}: - argv.one(kk, t, l, c, path) - case Con{Lex.Tok{k2, o, l2, c2}, r}: - argv.pair(kk, t, l, c, k2, o, l2, c2, r, path, argv.calls(rest, path), argv.calls(r, path)) - -def Laws.argv_counts(path, _text, toks, _tree, _bound, _items): - argv.calls(T.sig(toks), path) - # fromrev # ------- @@ -19279,89 +19067,6 @@ def Laws.inert_put(path, _text, toks, _tree, _bound, _items, _text2, toks2, _tre inert.via(List<&2, Lex.Tok>, z => Put.check.on(T.sig(z), path), toks, toks2, Laws.inert.toks(toks), Laws.inert.toks(toks2), inert.put.on(toks, path, ok), inert.put.on(toks2, path, ok2), e) -# argv -# ---- - -# a dotted name then an open bracket, their texts read that way: compared -# with `IO.args` and `(` as they were -law inert.argv.call: - for +b1: Bool - for +t: String - for +b2: Bool - for +o: String - for +l: U32 - for +c: U32 - for +path: String - for +more: List<&2, F.Finding> - for +e1: {Laws.inert.fits.go(b1, t) == True{} : Bool} - for +e2: {Laws.inert.fits.go(b2, o) == True{} : Bool} - {Argv.calls.one(Laws.inert.keep(b1, t), Laws.inert.keep(b2, o), l, c, path, more) - == Argv.calls.one(t, o, l, c, path, more) - : List<&2, F.Finding>} - -def inert.argv.call(b1, t, b2, o, l, c, path, more, e1, e2): - +x = {F.Finding{path, l, c, 7, "argv", "IO.args() starts with the program as invoked (bend 2.0.32); use Shake.argv(), or drop the first word before parsing."} - : F.Finding} - +lhs = Argv.calls.one(Laws.inert.keep(b1, t), Laws.inert.keep(b2, o), l, c, path, more) - %inert.eq_keep(b1, t, "IO.args", e1, {==}) : {lhs == Bool.pick(List<&2, F.Finding>, Bool.and(_, String.eq(o, "(")), - x <> more, more) : List<&2, F.Finding>} - %inert.eq_keep(b2, o, "(", e2, {==}) : {lhs == Bool.pick(List<&2, F.Finding>, - Bool.and(String.eq(Laws.inert.keep(b1, t), "IO.args"), _), x <> more, more) : List<&2, F.Finding>} - {==} - -# argv's walk reads no comment or string: it tests kinds, then compares texts -# with `IO.args` and `(` -law inert.argv.calls: - for ts: List<&2, Lex.Tok> - for +path: String - for +e: {Laws.inert.oks(ts) == True{} : Bool} - {Argv.calls(Laws.inert.toks(ts), path) == Argv.calls(ts, path) : List<&2, F.Finding>} - -def inert.argv.calls(ts, path, e): - match ts: - case Nil{}: {==} - case Con{Lex.Tok{+k, +t, +l, +c}, +rest}: - match rest: - case Nil{}: {==} - case Con{Lex.Tok{+k2, +o, +l2, +c2}, +r2}: - +h1 = {Lex.Tok{k, t, l, c} : Lex.Tok} - +h2 = {Lex.Tok{k2, o, l2, c2} : Lex.Tok} - +er = inert.and_r(Laws.inert.fits(h1), Laws.inert.oks(rest), e) - +e2 = inert.and_r(Laws.inert.fits(h2), Laws.inert.oks(r2), er) - +cr = Laws.inert.toks(rest) - +cond = Bool.and(Argv.calls.dotted(k), Lex.is_open(k2)) - +tt = Laws.inert.keep(Laws.inert.blanks(k), t) - +oo = Laws.inert.keep(Laws.inert.blanks(k2), o) - +lhs = Lazy.either(List<&2, F.Finding>, cond, _u => Argv.calls.one(tt, oo, l, c, path, - Argv.calls(Laws.inert.toks(r2), path)), _v => Argv.calls(cr, path)) - %inert.argv.calls(rest, path, er) : {lhs == Lazy.either(List<&2, F.Finding>, cond, - _u => Argv.calls.one(t, o, l, c, path, Argv.calls(r2, path)), _v => _) : List<&2, F.Finding>} - %inert.argv.calls(r2, path, e2) : {lhs == Lazy.either(List<&2, F.Finding>, cond, - _u => Argv.calls.one(t, o, l, c, path, _), _v => Argv.calls(cr, path)) : List<&2, F.Finding>} - %inert.argv.call(Laws.inert.blanks(k), t, Laws.inert.blanks(k2), o, l, c, path, - Argv.calls(Laws.inert.toks(r2), path), inert.and_l(Laws.inert.fits(h1), Laws.inert.oks(rest), e), - inert.and_l(Laws.inert.fits(h2), Laws.inert.oks(r2), er)) : {lhs == Lazy.either(List<&2, F.Finding>, cond, - _u => _, _v => Argv.calls(cr, path)) : List<&2, F.Finding>} - {==} - -# argv's check reads no comment or string -law inert.argv.on: - for +ts: List<&2, Lex.Tok> - for +path: String - for +e: {Laws.inert.oks(ts) == True{} : Bool} - {Argv.calls(T.sig(Laws.inert.toks(ts)), path) == Argv.calls(T.sig(ts), path) : List<&2, F.Finding>} - -def inert.argv.on(ts, path, e): - +s = T.sig(ts) - +cs = Laws.inert.toks(s) - %Equal.sym(List<&2, Lex.Tok>, T.sig(Laws.inert.toks(ts)), cs, inert.put.sig(ts)) : - {Argv.calls(_, path) == Argv.calls(s, path) : List<&2, F.Finding>} - inert.argv.calls(s, path, inert.put.sig_ok(ts, e)) - -def Laws.inert_argv(path, _text, toks, _tree, _bound, _items, _text2, toks2, _tree2, _bound2, _items2, ok, ok2, e): - inert.via(List<&2, Lex.Tok>, z => Argv.calls(T.sig(z), path), toks, toks2, Laws.inert.toks(toks), - Laws.inert.toks(toks2), inert.argv.on(toks, path, ok), inert.argv.on(toks2, path, ok2), e) - # fromrev # ------- diff --git a/src/rules/suspicious/argv.bend b/src/rules/suspicious/argv.bend deleted file mode 100644 index 6154c7a..0000000 --- a/src/rules/suspicious/argv.bend +++ /dev/null @@ -1,57 +0,0 @@ -# rule argv: a call to `IO.args(`: among the significant tokens, an `IO.args` -# token with a `(` token right after it, and nothing else. Since bend 2.0.32 -# IO.args gives the program as invoked first, as C's argv does, so a program -# that parses it as it comes takes its own path for its first argument (the -# move to bend 2.0.34 broke every such reader silently). Read the arguments -# through shake's `Shake.argv()`, or drop the first word before parsing. The -# rule does not try to tell a reader that drops it from one that does not: -# the one reader a program has carries `# noqa: U014`, and the rule is -# opt-in, off unless a bolt.bend names it (BOLT-CFG-6). No path is exempt: a -# law file, a proof or a test reads IO.args as wrongly as any other file. -import Base -import ../../src.bend as Src -import ../../lazy/lazy.bend as Lazy -import ../../finding.bend as F -import ../../syntax/lex.bend as Lex -import ../tokens.bend as T - -# a dotted name? -def calls.dotted(kk: Lex.TokKind) -> Bool: - match kk: - case Lex.TDotted{}: - True{} - case other: - False{} - -# a dotted name then an open bracket: a finding when they are `IO.args` and -# `(`, before what the rest reports -def calls.one( - +tt: String, - +oo: String, - +ll: U32, - +cc: U32, - +path: String, - +more: List<&2, F.Finding> -) -> List<&2, F.Finding>: - Bool.pick(List<&2, F.Finding>, Bool.and(String.eq(tt, "IO.args"), String.eq(oo, "(")), - F.Finding{path, ll, cc, 7, "argv", "IO.args() starts with the program as invoked (bend 2.0.32); use Shake.argv(), or drop the first word before parsing."} - <> more, - more) - -# every `IO.args(` among the significant tokens -def calls(toks: List<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>: - match toks: - case Con{Lex.Tok{k, +t, +l, +c}, +rest}: - match rest: - case Con{Lex.Tok{k2, +o, l2, c2}, r2}: - Lazy.either(List<&2, F.Finding>, Bool.and(calls.dotted(k), Lex.is_open(k2)), _u => calls.one(t, o, l, c, path, - calls(r2, path)), _v => calls(rest, path)) - case Nil{}: - Nil{} - case Nil{}: - Nil{} - -# the rule -def check(ss: Src.Src) -> List<&2, F.Finding>: - Src.Src{path, text, toks, tree, bound, items} = ss - calls(T.sig(toks), path) From ef75d66fd64d647f2413058c7bf1672b69a037a6 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 14:21:24 +0000 Subject: [PATCH 6/6] chore: turn scan (U013) off in bolt's own bolt.bend scan stays in bolt as an opt-in audit tool, its rule and laws unchanged; bolt's own tree no longer turns it on. Its 55 noqa comments go with it, since with scan off noqa (S005) would report each as naming a code that no finding has. No logic changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B --- bolt.bend | 4 ---- src/config.bend | 2 +- src/lint/plan.bend | 2 +- src/noqa.bend | 2 +- src/rules/digest.bend | 10 +++++----- src/rules/imports.bend | 8 ++++---- src/rules/laws/trace.bend | 10 +++++----- src/rules/laws/unsafe.bend | 2 +- src/rules/style/noqa.bend | 2 +- src/rules/suspicious/concat.bend | 2 +- src/rules/suspicious/eager.bend | 4 ++-- src/rules/suspicious/fuel.bend | 4 ++-- src/rules/suspicious/hoist.bend | 12 ++++++------ src/rules/suspicious/rewalk.bend | 18 +++++++++--------- src/rules/suspicious/ring.bend | 14 +++++++------- src/rules/suspicious/scan.bend | 12 ++++++------ src/rules/suspicious/table.bend | 2 +- src/rules/suspicious/unused.bend | 2 +- src/syntax/bind.bend | 2 +- 19 files changed, 55 insertions(+), 59 deletions(-) diff --git a/bolt.bend b/bolt.bend index c77dfc2..2034ed2 100644 --- a/bolt.bend +++ b/bolt.bend @@ -32,7 +32,3 @@ def unsafe() -> String: # SPEC.md's rows and the laws' tags agree def trace() -> String: "error" - -# a loop that walks a list it carries unchanged, on every step -def scan() -> String: - "error" diff --git a/src/config.bend b/src/config.bend index a643f50..8a435d6 100644 --- a/src/config.bend +++ b/src/config.bend @@ -159,7 +159,7 @@ def unknown.in(ss: List<&2, Setting>, +rows: List<&2, Codes.Entry>) -> List<&2, Nil{} case Con{Setting{+n, w, line}, rest}: +more = unknown.in(rest, rows) - Bool.pick(List<&2, Setting>, known.in(rows, n), # noqa: U013 the fixed code table + Bool.pick(List<&2, Setting>, known.in(rows, n), more, Setting{n, w, line} <> more) # the settings, in order, whose name is neither a rule's slug nor a group of diff --git a/src/lint/plan.bend b/src/lint/plan.bend index 2acf8c4..2e89580 100644 --- a/src/lint/plan.bend +++ b/src/lint/plan.bend @@ -424,7 +424,7 @@ def grade(+cs: List<&2, Conf>, +world: W.World, fs: List<&2, F.Finding>) -> List case Nil{}: Nil{} case Con{F.Finding{+path, line, col, len, rule, msg}, rest}: - cfg = config.at(cs, world, path) # noqa: U013 one config per directory + cfg = config.at(cs, world, path) List.append(&2, F.Graded, Rules.graded(cfg, [F.Finding{path, line, col, len, rule, msg}]), grade(cs, world, rest)) # --------------------------------------------------------------------------- diff --git a/src/noqa.bend b/src/noqa.bend index 8aeb42f..254483f 100644 --- a/src/noqa.bend +++ b/src/noqa.bend @@ -248,5 +248,5 @@ def keep(+ms: List<&2, Marks>, gs: List<&2, F.Graded>) -> List<&2, F.Graded>: Nil{} case Con{F.Graded{ll, F.Finding{+path, +line, col, len, +rule, msg}}, rest}: +more = keep(ms, rest) - Bool.pick(List<&2, F.Graded>, silenced(ms, path, line, Codes.code(rule)), more, # noqa: U013 files with marks + Bool.pick(List<&2, F.Graded>, silenced(ms, path, line, Codes.code(rule)), more, F.Graded{ll, F.Finding{path, line, col, len, rule, msg}} <> more) diff --git a/src/rules/digest.bend b/src/rules/digest.bend index 8085264..e003d5a 100644 --- a/src/rules/digest.bend +++ b/src/rules/digest.bend @@ -132,7 +132,7 @@ def mentions(us: List<&2, Bind.Use>, +ss: List<&2, Span>, +as: List<&2, Alias>, Nil{} case Con{Bind.Use{n, +l, c, tt}, rest}: +more = mentions(rest, ss, as, file) - +out = Bool.not(within(ss, l)) # noqa: U013 law spans + +out = Bool.not(within(ss, l)) Lazy.stop(List<&2, Mention>, out, more, _u => target(tt, as, file, more)) # the uses the binder recorded @@ -202,7 +202,7 @@ def called(us: List<&2, Bind.Use>, +as: List<&2, Alias>, +file: String) -> List< case Nil{}: Nil{} case Con{Bind.Use{n, l, c, tt}, rest}: - target(tt, as, file, called(rest, as, file)) # noqa: U013 as holds the file's import aliases + target(tt, as, file, called(rest, as, file)) # the top-level defs and types, by name and line: what the coverage rule # grades. The uses are read in order, once: each item but a constructor @@ -221,11 +221,11 @@ def ranged( ranged(rest, us, as, file) case Con{Outline.Item{Outline.IDef{}, name, line, sig, doc, path}, +rest}: +nx = next_line(rest) - cs = called(upto(us, nx), as, file) # noqa: U013 import aliases + cs = called(upto(us, nx), as, file) Top{Outline.IDef{}, name, line, [], cs} <> ranged(rest, past(us, nx), as, file) case Con{Outline.Item{Outline.IType{}, name, line, sig, doc, path}, +rest}: +nx = next_line(rest) - Top{Outline.IType{}, name, line, ctors(rest), called(upto(us, nx), as, file)} # noqa: U013 import aliases + Top{Outline.IType{}, name, line, ctors(rest), called(upto(us, nx), as, file)} <> ranged(rest, past(us, nx), as, file) case Con{Outline.Item{kind, name, line, sig, doc, path}, +rest}: ranged(rest, past(us, next_line(rest)), as, file) @@ -312,7 +312,7 @@ def laws_of(root: Tree.Node, +items: List<&2, Outline.Item>) -> List<&2, Law>: match root: case Tree.NCons{Tree.Stmt{Tree.SLaw{}, +kids, body}, rest}: +at = Tree.line(kids) - dd = doc_at(items, at) # noqa: U013 stops at the law's line + dd = doc_at(items, at) Law{Closed.name.of(Bind.declared(kids)), at, Closed.binds(body), String.lines(dd)} <> laws_of(rest, items) case Tree.NCons{h, rest}: laws_of(rest, items) diff --git a/src/rules/imports.bend b/src/rules/imports.bend index fc9052a..2f1dc9c 100644 --- a/src/rules/imports.bend +++ b/src/rules/imports.bend @@ -91,7 +91,7 @@ def fresh.spec(ds: List<&2, String>, +seen: List<&2, String>, +read: List<&2, St Nil{} case Con{+d, rest}: +more = fresh.spec(rest, seen, read) - +known = Bool.and(has(read, d), Bool.not(has(seen, d))) # noqa: U013 the spec fresh.fast is proven against + +known = Bool.and(has(read, d), Bool.not(has(seen, d))) Bool.pick(List<&2, String>, Bool.and(known, Bool.not(has(more, d))), d <> more, more) # the paths of the files @@ -119,7 +119,7 @@ def walk.spec( case 1n+f Nil{}: seen case 1n+f Con{p, rest}: - +found = fresh.spec(deps.spec(es, p), seen, read) # noqa: U013 the spec walk is proven against + +found = fresh.spec(deps.spec(es, p), seen, read) walk.spec(f, List.append(&2, String, found, rest), List.append(&2, String, List.reverse(&2, String, found), seen), es, read) @@ -165,7 +165,7 @@ def walk( case 1n+f Nil{}: seen case 1n+f Con{p, rest}: - +found = fresh.fast(deps.first(es, p), seen, read) # noqa: U013 one lookup per file reached, fuel-bound + +found = fresh.fast(deps.first(es, p), seen, read) walk(f, List.append(&2, String, found, rest), List.append(&2, String, List.reverse(&2, String, found), seen), es, read) @@ -203,7 +203,7 @@ def trail.go( case 1n+f Nil{}: Nil{} case 1n+f Con{Step{+at, +back}, rest}: - +found = fresh.fast(deps.first(es, at), seen, read) # noqa: U013 one lookup per file on the path + +found = fresh.fast(deps.first(es, at), seen, read) Lazy.stop(List<&2, String>, String.eq(at, to), List.reverse(&2, String, back), _u => trail.go(f, List.append(&2, Step, rest, steps(found, back)), List.append(&2, String, List.reverse(&2, String, found), seen), es, read, to)) diff --git a/src/rules/laws/trace.bend b/src/rules/laws/trace.bend index 5744043..fbeb397 100644 --- a/src/rules/laws/trace.bend +++ b/src/rules/laws/trace.bend @@ -295,7 +295,7 @@ def judge_entries(es: List<&2, String>, +ds: List<&2, Digest.Digest>, +id: Strin case Nil{}: Nil{} case Con{e, rest}: - List.append(&2, F.Finding, judge_entry(ds, id, e, nn), judge_entries(rest, ds, id, nn)) # noqa: U013 one per file + List.append(&2, F.Finding, judge_entry(ds, id, e, nn), judge_entries(rest, ds, id, nn)) # is the row a claim: Proved, and proved or pending? def claims(+lv: String, +st: String) -> Bool: @@ -330,7 +330,7 @@ def judge_rows(rs: List<&2, Row>, +sp: Spec, +ds: List<&2, Digest.Digest>) -> Li case Nil{}: Nil{} case Con{r, rest}: - List.append(&2, F.Finding, judge_row(r, sp, ds), judge_rows(rest, sp, ds)) # noqa: U013 one per file + List.append(&2, F.Finding, judge_row(r, sp, ds), judge_rows(rest, sp, ds)) # is the ID a row that is a claim: Proved, and proved or pending? def claimed(rs: List<&2, Row>, +id: String) -> Bool: @@ -363,7 +363,7 @@ def strays.laws(ls: List<&2, Digest.Law>, +rs: List<&2, Row>, +path: String) -> case Nil{}: Nil{} case Con{Digest.Law{+n, +l, b, d}, rest}: - List.append(&2, F.Finding, stray(d, rs, path, n, l), strays.laws(rest, rs, path)) # noqa: U013 SPEC.md rows + List.append(&2, F.Finding, stray(d, rs, path, n, l), strays.laws(rest, rs, path)) # every stray tag of every law file def strays(ds: List<&2, Digest.Digest>, +rs: List<&2, Row>) -> List<&2, F.Finding>: @@ -371,7 +371,7 @@ def strays(ds: List<&2, Digest.Digest>, +rs: List<&2, Row>) -> List<&2, F.Findin case Nil{}: Nil{} case Con{Digest.Digest{+path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}: - List.append(&2, F.Finding, strays.laws(laws, rs, path), strays(rest, rs)) # noqa: U013 rs holds SPEC.md's rows + List.append(&2, F.Finding, strays.laws(laws, rs, path), strays(rest, rs)) # the rows that are not rows def malformed(ms: List<&2, Mark>) -> List<&2, F.Finding>: @@ -388,7 +388,7 @@ def twins(ms: List<&2, Mark>, +all: List<&2, Mark>) -> List<&2, F.Finding>: Nil{} case Con{Mark{+id, +nn}, rest}: +more = twins(rest, all) - +dup = Nat.is_gt(marks_with(all, id), 1n) # noqa: U013 SPEC.md's IDs + +dup = Nat.is_gt(marks_with(all, id), 1n) +twice = Bool.pick(List<&2, F.Finding>, dup, at(nn, id ++ " is listed twice.") <> more, more) Bool.pick(List<&2, F.Finding>, is_id(id), twice, at(nn, id ++ " is not a valid ID; an ID matches [A-Z][A-Z0-9]*(-[A-Z0-9]+)+.") <> twice) diff --git a/src/rules/laws/unsafe.bend b/src/rules/laws/unsafe.bend index 2e95fac..8b588fa 100644 --- a/src/rules/laws/unsafe.bend +++ b/src/rules/laws/unsafe.bend @@ -119,7 +119,7 @@ def check.go( case Nil{}: Nil{} case Con{Digest.Digest{path, +norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}: - List.append(&2, F.Finding, found(reacher(rs, norm), unsafes, path, norm, es, read, fuel), # noqa: U013 law files + List.append(&2, F.Finding, found(reacher(rs, norm), unsafes, path, norm, es, read, fuel), check.go(rest, rs, es, read, fuel)) # the rule, over every file the linter read diff --git a/src/rules/style/noqa.bend b/src/rules/style/noqa.bend index d00dc5f..fa85b45 100644 --- a/src/rules/style/noqa.bend +++ b/src/rules/style/noqa.bend @@ -92,4 +92,4 @@ def check(mks: List<&2, Noqa.Mark>, +whole: Bool, +path: String, +gs: List<&2, F case Nil{}: Nil{} case Con{mk, rest}: - List.append(&2, F.Finding, check.mark(mk, whole, path, gs), check(rest, whole, path, gs)) # noqa: U013 one file's + List.append(&2, F.Finding, check.mark(mk, whole, path, gs), check(rest, whole, path, gs)) diff --git a/src/rules/suspicious/concat.bend b/src/rules/suspicious/concat.bend index 6837504..4812c70 100644 --- a/src/rules/suspicious/concat.bend +++ b/src/rules/suspicious/concat.bend @@ -185,7 +185,7 @@ def hits( List.reverse(&2, F.Finding, acc) case Con{+a, rest}: +slot = Maybe.default(&2, String, List.head(&2, String, params), "") - was = seen(a, lets) # noqa: U013 a def's lets + was = seen(a, lets) hits(rest, List.tail(&2, String, params), lets, path, hit(was, slot, path, acc)) # the lets a statement leaves in scope for the statements after it diff --git a/src/rules/suspicious/eager.bend b/src/rules/suspicious/eager.bend index 064ac0e..31e06c8 100644 --- a/src/rules/suspicious/eager.bend +++ b/src/rules/suspicious/eager.bend @@ -49,7 +49,7 @@ def any_of(cs: List<&2, String>, +set: List<&2, String>) -> Bool: case Nil{}: False{} case Con{c, t}: - Lazy.or_else(List.contains(~String, ~String.eq, set, c), _u => any_of(t, set)) # noqa: U013 a def's names + Lazy.or_else(List.contains(~String, ~String.eq, set, c), _u => any_of(t, set)) def loops.go(ds: List<&2, Calls.Def>, +acc: List<&2, String>) -> List<&2, String>: match ds: @@ -121,7 +121,7 @@ def work( +now = work.hot(k, hot, seg, keep) +call = Bool.and(work.name(k), String.eq(o, "(")) +is_pick = Bool.and(call, String.eq(t, "Bool.pick")) - +known = List.contains(~String, ~String.eq, ns, t) # noqa: U013 a def's names + +known = List.contains(~String, ~String.eq, ns, t) +mine = Bool.and(Bool.not(String.eq(t, self)), known) +report = Bool.and(now, Bool.and(call, mine)) +inner = Bool.and(now, Bool.not(is_pick)) diff --git a/src/rules/suspicious/fuel.bend b/src/rules/suspicious/fuel.bend index 0c0f99f..52e8f8b 100644 --- a/src/rules/suspicious/fuel.bend +++ b/src/rules/suspicious/fuel.bend @@ -169,8 +169,8 @@ def check.go(root: Tree.Node, +fs: List<&2, Fuel>, +path: String) -> List<&2, F. match root: case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}: +self = own(Bind.declared(kids)) - +head = calls(kids, fs, self, path) # noqa: U013 the file's fuel defs - +inner = calls(body, fs, self, path) # noqa: U013 the file's fuel defs + +head = calls(kids, fs, self, path) + +inner = calls(body, fs, self, path) List.concat(&2, F.Finding, [head, inner, check.go(rest, fs, path)]) case Tree.NCons{h, rest}: check.go(rest, fs, path) diff --git a/src/rules/suspicious/hoist.bend b/src/rules/suspicious/hoist.bend index e342bea..f119de4 100644 --- a/src/rules/suspicious/hoist.bend +++ b/src/rules/suspicious/hoist.bend @@ -92,7 +92,7 @@ def carried.go( List.reverse(&2, String, acc) case Con{p, rest}: +nm = Calls.param_name(p) - +keep = Bool.and(Bool.not(String.is_empty(nm)), all_same(cs, ii, nm)) # noqa: U013 cs holds one def's self-calls + +keep = Bool.and(Bool.not(String.is_empty(nm)), all_same(cs, ii, nm)) carried.go(rest, cs, (ii + 1n : Nat), Bool.pick(List<&2, String>, keep, nm <> acc, acc)) # parameters passed through unchanged; empty when nothing recurses @@ -136,18 +136,18 @@ def value_ok(+app: Bool, kk: Lex.TokKind, +tt: String, +carried: List<&2, String def closed(nn: Tree.Node, +carried: List<&2, String>) -> Bool: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TOp{}, +op, l, c}}, Tree.NCons{Tree.Leaf{+tok}, tail}}: - +ok = leaf_ok(String.eq(op, "~"), tok, carried) # noqa: U013 carried holds one def's parameters + +ok = leaf_ok(String.eq(op, "~"), tok, carried) +aft = closed(tail, carried) Bool.and(ok, aft) case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TOp{}, op, l, c}}, rest}: closed(rest, carried) case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}: - +ok = value_ok(String.eq(o, "("), k, t, carried) # noqa: U013 carried holds one def's parameters + +ok = value_ok(String.eq(o, "("), k, t, carried) +inn = closed(kids, carried) +aft = closed(rest, carried) Bool.and(ok, Bool.and(inn, aft)) case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, +t, l, c}}, rest}: - +ok = List.contains(~String, ~String.eq, carried, t) # noqa: U013 carried holds one def's parameters + +ok = List.contains(~String, ~String.eq, carried, t) +aft = closed(rest, carried) Bool.and(ok, aft) case Tree.NCons{Tree.Leaf{tok}, rest}: @@ -609,7 +609,7 @@ def walk( match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}: +heat = warm(hot, k) - +own = call_table(heat, String.eq(o, "("), t, kids, self, wides, carried, path) # noqa: U013 a def's parameters + +own = call_table(heat, String.eq(o, "("), t, kids, self, wides, carried, path) +inn = walk(kids, self, wides, carried, path, heat) +aft = walk(rest, self, wides, carried, path, heat) List.concat(&2, F.Finding, [own, inn, aft]) @@ -623,7 +623,7 @@ def walk( List.concat(&2, F.Finding, [walk(kids, self, wides, carried, path, False{}), walk(body, self, wides, carried, path, arm), walk(rest, self, wides, carried, path, hot)]) case Tree.NCons{Tree.Stmt{kind, +kids, +body}, +rest}: - +own = let_hit(hot, kids, body, rest, self, wides, carried, path) # noqa: U013 carried holds one def's parameters + +own = let_hit(hot, kids, body, rest, self, wides, carried, path) List.concat(&2, F.Finding, [own, walk(kids, self, wides, carried, path, hot), walk(body, self, wides, carried, path, hot), walk(rest, self, wides, carried, path, hot)]) case Tree.NCons{h, rest}: diff --git a/src/rules/suspicious/rewalk.bend b/src/rules/suspicious/rewalk.bend index e3b4777..787067d 100644 --- a/src/rules/suspicious/rewalk.bend +++ b/src/rules/suspicious/rewalk.bend @@ -391,7 +391,7 @@ def any_of(cs: List<&2, String>, +set: List<&2, String>) -> Bool: case Nil{}: False{} case Con{c, t}: - Lazy.or_else(List.contains(~String, ~String.eq, set, c), _u => any_of(t, set)) # noqa: U013 the file's loops + Lazy.or_else(List.contains(~String, ~String.eq, set, c), _u => any_of(t, set)) def loops.go(ds: List<&2, Calls.Def>, +acc: List<&2, String>) -> List<&2, String>: match ds: @@ -553,15 +553,15 @@ def stamp(ns: List<&2, String>, +bs: List<&2, Bind>, +line: U32, +col: U32) -> S case Nil{}: "" case Con{+nm, rest}: - "|" ++ nm ++ "=" ++ U32.show(count(bs, nm, line, col)) ++ stamp(rest, bs, line, col) # noqa: U013 a piece's lets + "|" ++ nm ++ "=" ++ U32.show(count(bs, nm, line, col)) ++ stamp(rest, bs, line, col) # every expensive call, wide unless the call is indexed on the spot; its # arguments are their text and which let of each name they read def gather(nn: Tree.Node, +self: String, +lp: List<&2, String>, +bs: List<&2, Bind>) -> List<&2, Site>: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, +rest}}: - +args = Tree.show(kids) ++ stamp(names(kids, []), bs, l, c) # noqa: U013 bs holds one piece's lets - +here = open_site(String.eq(o, "("), indexed(rest), t, args, l, c, # noqa: U013 lp holds the file's loops + +args = Tree.show(kids) ++ stamp(names(kids, []), bs, l, c) + +here = open_site(String.eq(o, "("), indexed(rest), t, args, l, c, U32.from_nat(String.length(t)), self, lp) List.concat(&2, Site, [here, gather(kids, self, lp, bs), gather(rest, self, lp, bs)]) case Tree.NCons{Tree.Group{open, +kids, close}, rest}: @@ -754,7 +754,7 @@ def pin(+ps: List<&2, Pos>, sites: List<&2, Site>) -> List<&2, Site>: case Nil{}: Nil{} case Con{s, rest}: - pin_one(ps, s) <> pin(ps, rest) # noqa: U013 ps holds one piece's marks + pin_one(ps, s) <> pin(ps, rest) # the other site keeps the whole result def other_full(+yes: Bool, how: How, +body: Tree.Node) -> Bool: @@ -772,7 +772,7 @@ def other_go(sites: List<&2, Site>, +name: String, +args: String, +line: U32, +c case Con{Site{+nm, +as, +l, +c, len, how}, rest}: +same = Bool.and(String.eq(nm, name), String.eq(as, args)) +diff = Bool.not(Bool.and(U32.is_eq(l, line), U32.is_eq(c, col))) - +here = other_full(Bool.and(same, diff), how, body) # noqa: U013 body is one straight piece + +here = other_full(Bool.and(same, diff), how, body) +more = other_go(rest, name, args, line, col, body) Bool.or(here, more) @@ -797,7 +797,7 @@ def earlier(seen: List<&2, Site>, +name: String, +args: String, +line: U32, +col case Nil{}: False{} case Con{s, rest}: - +here = earlier_one(s, name, args, line, col, body) # noqa: U013 body is one straight piece + +here = earlier_one(s, name, args, line, col, body) +more = earlier(rest, name, args, line, col, body) Bool.or(here, more) @@ -876,7 +876,7 @@ def report( case Nil{}: Nil{} case Con{+s, rest}: - +mine = report_one(s, all, body, path, seen) # noqa: U013 one straight piece + +mine = report_one(s, all, body, path, seen) List.append(&2, F.Finding, mine, report(rest, all, body, path, s <> seen)) # findings in one straight region; a case arm is not part of it @@ -888,7 +888,7 @@ def local(+nn: Tree.Node, +self: String, +lp: List<&2, String>, +path: String) - def visit(nn: Tree.Node, +self: String, +lp: List<&2, String>, +path: String) -> List<&2, F.Finding>: match nn: case Tree.NCons{Tree.Stmt{Tree.SCase{}, kids, +body}, rest}: - +here = local(body, self, lp, path) # noqa: U013 the file's loops + +here = local(body, self, lp, path) List.concat(&2, F.Finding, [here, visit(body, self, lp, path), visit(rest, self, lp, path)]) case Tree.NCons{Tree.Stmt{kind, +kids, +body}, rest}: List.concat(&2, F.Finding, [visit(kids, self, lp, path), visit(body, self, lp, path), diff --git a/src/rules/suspicious/ring.bend b/src/rules/suspicious/ring.bend index 4cfd8e6..e01b7ae 100644 --- a/src/rules/suspicious/ring.bend +++ b/src/rules/suspicious/ring.bend @@ -51,7 +51,7 @@ def has_name(as: List<&2, Tree.Node>, +wins: List<&2, String>) -> Bool: False{} case Con{h, rest}: +more = has_name(rest, wins) - Bool.or(win_name(h, wins), more) # noqa: U013 wins holds one def's windows + Bool.or(win_name(h, wins), more) # is the last argument a number? def last_num(as: List<&2, Tree.Node>) -> Bool: @@ -100,7 +100,7 @@ def here_of( def drop_in(nn: Tree.Node, +wins: List<&2, String>) -> Maybe<&2, Lex.Tok>: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}: - +here = here_of(String.eq(o, "("), k, t, l, c, kids, wins) # noqa: U013 wins holds one def's windows + +here = here_of(String.eq(o, "("), k, t, l, c, kids, wins) +inn = drop_in(kids, wins) +aft = drop_in(rest, wins) or_tok(here, or_tok(inn, aft)) @@ -177,14 +177,14 @@ def plus_scan(nn: Tree.Node, +seen: Maybe<&2, Lex.Tok>, +wins: List<&2, String>) or_tok(pp_found(is_pp, seen), plus_scan(rest, pp_seen(is_pp, seen), wins)) case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}: +open = String.eq(o, "(") - +recv = call_recv(open, t, kids, wins) # noqa: U013 wins holds one def's windows + +recv = call_recv(open, t, kids, wins) +inn = plus_scan(kids, None{}, wins) - +drop = call_drop(open, k, t, l, c, kids, wins) # noqa: U013 wins holds one def's windows + +drop = call_drop(open, k, t, l, c, kids, wins) +aft = plus_scan(rest, or_tok(seen, drop), wins) or_tok(recv, or_tok(inn, aft)) case Tree.NCons{Tree.Group{open, +kids, close}, rest}: +inn = plus_scan(kids, None{}, wins) - +aft = plus_scan(rest, or_tok(seen, drop_in(kids, wins)), wins) # noqa: U013 wins holds one def's windows + +aft = plus_scan(rest, or_tok(seen, drop_in(kids, wins)), wins) or_tok(inn, aft) case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}: or_tok(plus_scan(kids, None{}, wins), or_tok(plus_scan(body, None{}, wins), plus_scan(rest, seen, wins))) @@ -224,7 +224,7 @@ def slides( Nil{} case Con{h, rest}: +slot = Maybe.default(&2, String, List.head(&2, String, params), "") - List.append(&2, F.Finding, slide(h, path, slot_wins(slot, wins)), # noqa: U013 wins holds one def's windows + List.append(&2, F.Finding, slide(h, path, slot_wins(slot, wins)), slides(rest, List.tail(&2, String, params), path, wins)) # every self-call's sliding arguments @@ -289,7 +289,7 @@ def windows.go(ps: List<&2, String>, +bad: List<&2, String>, +acc: List<&2, Stri case Nil{}: List.reverse(&2, String, acc) case Con{+p, rest}: - +known = List.contains(~String, ~String.eq, bad, p) # noqa: U013 a def's parameters + +known = List.contains(~String, ~String.eq, bad, p) +keep = Bool.and(Bool.not(String.is_empty(p)), Bool.not(known)) windows.go(rest, bad, Bool.pick(List<&2, String>, keep, p <> acc, acc)) diff --git a/src/rules/suspicious/scan.bend b/src/rules/suspicious/scan.bend index c608cdc..bb8e5da 100644 --- a/src/rules/suspicious/scan.bend +++ b/src/rules/suspicious/scan.bend @@ -104,7 +104,7 @@ def found(ss: List<&2, Nat>, +as: List<&2, Tree.Node>, +names: List<&2, String>) None{} case Con{at, rest}: +more = found(rest, as, names) - first(keep_in(name_of(Calls.arg(as, at)), names), more) # noqa: U013 a call's parameters + first(keep_in(name_of(Calls.arg(as, at)), names), more) # where a name sits among the parameter names def index_of(ps: List<&2, String>, +nm: String, +ii: Nat) -> Maybe<&2, Nat>: @@ -129,7 +129,7 @@ def params_at(ss: List<&2, Nat>, +as: List<&2, Tree.Node>, +ps: List<&2, String> Nil{} case Con{at, rest}: +more = params_at(rest, as, ps) - List.append(&2, Nat, opt(index_in(name_of(Calls.arg(as, at)), ps)), more) # noqa: U013 a def's parameters + List.append(&2, Nat, opt(index_in(name_of(Calls.arg(as, at)), ps)), more) # a call's walked parameters, when its callee is a name and it is a call def pass_hit( @@ -152,7 +152,7 @@ def pass_hit( def passes(nn: Tree.Node, +ps: List<&2, String>, +ws: List<&2, Walk>) -> List<&2, Nat>: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}: - +own = pass_hit(k, String.eq(o, "("), t, kids, ps, ws) # noqa: U013 a def's parameters + +own = pass_hit(k, String.eq(o, "("), t, kids, ps, ws) List.concat(&2, Nat, [own, passes(kids, ps, ws), passes(rest, ps, ws)]) case Tree.NCons{Tree.Group{open, +kids, close}, rest}: List.concat(&2, Nat, [passes(kids, ps, ws), passes(rest, ps, ws)]) @@ -181,7 +181,7 @@ def own.go(ps: List<&2, Tree.Node>, +carried: List<&2, String>, +ii: Nat) -> May case Nil{}: None{} case Con{+p, rest}: - +here = moves(p, carried) # noqa: U013 a def's parameters + +here = moves(p, carried) Lazy.stop(Maybe<&2, Nat>, here, place(p, ii), _u => own.go(rest, carried, 1n+ii)) # where the parameter a def shrinks sits, when it calls itself and it is no count or text @@ -215,7 +215,7 @@ def lead.go(ps: List<&2, Tree.Node>, +carried: List<&2, String>) -> String: case Nil{}: "" case Con{+p, rest}: - +here = moves(p, carried) # noqa: U013 a def's parameters + +here = moves(p, carried) Lazy.stop(String, here, Calls.param_name(p), _u => lead.go(rest, carried)) # a finding on the callee, naming the carried list @@ -289,7 +289,7 @@ def walk( match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}: +heat = Hoist.warm(hot, k) - +own = call_hit(k, heat, String.eq(o, "("), t, l, c, kids, self, ws, carried, lead, path) # noqa: U013 parameters + +own = call_hit(k, heat, String.eq(o, "("), t, l, c, kids, self, ws, carried, lead, path) +inn = walk(kids, self, ws, carried, lead, path, heat) +aft = walk(rest, self, ws, carried, lead, path, heat) List.concat(&2, F.Finding, [own, inn, aft]) diff --git a/src/rules/suspicious/table.bend b/src/rules/suspicious/table.bend index e51e772..6a2ffdf 100644 --- a/src/rules/suspicious/table.bend +++ b/src/rules/suspicious/table.bend @@ -259,7 +259,7 @@ def hit( def walk(nn: Tree.Node, +path: String, +fixed: List<&2, String>) -> List<&2, F.Finding>: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}: - +own = hit(String.eq(o, "("), t, kids, fixed, path, l, c) # noqa: U013 fixed holds the file's table defs + +own = hit(String.eq(o, "("), t, kids, fixed, path, l, c) List.concat(&2, F.Finding, [own, walk(kids, path, fixed), walk(rest, path, fixed)]) case Tree.NCons{Tree.Group{open, +kids, close}, rest}: List.concat(&2, F.Finding, [walk(kids, path, fixed), walk(rest, path, fixed)]) diff --git a/src/rules/suspicious/unused.bend b/src/rules/suspicious/unused.bend index 26247ce..eb32814 100644 --- a/src/rules/suspicious/unused.bend +++ b/src/rules/suspicious/unused.bend @@ -244,7 +244,7 @@ def check.go( Nil{} case Con{Bind.Bind{+name, +line, +col, +kind, note}, rest}: +more = check.go(rest, hh, uses, fl, path) - +shown = reportable(kind, note, line, fl) # noqa: U013 the file's foreign lines + +shown = reportable(kind, note, line, fl) +hit = Bool.and(shown, Bool.not(String.starts_with(name, "_"))) Bool.pick(List<&2, F.Finding>, Lazy.and_then(hit, _u => Bool.not(seen(hh, uses, line, col))), F.Finding{path, line, col, U32.from_nat(String.length(name)), "unused", diff --git a/src/syntax/bind.bend b/src/syntax/bind.bend index 2e683f0..1b95cde 100644 --- a/src/syntax/bind.bend +++ b/src/syntax/bind.bend @@ -959,7 +959,7 @@ def refresh(env: List<&2, Bind>, +binds: List<&2, Bind>) -> List<&2, Bind>: case Nil{}: Nil{} case Con{Bind{name, +l, +c, kind, note}, rest}: - noted(binder(binds, l, c), Bind{name, l, c, kind, note}) <> refresh(rest, binds) # noqa: U013 annotated binders + noted(binder(binds, l, c), Bind{name, l, c, kind, note}) <> refresh(rest, binds) # the names in scope at a line: those of the statement on it, else of the # nearest statement above