diff --git a/AGENTS.md b/AGENTS.md index becdf99..d6d506b 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -153,10 +153,19 @@ Design specs and plans are not kept in this repo; they live under do not hide a search's recursion in one branch either: it runs whatever the condition says, so the search never exits early (native, 100 searches over 100k cells: 0.10 s for a hit at the head, 0.11 s at the end). Bind the one - recursive call with `+rest = ..` and pick between values built from it, or - take the early exit from `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; the same search costs 0.00 s). The same goes for + recursive call with `+rest = ..` and pick between values built from it. For + a search, carry the test as a Bool into the next call and match on it + first (`has.go(t, k, U32.is_eq(h, k))`, then `match hit` before the next + step): the self-call stays a tail call and compiles to a `for(;;)` loop. + Do not wrap the recursive step in a thunk (`Lazy.or_else(U32.is_eq(h, k), + _u => has(t, k))`): it exits early, but it allocates a closure and leaves + 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 + `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 any expensive expression in a branch: a scan of the whole token list inside a per-token pick runs for every token (bind's notes were 20 s that way, 20 ms as one pass). `bolt`'s `strict` rule catches the Bool.and/or shape. diff --git a/SPEC.md b/SPEC.md index c713563..055081a 100644 --- a/SPEC.md +++ b/SPEC.md @@ -33,6 +33,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-RULE-C008 | `strings` reports exactly a match whose closed string-literal arms, read in the first match column, total over 64 characters. | Proved | proved | src/rules/LAWS.bend strings_counts | | 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-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 | @@ -44,14 +45,17 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | 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 | | 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: 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-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`) 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 | -| 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 | +| 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 | ### Laws rules (BOLT-LAW) @@ -72,14 +76,14 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-CFG-4 | A finding is graded by the nearest readable bolt.bend in its file's directory, then each parent, and only that one applies. | Proved | proved | src/LAWS.bend absolute_root; src/LAWS.bend absolute_under; src/LAWS.bend home_empty; src/LAWS.bend home_here; src/LAWS.bend home_up; src/LAWS.bend home_down; src/LAWS.bend chain_parent; src/LAWS.bend nearest_grades | | BOLT-CFG-5 | Group defaults are correctness at error, pedantic off, and the rest at warn. | Proved | proved | src/LAWS.bend default_correctness; src/LAWS.bend default_pedantic; src/LAWS.bend default_rest | | BOLT-CFG-6 | An opt-in rule is off unless its own setting names it. | Proved | proved | src/LAWS.bend level_own; src/LAWS.bend opt_in_off | -| BOLT-CFG-7 | A setting in a bolt.bend whose name is no rule or group is a finding. | Proved | pending | | +| BOLT-CFG-7 | A setting in a bolt.bend whose name is no rule or group is a finding: of the settings grading reads from a bolt.bend (each `def` whose body holds a string), `unknown` holds exactly those whose name is neither the slug nor the group of any row of the code table, in file order, one each. | Proved | proved | src/LAWS.bend unknown_exact; src/LAWS.bend settings_graded | ### Scope (BOLT-SCOPE) | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | | BOLT-SCOPE-1 | With no files named, bolt lints every `.bend` file under `.` found within the first 100000 directories the walk reads, not descending into hidden directories or `node_modules`, sorted by code point; past that bound the walk stops silently. | Proved | proved | src/LAWS.bend walk_files | -| BOLT-SCOPE-2 | A per-file rule sees one file's `Src`; a project rule sees the digests of every file in the run, and nothing else. | Proved | proved | src/LAWS.bend scope_findings | +| BOLT-SCOPE-2 | A per-file rule sees one file's `Src`; a project rule sees the digests of every file in the run; `setting` sees the text of each bolt.bend grading reads; and nothing else. | Proved | proved | src/LAWS.bend scope_findings | | BOLT-SCOPE-3 | When the files in the run include a LAWS.bend, every file in the run that is not exempt is under law; otherwise none is. | Proved | proved | src/LAWS.bend under_law_all | | BOLT-SCOPE-4 | Path exemptions are decided by the path alone, never by content: two files at one path are exempt from `law` alike whatever each holds, and on a path a per-file rule's header exempts (a LAWS.bend, a PROOF.bend, a file under a `tests` directory, and for `closed` any file but a LAWS.bend) that rule's findings are the same for every source. What a rule reads from content to skip a def, a line or a file (a def that is a proof, returning one or written with no type, a file that defines `Map.put`, `# lanes: native`, `main` and dotted names) is that rule's behavior, not a path exemption. | Proved | proved | src/rules/LAWS.bend scope_digest_exempt; src/rules/LAWS.bend scope_hole; src/rules/LAWS.bend scope_doc; src/rules/LAWS.bend scope_param; src/rules/LAWS.bend scope_law_file; src/rules/LAWS.bend scope_closed | | BOLT-SCOPE-5 | A bolt.bend is read, never linted, even when named. | Proved | proved | src/LAWS.bend no_config_linted | @@ -91,7 +95,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-OUT-1 | The code table maps each rule slug to exactly one code and each code to exactly one slug. | Proved | proved | src/LAWS.bend slug_finds_row; src/LAWS.bend code_finds_row | | BOLT-OUT-6 | A released code is never renumbered or reused. | Trusted | | | | BOLT-OUT-2 | A finding prints as `path:line:col: level: CODE: message`, 1-based. | Proved | proved | src/LAWS.bend shown | -| BOLT-OUT-3 | Output order is read failures, then per-file findings in file-list order and `Rules.on` order, then `coverage`, `unsafe` and `trace`, less the findings a noqa comment silences (BOLT-OUT-7), then `noqa`'s findings (S005) in file-list order. | Proved | proved | src/LAWS.bend lines_in_order | +| BOLT-OUT-3 | Output order is read failures, then per-file findings in file-list order and `Rules.on` order, then `setting`'s findings (C011), then `coverage`, `unsafe` and `trace`, less the findings a noqa comment silences (BOLT-OUT-7), then `noqa`'s findings (S005) in file-list order. | Proved | proved | src/LAWS.bend lines_in_order | | BOLT-OUT-4 | The last line is `clean` or `N errors, M warnings`, and the exit status is 1 exactly when some graded finding is an error, counting the findings BOLT-OUT-3 prints. | Proved | proved | src/LAWS.bend last_line_summary; src/LAWS.bend exit_on_error | | BOLT-OUT-5 | A path that cannot be read is a `read` finding graded with correctness. | Proved | proved | src/LAWS.bend unread_one_finding; src/LAWS.bend directory_one_finding; src/LAWS.bend read_is_correctness | | BOLT-OUT-7 | A finding whose line carries a `# noqa:` comment naming its code is not reported and not counted: a comment token whose text is `#`, any spaces, `noqa:` and then codes (runs of ASCII letters and digits, case-sensitive, split by commas with spaces around them allowed, any text after) silences every graded finding of its own file on its own line whose code it names, once every rule has run, the project rules included, and the summary and the exit status count only what remains. The filter reads comment tokens only, so a `noqa` inside a string literal is never one and no rule's findings change. | Proved | proved | src/LAWS.bend noqa_comments; src/LAWS.bend noqa_codes; src/LAWS.bend noqa_bare; src/LAWS.bend noqa_bare_text; src/LAWS.bend noqa_keeps; src/LAWS.bend lines_in_order; src/LAWS.bend last_line_summary; src/LAWS.bend exit_on_error | diff --git a/bolt.bend b/bolt.bend index 2034ed2..e1fd204 100644 --- a/bolt.bend +++ b/bolt.bend @@ -32,3 +32,12 @@ 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" + +# 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 de98773..6e777a2 100644 --- a/src/LAWS.bend +++ b/src/LAWS.bend @@ -159,6 +159,64 @@ 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. + +# whether some row of the table has the name as its slug. Law vocabulary, as +# are group_in and unknown_of. +def slug_in(rows: List<&2, Codes.Entry>, +name: String) -> Bool: + match rows: + case Nil{}: + False{} + case Con{Codes.Entry{+s, _id, _grp}, rest}: + +more = slug_in(rest, name) + Bool.or(String.eq(s, name), more) + +# whether some row of the table has the name as its group +def group_in(rows: List<&2, Codes.Entry>, +name: String) -> Bool: + match rows: + case Nil{}: + False{} + case Con{Codes.Entry{_s, _id, +grp}, rest}: + +more = group_in(rest, name) + Bool.or(String.eq(grp, name), more) + +# the settings, in order, whose name is neither the slug nor the group of any +# row of the code table +def unknown_of(ss: List<&2, Config.Setting>) -> List<&2, Config.Setting>: + match ss: + case Nil{}: + Nil{} + case Con{Config.Setting{+n, w, line}, rest}: + +more = unknown_of(rest) + Bool.pick(List<&2, Config.Setting>, Bool.or(slug_in(Codes.table(), n), group_in(Codes.table(), n)), more, + Config.Setting{n, w, line} <> more) + +# LAW: of a bolt.bend's settings, `unknown` holds exactly those whose name is +# neither the slug nor the group of any row of the code table, in file order, +# one each +# BOLT-CFG-7 +# BOLT-RULE-C011 +law unknown_exact: + for ss: List<&2, Config.Setting> + {Config.unknown(ss) == unknown_of(ss) : List<&2, Config.Setting>} + +# LAW: the settings `unknown` judges are the ones grading reads: a bolt.bend's +# config is its settings, in file order, each at the level its word gives +# BOLT-CFG-7 +law settings_graded: + for text: String + {Config.parse(text) == Config.Config{Config.levels(Config.settings(text))} : Config.Config} + # The code table and the printed line (BOLT-OUT). The table is finite, so # its laws quantify over every index into it: the row there, looked up again # by its slug and by its code, is the same row. @@ -313,19 +371,104 @@ def on_all(+world: W.World, ps: List<&2, String>) -> List<&2, F.Finding>: case Con{+p, rest}: List.append(&2, F.Finding, on_at(p, W.text(world, p)), on_all(world, rest)) +# the path of the first of the paths the World read a text for, as a list of +# one; none when it read none +def read_first.at(+path: String, mm: Maybe<&2, W.Answer>, more: List<&2, String>) -> List<&2, String>: + match mm: + case None{}: + more + case Some{W.Listed{_names}}: + more + case Some{W.Read{_text}}: + [path] + case Some{W.Unread{}}: + more + case Some{W.Directory{}}: + more + +# the path of the first of the paths the World read a text for +def read_first(+world: W.World, ps: List<&2, String>) -> List<&2, String>: + match ps: + case Nil{}: + [] + case Con{+p, rest}: + read_first.at(p, W.answer(world, W.Text{p}), read_first(world, rest)) + +# the bolt.bend that grades each directory, in directory order: of its +# candidates (the directory resolved against the World's working directory, +# then each parent up to the root) the first the World read, as +# nearest_grades says; none for a directory the defaults grade +def graders_all(+world: W.World, ds: List<&2, String>) -> List<&2, String>: + match ds: + case Nil{}: + [] + case Con{d, rest}: + List.append(&2, String, read_first(world, Config.chain(Config.home(W.cwd.of(world), d))), + graders_all(world, rest)) + +# one `setting` finding for each setting, at the bolt.bend's path and the +# line of the setting's def, in order +def flagged(+path: String, ss: List<&2, Config.Setting>) -> List<&2, F.Finding>: + match ss: + case Nil{}: + [] + case Con{Config.Setting{n, _w, line}, rest}: + F.Finding{path, line, 0, 0, "setting", "`" ++ n ++ "` names no rule or group, so it sets nothing."} + <> flagged(path, rest) + +# a bolt.bend's `setting` findings, its unknown settings, when the World +# read it +def flagged_at(+path: String, mm: Maybe<&2, W.Answer>) -> List<&2, F.Finding>: + match mm: + case None{}: + [] + case Some{W.Listed{_names}}: + [] + case Some{W.Read{text}}: + flagged(path, Config.unknown(Config.settings(text))) + case Some{W.Unread{}}: + [] + case Some{W.Directory{}}: + [] + +# each bolt.bend's `setting` findings, in order +def flagged_all(+world: W.World, ps: List<&2, String>) -> List<&2, F.Finding>: + match ps: + case Nil{}: + [] + case Con{+p, rest}: + List.append(&2, F.Finding, flagged_at(p, W.answer(world, W.Text{p})), flagged_all(world, rest)) + +# `setting`'s findings in a run: the unknown settings of every bolt.bend that +# grades a directory grading needs (a source's or SPEC.md's), each bolt.bend +# once, in the order its directories come +def settings_found(+world: W.World) -> List<&2, F.Finding>: + flagged_all(world, Plan.uniq(graders_all(world, Plan.conf.dirs(Plan.inputs(world))), [])) + +# LAW: `setting` reports, for each bolt.bend that grades a directory of the +# run, each bolt.bend once in the order its directories come, one finding for +# each setting `unknown` holds, at that bolt.bend's path and the line of the +# setting's def, in file order, and nothing else +# BOLT-RULE-C011 +law setting_reports: + for +world: W.World + {Plan.settings(world) == settings_found(world) : List<&2, F.Finding>} + # every finding of a run, ungraded: the read failures, then each source's -# per-file findings, each rule seeing that one source, then coverage, unsafe -# and trace, each seeing the digests of every source in the run (trace also -# whether the run is the whole tree, and SPEC.md's text) +# per-file findings, each rule seeing that one source, then `setting`'s, +# seeing each bolt.bend grading reads, then coverage, unsafe and trace, each +# seeing the digests of every source in the run (trace also whether the run +# is the whole tree, and SPEC.md's text) def in_scope(+world: W.World) -> List<&2, F.Finding>: +ps = Plan.inputs(world) +ds = Digest.all(parsed_all(world, ps)) - List.concat(&2, F.Finding, [unread_all(world, ps), on_all(world, ps), Law.check(ds), Unsafe.check(ds), - Trace.check(List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md"), ds)]) + List.concat(&2, F.Finding, [unread_all(world, ps), on_all(world, ps), settings_found(world), Law.check(ds), + Unsafe.check(ds), Trace.check(List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md"), ds)]) # LAW: the planner's findings are the read failures, then the per-file rules -# on each source's Src alone, then the project rules on the digests of every -# source in the run, and nothing else +# on each source's Src alone, then `setting` on each bolt.bend grading reads, +# then the project rules on the digests of every source in the run, and +# nothing else # BOLT-SCOPE-2 law scope_findings: for +world: W.World @@ -445,10 +588,10 @@ def out_lines(+world: W.World) -> List<&2, String>: List.append(&2, String, shown_all(gs), [summary_of(gs)]) # LAW: `bolt` prints the read failures, then the per-file findings in -# file-list order and `Rules.on` order, then coverage, unsafe and trace, each -# graded finding as one line, the ones at off dropped and the ones a noqa -# comment on their line names dropped, then `noqa`'s findings, then the -# summary +# file-list order and `Rules.on` order, then `setting`'s, then coverage, +# unsafe and trace, each graded finding as one line, the ones at off dropped +# and the ones a noqa comment on their line names dropped, then `noqa`'s +# findings, then the summary # BOLT-OUT-3 # BOLT-OUT-7 law lines_in_order: diff --git a/src/PROOF.bend b/src/PROOF.bend index 69f4198..d68772f 100644 --- a/src/PROOF.bend +++ b/src/PROOF.bend @@ -10,6 +10,7 @@ import ./lint/plan.bend as Plan import ./noqa.bend as Noqa import ./rules/style/noqa.bend as NoqaRule import ./codes.bend as Codes +import ./rules/correctness/setting.bend as Setting import ./syntax/lex.bend as Lex import ./rules/digest.bend as Digest import ./rules/laws/law.bend as Law @@ -147,7 +148,111 @@ def Laws.opt_in_off(sets, group, rule, h_opt, h_rule): == Config.Off{} : Config.Level} {==} -# one arm per row of the code table (29), each checked by evaluation, and one +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. + +# one row onto the slug lookup: the table finds a row exactly when the spec +# says one has the slug +law cfg7.slug.step: + for bb: Bool + for -row: Codes.Entry + for rest: List<&2, Codes.Entry> + for +name: String + for -sl: Bool + for ih: {Maybe.is_some(&2, Codes.Entry, Codes.find(rest, name)) == sl : Bool} + {Maybe.is_some(&2, Codes.Entry, Lazy.stop(Maybe<&2, Codes.Entry>, bb, Some{row}, _u => Codes.find(rest, name))) + == Bool.or(bb, sl) : Bool} + +def cfg7.slug.step(bb, _row, _rest, _name, _sl, ih): + match bb: + case True{}: + {==} + case False{}: + ih + +# the table finds a row by a slug exactly when some row has it +law cfg7.slug: + for rows: List<&2, Codes.Entry> + for +name: String + {Maybe.is_some(&2, Codes.Entry, Codes.find(rows, name)) == Laws.slug_in(rows, name) : Bool} + +def cfg7.slug(rows, name): + match rows: + case Nil{}: + {==} + case Con{Codes.Entry{+s, +id, +grp}, +tl}: + cfg7.slug.step(String.eq(s, name), Codes.Entry{s, id, grp}, tl, name, Laws.slug_in(tl, name), cfg7.slug(tl, name)) + +# one row onto the group lookup +law cfg7.group.step: + for bb: Bool + for rest: List<&2, Codes.Entry> + for +name: String + for -gl: Bool + for ih: {Config.known.group(rest, name) == gl : Bool} + {Lazy.or_else(bb, _u => Config.known.group(rest, name)) == Bool.or(bb, gl) : Bool} + +def cfg7.group.step(bb, _rest, _name, _gl, ih): + match bb: + case True{}: + {==} + case False{}: + ih + +# a name is some row's group exactly when the spec says so +law cfg7.group: + for rows: List<&2, Codes.Entry> + for +name: String + {Config.known.group(rows, name) == Laws.group_in(rows, name) : Bool} + +def cfg7.group(rows, name): + match rows: + case Nil{}: + {==} + case Con{Codes.Entry{_s, _id, +grp}, +tl}: + cfg7.group.step(String.eq(grp, name), tl, name, Laws.group_in(tl, name), cfg7.group(tl, name)) + +# a name is known exactly when some row has it as its slug or its group +law cfg7.known: + for +rows: List<&2, Codes.Entry> + for +name: String + {Config.known.in(rows, name) == Bool.or(Laws.slug_in(rows, name), Laws.group_in(rows, name)) : Bool} + +def cfg7.known(rows, name): + a = Equal.sym(Bool, Maybe.is_some(&2, Codes.Entry, Codes.find(rows, name)), Laws.slug_in(rows, name), + cfg7.slug(rows, name)) + %a : {Bool.or(_, Config.known.group(rows, name)) == Bool.or(Laws.slug_in(rows, name), Laws.group_in(rows, name)) + : Bool} + b = Equal.sym(Bool, Config.known.group(rows, name), Laws.group_in(rows, name), cfg7.group(rows, name)) + %b : {Bool.or(Laws.slug_in(rows, name), _) == Bool.or(Laws.slug_in(rows, name), Laws.group_in(rows, name)) : Bool} + {==} + +def Laws.unknown_exact(ss): + match ss: + case Nil{}: + {==} + case Con{Config.Setting{+n, +w, +line}, +tl}: + k = Equal.sym(Bool, Config.known.in(Codes.table(), n), + Bool.or(Laws.slug_in(Codes.table(), n), Laws.group_in(Codes.table(), n)), cfg7.known(Codes.table(), n)) + %k : {Bool.pick(List<&2, Config.Setting>, _, Config.unknown.in(tl, Codes.table()), + Config.Setting{n, w, line} <> Config.unknown.in(tl, Codes.table())) + == Laws.unknown_of(Config.Setting{n, w, line} <> tl) : List<&2, Config.Setting>} + r = Equal.sym(List<&2, Config.Setting>, Config.unknown.in(tl, Codes.table()), Laws.unknown_of(tl), + Laws.unknown_exact(tl)) + %r : {Bool.pick(List<&2, Config.Setting>, + Bool.or(Laws.slug_in(Codes.table(), n), Laws.group_in(Codes.table(), n)), + _, Config.Setting{n, w, line} <> _) + == Laws.unknown_of(Config.Setting{n, w, line} <> tl) : List<&2, Config.Setting>} + {==} + +def Laws.settings_graded(_text): + {==} + +# 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: @@ -211,7 +316,15 @@ def Laws.slug_finds_row(n): {==} case 29n: {==} - case 30n+_p: + case 30n: + {==} + case 31n: + {==} + case 32n: + {==} + case 33n: + {==} + case 34n+_p: {==} # the same arms, looked up by code @@ -277,7 +390,15 @@ def Laws.code_finds_row(n): {==} case 29n: {==} - case 30n+_p: + case 30n: + {==} + case 31n: + {==} + case 32n: + {==} + case 33n: + {==} + case 34n+_p: {==} def Laws.shown(_path, _line, _col, _len, _rule, _msg, _level): @@ -522,6 +643,130 @@ def lint.on(ps, world): case Con{+p, +tl}: lint.on.step(p, W.text(world, p), Plan.gots(tl, world), Laws.on_all(world, tl), lint.on(tl, world)) +# `setting` (BOLT-RULE-C011): the planner's walk to each grading bolt.bend +# and its findings there are the spec's. + +# one candidate onto the first one read +law c011.first.step: + for +path: String + for mm: Maybe<&2, W.Answer> + for gs: List<&2, Plan.Got> + for -more: List<&2, String> + for ih: {Plan.conf.first(gs) == more : List<&2, String>} + {Plan.conf.first(Plan.Got{path, W.text.got(mm)} <> gs) == Laws.read_first.at(path, mm, more) : List<&2, String>} + +def c011.first.step(_path, mm, _gs, _more, ih): + match mm: + case None{}: + ih + case Some{W.Listed{_names}}: + ih + case Some{W.Read{_text}}: + {==} + case Some{W.Unread{}}: + ih + case Some{W.Directory{}}: + ih + +# the planner's first read candidate is the spec's +law c011.first: + for ps: List<&2, String> + for +world: W.World + {Plan.conf.first(Plan.gots(ps, world)) == Laws.read_first(world, ps) : List<&2, String>} + +def c011.first(ps, world): + match ps: + case Nil{}: + {==} + case Con{+p, +tl}: + c011.first.step(p, W.answer(world, W.Text{p}), Plan.gots(tl, world), Laws.read_first(world, tl), + c011.first(tl, world)) + +# the planner's grading bolt.bend of each directory is the spec's +law c011.used: + for ds: List<&2, String> + for +world: W.World + {Plan.conf.used(ds, world) == Laws.graders_all(world, ds) : List<&2, String>} + +def c011.used(ds, world): + match ds: + case Nil{}: + {==} + case Con{+d, +tl}: + a = Equal.sym(List<&2, String>, Plan.conf.first(Plan.gots(Config.chain(Config.home(W.cwd.of(world), d)), world)), + Laws.read_first(world, Config.chain(Config.home(W.cwd.of(world), d))), + c011.first(Config.chain(Config.home(W.cwd.of(world), d)), world)) + %a : {List.append(&2, String, _, Plan.conf.used(tl, world)) + == Laws.graders_all(world, d <> tl) : List<&2, String>} + Equal.cong(List<&2, String>, List<&2, String>, + rr => List.append(&2, String, Laws.read_first(world, Config.chain(Config.home(W.cwd.of(world), d))), rr), + Plan.conf.used(tl, world), Laws.graders_all(world, tl), c011.used(tl, world)) + +# the rule's findings on settings are the spec's +law c011.found: + for ss: List<&2, Config.Setting> + for +path: String + {Setting.found(ss, path) == Laws.flagged(path, ss) : List<&2, F.Finding>} + +def c011.found(ss, path): + match ss: + case Nil{}: + {==} + case Con{Config.Setting{+n, _w, +line}, +tl}: + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, + rr => F.Finding{path, line, 0, 0, "setting", "`" ++ n ++ "` names no rule or group, so it sets nothing."} <> rr, + Setting.found(tl, path), Laws.flagged(path, tl), c011.found(tl, path)) + +# one bolt.bend onto the rule's findings +law c011.at.step: + for +path: String + for mm: Maybe<&2, W.Answer> + for gs: List<&2, Plan.Got> + for -fs: List<&2, F.Finding> + for ih: {Plan.settings.at(gs) == fs : List<&2, F.Finding>} + {Plan.settings.at(Plan.Got{path, W.text.got(mm)} <> gs) == List.append(&2, F.Finding, Laws.flagged_at(path, mm), fs) + : List<&2, F.Finding>} + +def c011.at.step(path, mm, gs, fs, ih): + match mm: + case None{}: + ih + case Some{W.Listed{_names}}: + ih + case Some{W.Read{+text}}: + a = Equal.sym(List<&2, F.Finding>, Setting.found(Config.unknown(Config.settings(text)), path), + Laws.flagged(path, Config.unknown(Config.settings(text))), + c011.found(Config.unknown(Config.settings(text)), path)) + %a : {List.append(&2, F.Finding, _, Plan.settings.at(gs)) + == List.append(&2, F.Finding, Laws.flagged(path, Config.unknown(Config.settings(text))), fs) + : List<&2, F.Finding>} + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, + rr => List.append(&2, F.Finding, Laws.flagged(path, Config.unknown(Config.settings(text))), rr), + Plan.settings.at(gs), fs, ih) + case Some{W.Unread{}}: + ih + case Some{W.Directory{}}: + ih + +# the rule's findings on each bolt.bend are the spec's +law c011.at: + for ps: List<&2, String> + for +world: W.World + {Plan.settings.at(Plan.gots(ps, world)) == Laws.flagged_all(world, ps) : List<&2, F.Finding>} + +def c011.at(ps, world): + match ps: + case Nil{}: + {==} + case Con{+p, +tl}: + c011.at.step(p, W.answer(world, W.Text{p}), Plan.gots(tl, world), Laws.flagged_all(world, tl), c011.at(tl, world)) + +def Laws.setting_reports(world): + u = Equal.sym(List<&2, String>, Plan.conf.used(Plan.conf.dirs(Plan.inputs(world)), world), + Laws.graders_all(world, Plan.conf.dirs(Plan.inputs(world))), c011.used(Plan.conf.dirs(Plan.inputs(world)), world)) + %u : {Plan.settings.at(Plan.gots(Plan.uniq(_, []), world)) == Laws.settings_found(world) : List<&2, F.Finding>} + c011.at(Plan.uniq(Laws.graders_all(world, Plan.conf.dirs(Plan.inputs(world))), []), world) + def Laws.scope_findings(world): n = Equal.sym(List<&2, F.Finding>, List.append(&2, F.Finding, Rules.project(Plan.srcs_of(Plan.gots(Plan.inputs(world), world)), @@ -531,27 +776,36 @@ def Laws.scope_findings(world): lint.app_nil(F.Finding, Rules.project(Plan.srcs_of(Plan.gots(Plan.inputs(world), world)), List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md")))) %n : {List.append(&2, F.Finding, Plan.unread(Plan.gots(Plan.inputs(world), world)), - List.append(&2, F.Finding, Plan.per_file(Plan.srcs_of(Plan.gots(Plan.inputs(world), world))), _)) + List.append(&2, F.Finding, Plan.per_file(Plan.srcs_of(Plan.gots(Plan.inputs(world), world))), + List.append(&2, F.Finding, Plan.settings(world), _))) == Laws.in_scope(world) : List<&2, F.Finding>} a = Equal.sym(List<&2, F.Finding>, Plan.unread(Plan.gots(Plan.inputs(world), world)), Laws.unread_all(world, Plan.inputs(world)), lint.unread(Plan.inputs(world), world)) %a : {List.append(&2, F.Finding, _, List.append(&2, F.Finding, Plan.per_file(Plan.srcs_of(Plan.gots(Plan.inputs(world), world))), - Rules.project(Plan.srcs_of(Plan.gots(Plan.inputs(world), world)), - List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md")))) + List.append(&2, F.Finding, Plan.settings(world), + Rules.project(Plan.srcs_of(Plan.gots(Plan.inputs(world), world)), + List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md"))))) == Laws.in_scope(world) : List<&2, F.Finding>} b = Equal.sym(List<&2, F.Finding>, Plan.per_file(Plan.srcs_of(Plan.gots(Plan.inputs(world), world))), Laws.on_all(world, Plan.inputs(world)), lint.on(Plan.inputs(world), world)) %b : {List.append(&2, F.Finding, Laws.unread_all(world, Plan.inputs(world)), - List.append(&2, F.Finding, _, + List.append(&2, F.Finding, _, List.append(&2, F.Finding, Plan.settings(world), + Rules.project(Plan.srcs_of(Plan.gots(Plan.inputs(world), world)), + List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md"))))) + == Laws.in_scope(world) : List<&2, F.Finding>} + t = Equal.sym(List<&2, F.Finding>, Plan.settings(world), Laws.settings_found(world), Laws.setting_reports(world)) + %t : {List.append(&2, F.Finding, Laws.unread_all(world, Plan.inputs(world)), + List.append(&2, F.Finding, Laws.on_all(world, Plan.inputs(world)), List.append(&2, F.Finding, _, Rules.project(Plan.srcs_of(Plan.gots(Plan.inputs(world), world)), - List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md")))) + List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md"))))) == Laws.in_scope(world) : List<&2, F.Finding>} c = Equal.sym(List<&2, Src.Src>, Plan.srcs_of(Plan.gots(Plan.inputs(world), world)), Laws.parsed_all(world, Plan.inputs(world)), lint.parsed(Plan.inputs(world), world)) %c : {List.append(&2, F.Finding, Laws.unread_all(world, Plan.inputs(world)), List.append(&2, F.Finding, Laws.on_all(world, Plan.inputs(world)), - Rules.project(_, List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md")))) + List.append(&2, F.Finding, Laws.settings_found(world), + Rules.project(_, List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md"))))) == Laws.in_scope(world) : List<&2, F.Finding>} {==} diff --git a/src/README.md b/src/README.md index de41783..358085d 100644 --- a/src/README.md +++ b/src/README.md @@ -50,8 +50,8 @@ unset group has its default. The groups: | group | rules | default | |---------------|----------------------------------------------------------------------------------|---------| -| `correctness` | `hole` `pick` `put` `arms` `escape` `twice` `strings` `chars` `foreign` | error | -| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` | warn | +| `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 | | `style` | `doc` `space` `wrap` `param` `noqa` | warn | | `laws` | `coverage` `closed` `unsafe` (`trace`: opt-in) | warn | | `pedantic` | `tail` | off | @@ -70,8 +70,11 @@ The stable codes, assigned once (do not renumber): | C008 | `strings` | U008 | `table` | L003 | `unsafe` | | C009 | `chars` | U009 | `hoist` | L004 | retired | | C010 | `foreign` | U010 | `ring` | L005 | `trace` | -| | | U011 | `rewalk` | P001 | `tail` | +| C011 | `setting` | U011 | `rewalk` | P001 | `tail` | | | | U012 | `unit` | | | +| | | U013 | `scan` | | | +| | | U014 | `argv` | | | +| | | U015 | `thunk` | | | Letters: `C` correctness, `U` suspicious, `S` style, `L` laws, `P` pedantic. @@ -79,8 +82,10 @@ Letters: `C` correctness, `U` suspicious, `S` style, `L` laws, `P` pedantic. 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: it is in `laws`, but no group setting reaches it; only `def trace()` in a -bolt.bend turns it on. An unknown level word grades as an error, so a typo shows. A `bolt.bend` is -read, never linted. Without one, the defaults apply. This repo's +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 +read, never linted. A setting whose name is no rule's slug and no group +sets nothing, so `setting` (C011) reports it. Without one, the defaults apply. This repo's [bolt.bend](../bolt.bend) sets every group to error: the gate must see `clean`. @@ -135,7 +140,7 @@ What the rules share, `rules/calls.bend` (the recursion rules), `rules/tokens.bend`, `rules/imports.bend` and `rules/digest.bend`, sits beside the groups. The cost rules built on `rules/calls.bend` (`pick`, `strict`, `eager`, `tail`, `concat`, `index`, `table`, `hoist`, `ring`, -`rewalk`, `unit`) skip what never runs: a law file, a proof file, and a def +`rewalk`, `unit`, `scan`, `thunk`) skip what never runs: a law file, a proof file, and a def that is a proof wherever it is, one that returns a proof (`-> {a == b : T}`) 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`. @@ -214,11 +219,14 @@ parameters and no `->`), which is how Bend fills the law named `f`. game's overlap test in a branch went 31 -> 55 fps once it moved out; one `gaps(..)` in a branch here cost 88 s of a 100 s run). `pick` sees only the self-call and `strict` only Bool.and/or, so the call to a neighbour is this - rule's. Bind it above the pick, or branch with `match` on the condition - (bolt's own code uses `src/lazy/lazy.bend`, which matches on the Bool and - applies a `Unit -> T` thunk in one branch). A call into Base is not - counted: a def of the file is the cheap proxy for work the file itself - wrote. Nor is a call in a lambda's body (from `=>` to the next comma of + rule's. Bind it above the pick, or branch with `match` on the condition. + For a search that recurses, carry the test as a Bool into the next call + (`go(rest, k, test(h))`) and match on it first, so the step stays a loop; + a `Unit -> T` thunk around the recursive call leaves the loop on every step + (`thunk`). `src/lazy/lazy.bend`, which matches on the Bool and applies a + thunk in one branch, stays right for work that does not recurse. A call + into Base is not counted: a def of the file is the cheap proxy for work the + file itself wrote. Nor is a call in a lambda's body (from `=>` to the next comma of its group), which the pick does not run; an argument after that comma counts again. - `concat` — a self-call whose argument grows a carried parameter by @@ -273,6 +281,40 @@ parameters and no `->`), which is how Bend fills the law named `f`. arm that does not call the def. Only a `case` arm can be a base case, so a `Bool.pick` branch beside a self-call is still the step, and so is a lambda body inside it. One finding per operation: `Nat.mul(1n, 1n)` is one. +- `scan` (opt-in) — a def that calls itself and, on the same step, hands a + parameter it carries unchanged (every self-call passes it back as the same + lone name in its own position) to a walk: a Base list search + (`List.contains`, `List.find`, `List.filter`, `List.length`, `List.any`, + `List.all`, `List.foldl`, `List.foldr`), or a def of the file that walks + that argument (the one it shrinks, unless a `Nat` or a `String`, or one it + passes to a walk). Every step walks the list again, O(|A| * |B|). Index it + once outside the loop, or merge two sorted walks. A literal table or an + expression in that argument, a lambda's body, a case arm that does not + 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: 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 + reads the shape and not the type. - `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 @@ -308,6 +350,15 @@ parameters and no `->`), which is how Bend fills the law named `f`. reverse: the missing lane cannot run it. A file headed `# lanes: native` needs no `.js`: that exact line must be one of the comment lines before the file's first non-comment line. +- `setting` — a setting in a bolt.bend whose name is no rule's slug and no + group (`def wrp() -> String: "off"`, or a retired name such as `quantify` + or `shadow`): grading only looks names up, so it sets nothing, and the + typo fails open. It is reported once for each bolt.bend that grades a + file of the run, at that bolt.bend's path and the setting's `def` line, + after the per-file findings and before `coverage`, `unsafe` and `trace`. + It is graded by that bolt.bend like any rule (`def setting() -> String: + "off"` there turns it off). A bolt.bend is read, not linted, so a noqa + comment in one silences nothing. bolt runs it; the editor does not. - `fuel` — a `Nat` literal (digits, then `n`), or `U32.to_nat` of a U32 literal (`U32.to_nat(100000)`), passed in a call, `name(..)`, to a fuel parameter of a def of the same file. A fuel parameter is known by its name diff --git a/src/args.bend b/src/args.bend index dd9ce52..e33e566 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() + ss : List<&1, String> <- IO.args() # noqa: U014 the one reader: args_of drops the program return args_of(ss) # whether a word names a subcommand diff --git a/src/codes.bend b/src/codes.bend index 40a99d1..dd8bdad 100644 --- a/src/codes.bend +++ b/src/codes.bend @@ -23,6 +23,7 @@ def table() -> List<&2, Entry>: Entry{"strings", "C008", "correctness"}, Entry{"chars", "C009", "correctness"}, Entry{"foreign", "C010", "correctness"}, + Entry{"setting", "C011", "correctness"}, Entry{"unused", "U001", "suspicious"}, Entry{"strict", "U002", "suspicious"}, Entry{"eager", "U003", "suspicious"}, @@ -34,6 +35,9 @@ def table() -> List<&2, Entry>: Entry{"ring", "U010", "suspicious"}, Entry{"rewalk", "U011", "suspicious"}, Entry{"unit", "U012", "suspicious"}, + Entry{"scan", "U013", "suspicious"}, + Entry{"argv", "U014", "suspicious"}, + Entry{"thunk", "U015", "suspicious"}, Entry{"doc", "S001", "style"}, Entry{"space", "S002", "style"}, Entry{"wrap", "S003", "style"}, diff --git a/src/config.bend b/src/config.bend index 54670ae..55d9422 100644 --- a/src/config.bend +++ b/src/config.bend @@ -15,12 +15,14 @@ # def space() -> String: # "warn" # -# A level is "off", "warn" or "error". +# A level is "off", "warn" or "error". A setting whose name is no rule's slug +# and no group is `unknown`, and sets nothing. import Base import ./lazy/lazy.bend as Lazy import ./syntax/lex.bend as Lex import ./syntax/tree.bend as Tree import ./syntax/bind.bend as Bind +import ./codes.bend as Codes # how much a finding matters type Level is Data: @@ -88,27 +90,81 @@ def first_str(toks: List<&2, Lex.Tok>) -> Maybe<&2, String>: case Con{h, rest}: first_str(rest) -# a def's name and the string it returns, as a setting -def setting(name: Maybe<&2, String>, word: Maybe<&2, String>) -> List<&2, LevelSet>: +# a setting as a bolt.bend writes it: the def's name, the word its body +# returns, and the line of its `def` (0-based) +type Setting is Data: + Setting{name: String, word: String, line: U32} + +# a def's name and the string it returns, at its line, as a setting +def setting(name: Maybe<&2, String>, word: Maybe<&2, String>, +line: U32) -> List<&2, Setting>: match name word: case Some{n} Some{w}: - [LevelSet{n, of_word(w)}] - case a b: + [Setting{n, w, line}] + case _a _b: [] # every `def x(): "level"` of a tree -def sets(root: Tree.Node) -> List<&2, LevelSet>: +def settings.go(root: Tree.Node) -> List<&2, Setting>: match root: - case Tree.NCons{Tree.Stmt{Tree.SDef{}, kids, body}, rest}: - List.append(&2, LevelSet, setting(Bind.declared(kids), first_str(Tree.leaves(body))), sets(rest)) - case Tree.NCons{h, rest}: - sets(rest) - case other: + case Tree.NCons{Tree.Stmt{Tree.SDef{}, +kids, body}, rest}: + +ln = Tree.line(kids) + List.append(&2, Setting, setting(Bind.declared(kids), first_str(Tree.leaves(body)), ln), settings.go(rest)) + case Tree.NCons{_h, rest}: + settings.go(rest) + case _other: + Nil{} + +# every setting of a bolt.bend's text, in file order +def settings(text: String) -> List<&2, Setting>: + settings.go(Tree.parse(text)) + +# each setting as the level it sets its name to +def levels(ss: List<&2, Setting>) -> List<&2, LevelSet>: + match ss: + case Nil{}: Nil{} + case Con{Setting{n, w, _line}, rest}: + LevelSet{n, of_word(w)} <> levels(rest) -# a bolt.bend's text as a config +# a bolt.bend's text as a config: its settings, each at its level def parse(text: String) -> Config: - Config{sets(Tree.parse(text))} + Config{levels(settings(text))} + +# unknown names +# ------------- +# A name a bolt.bend may set is a rule's slug or a group, as the code table +# (src/codes.bend) lists them; a setting of any other name sets nothing, so +# `setting` (C011) reports it. + +# some row of the table has the name as its group +def known.group(rows: List<&2, Codes.Entry>, +name: String) -> Bool: + match rows: + case Nil{}: + False{} + case Con{Codes.Entry{_s, _id, +grp}, rest}: + Lazy.or_else(String.eq(grp, name), _u => known.group(rest, name)) + +# some row of the table has the name as its slug or its group +def known.in(+rows: List<&2, Codes.Entry>, +name: String) -> Bool: + +slug = Maybe.is_some(&2, Codes.Entry, Codes.find(rows, name)) + +grp = known.group(rows, name) + Bool.or(slug, grp) + +# the settings, in order, whose name no row of the table has as its slug or +# its group +def unknown.in(ss: List<&2, Setting>, +rows: List<&2, Codes.Entry>) -> List<&2, Setting>: + match ss: + case Nil{}: + 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 + more, Setting{n, w, line} <> more) + +# the settings, in order, whose name is neither a rule's slug nor a group of +# the code table +def unknown(ss: List<&2, Setting>) -> List<&2, Setting>: + unknown.in(ss, Codes.table()) # a path's directory, with its slash; `` at the top def dir_of.go(cs: List<&2, Char>, +acc: List<&2, Char>, best: List<&2, Char>) -> String: @@ -218,8 +274,10 @@ 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) def opt_in(+rule: String) -> Bool: - String.eq(rule, "trace") + List.contains(~String, ~String.eq, ["trace", "argv", "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/lazy/lazy.bend b/src/lazy/lazy.bend index 4d6d793..89424e3 100644 --- a/src/lazy/lazy.bend +++ b/src/lazy/lazy.bend @@ -4,7 +4,10 @@ # whatever `hit` says (measured native, 100 iterations over 100k cells: the # hit at the head costs 0.10 s, the same as the hit at the end, while the # forms here cost 0.00 s). A thunk `Unit -> T` is a value, so the branch -# that is not taken is never applied. +# that is not taken is never applied. Keep them for work that does not +# recurse: a thunk around a search's own recursive step allocates a closure +# and leaves the loop on every step, where carrying the test as a Bool into +# the next call keeps it a loop (the `thunk` rule, U015). import Base # `a` when c, else what rest gives: the early exit of a search diff --git a/src/lint/plan.bend b/src/lint/plan.bend index f9fd744..2acf8c4 100644 --- a/src/lint/plan.bend +++ b/src/lint/plan.bend @@ -13,7 +13,8 @@ # A directory's candidates are taken once it is resolved against the World's # working directory (Config.home), so a relative path is graded by the same # bolt.bend wherever bolt runs from. -# `wants` never parses a file; `plan` parses and lints once. Once every rule +# `wants` never parses a file; `plan` parses and lints once, and reads the +# settings of each bolt.bend that grades a directory for `setting` (C011). Once every rule # has run and each finding is graded, the noqa comments (src/noqa.bend) # silence what they name, and then the `noqa` rule reports the comments that # silenced nothing. @@ -26,6 +27,7 @@ import ../rules.bend as Rules import ../config.bend as Config import ../noqa.bend as Noqa import ../rules/style/noqa.bend as NoqaRule +import ../rules/correctness/setting.bend as Setting # what `bolt` prints, in order, and the status it exits with type Plan is Data: @@ -315,12 +317,53 @@ def per_file(ss: List<&2, Src.Src>) -> List<&2, F.Finding>: case Con{s, rest}: List.concat(&2, F.Finding, [Rules.on(s), per_file(rest)]) +# the path of the first candidate the World holds a text for, as a list of +# one; none when it holds none +def conf.first(gs: List<&2, Got>) -> List<&2, String>: + match gs: + case Nil{}: + Nil{} + case Con{Got{path, Some{_text}}, _rest}: + [path] + case Con{Got{_path, None{}}, rest}: + conf.first(rest) + +# the bolt.bend that grades each directory, in directory order: the first of +# its candidates the World read, as conf.near reads it; none for a directory +# graded by the defaults +def conf.used(ds: List<&2, String>, +world: W.World) -> List<&2, String>: + match ds: + case Nil{}: + Nil{} + case Con{d, rest}: + List.append(&2, String, conf.first(gots(conf.chain(world, d), world)), conf.used(rest, world)) + +# every bolt.bend grading reads, each once, in the order its directories come +def graders(+world: W.World) -> List<&2, String>: + uniq(conf.used(conf.dirs(inputs(world)), world), []) + +# the `setting` rule's findings on each bolt.bend the World read, in order +def settings.at(gs: List<&2, Got>) -> List<&2, F.Finding>: + match gs: + case Nil{}: + Nil{} + case Con{Got{+path, Some{text}}, rest}: + List.append(&2, F.Finding, Setting.check(path, text), settings.at(rest)) + case Con{Got{_path, None{}}, rest}: + settings.at(rest) + +# the `setting` rule's findings: each unknown setting of every bolt.bend +# grading reads (src/rules/correctness/setting.bend) +def settings(+world: W.World) -> List<&2, F.Finding>: + settings.at(gots(graders(world), world)) + # every finding of every rule, ungraded, from the sources and what the World # answers for them: the read failures, the per-file findings of each source, -# then the project rules' over every source, told whether the run is the -# whole tree, and SPEC.md's text +# then `setting`'s over each bolt.bend grading reads, then the project rules' +# over every source, told whether the run is the whole tree, and SPEC.md's +# text def found.at(+world: W.World, +gs: List<&2, Got>, +ss: List<&2, Src.Src>) -> List<&2, F.Finding>: - List.concat(&2, F.Finding, [unread(gs), per_file(ss), + List.concat(&2, F.Finding, [unread(gs), per_file(ss), settings(world), Rules.project(ss, List.is_empty(&2, String, W.paths.of(world)), W.text(world, "SPEC.md"))]) # every finding of every rule, ungraded @@ -381,8 +424,8 @@ 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}: - List.append(&2, F.Graded, Rules.graded(config.at(cs, world, path), [F.Finding{path, line, col, len, rule, msg}]), - grade(cs, world, rest)) + cfg = config.at(cs, world, path) # noqa: U013 one config per directory + List.append(&2, F.Graded, Rules.graded(cfg, [F.Finding{path, line, col, len, rule, msg}]), grade(cs, world, rest)) # --------------------------------------------------------------------------- # silencing, then the `noqa` rule diff --git a/src/noqa.bend b/src/noqa.bend index 6f631a5..b7cc122 100644 --- a/src/noqa.bend +++ b/src/noqa.bend @@ -247,5 +247,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, + Bool.pick(List<&2, F.Graded>, silenced(ms, path, line, Codes.code(rule)), more, # noqa: U013 files with marks F.Graded{ll, F.Finding{path, line, col, len, rule, msg}} <> more) diff --git a/src/rules.bend b/src/rules.bend index 0309583..a2e14ee 100644 --- a/src/rules.bend +++ b/src/rules.bend @@ -5,7 +5,10 @@ # names the group, and codes.bend says it again for the config. # Adding one is adding it here and a row in codes.bend. One rule is not # listed here, `noqa` (rules/style/noqa.bend): it reads the other rules' -# graded findings, so the planner runs it after them (lint/plan.bend). +# graded findings, so the planner runs it after them (lint/plan.bend). Nor +# is `setting` (rules/correctness/setting.bend): it reads each bolt.bend that +# grades the run, not a source, so the planner runs it between the per-file +# and the project rules. # The groups are what a bolt.bend switches at once: correctness (what will # fail or blow up), suspicious (what is probably a slip), style, laws, and # pedantic (advice that is noisy on idiomatic code: off unless a project @@ -34,6 +37,9 @@ import ./rules/suspicious/hoist.bend as Hoist 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/correctness/put.bend as Put import ./rules/correctness/escape.bend as Escape import ./rules/correctness/strings.bend as Strings @@ -80,6 +86,9 @@ def on.rules(+ss: Src.Src) -> List<&2, F.Finding>: Ring.check(ss), Rewalk.check(ss), Unit.check(ss), + Scan.check(ss), + Argv.check(ss), + Thunk.check(ss), Put.check(ss), Escape.check(ss), Strings.check(ss), diff --git a/src/rules/LAWS.bend b/src/rules/LAWS.bend index cfe2ec4..0fdcbdc 100644 --- a/src/rules/LAWS.bend +++ b/src/rules/LAWS.bend @@ -27,6 +27,9 @@ 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/thunk.bend as Thunk +import ./suspicious/scan.bend as Scan import ./correctness/chars.bend as Chars import ./correctness/strings.bend as Strings import ./calls.bend as Calls @@ -187,6 +190,41 @@ 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 the first token past spaces, newlines and comments is `TODO` def todo_next(toks: List<&2, Lex.Tok>) -> Bool: match toks: @@ -548,6 +586,30 @@ law unit_exempt: for e: {Paths.is_law_file(path) == True{} : Bool} {UnitRule.check(Src.Src{path, text, toks, tree, bound, items}) == Nil{} : List<&2, F.Finding>} +# LAW: thunk reports nothing in a LAWS.bend or a PROOF.bend, which never run, whatever the source holds +# BOLT-RULE-EXEMPT +law thunk_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} + {Thunk.check(Src.Src{path, text, toks, tree, bound, items}) == Nil{} : List<&2, F.Finding>} + +# LAW: scan reports nothing in a LAWS.bend or a PROOF.bend, which never run, whatever the source holds +# BOLT-RULE-EXEMPT +law scan_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} + {Scan.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 @@ -2271,6 +2333,260 @@ 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. + +# does a name leaf under the node spell the parameter, or it then a dot? +def thunk.reads(nn: Tree.Node, +pp: String) -> Bool: + match nn: + case Tree.Leaf{Lex.Tok{k, +t, l, c}}: + Bool.and(Lex.is_name(k), Bool.or(String.eq(t, pp), String.starts_with(t, pp ++ "."))) + case Tree.Group{o, kids, cl}: + thunk.reads(kids, pp) + case Tree.Stmt{sk, kids, body}: + Bool.or(thunk.reads(kids, pp), thunk.reads(body, pp)) + case Tree.NCons{h, t}: + Bool.or(thunk.reads(h, pp), thunk.reads(t, pp)) + case Tree.NNil{}: + False{} + +# is what follows the call the chain's end, or a comma? +def thunk.last(nn: Tree.Node) -> Bool: + match nn: + case Tree.NCons{h, t}: + Calls.kind.leaf(~Lex.is_comma, h) + case other: + True{} + +# the rest past the name: a `(` group that does not read the parameter, then +# the body's end +def thunk.call(kp: Lex.TokKind, +pp: String, +aa: String, +nm: String, r3: Tree.Node, +name: String) -> Bool: + match r3: + case Tree.NCons{Tree.Group{Lex.Tok{ko, o, lo, co}, kids, cl}, after}: + Bool.and(Bool.and(Lex.is_name(kp), Bool.not(thunk.reads(kids, pp))), + Bool.and(String.eq(aa, "=>"), Bool.and(String.eq(nm, name), Bool.and(String.eq(o, "("), thunk.last(after))))) + case other: + False{} + +# the rest past `=>`: a leaf, the name called +def thunk.callee(kp: Lex.TokKind, +pp: String, +aa: String, r2: Tree.Node, +name: String) -> Bool: + match r2: + case Tree.NCons{Tree.Leaf{Lex.Tok{kn, n, ln, cn}}, r3}: + thunk.call(kp, pp, aa, n, r3, name) + case other: + False{} + +# the rest past the parameter: a leaf, the arrow +def thunk.lam(kp: Lex.TokKind, +pp: String, rr: Tree.Node, +name: String) -> Bool: + match rr: + case Tree.NCons{Tree.Leaf{Lex.Tok{ka, a, la, ca}}, r2}: + thunk.callee(kp, pp, a, r2, name) + case other: + False{} + +# does the chain open with a thunk of a self-call of the name? +def thunk.at(nn: Tree.Node, +name: String) -> Bool: + match nn: + case Tree.NCons{Tree.Leaf{Lex.Tok{kp, p, lp, cp}}, rr}: + thunk.lam(kp, p, rr, name) + 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: + 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) + case Tree.Stmt{sk, kids, body}: + Nat.add(thunk.count(kids, name), thunk.count(body, name)) + case other: + 0n + +# LAW: over any node, thunk reports one finding for each thunk of a +# self-call, and none for anything else +# BOLT-RULE-U015 +law thunk_walk_counts: + for nn: Tree.Node + for +name: String + for +path: String + {List.length(&2, F.Finding, Thunk.walk(nn, name, path)) == thunk.count(nn, 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: + match ds: + 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)) + +# LAW: thunk reports exactly those, def by def, over the defs of the tree +# BOLT-RULE-U015 +law thunk_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, Thunk.check(Src.Src{path, text, toks, tree, bound, items})) + == thunk.defs(Calls.defs(tree), path) : Nat} + +# scan (BOLT-RULE-U013). Outside a law file the rule walks each def of the +# file that calls itself (Calls.calls) and is not a proof, its body hot, as +# hoist does: a `=>` token makes the rest of its chain cold, a case's pattern +# is cold, and a case arm's body stays hot only when it calls the def. In a +# hot region it reports each call, a plain or dotted name token then a `(` +# group, of a callee other than the def, when one of the arguments the +# callee walks (Scan.slots, over the file's walks, Scan.walks) is exactly the +# lone name of a carried parameter (Hoist.carried). + +# a callee is a plain or a dotted name +def scan.callee(kk: Lex.TokKind) -> Bool: + match kk: + case Lex.TName{}: + True{} + case Lex.TDotted{}: + True{} + case other: + False{} + +# is the token a plain name the list holds? +def scan.named(tok: Lex.Tok, +carried: List<&2, String>) -> Bool: + match tok: + case Lex.Tok{Lex.TName{}, +t, l, c}: + List.contains(~String, ~String.eq, carried, t) + case other: + False{} + +# is the argument exactly the lone name of a carried parameter? +def scan.lone(nn: Tree.Node, +carried: List<&2, String>) -> Bool: + match nn: + case Tree.NCons{Tree.Leaf{tok}, Tree.NNil{}}: + scan.named(tok, carried) + case other: + False{} + +# does some walked argument hold a carried parameter's lone name? +def scan.held(ss: List<&2, Nat>, +as: List<&2, Tree.Node>, +carried: List<&2, String>) -> Bool: + match ss: + case Nil{}: + False{} + case Con{at, rest}: + Bool.or(scan.lone(Calls.arg(as, at), carried), scan.held(rest, as, carried)) + +# does a call site report: a named callee, hot, a `(` group, not the def, +# and a walked argument carried +def scan.call( + kk: Lex.TokKind, + +hot: Bool, + +open: Bool, + +tt: String, + kids: Tree.Node, + +self: String, + +ws: List<&2, Scan.Walk>, + +carried: List<&2, String> +) -> Bool: + Bool.and(scan.callee(kk), Bool.and(hot, Bool.and(open, Bool.and(Bool.not(String.eq(tt, self)), + scan.held(Scan.slots(tt, ws), Calls.args(kids), carried))))) + +# how many calls scan reports under the node, entered hot or cold +def scan.count( + nn: Tree.Node, + +self: String, + +ws: List<&2, Scan.Walk>, + +carried: List<&2, String>, + +hot: Bool +) -> Nat: + 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) + Nat.add(Bool.pick(Nat, scan.call(k, heat, String.eq(o, "("), t, kids, self, ws, carried), 1n, 0n), + Nat.add(scan.count(kids, self, ws, carried, heat), scan.count(rest, self, ws, carried, heat))) + case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}: + scan.count(rest, self, ws, carried, Hoist.warm(hot, k)) + case Tree.NCons{Tree.Group{o, kids, cl}, rest}: + Nat.add(scan.count(kids, self, ws, carried, hot), scan.count(rest, self, ws, carried, hot)) + case Tree.NCons{Tree.Stmt{Tree.SCase{}, kids, +body}, rest}: + Nat.add(scan.count(kids, self, ws, carried, False{}), + Nat.add(scan.count(body, self, ws, carried, Bool.and(hot, Calls.calls(body, self))), + scan.count(rest, self, ws, carried, hot))) + case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}: + Nat.add(scan.count(kids, self, ws, carried, hot), + Nat.add(scan.count(body, self, ws, carried, hot), scan.count(rest, self, ws, carried, hot))) + case Tree.NCons{h, rest}: + scan.count(rest, self, ws, carried, hot) + case other: + 0n + +# how many scan reports over the defs: those in each def that calls itself +# and is not a proof, walked hot, with its carried parameters +def scan.total(ds: List<&2, Calls.Def>, +ws: List<&2, Scan.Walk>, +path: String) -> Nat: + match ds: + case Nil{}: + 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))), + scan.count(body, name, ws, Hoist.carried(sig, body, name), True{}), 0n), scan.total(rest, ws, path)) + +# LAW: outside a law file, scan reports one finding for each call the walk +# above counts, in each def that calls itself and is not a proof, with the +# file's walks; none for anything else +# BOLT-RULE-U013 +law scan_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> + for e: {Paths.is_law_file(path) == False{} : Bool} + {List.length(&2, F.Finding, Scan.check(Src.Src{path, text, toks, tree, bound, items})) + == scan.total(Calls.defs(tree), Scan.walks(Calls.defs(tree)), path) : Nat} + +# LAW: a walk whose def carries no parameter reports nothing, whatever the +# tree, the file's walks and the heat +# BOLT-RULE-U013 +law scan_quiet: + for nn: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +lead: String + for +path: String + for +hot: Bool + {Scan.walk(nn, self, ws, [], lead, path, hot) == Nil{} : List<&2, F.Finding>} + +# the list arguments of the Base list searches: 2, 3 or 4, counted from 0 +def scan.base(+tt: String) -> List<&2, Nat>: + Bool.pick(List<&2, Nat>, List.contains(~String, ~String.eq, ["List.contains", "List.find", "List.filter", + "List.length"], tt), [2n], + Bool.pick(List<&2, Nat>, List.contains(~String, ~String.eq, ["List.any", "List.all"], tt), [3n], + Bool.pick(List<&2, Nat>, List.contains(~String, ~String.eq, ["List.foldl", "List.foldr"], tt), [4n], []))) + +# the arguments the file's walks record for a name, in order +def scan.file(ws: List<&2, Scan.Walk>, +tt: String) -> List<&2, Nat>: + match ws: + case Nil{}: + Nil{} + case Con{Scan.Walk{+nm, at}, rest}: + +more = scan.file(rest, tt) + Bool.pick(List<&2, Nat>, String.eq(nm, tt), at <> more, more) + +# LAW: a callee walks the Base search's list argument, then each argument a +# walk of the file of that name records +# BOLT-RULE-U013 +law scan_slots: + for +tt: String + for ws: List<&2, Scan.Walk> + {Scan.slots(tt, ws) == List.append(&2, Nat, scan.base(tt), scan.file(ws, tt)) : List<&2, Nat>} + # The header rule wrap (BOLT-RULE-S003) judges each def header of the # outline by its sig's tokens (Lex.tokens), once: a finding or none. A # header is across lines when one of its tokens is a newline (Lex.is_nl), so @@ -3377,11 +3693,11 @@ law scope_param: # the findings of each rule a LAWS.bend or a PROOF.bend exempts, rule by rule def scope.law_file(+ss: Src.Src) -> List<&2, List<&2, F.Finding>>: [Pick.check(ss), Tail.check(ss), Concat.check(ss), Eager.check(ss), Rewalk.check(ss), Strict.check(ss), - Hoist.check(ss), Index.check(ss), Ring.check(ss), Table.check(ss), UnitRule.check(ss)] + Hoist.check(ss), Index.check(ss), Ring.check(ss), Table.check(ss), UnitRule.check(ss), Thunk.check(ss)] # LAW: on a LAWS.bend or a PROOF.bend, the findings of each rule its header # exempts there (pick, tail, concat, eager, rewalk, strict, hoist, index, -# ring, table, unit) are the same for any two sources at that path +# ring, table, unit, thunk) are the same for any two sources at that path # BOLT-SCOPE-4 law scope_law_file: for +path: String @@ -4171,6 +4487,29 @@ 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: 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`) @@ -4389,6 +4728,27 @@ law inert_unit: {UnitRule.check(Src.Src{path, text, toks, tree, bound, items}) == UnitRule.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} +# LAW: thunk reads what no string says: two sources as the lexer makes them +# whose trees read the same with strings cut have the same findings +# BOLT-RULE-INERT +law inert_thunk: + for +path: String + for text: String + for +tree: Tree.Node + for toks: List<&2, Lex.Tok> + for bound: Bind.Bound + for items: List<&2, Outline.Item> + for text2: String + for +tree2: Tree.Node + for toks2: List<&2, Lex.Tok> + for bound2: Bind.Bound + for items2: List<&2, Outline.Item> + for +ok: {inert.ok(tree) == True{} : Bool} + for +ok2: {inert.ok(tree2) == True{} : Bool} + for e: {inert.node(tree) == inert.node(tree2) : Tree.Node} + {Thunk.check(Src.Src{path, text, toks, tree, bound, items}) + == Thunk.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} + # LAW: eager reads what no string says: two sources as the lexer makes them # whose trees read the same with strings cut have the same findings # BOLT-RULE-INERT @@ -4811,6 +5171,28 @@ law inert_hoist: {Hoist.check(Src.Src{path, text, toks, tree, bound, items}) == Hoist.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} +# LAW: scan reads what no comment or string says: two sources as the lexer +# makes them whose trees read the same with comments and strings cut have +# the same findings +# BOLT-RULE-INERT +law inert_scan: + for +path: String + for text: String + for +tree: Tree.Node + for toks: List<&2, Lex.Tok> + for bound: Bind.Bound + for items: List<&2, Outline.Item> + for text2: String + for +tree2: Tree.Node + for toks2: List<&2, Lex.Tok> + for bound2: Bind.Bound + for items2: List<&2, Outline.Item> + for +ok: {inert.ok(tree) == True{} : Bool} + for +ok2: {inert.ok(tree2) == True{} : Bool} + for e: {inert.node(tree) == inert.node(tree2) : Tree.Node} + {Scan.check(Src.Src{path, text, toks, tree, bound, items}) + == Scan.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>} + # the tokens of each item's header, with comments and strings cut def inert.sigs(its: List<&2, Outline.Item>) -> List<&2, List<&2, Lex.Tok>>: match its: diff --git a/src/rules/PROOF.bend b/src/rules/PROOF.bend index 560d978..3178a6d 100644 --- a/src/rules/PROOF.bend +++ b/src/rules/PROOF.bend @@ -28,6 +28,8 @@ 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/scan.bend as Scan import ./correctness/chars.bend as Chars import ./correctness/strings.bend as Strings import ./correctness/foreign.bend as Foreign @@ -41,6 +43,7 @@ import ./laws/law.bend as Coverage import ./laws/unsafe.bend as Unsafe import ./imports.bend as Imports import ./digest.bend as Digest +import ./suspicious/thunk.bend as Thunk import ./LAWS.bend as Laws # String.eq's last step (bend 2.0.33 dropped Base's String.eq.fin): whether a @@ -684,6 +687,217 @@ 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) + # one token onto a list the TODO test agrees on law hole.todo.step: for kk: Lex.TokKind @@ -1427,6 +1641,28 @@ def ex.unit(ds, path, n, e): def Laws.unit_exempt(path, _text, _toks, tree, _bound, _items, e): ex.unit(Calls.defs(tree), path, 0n, e) +# thunk's def walk gathers nothing in a law file +law ex.thunk: + for ds: List<&2, Calls.Def> + for +path: String + for +n: Nat + for +e: {Paths.is_law_file(path) == True{} : Bool} + {Thunk.check.go(ds, path, ex.rep(n)) == Nil{} : List<&2, F.Finding>} + +def ex.thunk(ds, path, n, e): + match ds: + case Nil{}: + ex.flat(n, Nil{}) + case Con{Calls.Def{+name, +sig, +body}, rest}: + ex.push( + Calls.exempt(path, sig), + ex.calls(path, sig, e), + _u => Thunk.walk(body, 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): + ex.thunk(Calls.defs(tree), path, 0n, e) + # an or whose second side ends in a true or holds whatever the rest is law ex.or_true: for a: Bool @@ -10151,65 +10387,305 @@ def unit.go(ds, path, acc): def Laws.unit_counts(path, _text, _toks, tree, _bound, _items): unit.go(Calls.defs(tree), path, Nil{}) -# The header rule wrap (BOLT-RULE-S003). The width walk agrees with the -# spec's width from any state; the shape walk, read through wrap.of, takes -# each token the way the spec's read does, so the two agree on the whole -# header; the verdicts agree on what they read. +# 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. -# a token's share of the width is the spec's -law wrap.cost: - for kk: Lex.TokKind - for +tx: String - {Wrap.check.cost(kk, tx) == Laws.wrap.cost(kk, tx) : U32} +# the rule's reads is the law's +law thunk.reads: + for nn: Tree.Node + for +pp: String + {Thunk.reads(nn, pp) == Laws.thunk.reads(nn, pp) : Bool} -def wrap.cost(kk, _tx): - 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{}: +def thunk.reads(nn, pp): + match nn: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, t, l, c}: + {==} + case Tree.Group{o, +kids, cl}: + thunk.reads(kids, pp) + case Tree.Stmt{sk, +kids, +body}: + %thunk.reads(kids, pp) : {Bool.or(Thunk.reads(kids, pp), Thunk.reads(body, pp)) + == Bool.or(_, Laws.thunk.reads(body, pp)) : Bool} + %thunk.reads(body, pp) : {Bool.or(Thunk.reads(kids, pp), Thunk.reads(body, pp)) + == Bool.or(Thunk.reads(kids, pp), _) : Bool} {==} - case Lex.TClose{}: + case Tree.NCons{+h, +t}: + %thunk.reads(h, pp) : {Bool.or(Thunk.reads(h, pp), Thunk.reads(t, pp)) + == Bool.or(_, Laws.thunk.reads(t, pp)) : Bool} + %thunk.reads(t, pp) : {Bool.or(Thunk.reads(h, pp), Thunk.reads(t, pp)) + == Bool.or(Thunk.reads(h, pp), _) : Bool} {==} - case Lex.TComma{}: + case Tree.NNil{}: {==} -# a colon or not, and a colon or not later on: the walk from here is the spec's +# the rule's end of a body is the law's +law thunk.ends: + for nn: Tree.Node + {Thunk.ends(nn) == Laws.thunk.last(nn) : Bool} + +def thunk.ends(nn): + match nn: + case Tree.NCons{h, t}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, s, l, c}: {==} + case Tree.Group{a, b, c}: {==} + case Tree.Stmt{a, b, c}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{a, b}: {==} + case Tree.Leaf{x}: {==} + case Tree.Group{a, b, c}: {==} + case Tree.Stmt{a, b, c}: {==} + case Tree.NNil{}: {==} + +# a finding when b, none otherwise, counts one when b +law thunk.one: + for b: Bool + for -x: F.Finding + {List.length(&2, F.Finding, Bool.pick(List<&2, F.Finding>, b, [x], [])) == Bool.pick(Nat, b, 1n, 0n) : Nat} + +def thunk.one(b, _x): + match b: + case True{}: {==} + case False{}: {==} + +# past the name: the rule's finding is the law's count +law thunk.site.group: + for kp: Lex.TokKind + for +pp: String + for +aa: String + for +nm: String + for +ll: U32 + for +cc: U32 + for r3: Tree.Node + for +name: String + for +path: String + {List.length(&2, F.Finding, Thunk.site.group(kp, pp, aa, nm, ll, cc, r3, name, path)) + == Bool.pick(Nat, Laws.thunk.call(kp, pp, aa, nm, r3, name), 1n, 0n) : Nat} + +def thunk.site.group(kp, pp, aa, nm, ll, cc, r3, name, path): + match r3: + case Tree.NCons{h, +after}: + match h: + case Tree.Group{open, +kids, cl}: + match open: + case Lex.Tok{ko, +o, lo, co}: + +f = Thunk.cite(ll, cc, name, path) + +b = Thunk.hit(Bool.and(Lex.is_name(kp), Bool.not(Thunk.reads(kids, pp))), String.eq(aa, "=>"), + String.eq(nm, name), String.eq(o, "("), Thunk.ends(after)) + %thunk.reads(kids, pp) : {List.length(&2, F.Finding, Bool.pick(List<&2, F.Finding>, b, [f], [])) + == Bool.pick(Nat, Bool.and(Bool.and(Lex.is_name(kp), Bool.not(_)), Bool.and(String.eq(aa, "=>"), + Bool.and(String.eq(nm, name), Bool.and(String.eq(o, "("), Laws.thunk.last(after))))), 1n, 0n) : Nat} + %thunk.ends(after) : {List.length(&2, F.Finding, Bool.pick(List<&2, F.Finding>, b, [f], [])) + == Bool.pick(Nat, Bool.and(Bool.and(Lex.is_name(kp), Bool.not(Thunk.reads(kids, pp))), + Bool.and(String.eq(aa, "=>"), Bool.and(String.eq(nm, name), Bool.and(String.eq(o, "("), _)))), 1n, + 0n) : Nat} + thunk.one(b, f) + case Tree.Leaf{x}: {==} + case Tree.Stmt{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{}: {==} + +# past `=>`: the rule's finding is the law's count +law thunk.site.name: + for kp: Lex.TokKind + for +pp: String + for +aa: String + for r2: Tree.Node + for +name: String + for +path: String + {List.length(&2, F.Finding, Thunk.site.name(kp, pp, aa, r2, name, path)) + == Bool.pick(Nat, Laws.thunk.callee(kp, pp, aa, r2, name), 1n, 0n) : Nat} + +def thunk.site.name(kp, pp, aa, r2, name, path): + match r2: + case Tree.NCons{h, r3}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{kn, n, l, c}: thunk.site.group(kp, pp, aa, n, l, c, r3, name, path) + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{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{}: {==} + +# past the parameter: the rule's finding is the law's count +law thunk.site.lam: + for kp: Lex.TokKind + for +pp: String + for rest: Tree.Node + for +name: String + for +path: String + {List.length(&2, F.Finding, Thunk.site.lam(kp, pp, rest, name, path)) + == Bool.pick(Nat, Laws.thunk.lam(kp, pp, rest, name), 1n, 0n) : Nat} + +def thunk.site.lam(kp, pp, rest, name, path): + match rest: + case Tree.NCons{h, r2}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{ka, a, l, c}: thunk.site.name(kp, pp, a, r2, name, path) + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{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 node and the chain after it: the rule's finding is the law's count +law thunk.site: + for hh: Tree.Node + for rest: Tree.Node + for +name: String + for +path: String + {List.length(&2, F.Finding, Thunk.site(hh, rest, name, path)) + == Bool.pick(Nat, Laws.thunk.at(Tree.NCons{hh, rest}, name), 1n, 0n) : Nat} + +def thunk.site(hh, rest, name, path): + match hh: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{kp, p, l, c}: thunk.site.lam(kp, p, rest, name, path) + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{x, y, z}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + +def Laws.thunk_walk_counts(nn, 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) + 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)) + case Tree.Leaf{tok}: + {==} + case Tree.NNil{}: + {==} + +# one def's findings: none when it is exempt, else its walk +law thunk.stop: + for b: Bool + 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} + +def thunk.stop(b, body, name, path): + match b: + case True{}: + {==} + case False{}: + Laws.thunk_walk_counts(body, name, path) + +# thunk's def walk: the findings gathered so far, then each def's +law thunk.go: + for ds: List<&2, Calls.Def> + for +path: String + for +acc: List<&2, List<&2, F.Finding>> + {List.length(&2, F.Finding, Thunk.check.go(ds, path, acc)) == pick.sum(acc, Laws.thunk.defs(ds, path)) : Nat} + +def thunk.go(ds, path, acc): + match ds: + case Nil{}: + pick.rev(acc, Nil{}) + case Con{d, +rest}: + 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)) + 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))), + thunk.go(rest, path, x <> acc), + Equal.cong(Nat, Nat, n => pick.sum(acc, Nat.add(n, Laws.thunk.defs(rest, path))), + List.length(&2, F.Finding, x), cb, thunk.stop(b, body, name, path))) + +def Laws.thunk_counts(path, _text, _toks, tree, _bound, _items): + thunk.go(Calls.defs(tree), path, Nil{}) + +# The header rule wrap (BOLT-RULE-S003). The width walk agrees with the +# spec's width from any state; the shape walk, read through wrap.of, takes +# each token the way the spec's read does, so the two agree on the whole +# header; the verdicts agree on what they read. + +# a token's share of the width is the spec's +law wrap.cost: + for kk: Lex.TokKind + for +tx: String + {Wrap.check.cost(kk, tx) == Laws.wrap.cost(kk, tx) : U32} + +def wrap.cost(kk, _tx): + 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{}: + {==} + +# a colon or not, and a colon or not later on: the walk from here is the spec's law wrap.width_step: for c: Bool for h: Bool @@ -13754,68 +14230,73 @@ def Laws.scope_law_file(path, text, toks, tree, bound, items, text2, toks2, tree Laws.pick_exempt(path, text, toks, tree, bound, items, e), Laws.pick_exempt(path, text2, toks2, tree2, bound2, items2, e), [Tail.check(s), Concat.check(s), Eager.check(s), Rewalk.check(s), Strict.check(s), - Hoist.check(s), Index.check(s), Ring.check(s), Table.check(s), UnitRule.check(s)], + Hoist.check(s), Index.check(s), Ring.check(s), Table.check(s), UnitRule.check(s), Thunk.check(s)], [Tail.check(t), Concat.check(t), Eager.check(t), Rewalk.check(t), Strict.check(t), - Hoist.check(t), Index.check(t), Ring.check(t), Table.check(t), UnitRule.check(t)], + Hoist.check(t), Index.check(t), Ring.check(t), Table.check(t), UnitRule.check(t), Thunk.check(t)], scope.con(Tail.check(s), Tail.check(t), Laws.tail_exempt(path, text, toks, tree, bound, items, e), Laws.tail_exempt(path, text2, toks2, tree2, bound2, items2, e), [Concat.check(s), Eager.check(s), Rewalk.check(s), Strict.check(s), Hoist.check(s), - Index.check(s), Ring.check(s), Table.check(s), UnitRule.check(s)], + Index.check(s), Ring.check(s), Table.check(s), UnitRule.check(s), Thunk.check(s)], [Concat.check(t), Eager.check(t), Rewalk.check(t), Strict.check(t), Hoist.check(t), - Index.check(t), Ring.check(t), Table.check(t), UnitRule.check(t)], + Index.check(t), Ring.check(t), Table.check(t), UnitRule.check(t), Thunk.check(t)], scope.con(Concat.check(s), Concat.check(t), Laws.concat_exempt(path, text, toks, tree, bound, items, e), Laws.concat_exempt(path, text2, toks2, tree2, bound2, items2, e), [Eager.check(s), Rewalk.check(s), Strict.check(s), Hoist.check(s), Index.check(s), - Ring.check(s), Table.check(s), UnitRule.check(s)], + Ring.check(s), Table.check(s), UnitRule.check(s), Thunk.check(s)], [Eager.check(t), Rewalk.check(t), Strict.check(t), Hoist.check(t), Index.check(t), - Ring.check(t), Table.check(t), UnitRule.check(t)], + Ring.check(t), Table.check(t), UnitRule.check(t), Thunk.check(t)], scope.con(Eager.check(s), Eager.check(t), Laws.eager_exempt(path, text, toks, tree, bound, items, e), Laws.eager_exempt(path, text2, toks2, tree2, bound2, items2, e), [Rewalk.check(s), Strict.check(s), Hoist.check(s), Index.check(s), Ring.check(s), - Table.check(s), UnitRule.check(s)], + Table.check(s), UnitRule.check(s), Thunk.check(s)], [Rewalk.check(t), Strict.check(t), Hoist.check(t), Index.check(t), Ring.check(t), - Table.check(t), UnitRule.check(t)], + Table.check(t), UnitRule.check(t), Thunk.check(t)], scope.con(Rewalk.check(s), Rewalk.check(t), Laws.rewalk_exempt(path, text, toks, tree, bound, items, e), Laws.rewalk_exempt(path, text2, toks2, tree2, bound2, items2, e), [Strict.check(s), Hoist.check(s), Index.check(s), Ring.check(s), Table.check(s), - UnitRule.check(s)], + UnitRule.check(s), Thunk.check(s)], [Strict.check(t), Hoist.check(t), Index.check(t), Ring.check(t), Table.check(t), - UnitRule.check(t)], + UnitRule.check(t), Thunk.check(t)], scope.con(Strict.check(s), Strict.check(t), Laws.strict_exempt(path, text, toks, tree, bound, items, e), Laws.strict_exempt(path, text2, toks2, tree2, bound2, items2, e), - [Hoist.check(s), Index.check(s), Ring.check(s), Table.check(s), UnitRule.check(s)], - [Hoist.check(t), Index.check(t), Ring.check(t), Table.check(t), UnitRule.check(t)], + [Hoist.check(s), Index.check(s), Ring.check(s), Table.check(s), UnitRule.check(s), Thunk.check(s)], + [Hoist.check(t), Index.check(t), Ring.check(t), Table.check(t), UnitRule.check(t), Thunk.check(t)], scope.con(Hoist.check(s), Hoist.check(t), Laws.hoist_exempt(path, text, toks, tree, bound, items, e), Laws.hoist_exempt(path, text2, toks2, tree2, bound2, items2, e), - [Index.check(s), Ring.check(s), Table.check(s), UnitRule.check(s)], - [Index.check(t), Ring.check(t), Table.check(t), UnitRule.check(t)], + [Index.check(s), Ring.check(s), Table.check(s), UnitRule.check(s), Thunk.check(s)], + [Index.check(t), Ring.check(t), Table.check(t), UnitRule.check(t), Thunk.check(t)], scope.con(Index.check(s), Index.check(t), Laws.index_exempt(path, text, toks, tree, bound, items, e), Laws.index_exempt(path, text2, toks2, tree2, bound2, items2, e), - [Ring.check(s), Table.check(s), UnitRule.check(s)], - [Ring.check(t), Table.check(t), UnitRule.check(t)], + [Ring.check(s), Table.check(s), UnitRule.check(s), Thunk.check(s)], + [Ring.check(t), Table.check(t), UnitRule.check(t), Thunk.check(t)], scope.con(Ring.check(s), Ring.check(t), Laws.ring_exempt(path, text, toks, tree, bound, items, e), Laws.ring_exempt(path, text2, toks2, tree2, bound2, items2, e), - [Table.check(s), UnitRule.check(s)], - [Table.check(t), UnitRule.check(t)], + [Table.check(s), UnitRule.check(s), Thunk.check(s)], + [Table.check(t), UnitRule.check(t), Thunk.check(t)], scope.con(Table.check(s), Table.check(t), Laws.table_exempt(path, text, toks, tree, bound, items, e), Laws.table_exempt(path, text2, toks2, tree2, bound2, items2, e), - [UnitRule.check(s)], - [UnitRule.check(t)], + [UnitRule.check(s), Thunk.check(s)], + [UnitRule.check(t), Thunk.check(t)], scope.con(UnitRule.check(s), UnitRule.check(t), Laws.unit_exempt(path, text, toks, tree, bound, items, e), Laws.unit_exempt(path, text2, toks2, tree2, bound2, items2, e), + [Thunk.check(s)], + [Thunk.check(t)], + scope.con(Thunk.check(s), Thunk.check(t), + Laws.thunk_exempt(path, text, toks, tree, bound, items, e), + Laws.thunk_exempt(path, text2, toks2, tree2, bound2, items2, e), Nil{}, Nil{}, - {==}))))))))))) + {==})))))))))))) # closed reports nothing outside a LAWS.bend law scope.closed: @@ -18442,6 +18923,89 @@ 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) + # the tree rules: what calls.bend gives them # ------------------------------------------ @@ -23593,19 +24157,339 @@ def Laws.inert_unit(path, _text, tree, _toks, _bound, _items, _text2, tree2, _to inert.dok.of(tree2, ok2))), e) +# thunk +# ----- -# Inert text, eager and on (BOLT-RULE-INERT): more rules over a file's defs, -# on the lemmas above. +# a name is never cut, read in the order thunk tests it +law inert.thunk.name_code: + for k: Lex.TokKind + {Bool.and(Lex.is_name(k), Laws.inert.blanks(k)) == False{} : Bool} -# eager -# ----- +def inert.thunk.name_code(k): + 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{}: {==} -# a text as the lexer makes it, read that way: cut when it starts with `"` -# or `#`, what a token read that way says whatever its kind -def inert.mk(+tt: String) -> String: - Laws.inert.keep(Laws.inert.marked(tt), tt) +# a node read that way reads the parameter as it did: only name leaves are +# compared, and a name is never cut +law inert.thunk.reads: + for nn: Tree.Node + for +pp: String + {Thunk.reads(Laws.inert.node(nn), pp) == Thunk.reads(nn, pp) : Bool} -# the texts, each read that way +def inert.thunk.reads(nn, pp): + match nn: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{+k, +t, l, c}: + inert.guard(Lex.is_name(k), Laws.inert.blanks(k), t, + z => Bool.or(String.eq(z, pp), String.starts_with(z, pp ++ ".")), inert.thunk.name_code(k)) + case Tree.Group{o, +kids, cl}: + inert.thunk.reads(kids, pp) + case Tree.Stmt{sk, +kids, +body}: + %inert.thunk.reads(kids, pp) : {Bool.or(Thunk.reads(Laws.inert.node(kids), pp), Thunk.reads(Laws.inert.node(body), + pp)) == Bool.or(_, Thunk.reads(body, pp)) : Bool} + %inert.thunk.reads(body, pp) : {Bool.or(Thunk.reads(Laws.inert.node(kids), pp), Thunk.reads(Laws.inert.node(body), + pp)) == Bool.or(Thunk.reads(Laws.inert.node(kids), pp), _) : Bool} + {==} + case Tree.NCons{+h, +t}: + %inert.thunk.reads(h, pp) : {Bool.or(Thunk.reads(Laws.inert.node(h), pp), Thunk.reads(Laws.inert.node(t), pp)) + == Bool.or(_, Thunk.reads(t, pp)) : Bool} + %inert.thunk.reads(t, pp) : {Bool.or(Thunk.reads(Laws.inert.node(h), pp), Thunk.reads(Laws.inert.node(t), pp)) + == Bool.or(Thunk.reads(Laws.inert.node(h), pp), _) : Bool} + {==} + case Tree.NNil{}: + {==} + +# a chain read that way ends a body as it did: kinds are kept +law inert.thunk.ends: + for nn: Tree.Node + {Thunk.ends(Laws.inert.node(nn)) == Thunk.ends(nn) : Bool} + +def inert.thunk.ends(nn): + match nn: + case Tree.NCons{h, t}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, s, l, c}: {==} + case Tree.Group{a, b, c}: {==} + case Tree.Stmt{a, b, c}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{a, b}: {==} + case Tree.Leaf{x}: {==} + case Tree.Group{a, b, c}: {==} + case Tree.Stmt{a, b, c}: {==} + case Tree.NNil{}: {==} + +# the lead read that way is the lead: the group reads the parameter as it +# did, and a name parameter is never cut +law inert.thunk.lead: + for +kp: Lex.TokKind + for +pp: String + for +kids: Tree.Node + {Bool.and(Lex.is_name(kp), Bool.not(Thunk.reads(Laws.inert.node(kids), Laws.inert.keep(Laws.inert.blanks(kp), pp)))) + == Bool.and(Lex.is_name(kp), Bool.not(Thunk.reads(kids, pp))) : Bool} + +def inert.thunk.lead(kp, pp, kids): + Equal.trans(Bool, + Bool.and(Lex.is_name(kp), Bool.not(Thunk.reads(Laws.inert.node(kids), Laws.inert.keep(Laws.inert.blanks(kp), pp)))), + Bool.and(Lex.is_name(kp), Bool.not(Thunk.reads(kids, Laws.inert.keep(Laws.inert.blanks(kp), pp)))), + Bool.and(Lex.is_name(kp), Bool.not(Thunk.reads(kids, pp))), + Equal.cong(Bool, Bool, z => Bool.and(Lex.is_name(kp), Bool.not(z)), + Thunk.reads(Laws.inert.node(kids), Laws.inert.keep(Laws.inert.blanks(kp), pp)), + Thunk.reads(kids, Laws.inert.keep(Laws.inert.blanks(kp), pp)), + inert.thunk.reads(kids, Laws.inert.keep(Laws.inert.blanks(kp), pp))), + inert.guard(Lex.is_name(kp), Laws.inert.blanks(kp), pp, z => Bool.not(Thunk.reads(kids, z)), + inert.thunk.name_code(kp))) + +# past the name, read that way: the finding it gave +law inert.thunk.group: + for +kp: Lex.TokKind + for +pp: String + for +ka: Lex.TokKind + for +aa: String + for +kn: Lex.TokKind + for +nm: String + for +ll: U32 + for +cc: U32 + for r3: Tree.Node + for +name: String + for +path: String + for ea: {Laws.inert.fits.go(Laws.inert.blanks(ka), aa) == True{} : Bool} + for ef: {Laws.inert.fits.go(Laws.inert.blanks(kn), nm) == True{} : Bool} + for en: {Laws.inert.marked(name) == False{} : Bool} + {Thunk.site.group(kp, Laws.inert.keep(Laws.inert.blanks(kp), pp), Laws.inert.keep(Laws.inert.blanks(ka), aa), + Laws.inert.keep(Laws.inert.blanks(kn), nm), ll, cc, Laws.inert.node(r3), name, path) + == Thunk.site.group(kp, pp, aa, nm, ll, cc, r3, name, path) : List<&2, F.Finding>} + +def inert.thunk.group(kp, pp, ka, aa, kn, nm, ll, cc, r3, name, path, ea, ef, en): + match r3: + case Tree.NCons{h, +after}: + match h: + case Tree.Group{open, +kids, cl}: + match open: + case Lex.Tok{ko, +o, lo, co}: + +f = Thunk.cite(ll, cc, name, path) + +l1 = Bool.and(Lex.is_name(kp), + Bool.not(Thunk.reads(Laws.inert.node(kids), Laws.inert.keep(Laws.inert.blanks(kp), pp)))) + +a1 = String.eq(Laws.inert.keep(Laws.inert.blanks(ka), aa), "=>") + +n1 = String.eq(Laws.inert.keep(Laws.inert.blanks(kn), nm), name) + +e1 = Thunk.ends(Laws.inert.node(after)) + +oo = String.eq(o, "(") + %inert.thunk.lead(kp, pp, kids) : {Bool.pick(List<&2, F.Finding>, Thunk.hit(l1, a1, n1, oo, e1), [f], []) + == Bool.pick(List<&2, F.Finding>, Thunk.hit(_, String.eq(aa, "=>"), String.eq(nm, name), oo, + Thunk.ends(after)), [f], []) : List<&2, F.Finding>} + %inert.eq_keep(Laws.inert.blanks(ka), aa, "=>", ea, {==}) : {Bool.pick(List<&2, F.Finding>, + Thunk.hit(l1, a1, n1, oo, e1), [f], []) + == Bool.pick(List<&2, F.Finding>, Thunk.hit(l1, _, String.eq(nm, name), oo, Thunk.ends(after)), [f], + []) : List<&2, F.Finding>} + %inert.eq_keep(Laws.inert.blanks(kn), nm, name, ef, en) : {Bool.pick(List<&2, F.Finding>, + Thunk.hit(l1, a1, n1, oo, e1), [f], []) + == Bool.pick(List<&2, F.Finding>, Thunk.hit(l1, a1, _, oo, Thunk.ends(after)), [f], []) + : List<&2, F.Finding>} + %inert.thunk.ends(after) : {Bool.pick(List<&2, F.Finding>, Thunk.hit(l1, a1, n1, oo, e1), [f], []) + == Bool.pick(List<&2, F.Finding>, Thunk.hit(l1, a1, n1, oo, _), [f], []) : List<&2, F.Finding>} + {==} + case Tree.Leaf{x}: {==} + case Tree.Stmt{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{}: {==} + +# past `=>`, read that way: the finding it gave +law inert.thunk.name: + for +kp: Lex.TokKind + for +pp: String + for +ka: Lex.TokKind + for +aa: String + for r2: Tree.Node + for +name: String + for +path: String + for ea: {Laws.inert.fits.go(Laws.inert.blanks(ka), aa) == True{} : Bool} + for en: {Laws.inert.marked(name) == False{} : Bool} + for e: {Laws.inert.ok(r2) == True{} : Bool} + {Thunk.site.name(kp, Laws.inert.keep(Laws.inert.blanks(kp), pp), Laws.inert.keep(Laws.inert.blanks(ka), aa), + Laws.inert.node(r2), name, path) + == Thunk.site.name(kp, pp, aa, r2, name, path) : List<&2, F.Finding>} + +def inert.thunk.name(kp, pp, ka, aa, r2, name, path, ea, en, e): + match r2: + case Tree.NCons{h, +r3}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{+kn, +n, l, c}: + inert.thunk.group(kp, pp, ka, aa, kn, n, l, c, r3, name, path, ea, + inert.and_l(Laws.inert.fits.go(Laws.inert.blanks(kn), n), Laws.inert.ok(r3), e), en) + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{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{}: {==} + +# past the parameter, read that way: the finding it gave +law inert.thunk.lam: + for +kp: Lex.TokKind + for +pp: String + for rest: Tree.Node + for +name: String + for +path: String + for en: {Laws.inert.marked(name) == False{} : Bool} + for +e: {Laws.inert.ok(rest) == True{} : Bool} + {Thunk.site.lam(kp, Laws.inert.keep(Laws.inert.blanks(kp), pp), Laws.inert.node(rest), name, path) + == Thunk.site.lam(kp, pp, rest, name, path) : List<&2, F.Finding>} + +def inert.thunk.lam(kp, pp, rest, name, path, en, e): + match rest: + case Tree.NCons{h, +r2}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{+ka, +a, l, c}: + inert.thunk.name(kp, pp, ka, a, r2, name, path, + inert.and_l(Laws.inert.fits.go(Laws.inert.blanks(ka), a), Laws.inert.ok(r2), e), en, + inert.and_r(Laws.inert.fits.go(Laws.inert.blanks(ka), a), Laws.inert.ok(r2), e)) + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{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 node and the chain after it, read that way: the finding they gave +law inert.thunk.site: + for hh: Tree.Node + for rest: Tree.Node + for +name: String + for +path: String + for en: {Laws.inert.marked(name) == False{} : Bool} + for e: {Laws.inert.ok(rest) == True{} : Bool} + {Thunk.site(Laws.inert.node(hh), Laws.inert.node(rest), name, path) == Thunk.site(hh, rest, name, path) + : List<&2, F.Finding>} + +def inert.thunk.site(hh, rest, name, path, en, e): + match hh: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{+kp, +p, l, c}: inert.thunk.lam(kp, p, rest, name, path, en, e) + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{x, y, z}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + +# 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 +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>} + +def inert.thunk.walk(nn, 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) + 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)]) + : List<&2, F.Finding>} + %inert.thunk.walk(body, 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}: + {==} + case Tree.NNil{}: + {==} + +# thunk over the defs read that way reports what it reports over the defs +law inert.thunk.go: + for ds: List<&2, Calls.Def> + for +path: String + for +acc: List<&2, List<&2, F.Finding>> + for +e: {inert.dok(ds) == True{} : Bool} + {Thunk.check.go(inert.defs(ds), path, acc) == Thunk.check.go(ds, path, acc) : List<&2, F.Finding>} + +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)) + %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.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>} + inert.thunk.go(rest, path, lst <> acc, inert.dok.rest(name, sig, body, rest, e)) + +def Laws.inert_thunk(path, _text, tree, _toks, _bound, _items, _text2, tree2, _toks2, _bound2, _items2, ok, ok2, e): + inert.via(Tree.Node, z => Thunk.check.go(Calls.defs(z), path, []), tree, tree2, Laws.inert.node(tree), + Laws.inert.node(tree2), + inert.lift(z => Thunk.check.go(z, path, []), tree, inert.thunk.go(Calls.defs(tree), path, [], inert.dok.of(tree, + ok))), + inert.lift(z => Thunk.check.go(z, path, []), tree2, inert.thunk.go(Calls.defs(tree2), path, [], + inert.dok.of(tree2, ok2))), + e) + + +# Inert text, eager and on (BOLT-RULE-INERT): more rules over a file's defs, +# on the lemmas above. + +# eager +# ----- + +# a text as the lexer makes it, read that way: cut when it starts with `"` +# or `#`, what a token read that way says whatever its kind +def inert.mk(+tt: String) -> String: + Laws.inert.keep(Laws.inert.marked(tt), tt) + +# the texts, each read that way def inert.mks(xs: List<&2, String>) -> List<&2, String>: match xs: case Nil{}: Nil{} @@ -31267,3 +32151,1669 @@ def Laws.inert_wrap(path, _text, _toks, _tree, _bound, items, _text2, _toks2, _t %ei : {inert.wrap.go(i1, s1, path) == inert.wrap.go(_, Laws.inert.sigs(items2), path) : List<&2, F.Finding>} %es : {inert.wrap.go(i1, s1, path) == inert.wrap.go(i1, _, path) : List<&2, F.Finding>} {==} + +# scan +# ---- + +def Laws.scan_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 => Scan.check.on(Calls.defs(tree), 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> + for +tt: String + {Scan.file_at(ws, tt) == Laws.scan.file(ws, tt) : List<&2, Nat>} + +def scan.file_at(ws, tt): + match ws: + case Nil{}: + {==} + case Con{Scan.Walk{+nm, +at}, +rest}: + %scan.file_at(rest, tt) : {Scan.file_at(Scan.Walk{nm, at} <> rest, tt) + == Bool.pick(List<&2, Nat>, String.eq(nm, tt), at <> _, _) : List<&2, Nat>} + {==} + +def Laws.scan_slots(tt, ws): + %scan.file_at(ws, tt) : {Scan.slots(tt, ws) == List.append(&2, Nat, Laws.scan.base(tt), _) : List<&2, Nat>} + {==} + +# three finding lists, each empty, join empty +law scan.nil3: + for -a: List<&2, F.Finding> + for -b: List<&2, F.Finding> + for -c: List<&2, F.Finding> + for ea: {a == Nil{} : List<&2, F.Finding>} + for eb: {b == Nil{} : List<&2, F.Finding>} + for ec: {c == Nil{} : List<&2, F.Finding>} + {List.concat(&2, F.Finding, [a, b, c]) == Nil{} : List<&2, F.Finding>} + +def scan.nil3(a, b, c, ea, eb, ec): + %Equal.sym(List<&2, F.Finding>, a, Nil{}, ea) : {List.concat(&2, F.Finding, [_, b, c]) == Nil{} + : List<&2, F.Finding>} + %Equal.sym(List<&2, F.Finding>, b, Nil{}, eb) : {List.concat(&2, F.Finding, [Nil{}, _, c]) == Nil{} + : List<&2, F.Finding>} + %Equal.sym(List<&2, F.Finding>, c, Nil{}, ec) : {List.concat(&2, F.Finding, [Nil{}, Nil{}, _]) == Nil{} + : List<&2, F.Finding>} + {==} + +# two finding lists, each empty, join empty +law scan.nil2: + for -a: List<&2, F.Finding> + for -b: List<&2, F.Finding> + for ea: {a == Nil{} : List<&2, F.Finding>} + for eb: {b == Nil{} : List<&2, F.Finding>} + {List.concat(&2, F.Finding, [a, b]) == Nil{} : List<&2, F.Finding>} + +def scan.nil2(a, b, ea, eb): + %Equal.sym(List<&2, F.Finding>, a, Nil{}, ea) : {List.concat(&2, F.Finding, [_, b]) == Nil{} : List<&2, F.Finding>} + %Equal.sym(List<&2, F.Finding>, b, Nil{}, eb) : {List.concat(&2, F.Finding, [Nil{}, _]) == Nil{} + : List<&2, F.Finding>} + {==} + +# no name is kept against no names +law scan.keep_nil: + for mm: Maybe<&2, String> + {Scan.keep_in(mm, []) == None{} : Maybe<&2, String>} + +def scan.keep_nil(mm): + match mm: + case None{}: + {==} + case Some{nm}: + {==} + +# no walked argument is one of no names +law scan.found_nil: + for ss: List<&2, Nat> + for +as: List<&2, Tree.Node> + {Scan.found(ss, as, []) == None{} : Maybe<&2, String>} + +def scan.found_nil(ss, as): + match ss: + case Nil{}: + {==} + case Con{+at, +rest}: + %Equal.sym(Maybe<&2, String>, Scan.keep_in(Scan.name_of(Calls.arg(as, at)), []), None{}, + scan.keep_nil(Scan.name_of(Calls.arg(as, at)))) : {Scan.first(_, Scan.found(rest, as, [])) == None{} + : Maybe<&2, String>} + scan.found_nil(rest, as) + +# a stop that gives nothing either way gives nothing +law scan.stop_nil: + for c: Bool + {Lazy.stop(List<&2, F.Finding>, c, [], _u => Nil{}) == Nil{} : List<&2, F.Finding>} + +def scan.stop_nil(c): + match c: + case True{}: + {==} + case False{}: + {==} + +# a named call reports nothing when nothing is carried +law scan.on_nil: + for +hot: Bool + for +open: Bool + for +tt: String + for +line: U32 + for +col: U32 + for +kids: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +lead: String + for +path: String + {Scan.on_name(hot, open, tt, line, col, kids, self, ws, [], lead, path) == Nil{} : List<&2, F.Finding>} + +def scan.on_nil(hot, open, tt, line, col, kids, self, ws, lead, path): + %Equal.sym(Maybe<&2, String>, Scan.found(Scan.slots(tt, ws), Calls.args(kids), []), None{}, + scan.found_nil(Scan.slots(tt, ws), Calls.args(kids))) : {Lazy.stop(List<&2, F.Finding>, + Bool.not(Bool.and(hot, Bool.and(open, Bool.not(String.eq(tt, self))))), [], + _u => Scan.cite(_, tt, line, col, self, lead, path)) == Nil{} : List<&2, F.Finding>} + scan.stop_nil(Bool.not(Bool.and(hot, Bool.and(open, Bool.not(String.eq(tt, self)))))) + +# a call reports nothing when nothing is carried, whatever its callee's kind +law scan.hit_nil: + for kk: Lex.TokKind + for +hot: Bool + for +open: Bool + for +tt: String + for +line: U32 + for +col: U32 + for +kids: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +lead: String + for +path: String + {Scan.call_hit(kk, hot, open, tt, line, col, kids, self, ws, [], lead, path) == Nil{} : List<&2, F.Finding>} + +def scan.hit_nil(kk, hot, open, tt, line, col, kids, self, ws, lead, path): + match kk: + case Lex.TName{}: + scan.on_nil(hot, open, tt, line, col, kids, self, ws, lead, path) + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + scan.on_nil(hot, open, tt, line, col, kids, self, ws, lead, path) + 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{}: + {==} + +def Laws.scan_quiet(nn, self, ws, lead, path, hot): + match nn: + case Tree.Leaf{tok}: + {==} + case Tree.Group{o, gk, cl}: + {==} + case Tree.Stmt{kind, sk, sb}: + {==} + case Tree.NNil{}: + {==} + case Tree.NCons{h, +rest}: + match h: + case Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}: + match rest: + case Tree.Leaf{tok}: + {==} + case Tree.Group{o, gk, cl}: + {==} + case Tree.Stmt{kind, sk, sb}: + {==} + case Tree.NNil{}: + {==} + case Tree.NCons{rh, +rr}: + match rh: + case Tree.Group{Lex.Tok{gk, +o, gl, gc}, +kids, cl}: + scan.nil3(Scan.call_hit(k, Hoist.warm(hot, k), String.eq(o, "("), t, l, c, kids, self, ws, [], lead, + path), + Scan.walk(kids, self, ws, [], lead, path, Hoist.warm(hot, k)), + Scan.walk(rr, self, ws, [], lead, path, Hoist.warm(hot, k)), + scan.hit_nil(k, Hoist.warm(hot, k), String.eq(o, "("), t, l, c, kids, self, ws, lead, path), + Laws.scan_quiet(kids, self, ws, lead, path, Hoist.warm(hot, k)), Laws.scan_quiet(rr, self, ws, + lead, path, Hoist.warm(hot, k))) + case Tree.Leaf{tok}: + Laws.scan_quiet(rest, self, ws, lead, path, Hoist.warm(hot, k)) + case Tree.Stmt{kind, sk, sb}: + Laws.scan_quiet(rest, self, ws, lead, path, Hoist.warm(hot, k)) + case Tree.NNil{}: + Laws.scan_quiet(rest, self, ws, lead, path, Hoist.warm(hot, k)) + case Tree.NCons{nh, nt}: + Laws.scan_quiet(rest, self, ws, lead, path, Hoist.warm(hot, k)) + case Tree.Group{o, +kids, cl}: + scan.nil2(Scan.walk(kids, self, ws, [], lead, path, hot), Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, hot), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.Stmt{kind, +kids, +body}: + match kind: + case Tree.SDef{}: + scan.nil3(Scan.walk(kids, self, ws, [], lead, path, hot), Scan.walk(body, self, ws, [], lead, path, hot), + Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, hot), Laws.scan_quiet(body, self, ws, lead, path, + hot), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.SType{}: + scan.nil3(Scan.walk(kids, self, ws, [], lead, path, hot), Scan.walk(body, self, ws, [], lead, path, hot), + Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, hot), Laws.scan_quiet(body, self, ws, lead, path, + hot), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.SLaw{}: + scan.nil3(Scan.walk(kids, self, ws, [], lead, path, hot), Scan.walk(body, self, ws, [], lead, path, hot), + Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, hot), Laws.scan_quiet(body, self, ws, lead, path, + hot), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.SImport{}: + scan.nil3(Scan.walk(kids, self, ws, [], lead, path, hot), Scan.walk(body, self, ws, [], lead, path, hot), + Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, hot), Laws.scan_quiet(body, self, ws, lead, path, + hot), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.SCase{}: + scan.nil3(Scan.walk(kids, self, ws, [], lead, path, False{}), Scan.walk(body, self, ws, [], lead, path, + Bool.and(hot, Calls.calls(body, self))), Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, False{}), Laws.scan_quiet(body, self, ws, lead, path, + Bool.and(hot, Calls.calls(body, self))), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.SFor{}: + scan.nil3(Scan.walk(kids, self, ws, [], lead, path, hot), Scan.walk(body, self, ws, [], lead, path, hot), + Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, hot), Laws.scan_quiet(body, self, ws, lead, path, + hot), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.SLet{}: + scan.nil3(Scan.walk(kids, self, ws, [], lead, path, hot), Scan.walk(body, self, ws, [], lead, path, hot), + Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, hot), Laws.scan_quiet(body, self, ws, lead, path, + hot), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.STerm{}: + scan.nil3(Scan.walk(kids, self, ws, [], lead, path, hot), Scan.walk(body, self, ws, [], lead, path, hot), + Scan.walk(rest, self, ws, [], lead, path, hot), + Laws.scan_quiet(kids, self, ws, lead, path, hot), Laws.scan_quiet(body, self, ws, lead, path, + hot), Laws.scan_quiet(rest, self, ws, lead, path, hot)) + case Tree.NNil{}: + Laws.scan_quiet(rest, self, ws, lead, path, hot) + case Tree.NCons{nh, nt}: + Laws.scan_quiet(rest, self, ws, lead, path, hot) + +# whether an answer has a name +def scan.some(mm: Maybe<&2, String>) -> Bool: + match mm: + case None{}: + False{} + case Some{nm}: + True{} + +# a finding exactly when there is a name +law scan.cite_len: + for mm: Maybe<&2, String> + for +tt: String + for +line: U32 + for +col: U32 + for +self: String + for +lead: String + for +path: String + {List.length(&2, F.Finding, Scan.cite(mm, tt, line, col, self, lead, path)) == Bool.pick(Nat, scan.some(mm), 1n, 0n) + : Nat} + +def scan.cite_len(mm, _tt, _line, _col, _self, _lead, _path): + match mm: + case None{}: + {==} + case Some{nm}: + {==} + +# the first of two answers has a name when either has +law scan.first_some: + for aa: Maybe<&2, String> + for bb: Maybe<&2, String> + {scan.some(Scan.first(aa, bb)) == Bool.or(scan.some(aa), scan.some(bb)) : Bool} + +def scan.first_some(aa, _bb): + match aa: + case None{}: + {==} + case Some{nm}: + {==} + +# a kept name is there exactly when the list holds it +law scan.pick_some: + for b: Bool + for +nm: String + {scan.some(Bool.pick(Maybe<&2, String>, b, Some{nm}, None{})) == b : Bool} + +def scan.pick_some(b, _nm): + match b: + case True{}: + {==} + case False{}: + {==} + +# a token kept against the names is the law's named token +law scan.named: + for tok: Lex.Tok + for +carried: List<&2, String> + {scan.some(Scan.keep_in(Scan.name_tok(tok), carried)) == Laws.scan.named(tok, carried) : Bool} + +def scan.named(tok, carried): + match tok: + case Lex.Tok{k, +t, l, c}: + match k: + case Lex.TName{}: + scan.pick_some(List.contains(~String, ~String.eq, carried, t), t) + 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 argument kept against the names is the law's lone name +law scan.lone: + for nn: Tree.Node + for +carried: List<&2, String> + {scan.some(Scan.keep_in(Scan.name_of(nn), carried)) == Laws.scan.lone(nn, carried) : Bool} + +def scan.lone(nn, carried): + match nn: + case Tree.NCons{h, r}: + match h: + case Tree.Leaf{tok}: + match r: + case Tree.NNil{}: + scan.named(tok, carried) + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NCons{x, y}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{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 found step's two sides are the law's +law scan.found.or: + for +arg: Tree.Node + for rest: List<&2, Nat> + for +as: List<&2, Tree.Node> + for +carried: List<&2, String> + for ih: {scan.some(Scan.found(rest, as, carried)) == Laws.scan.held(rest, as, carried) : Bool} + {Bool.or(scan.some(Scan.keep_in(Scan.name_of(arg), carried)), scan.some(Scan.found(rest, as, carried))) + == Bool.or(Laws.scan.lone(arg, carried), Laws.scan.held(rest, as, carried)) : Bool} + +def scan.found.or(arg, rest, as, carried, ih): + %scan.lone(arg, carried) : {Bool.or(scan.some(Scan.keep_in(Scan.name_of(arg), carried)), + scan.some(Scan.found(rest, as, carried))) == Bool.or(_, Laws.scan.held(rest, as, carried)) : Bool} + %ih : {Bool.or(scan.some(Scan.keep_in(Scan.name_of(arg), carried)), + scan.some(Scan.found(rest, as, carried))) == Bool.or(scan.some(Scan.keep_in(Scan.name_of(arg), carried)), _) + : Bool} + {==} + +# a walked argument is found exactly when the law's held says so +law scan.found: + for ss: List<&2, Nat> + for +as: List<&2, Tree.Node> + for +carried: List<&2, String> + {scan.some(Scan.found(ss, as, carried)) == Laws.scan.held(ss, as, carried) : Bool} + +def scan.found(ss, as, carried): + match ss: + case Nil{}: + {==} + case Con{+at, +rest}: + +arg = Calls.arg(as, at) + +lh = Laws.scan.lone(arg, carried) + Equal.trans(Bool, scan.some(Scan.first(Scan.keep_in(Scan.name_of(arg), carried), Scan.found(rest, as, carried))), + Bool.or(scan.some(Scan.keep_in(Scan.name_of(arg), carried)), scan.some(Scan.found(rest, as, carried))), + Bool.or(lh, Laws.scan.held(rest, as, carried)), + scan.first_some(Scan.keep_in(Scan.name_of(arg), carried), Scan.found(rest, as, carried)), + scan.found.or(arg, rest, as, carried, scan.found(rest, as, carried))) + +# a gated finding list counts when the gate opens and it counts +law scan.gate_len: + for hot: Bool + for open: Bool + for q: Bool + for -x: List<&2, F.Finding> + for -hb: Bool + for ex: {List.length(&2, F.Finding, x) == Bool.pick(Nat, hb, 1n, 0n) : Nat} + {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(hot, Bool.and(open, Bool.not(q)))), [], + _u => x)) == Bool.pick(Nat, Bool.and(hot, Bool.and(open, Bool.and(Bool.not(q), hb))), 1n, 0n) : Nat} + +def scan.gate_len(hot, open, q, _x, _hb, ex): + match hot: + case False{}: + {==} + case True{}: + match open: + case False{}: + {==} + case True{}: + match q: + case True{}: + {==} + case False{}: + ex + +# a named call's finding count is the law's +law scan.on_len: + for +hot: Bool + for +open: Bool + for +tt: String + for +line: U32 + for +col: U32 + for +kids: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +carried: List<&2, String> + for +lead: String + for +path: String + {List.length(&2, F.Finding, Scan.on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path)) + == Bool.pick(Nat, Bool.and(hot, Bool.and(open, Bool.and(Bool.not(String.eq(tt, self)), + Laws.scan.held(Scan.slots(tt, ws), Calls.args(kids), carried)))), 1n, 0n) : Nat} + +def scan.on_len(hot, open, tt, line, col, kids, self, ws, carried, lead, path): + +fd = Scan.found(Scan.slots(tt, ws), Calls.args(kids), carried) + +hb = Laws.scan.held(Scan.slots(tt, ws), Calls.args(kids), carried) + scan.gate_len(hot, open, String.eq(tt, self), Scan.cite(fd, tt, line, col, self, lead, path), hb, + Equal.trans(Nat, List.length(&2, F.Finding, Scan.cite(fd, tt, line, col, self, lead, path)), + Bool.pick(Nat, scan.some(fd), 1n, 0n), Bool.pick(Nat, hb, 1n, 0n), + scan.cite_len(fd, tt, line, col, self, lead, path), + Equal.cong(Bool, Nat, b => Bool.pick(Nat, b, 1n, 0n), scan.some(fd), hb, + scan.found(Scan.slots(tt, ws), Calls.args(kids), carried)))) + +# a call's finding count is the law's, whatever its callee's kind +law scan.hit_len: + for kk: Lex.TokKind + for +hot: Bool + for +open: Bool + for +tt: String + for +line: U32 + for +col: U32 + for +kids: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +carried: List<&2, String> + for +lead: String + for +path: String + {List.length(&2, F.Finding, Scan.call_hit(kk, hot, open, tt, line, col, kids, self, ws, carried, lead, path)) + == Bool.pick(Nat, Laws.scan.call(kk, hot, open, tt, kids, self, ws, carried), 1n, 0n) : Nat} + +def scan.hit_len(kk, hot, open, tt, line, col, kids, self, ws, carried, lead, path): + match kk: + case Lex.TName{}: + scan.on_len(hot, open, tt, line, col, kids, self, ws, carried, lead, path) + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + scan.on_len(hot, open, tt, line, col, kids, self, ws, carried, lead, path) + 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{}: + {==} + +# scan's walk counts the calls the law counts, at every heat +law scan.walk: + for nn: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +carried: List<&2, String> + for +lead: String + for +path: String + for +hot: Bool + {List.length(&2, F.Finding, Scan.walk(nn, self, ws, carried, lead, path, hot)) + == Laws.scan.count(nn, self, ws, carried, hot) : Nat} + +def scan.walk(nn, self, ws, carried, lead, path, hot): + match nn: + case Tree.Leaf{tok}: + {==} + case Tree.Group{o, gk, cl}: + {==} + case Tree.Stmt{kind, sk, sb}: + {==} + case Tree.NNil{}: + {==} + case Tree.NCons{h, +rest}: + match h: + case Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}: + match rest: + case Tree.Leaf{tok}: + {==} + case Tree.Group{o, gk, cl}: + {==} + case Tree.Stmt{kind, sk, sb}: + {==} + case Tree.NNil{}: + {==} + case Tree.NCons{rh, +rr}: + match rh: + case Tree.Group{Lex.Tok{gk, +o, gl, gc}, +kids, cl}: + chars.sum(Scan.call_hit(k, Hoist.warm(hot, k), String.eq(o, "("), t, l, c, kids, self, ws, carried, + lead, path), + Scan.walk(kids, self, ws, carried, lead, path, Hoist.warm(hot, k)), + Scan.walk(rr, self, ws, carried, lead, path, Hoist.warm(hot, k)), + Bool.pick(Nat, Laws.scan.call(k, Hoist.warm(hot, k), String.eq(o, "("), t, kids, self, ws, + carried), 1n, 0n), + Laws.scan.count(kids, self, ws, carried, Hoist.warm(hot, k)), Laws.scan.count(rr, self, ws, + carried, Hoist.warm(hot, k)), + scan.hit_len(k, Hoist.warm(hot, k), String.eq(o, "("), t, l, c, kids, self, ws, carried, lead, + path), + scan.walk(kids, self, ws, carried, lead, path, Hoist.warm(hot, k)), + scan.walk(rr, self, ws, carried, lead, path, Hoist.warm(hot, k))) + case Tree.Leaf{tok}: + scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k)) + case Tree.Stmt{kind, sk, sb}: + scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k)) + case Tree.NNil{}: + scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k)) + case Tree.NCons{nh, nt}: + scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k)) + case Tree.Group{o, +kids, cl}: + index.two(Scan.walk(kids, self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, carried, lead, path, + hot), + Laws.scan.count(kids, self, ws, carried, hot), Laws.scan.count(rest, self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, hot), scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.Stmt{kind, +kids, +body}: + match kind: + case Tree.SDef{}: + chars.sum(Scan.walk(kids, self, ws, carried, lead, path, hot), Scan.walk(body, self, ws, carried, lead, + path, hot), + Scan.walk(rest, self, ws, carried, lead, path, hot), Laws.scan.count(kids, self, ws, carried, hot), + Laws.scan.count(body, self, ws, carried, hot), Laws.scan.count(rest, self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, hot), scan.walk(body, self, ws, carried, lead, path, + hot), + scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.SType{}: + chars.sum(Scan.walk(kids, self, ws, carried, lead, path, hot), Scan.walk(body, self, ws, carried, lead, + path, hot), + Scan.walk(rest, self, ws, carried, lead, path, hot), Laws.scan.count(kids, self, ws, carried, hot), + Laws.scan.count(body, self, ws, carried, hot), Laws.scan.count(rest, self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, hot), scan.walk(body, self, ws, carried, lead, path, + hot), + scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.SLaw{}: + chars.sum(Scan.walk(kids, self, ws, carried, lead, path, hot), Scan.walk(body, self, ws, carried, lead, + path, hot), + Scan.walk(rest, self, ws, carried, lead, path, hot), Laws.scan.count(kids, self, ws, carried, hot), + Laws.scan.count(body, self, ws, carried, hot), Laws.scan.count(rest, self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, hot), scan.walk(body, self, ws, carried, lead, path, + hot), + scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.SImport{}: + chars.sum(Scan.walk(kids, self, ws, carried, lead, path, hot), Scan.walk(body, self, ws, carried, lead, + path, hot), + Scan.walk(rest, self, ws, carried, lead, path, hot), Laws.scan.count(kids, self, ws, carried, hot), + Laws.scan.count(body, self, ws, carried, hot), Laws.scan.count(rest, self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, hot), scan.walk(body, self, ws, carried, lead, path, + hot), + scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.SCase{}: + chars.sum(Scan.walk(kids, self, ws, carried, lead, path, False{}), Scan.walk(body, self, ws, carried, + lead, path, Bool.and(hot, Calls.calls(body, self))), + Scan.walk(rest, self, ws, carried, lead, path, hot), Laws.scan.count(kids, self, ws, carried, False{}), + Laws.scan.count(body, self, ws, carried, Bool.and(hot, Calls.calls(body, self))), Laws.scan.count(rest, + self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, False{}), scan.walk(body, self, ws, carried, lead, path, + Bool.and(hot, Calls.calls(body, self))), + scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.SFor{}: + chars.sum(Scan.walk(kids, self, ws, carried, lead, path, hot), Scan.walk(body, self, ws, carried, lead, + path, hot), + Scan.walk(rest, self, ws, carried, lead, path, hot), Laws.scan.count(kids, self, ws, carried, hot), + Laws.scan.count(body, self, ws, carried, hot), Laws.scan.count(rest, self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, hot), scan.walk(body, self, ws, carried, lead, path, + hot), + scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.SLet{}: + chars.sum(Scan.walk(kids, self, ws, carried, lead, path, hot), Scan.walk(body, self, ws, carried, lead, + path, hot), + Scan.walk(rest, self, ws, carried, lead, path, hot), Laws.scan.count(kids, self, ws, carried, hot), + Laws.scan.count(body, self, ws, carried, hot), Laws.scan.count(rest, self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, hot), scan.walk(body, self, ws, carried, lead, path, + hot), + scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.STerm{}: + chars.sum(Scan.walk(kids, self, ws, carried, lead, path, hot), Scan.walk(body, self, ws, carried, lead, + path, hot), + Scan.walk(rest, self, ws, carried, lead, path, hot), Laws.scan.count(kids, self, ws, carried, hot), + Laws.scan.count(body, self, ws, carried, hot), Laws.scan.count(rest, self, ws, carried, hot), + scan.walk(kids, self, ws, carried, lead, path, hot), scan.walk(body, self, ws, carried, lead, path, + hot), + scan.walk(rest, self, ws, carried, lead, path, hot)) + case Tree.NNil{}: + scan.walk(rest, self, ws, carried, lead, path, hot) + case Tree.NCons{nh, nt}: + scan.walk(rest, self, ws, carried, lead, path, hot) + +# a def that calls itself and is not a proof gathers its walk, entered hot, +# any other nothing +law scan.def: + for g: Bool + for +sig: Tree.Node + for +body: Tree.Node + for +name: String + for +ws: List<&2, Scan.Walk> + for +path: String + {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, Bool.not(g), [], _u => Scan.run(sig, body, name, ws, + path))) + == Bool.pick(Nat, g, Laws.scan.count(body, name, ws, Hoist.carried(sig, body, name), True{}), 0n) : Nat} + +def scan.def(g, sig, body, name, ws, path): + match g: + case True{}: + +carried = Hoist.carried(sig, body, name) + scan.walk(body, name, ws, carried, Scan.lead.go(Calls.params(sig), carried), path, True{}) + case False{}: + {==} + +# over the defs, the rule's join counts what it gathered and what the law +# counts +law scan.go: + for ds: List<&2, Calls.Def> + for +ws: List<&2, Scan.Walk> + for +path: String + for +acc: List<&2, List<&2, F.Finding>> + {List.length(&2, F.Finding, Scan.check.go(ds, ws, path, acc)) + == Nat.add(index.sum(acc), Laws.scan.total(ds, ws, path)) : Nat} + +def scan.go(ds, ws, path, acc): + match ds: + case Nil{}: + index.flat(acc, Nil{}) + case Con{Calls.Def{+name, +sig, +body}, +rest}: + +g = Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig))) + +x = Lazy.stop(List<&2, F.Finding>, Bool.not(g), [], _u => Scan.run(sig, body, name, ws, path)) + +n = Bool.pick(Nat, g, Laws.scan.count(body, name, ws, Hoist.carried(sig, body, name), True{}), 0n) + +tot = Laws.scan.total(rest, ws, path) + Equal.trans(Nat, + List.length(&2, F.Finding, Scan.check.go(rest, ws, path, x <> acc)), + Nat.add(Nat.add(index.sum(acc), List.length(&2, F.Finding, x)), tot), + Nat.add(index.sum(acc), Nat.add(n, tot)), + scan.go(rest, ws, path, x <> acc), + Equal.trans(Nat, + Nat.add(Nat.add(index.sum(acc), List.length(&2, F.Finding, x)), tot), + Nat.add(index.sum(acc), Nat.add(List.length(&2, F.Finding, x), tot)), + 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, + scan.def(g, sig, body, name, ws, path)))) + +def Laws.scan_counts(path, _text, _toks, tree, _bound, _items, e): + +ds = Calls.defs(tree) + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], _u => Scan.check.on(ds, path))) == Laws.scan.total(ds, Scan.walks(ds), path) : Nat} + scan.go(ds, Scan.walks(ds), path, Nil{}) + +# scan reads no string: a string is never a callee or a lone name, so each +# walk and each call reads the same over a tree read that way + +# a lone name read that way is the name it was +law inert.scan.name_tok: + for tok: Lex.Tok + {Scan.name_tok(Laws.inert.tok(tok)) == Scan.name_tok(tok) : Maybe<&2, String>} + +def inert.scan.name_tok(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{}: + {==} + +# an argument read that way is the lone name it was +law inert.scan.name_of: + for nn: Tree.Node + {Scan.name_of(Laws.inert.node(nn)) == Scan.name_of(nn) : Maybe<&2, String>} + +def inert.scan.name_of(nn): + match nn: + case Tree.NCons{h, r}: + match h: + case Tree.Leaf{tok}: + match r: + case Tree.NNil{}: + inert.scan.name_tok(tok) + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NCons{x, y}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{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{}: + {==} + +# the walked argument of arguments read that way is the lone name it was +law inert.scan.arg_name: + for +as: List<&2, Tree.Node> + for +at: Nat + {Scan.name_of(Calls.arg(inert.nodes(as), at)) == Scan.name_of(Calls.arg(as, at)) : Maybe<&2, String>} + +def inert.scan.arg_name(as, at): + %Equal.sym(Tree.Node, Calls.arg(inert.nodes(as), at), Laws.inert.node(Calls.arg(as, at)), inert.arg(as, at)) : + {Scan.name_of(_) == Scan.name_of(Calls.arg(as, at)) : Maybe<&2, String>} + inert.scan.name_of(Calls.arg(as, at)) + +# the first carried name among arguments read that way is the one it was +law inert.scan.found: + for ss: List<&2, Nat> + for +as: List<&2, Tree.Node> + for +carried: List<&2, String> + {Scan.found(ss, inert.nodes(as), carried) == Scan.found(ss, as, carried) : Maybe<&2, String>} + +def inert.scan.found(ss, as, carried): + match ss: + case Nil{}: + {==} + case Con{+at, +rest}: + %inert.scan.arg_name(as, at) : {Scan.first(Scan.keep_in(Scan.name_of(Calls.arg(inert.nodes(as), at)), carried), + Scan.found(rest, inert.nodes(as), carried)) == Scan.first(Scan.keep_in(_, carried), Scan.found(rest, as, + carried)) : Maybe<&2, String>} + %inert.scan.found(rest, as, carried) : {Scan.first(Scan.keep_in(Scan.name_of(Calls.arg(inert.nodes(as), at)), + carried), Scan.found(rest, inert.nodes(as), carried)) == Scan.first(Scan.keep_in(Scan.name_of(Calls.arg( + inert.nodes(as), at)), carried), _) : Maybe<&2, String>} + {==} + +# a named call whose arguments are read that way reports what it did +law inert.scan.on_name: + for +hot: Bool + for +open: Bool + for +tt: String + for +line: U32 + for +col: U32 + for +kids: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +carried: List<&2, String> + for +lead: String + for +path: String + {Scan.on_name(hot, open, tt, line, col, Laws.inert.node(kids), self, ws, carried, lead, path) + == Scan.on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path) : List<&2, F.Finding>} + +def inert.scan.on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path): + +g = Bool.not(Bool.and(hot, Bool.and(open, Bool.not(String.eq(tt, self))))) + +lhs = Scan.on_name(hot, open, tt, line, col, Laws.inert.node(kids), self, ws, carried, lead, path) + %inert.scan.found(Scan.slots(tt, ws), Calls.args(kids), carried) : {lhs == Lazy.stop(List<&2, F.Finding>, g, [], + _u => Scan.cite(_, tt, line, col, self, lead, path)) : List<&2, F.Finding>} + %inert.args(kids) : {lhs == Lazy.stop(List<&2, F.Finding>, g, [], + _u => Scan.cite(Scan.found(Scan.slots(tt, ws), _, carried), tt, line, col, self, lead, path)) + : List<&2, F.Finding>} + {==} + +# a call read that way reports what it did: only a name is a callee, and a +# name is never cut +law inert.scan.call_hit: + for kk: Lex.TokKind + for +hot: Bool + for +open: Bool + for +tt: String + for +line: U32 + for +col: U32 + for +kids: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +carried: List<&2, String> + for +lead: String + for +path: String + {Scan.call_hit(kk, hot, open, Laws.inert.keep(Laws.inert.blanks(kk), tt), line, col, Laws.inert.node(kids), self, + ws, carried, lead, path) + == Scan.call_hit(kk, hot, open, tt, line, col, kids, self, ws, carried, lead, path) : List<&2, F.Finding>} + +def inert.scan.call_hit(kk, hot, open, tt, line, col, kids, self, ws, carried, lead, path): + match kk: + case Lex.TName{}: + inert.scan.on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path) + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + inert.scan.on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path) + 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{}: + {==} + +# a name then a group read that way: its call, the group and the rest walked +# as they were +law inert.scan.walk_lg: + for +k: Lex.TokKind + for +t: String + for +o: String + for +l: U32 + for +c: U32 + for +kids: Tree.Node + for +r2: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +carried: List<&2, String> + for +lead: String + for +path: String + for +hot: Bool + for ik: {Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, Hoist.warm(hot, k)) == Scan.walk(kids, self, + ws, carried, lead, path, Hoist.warm(hot, k)) : List<&2, F.Finding>} + for ir: {Scan.walk(Laws.inert.node(r2), self, ws, carried, lead, path, Hoist.warm(hot, k)) == Scan.walk(r2, self, ws, + carried, lead, path, Hoist.warm(hot, k)) : List<&2, F.Finding>} + {List.concat(&2, F.Finding, [Scan.call_hit(k, Hoist.warm(hot, k), String.eq(o, "("), + Laws.inert.keep(Laws.inert.blanks(k), t), + l, c, Laws.inert.node(kids), self, ws, carried, lead, path), Scan.walk(Laws.inert.node(kids), self, ws, carried, + lead, path, Hoist.warm(hot, k)), Scan.walk(Laws.inert.node(r2), self, ws, carried, lead, path, Hoist.warm(hot, + k))]) + == List.concat(&2, F.Finding, [Scan.call_hit(k, Hoist.warm(hot, k), String.eq(o, "("), t, l, c, kids, self, ws, + carried, lead, + path), Scan.walk(kids, self, ws, carried, lead, path, Hoist.warm(hot, + k)), Scan.walk(r2, self, ws, carried, lead, path, Hoist.warm(hot, k))]) : List<&2, F.Finding>} + +def inert.scan.walk_lg(k, t, o, l, c, kids, r2, self, ws, carried, lead, path, hot, ik, ir): + +w = Hoist.warm(hot, k) + inert.cat3(Scan.call_hit(k, w, String.eq(o, "("), Laws.inert.keep(Laws.inert.blanks(k), t), l, c, + Laws.inert.node(kids), self, + ws, carried, lead, path), Scan.call_hit(k, w, String.eq(o, "("), t, l, c, kids, self, ws, carried, lead, path), + Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, w), Scan.walk(kids, self, ws, carried, lead, path, + w), + Scan.walk(Laws.inert.node(r2), self, ws, carried, lead, path, w), Scan.walk(r2, self, ws, carried, lead, path, w), + inert.scan.call_hit(k, w, String.eq(o, "("), t, l, c, kids, self, ws, carried, lead, path), ik, ir) + +# a case arm read that way: hot as it was, and its pattern, body and the rest +# walked as they were +law inert.scan.walk_case: + for +kids: Tree.Node + for +body: Tree.Node + for +rest: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +carried: List<&2, String> + for +lead: String + for +path: String + for +hot: Bool + for +es: {Laws.inert.marked(self) == False{} : Bool} + for +eb: {Laws.inert.ok(body) == True{} : Bool} + for ik: {Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, False{}) == Scan.walk(kids, self, ws, + carried, lead, path, False{}) : List<&2, F.Finding>} + for ib: {Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, Bool.and(hot, + Calls.calls(Laws.inert.node(body), + self))) == Scan.walk(body, self, ws, carried, lead, path, Bool.and(hot, Calls.calls(Laws.inert.node(body), + self))) : List<&2, F.Finding>} + for ir: {Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot) == Scan.walk(rest, self, ws, carried, + lead, path, hot) : List<&2, F.Finding>} + {List.concat(&2, F.Finding, [Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, False{}), + Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, Bool.and(hot, Calls.calls(Laws.inert.node(body), + self))), Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot)]) + == List.concat(&2, F.Finding, [Scan.walk(kids, self, ws, carried, lead, path, False{}), Scan.walk(body, self, ws, + carried, lead, path, Bool.and(hot, Calls.calls(body, + self))), Scan.walk(rest, self, ws, carried, lead, path, hot)]) + : List<&2, F.Finding>} + +def inert.scan.walk_case(kids, body, rest, self, ws, carried, lead, path, hot, es, eb, ik, ib, ir): + +arm = Bool.and(hot, Calls.calls(Laws.inert.node(body), self)) + +lhs = List.concat(&2, F.Finding, [Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, False{}), + Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, arm), Scan.walk(Laws.inert.node(rest), self, ws, + carried, lead, path, hot)]) + %inert.calls(body, self, es, eb) : {lhs == List.concat(&2, F.Finding, [Scan.walk(kids, self, ws, carried, lead, path, + False{}), + Scan.walk(body, self, ws, carried, lead, path, Bool.and(hot, _)), Scan.walk(rest, self, ws, carried, lead, path, + hot)]) : List<&2, F.Finding>} + inert.cat3(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, False{}), Scan.walk(kids, self, ws, + carried, lead, path, False{}), Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, arm), + Scan.walk(body, self, ws, carried, lead, path, arm), + Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, carried, lead, + path, hot), ik, ib, ir) + +# scan's walk reads no string: a string is never a callee or a lone name +law inert.scan.walk: + for nn: Tree.Node + for +self: String + for +ws: List<&2, Scan.Walk> + for +carried: List<&2, String> + for +lead: String + for +path: String + for +hot: Bool + for +es: {Laws.inert.marked(self) == False{} : Bool} + for +e: {Laws.inert.ok(nn) == True{} : Bool} + {Scan.walk(Laws.inert.node(nn), self, ws, carried, lead, path, hot) == Scan.walk(nn, self, ws, carried, lead, path, + hot) : List<&2, F.Finding>} + +def inert.scan.walk(nn, self, ws, carried, lead, path, hot, es, e): + match nn: + case Tree.NCons{h, +rest}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{+k, +t, +l, +c}: + match rest: + case Tree.NCons{h2, +r2}: + match h2: + case Tree.Group{go, +kids, +gcl}: + match go: + case Lex.Tok{+gk, +o, +gl, +gc}: + +lf = {Tree.Leaf{Lex.Tok{k, t, l, c}} : Tree.Node} + +gp = {Tree.Group{Lex.Tok{gk, o, gl, gc}, kids, gcl} : Tree.Node} + +eg = inert.ok_t(lf, Tree.NCons{gp, r2}, e) + inert.scan.walk_lg(k, t, o, l, c, kids, r2, self, ws, carried, lead, path, hot, + inert.scan.walk(kids, self, ws, carried, lead, path, Hoist.warm(hot, k), es, inert.ok_h(gp, + r2, eg)), + inert.scan.walk(r2, self, ws, carried, lead, path, Hoist.warm(hot, k), es, inert.ok_t(gp, + r2, eg))) + case Tree.Leaf{x}: + inert.scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k), es, + inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + case Tree.Stmt{x, y, z}: + inert.scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k), es, + inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + case Tree.NNil{}: + inert.scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k), es, + inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + case Tree.NCons{x, y}: + inert.scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k), es, + inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + case Tree.Leaf{x}: + inert.scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k), es, + inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + case Tree.Group{x, y, z}: + inert.scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k), es, + inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + case Tree.Stmt{x, y, z}: + inert.scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k), es, + inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + case Tree.NNil{}: + inert.scan.walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k), es, + inert.ok_t(Tree.Leaf{Lex.Tok{k, t, l, c}}, rest, e)) + case Tree.Group{+o, +kids, +cl}: + inert.cat2(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, hot), Scan.walk(kids, self, ws, + carried, lead, path, hot), Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), + Scan.walk(rest, self, ws, carried, lead, path, hot), + inert.scan.walk(kids, self, ws, carried, lead, path, hot, es, inert.ok_h(Tree.Group{o, kids, cl}, rest, e)), + inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, inert.ok_t(Tree.Group{o, kids, cl}, rest, e))) + case Tree.Stmt{sk, +kids, +body}: + match sk: + case Tree.SDef{}: + +es2 = inert.and_l(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + +ek = inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +eb = inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +er = inert.and_r(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + inert.cat3(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, hot), Scan.walk(kids, self, + ws, carried, lead, path, hot), Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, hot), + Scan.walk(body, self, ws, carried, lead, path, hot), + Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, + carried, lead, path, hot), + inert.scan.walk(kids, self, ws, carried, lead, path, hot, es, ek), inert.scan.walk(body, self, ws, + carried, lead, path, hot, es, eb), inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, + er)) + case Tree.SType{}: + +es2 = inert.and_l(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + +ek = inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +eb = inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +er = inert.and_r(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + inert.cat3(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, hot), Scan.walk(kids, self, + ws, carried, lead, path, hot), Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, hot), + Scan.walk(body, self, ws, carried, lead, path, hot), + Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, + carried, lead, path, hot), + inert.scan.walk(kids, self, ws, carried, lead, path, hot, es, ek), inert.scan.walk(body, self, ws, + carried, lead, path, hot, es, eb), inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, + er)) + case Tree.SLaw{}: + +es2 = inert.and_l(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + +ek = inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +eb = inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +er = inert.and_r(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + inert.cat3(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, hot), Scan.walk(kids, self, + ws, carried, lead, path, hot), Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, hot), + Scan.walk(body, self, ws, carried, lead, path, hot), + Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, + carried, lead, path, hot), + inert.scan.walk(kids, self, ws, carried, lead, path, hot, es, ek), inert.scan.walk(body, self, ws, + carried, lead, path, hot, es, eb), inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, + er)) + case Tree.SImport{}: + +es2 = inert.and_l(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + +ek = inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +eb = inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +er = inert.and_r(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + inert.cat3(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, hot), Scan.walk(kids, self, + ws, carried, lead, path, hot), Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, hot), + Scan.walk(body, self, ws, carried, lead, path, hot), + Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, + carried, lead, path, hot), + inert.scan.walk(kids, self, ws, carried, lead, path, hot, es, ek), inert.scan.walk(body, self, ws, + carried, lead, path, hot, es, eb), inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, + er)) + case Tree.SCase{}: + +es2 = inert.and_l(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + +ek = inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +eb = inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +er = inert.and_r(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + inert.scan.walk_case(kids, body, rest, self, ws, carried, lead, path, hot, es, eb, + inert.scan.walk(kids, self, ws, carried, lead, path, False{}, es, ek), + inert.scan.walk(body, self, ws, carried, lead, path, Bool.and(hot, Calls.calls(Laws.inert.node(body), + self)), es, eb), + inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, er)) + case Tree.SFor{}: + +es2 = inert.and_l(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + +ek = inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +eb = inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +er = inert.and_r(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + inert.cat3(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, hot), Scan.walk(kids, self, + ws, carried, lead, path, hot), Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, hot), + Scan.walk(body, self, ws, carried, lead, path, hot), + Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, + carried, lead, path, hot), + inert.scan.walk(kids, self, ws, carried, lead, path, hot, es, ek), inert.scan.walk(body, self, ws, + carried, lead, path, hot, es, eb), inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, + er)) + case Tree.SLet{}: + +es2 = inert.and_l(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + +ek = inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +eb = inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +er = inert.and_r(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + inert.cat3(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, hot), Scan.walk(kids, self, + ws, carried, lead, path, hot), Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, hot), + Scan.walk(body, self, ws, carried, lead, path, hot), + Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, + carried, lead, path, hot), + inert.scan.walk(kids, self, ws, carried, lead, path, hot, es, ek), inert.scan.walk(body, self, ws, + carried, lead, path, hot, es, eb), inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, + er)) + case Tree.STerm{}: + +es2 = inert.and_l(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + +ek = inert.and_l(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +eb = inert.and_r(Laws.inert.ok(kids), Laws.inert.ok(body), es2) + +er = inert.and_r(Bool.and(Laws.inert.ok(kids), Laws.inert.ok(body)), Laws.inert.ok(rest), e) + inert.cat3(Scan.walk(Laws.inert.node(kids), self, ws, carried, lead, path, hot), Scan.walk(kids, self, + ws, carried, lead, path, hot), Scan.walk(Laws.inert.node(body), self, ws, carried, lead, path, hot), + Scan.walk(body, self, ws, carried, lead, path, hot), + Scan.walk(Laws.inert.node(rest), self, ws, carried, lead, path, hot), Scan.walk(rest, self, ws, + carried, lead, path, hot), + inert.scan.walk(kids, self, ws, carried, lead, path, hot, es, ek), inert.scan.walk(body, self, ws, + carried, lead, path, hot, es, eb), inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, + er)) + case Tree.NNil{}: + inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, e) + case Tree.NCons{x, y}: + inert.scan.walk(rest, self, ws, carried, lead, path, hot, es, inert.ok_t(Tree.NCons{x, y}, rest, e)) + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NNil{}: + {==} + +# three lists of numbers that read alike join alike +law scan.ncat3: + for -a1: List<&2, Nat> + for -a2: List<&2, Nat> + for -b1: List<&2, Nat> + for -b2: List<&2, Nat> + for -c1: List<&2, Nat> + for -c2: List<&2, Nat> + for ea: {a1 == a2 : List<&2, Nat>} + for eb: {b1 == b2 : List<&2, Nat>} + for ec: {c1 == c2 : List<&2, Nat>} + {List.concat(&2, Nat, [a1, b1, c1]) == List.concat(&2, Nat, [a2, b2, c2]) : List<&2, Nat>} + +def scan.ncat3(a1, _a2, b1, b2, c1, c2, ea, eb, ec): + %ea : {List.concat(&2, Nat, [a1, b1, c1]) == List.concat(&2, Nat, [_, b2, c2]) : List<&2, Nat>} + %eb : {List.concat(&2, Nat, [a1, b1, c1]) == List.concat(&2, Nat, [a1, _, c2]) : List<&2, Nat>} + %ec : {List.concat(&2, Nat, [a1, b1, c1]) == List.concat(&2, Nat, [a1, b1, _]) : List<&2, Nat>} + {==} + +# two lists of numbers that read alike join alike +law scan.ncat2: + for -a1: List<&2, Nat> + for -a2: List<&2, Nat> + for -b1: List<&2, Nat> + for -b2: List<&2, Nat> + for ea: {a1 == a2 : List<&2, Nat>} + for eb: {b1 == b2 : List<&2, Nat>} + {List.concat(&2, Nat, [a1, b1]) == List.concat(&2, Nat, [a2, b2]) : List<&2, Nat>} + +def scan.ncat2(a1, _a2, b1, b2, ea, eb): + %ea : {List.concat(&2, Nat, [a1, b1]) == List.concat(&2, Nat, [_, b2]) : List<&2, Nat>} + %eb : {List.concat(&2, Nat, [a1, b1]) == List.concat(&2, Nat, [a1, _]) : List<&2, Nat>} + {==} + +# the parameters at walked arguments read that way are the ones they were +law inert.scan.params_at: + for ss: List<&2, Nat> + for +as: List<&2, Tree.Node> + for +ps: List<&2, String> + {Scan.params_at(ss, inert.nodes(as), ps) == Scan.params_at(ss, as, ps) : List<&2, Nat>} + +def inert.scan.params_at(ss, as, ps): + match ss: + case Nil{}: + {==} + case Con{+at, +rest}: + %inert.scan.arg_name(as, at) : {List.append(&2, Nat, + Scan.opt(Scan.index_in(Scan.name_of(Calls.arg(inert.nodes(as), + at)), ps)), Scan.params_at(rest, inert.nodes(as), ps)) == List.append(&2, Nat, Scan.opt(Scan.index_in(_, ps)), + Scan.params_at(rest, as, ps)) : List<&2, Nat>} + %inert.scan.params_at(rest, as, ps) : {List.append(&2, Nat, Scan.opt(Scan.index_in(Scan.name_of(Calls.arg( + inert.nodes(as), at)), ps)), Scan.params_at(rest, inert.nodes(as), ps)) == List.append(&2, Nat, + Scan.opt(Scan.index_in(Scan.name_of(Calls.arg(inert.nodes(as), at)), ps)), _) : List<&2, Nat>} + {==} + +# a named call's walked parameters, its arguments read that way +law inert.scan.pass_name: + for +open: Bool + for +tt: String + for +kids: Tree.Node + for +ps: List<&2, String> + for +ws: List<&2, Scan.Walk> + {Lazy.stop(List<&2, Nat>, Bool.not(open), [], _u => Scan.params_at(Scan.slots(tt, ws), + Calls.args(Laws.inert.node(kids)), ps)) + == Lazy.stop(List<&2, Nat>, Bool.not(open), [], _u => Scan.params_at(Scan.slots(tt, ws), Calls.args(kids), + ps)) : List<&2, Nat>} + +def inert.scan.pass_name(open, tt, kids, ps, ws): + +lhs = Lazy.stop(List<&2, Nat>, Bool.not(open), [], _u => Scan.params_at(Scan.slots(tt, ws), + Calls.args(Laws.inert.node(kids)), ps)) + %inert.scan.params_at(Scan.slots(tt, ws), Calls.args(kids), ps) : {lhs == Lazy.stop(List<&2, Nat>, Bool.not(open), [], + _u => _) : List<&2, Nat>} + %inert.args(kids) : {lhs == Lazy.stop(List<&2, Nat>, Bool.not(open), [], _u => Scan.params_at(Scan.slots(tt, ws), _, + ps)) + : List<&2, Nat>} + {==} + +# a call read that way passes what it passed: only a name is a callee +law inert.scan.pass_hit: + for kk: Lex.TokKind + for +open: Bool + for +tt: String + for +kids: Tree.Node + for +ps: List<&2, String> + for +ws: List<&2, Scan.Walk> + {Scan.pass_hit(kk, open, Laws.inert.keep(Laws.inert.blanks(kk), tt), Laws.inert.node(kids), ps, ws) + == Scan.pass_hit(kk, open, tt, kids, ps, ws) : List<&2, Nat>} + +def inert.scan.pass_hit(kk, open, tt, kids, ps, ws): + match kk: + case Lex.TName{}: + inert.scan.pass_name(open, tt, kids, ps, ws) + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + inert.scan.pass_name(open, tt, kids, ps, ws) + 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{}: + {==} + +# what a body read that way passes is what it passed +law inert.scan.passes: + for nn: Tree.Node + for +ps: List<&2, String> + for +ws: List<&2, Scan.Walk> + {Scan.passes(Laws.inert.node(nn), ps, ws) == Scan.passes(nn, ps, ws) : List<&2, Nat>} + +def inert.scan.passes(nn, ps, ws): + match nn: + case Tree.NCons{h, +rest}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{+k, +t, +l, +c}: + match rest: + case Tree.NCons{h2, +r2}: + match h2: + case Tree.Group{go, +kids, +gcl}: + match go: + case Lex.Tok{+gk, +o, +gl, +gc}: + scan.ncat3(Scan.pass_hit(k, String.eq(o, "("), Laws.inert.keep(Laws.inert.blanks(k), t), + Laws.inert.node(kids), ps, ws), Scan.pass_hit(k, String.eq(o, "("), t, kids, ps, ws), + Scan.passes(Laws.inert.node(kids), ps, ws), Scan.passes(kids, ps, ws), + Scan.passes(Laws.inert.node(r2), ps, ws), Scan.passes(r2, ps, ws), + inert.scan.pass_hit(k, String.eq(o, "("), t, kids, ps, ws), + inert.scan.passes(kids, ps, ws), inert.scan.passes(r2, ps, ws)) + case Tree.Leaf{x}: + inert.scan.passes(rest, ps, ws) + case Tree.Stmt{x, y, z}: + inert.scan.passes(rest, ps, ws) + case Tree.NNil{}: + inert.scan.passes(rest, ps, ws) + case Tree.NCons{x, y}: + inert.scan.passes(rest, ps, ws) + case Tree.Leaf{x}: + inert.scan.passes(rest, ps, ws) + case Tree.Group{x, y, z}: + inert.scan.passes(rest, ps, ws) + case Tree.Stmt{x, y, z}: + inert.scan.passes(rest, ps, ws) + case Tree.NNil{}: + inert.scan.passes(rest, ps, ws) + case Tree.Group{o, +kids, cl}: + scan.ncat2(Scan.passes(Laws.inert.node(kids), ps, ws), Scan.passes(kids, ps, ws), + Scan.passes(Laws.inert.node(rest), ps, ws), + Scan.passes(rest, ps, ws), inert.scan.passes(kids, ps, ws), inert.scan.passes(rest, ps, ws)) + case Tree.Stmt{sk, +kids, +body}: + scan.ncat3(Scan.passes(Laws.inert.node(kids), ps, ws), Scan.passes(kids, ps, ws), + Scan.passes(Laws.inert.node(body), ps, ws), + Scan.passes(body, ps, ws), Scan.passes(Laws.inert.node(rest), ps, ws), Scan.passes(rest, ps, ws), + inert.scan.passes(kids, ps, ws), inert.scan.passes(body, ps, ws), inert.scan.passes(rest, ps, ws)) + case Tree.NNil{}: + inert.scan.passes(rest, ps, ws) + case Tree.NCons{x, y}: + inert.scan.passes(rest, ps, ws) + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NNil{}: + {==} + +# a parameter read that way moves as it did +law inert.scan.moves: + for +pp: Tree.Node + for +carried: List<&2, String> + {Scan.moves(Laws.inert.node(pp), carried) == Scan.moves(pp, carried) : Bool} + +def inert.scan.moves(pp, carried): + +lhs = Scan.moves(Laws.inert.node(pp), carried) + %inert.is_live(pp) : {lhs == Bool.and(_, Bool.not(List.contains(~String, ~String.eq, carried, Calls.param_name(pp)))) + : Bool} + %inert.param_name(pp) : {lhs == Bool.and(Calls.is_live(Laws.inert.node(pp)), Bool.not(List.contains(~String, + ~String.eq, + carried, _))) : Bool} + {==} + +# a parameter read that way is a count or a text as it was +law inert.scan.place: + for +pp: Tree.Node + for +ii: Nat + {Scan.place(Laws.inert.node(pp), ii) == Scan.place(pp, ii) : Maybe<&2, Nat>} + +def inert.scan.place(pp, ii): + %inert.type_head(pp, False{}) : {Scan.place(Laws.inert.node(pp), ii) == Bool.pick(Maybe<&2, Nat>, + Bool.or(String.eq(_, "Nat"), String.eq(_, "String")), None{}, Some{ii}) : Maybe<&2, Nat>} + {==} + +# the parameter shrunk, among parameters read that way, sits where it sat +law inert.scan.own.go: + for ps: List<&2, Tree.Node> + for +carried: List<&2, String> + for +ii: Nat + {Scan.own.go(inert.nodes(ps), carried, ii) == Scan.own.go(ps, carried, ii) : Maybe<&2, Nat>} + +def inert.scan.own.go(ps, carried, ii): + match ps: + case Nil{}: + {==} + case Con{+p, +rest}: + +lhs = Scan.own.go(inert.nodes(p <> rest), carried, ii) + %inert.scan.moves(p, carried) : {lhs == Lazy.stop(Maybe<&2, Nat>, _, Scan.place(p, ii), + _u => Scan.own.go(rest, carried, 1n+ii)) : Maybe<&2, Nat>} + %inert.scan.place(p, ii) : {lhs == Lazy.stop(Maybe<&2, Nat>, Scan.moves(Laws.inert.node(p), carried), _, + _u => Scan.own.go(rest, carried, 1n+ii)) : Maybe<&2, Nat>} + %inert.scan.own.go(rest, carried, 1n+ii) : {lhs == Lazy.stop(Maybe<&2, Nat>, Scan.moves(Laws.inert.node(p), + carried), Scan.place(Laws.inert.node(p), ii), _u => _) : Maybe<&2, Nat>} + {==} + +# the name of the parameter shrunk, among parameters read that way, is the one it was +law inert.scan.lead.go: + for ps: List<&2, Tree.Node> + for +carried: List<&2, String> + {Scan.lead.go(inert.nodes(ps), carried) == Scan.lead.go(ps, carried) : String} + +def inert.scan.lead.go(ps, carried): + match ps: + case Nil{}: + {==} + case Con{+p, +rest}: + +lhs = Scan.lead.go(inert.nodes(p <> rest), carried) + %inert.scan.moves(p, carried) : {lhs == Lazy.stop(String, _, Calls.param_name(p), _u => Scan.lead.go(rest, + carried)) : String} + %inert.param_name(p) : {lhs == Lazy.stop(String, Scan.moves(Laws.inert.node(p), carried), _, + _u => Scan.lead.go(rest, + carried)) : String} + %inert.scan.lead.go(rest, carried) : {lhs == Lazy.stop(String, Scan.moves(Laws.inert.node(p), carried), + Calls.param_name(Laws.inert.node(p)), _u => _) : String} + {==} + +# a signature read that way has its parameters read that way +law inert.scan.params: + for +sig: Tree.Node + {Calls.params(Laws.inert.node(sig)) == inert.nodes(Calls.params(sig)) : List<&2, Tree.Node>} + +def inert.scan.params(sig): + %Equal.sym(Tree.Node, Calls.params.of(Laws.inert.node(sig)), Laws.inert.node(Calls.params.of(sig)), + inert.params.of(sig)) : {Calls.args(_) == inert.nodes(Calls.params(sig)) : List<&2, Tree.Node>} + inert.args(Calls.params.of(sig)) + +# the parameter a def read that way shrinks is the one it shrank +law inert.scan.own: + for +sig: Tree.Node + for +body: Tree.Node + for +name: String + for +en: {Laws.inert.marked(name) == False{} : Bool} + for +eb: {Laws.inert.ok(body) == True{} : Bool} + {Scan.own(Laws.inert.node(sig), Laws.inert.node(body), name) == Scan.own(sig, body, name) : Maybe<&2, Nat>} + +def inert.scan.own(sig, body, name, en, eb): + +isg = Laws.inert.node(sig) + +ib = Laws.inert.node(body) + +lhs = Scan.own(isg, ib, name) + %inert.calls(body, name, en, eb) : {lhs == Lazy.stop(Maybe<&2, Nat>, Bool.not(_), None{}, + _u => Scan.own.go(Calls.params(sig), Hoist.carried(sig, body, name), 0n)) : Maybe<&2, Nat>} + %inert.hoist.carried(sig, body, name, en, eb) : {lhs == Lazy.stop(Maybe<&2, Nat>, Bool.not(Calls.calls(ib, name)), + None{}, _u => Scan.own.go(Calls.params(sig), _, 0n)) : Maybe<&2, Nat>} + %inert.scan.own.go(Calls.params(sig), Hoist.carried(isg, ib, name), 0n) : {lhs == Lazy.stop(Maybe<&2, Nat>, + Bool.not(Calls.calls(ib, name)), None{}, _u => _) : Maybe<&2, Nat>} + %inert.scan.params(sig) : {lhs == Lazy.stop(Maybe<&2, Nat>, Bool.not(Calls.calls(ib, name)), None{}, + _u => Scan.own.go(_, Hoist.carried(isg, ib, name), 0n)) : Maybe<&2, Nat>} + {==} + +# a def read that way records the walks it recorded +law inert.scan.walks.go: + for ds: List<&2, Calls.Def> + for +ws: List<&2, Scan.Walk> + for +e: {inert.dok(ds) == True{} : Bool} + {Scan.walks.go(inert.defs(ds), ws) == Scan.walks.go(ds, ws) : List<&2, Scan.Walk>} + +def inert.scan.walks.go(ds, ws, e): + match ds: + case Nil{}: + {==} + case Con{Calls.Def{+name, +sig, +body}, +rest}: + +en = inert.dok.head(name, sig, body, rest, e) + +eb = inert.dok.body(name, sig, body, rest, e) + +isg = Laws.inert.node(sig) + +ib = Laws.inert.node(body) + +lhs = Scan.walks.go(inert.defs(Calls.Def{name, sig, body} <> rest), ws) + %inert.scan.own(sig, body, name, en, eb) : {lhs == Scan.walks.go(rest, Scan.tag(List.append(&2, Nat, + Scan.opt(_), Scan.passes(body, Calls.names(sig), ws)), name, ws)) : List<&2, Scan.Walk>} + %inert.scan.passes(body, Calls.names(sig), ws) : {lhs == Scan.walks.go(rest, Scan.tag(List.append(&2, Nat, + Scan.opt(Scan.own(isg, ib, name)), _), name, ws)) : List<&2, Scan.Walk>} + %inert.names(sig) : {lhs == Scan.walks.go(rest, Scan.tag(List.append(&2, Nat, + Scan.opt(Scan.own(isg, ib, name)), Scan.passes(ib, _, ws)), name, ws)) : List<&2, Scan.Walk>} + inert.scan.walks.go(rest, Scan.tag(List.append(&2, Nat, Scan.opt(Scan.own(isg, ib, name)), + Scan.passes(ib, Calls.names(isg), ws)), name, ws), inert.dok.rest(name, sig, body, rest, e)) + +# a def read that way is walked as it was +law inert.scan.run: + for +sig: Tree.Node + for +body: Tree.Node + for +name: String + for +ws: List<&2, Scan.Walk> + for +path: String + for +en: {Laws.inert.marked(name) == False{} : Bool} + for +eb: {Laws.inert.ok(body) == True{} : Bool} + {Scan.run(Laws.inert.node(sig), Laws.inert.node(body), name, ws, path) == Scan.run(sig, body, name, ws, + path) : List<&2, F.Finding>} + +def inert.scan.run(sig, body, name, ws, path, en, eb): + +isg = Laws.inert.node(sig) + +ib = Laws.inert.node(body) + +cr = Hoist.carried(isg, ib, name) + +lhs = Scan.run(isg, ib, name, ws, path) + %inert.hoist.carried(sig, body, name, en, eb) : {lhs == Scan.walk(body, name, ws, _, Scan.lead.go(Calls.params(sig), + _), path, True{}) : List<&2, F.Finding>} + %inert.scan.lead.go(Calls.params(sig), cr) : {lhs == Scan.walk(body, name, ws, cr, _, path, True{}) + : List<&2, F.Finding>} + %inert.scan.params(sig) : {lhs == Scan.walk(body, name, ws, cr, Scan.lead.go(_, cr), path, True{}) + : List<&2, F.Finding>} + inert.scan.walk(body, name, ws, cr, Scan.lead.go(Calls.params(isg), cr), path, True{}, en, eb) + +# scan over the defs read that way reports what it reports over the defs +law inert.scan.go: + for ds: List<&2, Calls.Def> + for +ws: List<&2, Scan.Walk> + for +path: String + for +acc: List<&2, List<&2, F.Finding>> + for +e: {inert.dok(ds) == True{} : Bool} + {Scan.check.go(inert.defs(ds), ws, path, acc) == Scan.check.go(ds, ws, path, acc) : List<&2, F.Finding>} + +def inert.scan.go(ds, ws, path, acc, e): + match ds: + case Nil{}: + {==} + case Con{Calls.Def{+name, +sig, +body}, +rest}: + +en = inert.dok.head(name, sig, body, rest, e) + +eb = inert.dok.body(name, sig, body, rest, e) + +ib = Laws.inert.node(body) + +isg = Laws.inert.node(sig) + +lst = Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(Calls.calls(ib, name), Bool.not(Calls.exempt(path, + isg)))), [], _u => Scan.run(isg, ib, name, ws, path)) + %inert.stop(Bool.not(Bool.and(Calls.calls(ib, name), Bool.not(Calls.exempt(path, isg)))), + Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), + Scan.run(isg, ib, name, ws, path), Scan.run(sig, body, name, ws, path), + inert.gate(path, name, sig, body, en, eb), inert.scan.run(sig, body, name, ws, path, en, eb)) : + {Scan.check.go(inert.defs(rest), ws, path, lst <> acc) == Scan.check.go(rest, ws, path, _ <> acc) + : List<&2, F.Finding>} + inert.scan.go(rest, ws, path, lst <> acc, inert.dok.rest(name, sig, body, rest, e)) + +# scan over the defs read that way, their walks read that way too +law inert.scan.on: + for +ds: List<&2, Calls.Def> + for +path: String + for +e: {inert.dok(ds) == True{} : Bool} + {Scan.check.on(inert.defs(ds), path) == Scan.check.on(ds, path) : List<&2, F.Finding>} + +def inert.scan.on(ds, path, e): + %inert.scan.walks.go(ds, [], e) : {Scan.check.go(inert.defs(ds), Scan.walks(inert.defs(ds)), path, []) + == Scan.check.go(ds, _, path, []) : List<&2, F.Finding>} + inert.scan.go(ds, Scan.walks(inert.defs(ds)), path, [], e) + +# the rule's law-file gate over the defs read that way +law inert.scan.gated: + for +ds: List<&2, Calls.Def> + for +path: String + for +e: {inert.dok(ds) == True{} : Bool} + {Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => Scan.check.on(inert.defs(ds), path)) + == Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _v => Scan.check.on(ds, path)) + : List<&2, F.Finding>} + +def inert.scan.gated(ds, path, e): + inert.stop(Paths.is_law_file(path), Paths.is_law_file(path), Scan.check.on(inert.defs(ds), path), + Scan.check.on(ds, path), {==}, inert.scan.on(ds, path, e)) + +def Laws.inert_scan(path, _text, tree, _toks, _bound, _items, _text2, tree2, _toks2, _bound2, _items2, ok, ok2, e): + inert.via(Tree.Node, z => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], + _u => Scan.check.on(Calls.defs(z), path)), tree, tree2, Laws.inert.node(tree), Laws.inert.node(tree2), + inert.lift(z => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => Scan.check.on(z, path)), tree, + inert.scan.gated(Calls.defs(tree), path, inert.dok.of(tree, ok))), + inert.lift(z => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => Scan.check.on(z, path)), tree2, + inert.scan.gated(Calls.defs(tree2), path, inert.dok.of(tree2, ok2))), + e) diff --git a/src/rules/correctness/setting.bend b/src/rules/correctness/setting.bend new file mode 100644 index 0000000..bc2be53 --- /dev/null +++ b/src/rules/correctness/setting.bend @@ -0,0 +1,33 @@ +# rule setting: a setting in a bolt.bend (a `def` whose body holds a string) +# whose name is neither a rule's slug nor a group, as the code table +# (src/codes.bend) lists them. Grading only looks names up, so such a setting +# sets nothing and fails open: `def wrp() -> String: "off"` leaves `wrap` at +# its group's level, and a retired name (`def quantify()`, `def shadow()`) +# does nothing at all. Rename it to the rule or group it meant, or delete it. +# +# A bolt.bend is read, never linted (BOLT-SCOPE-5), so this is not a per-file +# rule: the planner (src/lint/plan.bend) runs it once over each bolt.bend +# that grades a directory of the run, the first of that directory's +# candidates it read (BOLT-CFG-4), and reports each unknown setting at that +# bolt.bend's path and the line of its `def`, in file order, after the +# per-file findings and before the project rules'. It is graded by the +# bolt.bend it reports on, like any rule (`def setting() -> String: "off"` +# turns it off there). A noqa comment in a bolt.bend silences nothing, since +# the file is never read for marks. The editor does not run it (BOLT-LSP-4). +import Base +import ../../finding.bend as F +import ../../config.bend as Config + +# each setting as a finding at the bolt.bend's path and its def's line +def found(ss: List<&2, Config.Setting>, +path: String) -> List<&2, F.Finding>: + match ss: + case Nil{}: + Nil{} + case Con{Config.Setting{n, _w, line}, rest}: + F.Finding{path, line, 0, 0, "setting", "`" ++ n ++ "` names no rule or group, so it sets nothing."} + <> found(rest, path) + +# the findings on a bolt.bend's text: one for each setting whose name is no +# rule or group, in file order +def check(+path: String, text: String) -> List<&2, F.Finding>: + found(Config.unknown(Config.settings(text)), path) diff --git a/src/rules/digest.bend b/src/rules/digest.bend index 2c6601f..8085264 100644 --- a/src/rules/digest.bend +++ b/src/rules/digest.bend @@ -132,7 +132,8 @@ 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) - Lazy.stop(List<&2, Mention>, Bool.not(within(ss, l)), more, _u => target(tt, as, file, more)) + +out = Bool.not(within(ss, l)) # noqa: U013 law spans + Lazy.stop(List<&2, Mention>, out, more, _u => target(tt, as, file, more)) # the uses the binder recorded def uses.of(bb: Bind.Bound) -> List<&2, Bind.Use>: @@ -201,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)) + target(tt, as, file, called(rest, as, file)) # noqa: U013 as holds the file's import aliases # 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 @@ -220,10 +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) - Top{Outline.IDef{}, name, line, [], called(upto(us, nx), as, file)} <> ranged(rest, past(us, nx), as, file) + cs = called(upto(us, nx), as, file) # noqa: U013 import aliases + 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)} + Top{Outline.IType{}, name, line, ctors(rest), called(upto(us, nx), as, file)} # noqa: U013 import aliases <> 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) @@ -310,8 +312,8 @@ 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) - Law{Closed.name.of(Bind.declared(kids)), at, Closed.binds(body), String.lines(doc_at(items, at))} - <> laws_of(rest, items) + dd = doc_at(items, at) # noqa: U013 stops at the law's line + 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) case other: diff --git a/src/rules/imports.bend b/src/rules/imports.bend index cca9ec1..fc9052a 100644 --- a/src/rules/imports.bend +++ b/src/rules/imports.bend @@ -91,8 +91,8 @@ 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) - Bool.pick(List<&2, String>, Bool.and(Bool.and(has(read, d), Bool.not(has(seen, d))), Bool.not(has(more, d))), - d <> more, more) + +known = Bool.and(has(read, d), Bool.not(has(seen, d))) # noqa: U013 the spec fresh.fast is proven against + Bool.pick(List<&2, String>, Bool.and(known, Bool.not(has(more, d))), d <> more, more) # the paths of the files def paths(es: List<&2, Edge>) -> List<&2, String>: @@ -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) + +found = fresh.spec(deps.spec(es, p), seen, read) # noqa: U013 the spec walk is proven against 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) + +found = fresh.fast(deps.first(es, p), seen, read) # noqa: U013 one lookup per file reached, fuel-bound 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) + +found = fresh.fast(deps.first(es, at), seen, read) # noqa: U013 one lookup per file on the path 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 079ab4c..613501e 100644 --- a/src/rules/laws/trace.bend +++ b/src/rules/laws/trace.bend @@ -294,7 +294,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)) + List.append(&2, F.Finding, judge_entry(ds, id, e, nn), judge_entries(rest, ds, id, nn)) # noqa: U013 one per file # is the row a claim: Proved, and proved or pending? def claims(+lv: String, +st: String) -> Bool: @@ -329,7 +329,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)) + List.append(&2, F.Finding, judge_row(r, sp, ds), judge_rows(rest, sp, ds)) # noqa: U013 one per file # is the ID a row that is a claim: Proved, and proved or pending? def claimed(rs: List<&2, Row>, +id: String) -> Bool: @@ -362,7 +362,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)) + List.append(&2, F.Finding, stray(d, rs, path, n, l), strays.laws(rest, rs, path)) # noqa: U013 SPEC.md rows # every stray tag of every law file def strays(ds: List<&2, Digest.Digest>, +rs: List<&2, Row>) -> List<&2, F.Finding>: @@ -370,7 +370,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)) + List.append(&2, F.Finding, strays.laws(laws, rs, path), strays(rest, rs)) # noqa: U013 rs holds SPEC.md's rows # the rows that are not rows def malformed(ms: List<&2, Mark>) -> List<&2, F.Finding>: @@ -387,8 +387,8 @@ 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) - +twice = Bool.pick(List<&2, F.Finding>, Nat.is_gt(marks_with(all, id), 1n), at(nn, id ++ " is listed twice.") <> more, - more) + +dup = Nat.is_gt(marks_with(all, id), 1n) # noqa: U013 SPEC.md's IDs + +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) # the rule over a SPEC.md that was read diff --git a/src/rules/laws/unsafe.bend b/src/rules/laws/unsafe.bend index 8b588fa..2e95fac 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), + List.append(&2, F.Finding, found(reacher(rs, norm), unsafes, path, norm, es, read, fuel), # noqa: U013 law files 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 fa85b45..d00dc5f 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)) + List.append(&2, F.Finding, check.mark(mk, whole, path, gs), check(rest, whole, path, gs)) # noqa: U013 one file's diff --git a/src/rules/suspicious/argv.bend b/src/rules/suspicious/argv.bend new file mode 100644 index 0000000..6154c7a --- /dev/null +++ b/src/rules/suspicious/argv.bend @@ -0,0 +1,57 @@ +# 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) diff --git a/src/rules/suspicious/concat.bend b/src/rules/suspicious/concat.bend index d49b854..6837504 100644 --- a/src/rules/suspicious/concat.bend +++ b/src/rules/suspicious/concat.bend @@ -185,7 +185,8 @@ def hits( List.reverse(&2, F.Finding, acc) case Con{+a, rest}: +slot = Maybe.default(&2, String, List.head(&2, String, params), "") - hits(rest, List.tail(&2, String, params), lets, path, hit(seen(a, lets), slot, path, acc)) + was = seen(a, lets) # noqa: U013 a def's 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 def after(kind: Tree.StmtKind, +kids: Tree.Node, +lets: List<&2, Let>) -> List<&2, Let>: diff --git a/src/rules/suspicious/eager.bend b/src/rules/suspicious/eager.bend index a67a9ad..064ac0e 100644 --- a/src/rules/suspicious/eager.bend +++ b/src/rules/suspicious/eager.bend @@ -6,15 +6,20 @@ # sees it (a game's overlap test moved out of a pick branch took a scene from # 31 to 55 fps; one `gaps(..)` in a branch here ran on every file the linter # read, 88 s of a 100 s run). Bind the call above the pick (`+x = gaps(..)`), -# or take the branch lazily (`Lazy.stop`, `Lazy.or_else` from src/lazy/lazy.bend: -# the last argument is a `Unit -> T` thunk, applied only on the branch that -# needs it). Two things keep it off idiomatic code: only a call to a def of -# this file counts, and only to one that loops (it calls itself, or reaches -# something that does), since a Base call and a one-line accessor are -# everywhere and cost nothing; only the branch arguments count, not the type -# and the condition, which run whatever is written; and what sits after a -# `=>` is a lambda's body, which the call does not run. The body ends at the -# next comma of its group, so an argument after it counts again. +# or branch with `match` on the condition. For a search that recurses, carry +# the test as a Bool into the next call (`go(rest, k, test(h))`) and match on +# it first: the step stays a tail call and compiles to a loop, where a thunk +# around the recursive call (`Lazy.or_else(hit, _u => go(rest))`) allocates a +# closure and leaves the loop on every step (`thunk`, U015). The early exits +# of src/lazy/lazy.bend (`Lazy.stop`, `Lazy.or_else`: the last argument is a +# `Unit -> T` thunk, applied only on the branch that needs it) stay right for +# work that does not recurse. Two things keep it off idiomatic code: only a +# call to a def of this file counts, and only to one that loops (it calls +# itself, or reaches something that does), since a Base call and a one-line +# accessor are everywhere and cost nothing; only the branch arguments count, +# not the type and the condition, which run whatever is written; and what +# sits after a `=>` is a lambda's body, which the call does not run. The body +# ends at the next comma of its group, so an argument after it counts again. import Base import ../../src.bend as Src import ../../finding.bend as F @@ -44,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)) + Lazy.or_else(List.contains(~String, ~String.eq, set, c), _u => any_of(t, set)) # noqa: U013 a def's names def loops.go(ds: List<&2, Calls.Def>, +acc: List<&2, String>) -> List<&2, String>: match ds: @@ -116,7 +121,8 @@ 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")) - +mine = Bool.and(Bool.not(String.eq(t, self)), List.contains(~String, ~String.eq, ns, t)) + +known = List.contains(~String, ~String.eq, ns, t) # noqa: U013 a def's names + +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)) +more = List.concat(&2, F.Finding, diff --git a/src/rules/suspicious/fuel.bend b/src/rules/suspicious/fuel.bend index b737574..216fe6b 100644 --- a/src/rules/suspicious/fuel.bend +++ b/src/rules/suspicious/fuel.bend @@ -121,7 +121,9 @@ 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)) - List.concat(&2, F.Finding, [calls(kids, fs, self, path), calls(body, fs, self, path), check.go(rest, fs, path)]) + +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 + List.concat(&2, F.Finding, [head, inner, check.go(rest, fs, path)]) case Tree.NCons{h, rest}: check.go(rest, fs, path) case other: diff --git a/src/rules/suspicious/hoist.bend b/src/rules/suspicious/hoist.bend index f119de4..e342bea 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)) + +keep = Bool.and(Bool.not(String.is_empty(nm)), all_same(cs, ii, nm)) # noqa: U013 cs holds one def's self-calls 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) + +ok = leaf_ok(String.eq(op, "~"), tok, carried) # noqa: U013 carried holds one def's parameters +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) + +ok = value_ok(String.eq(o, "("), k, t, carried) # noqa: U013 carried holds one def's parameters +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) + +ok = List.contains(~String, ~String.eq, carried, t) # noqa: U013 carried holds one def's parameters +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) + +own = call_table(heat, String.eq(o, "("), t, kids, self, wides, carried, path) # noqa: U013 a def's parameters +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) + +own = let_hit(hot, kids, body, rest, self, wides, carried, path) # noqa: U013 carried holds one def's parameters 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 9ee9832..e3b4777 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)) + Lazy.or_else(List.contains(~String, ~String.eq, set, c), _u => any_of(t, set)) # noqa: U013 the file's loops 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) + "|" ++ nm ++ "=" ++ U32.show(count(bs, nm, line, col)) ++ stamp(rest, bs, line, col) # noqa: U013 a piece's lets # 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) - +here = open_site(String.eq(o, "("), indexed(rest), t, args, l, c, + +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 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) + pin_one(ps, s) <> pin(ps, rest) # noqa: U013 ps holds one piece's marks # 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) + +here = other_full(Bool.and(same, diff), how, body) # noqa: U013 body is one straight piece +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) + +here = earlier_one(s, name, args, line, col, body) # noqa: U013 body is one straight piece +more = earlier(rest, name, args, line, col, body) Bool.or(here, more) @@ -876,7 +876,8 @@ def report( case Nil{}: Nil{} case Con{+s, rest}: - List.append(&2, F.Finding, report_one(s, all, body, path, seen), report(rest, all, body, path, s <> seen)) + +mine = report_one(s, all, body, path, seen) # noqa: U013 one straight piece + 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 def local(+nn: Tree.Node, +self: String, +lp: List<&2, String>, +path: String) -> List<&2, F.Finding>: @@ -887,8 +888,8 @@ 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}: - List.concat(&2, F.Finding, [local(body, self, lp, path), visit(body, self, lp, path), - visit(rest, self, lp, path)]) + +here = local(body, self, lp, path) # noqa: U013 the file's loops + 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), visit(rest, self, lp, path)]) diff --git a/src/rules/suspicious/ring.bend b/src/rules/suspicious/ring.bend index b2e5203..4cfd8e6 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) + Bool.or(win_name(h, wins), more) # noqa: U013 wins holds one def's windows # 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) + +here = here_of(String.eq(o, "("), k, t, l, c, kids, wins) # noqa: U013 wins holds one def's windows +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) + +recv = call_recv(open, t, kids, wins) # noqa: U013 wins holds one def's windows +inn = plus_scan(kids, None{}, wins) - +drop = call_drop(open, k, t, l, c, kids, wins) + +drop = call_drop(open, k, t, l, c, kids, wins) # noqa: U013 wins holds one def's windows +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) + +aft = plus_scan(rest, or_tok(seen, drop_in(kids, wins)), wins) # noqa: U013 wins holds one def's windows 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)), + List.append(&2, F.Finding, slide(h, path, slot_wins(slot, wins)), # noqa: U013 wins holds one def's windows slides(rest, List.tail(&2, String, params), path, wins)) # every self-call's sliding arguments @@ -289,7 +289,8 @@ 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}: - +keep = Bool.and(Bool.not(String.is_empty(p)), Bool.not(List.contains(~String, ~String.eq, bad, p))) + +known = List.contains(~String, ~String.eq, bad, p) # noqa: U013 a def's parameters + +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)) # parameters that are not matched as input diff --git a/src/rules/suspicious/scan.bend b/src/rules/suspicious/scan.bend new file mode 100644 index 0000000..c608cdc --- /dev/null +++ b/src/rules/suspicious/scan.bend @@ -0,0 +1,340 @@ +# rule scan: a def that calls itself and, on the same step, hands a +# parameter it carries unchanged to a walk. Every step walks that list again: +# O(|A| * |B|), A what the def walks and B what it carries. Index it once +# outside the loop, or merge two sorted walks. A parameter is carried when +# every self-call passes it back as that same lone name in its own position +# (hoist's notion). A call is a name token (plain or dotted), then a `(` +# group, and what it walks is some of its arguments, counted from 0. A Base +# list search walks its list: argument 2 of `List.contains`, `List.find`, +# `List.filter` and `List.length`, 3 of `List.any` and `List.all`, 4 of +# `List.foldl` and `List.foldr`; a Base walk that rebuilds the list +# (`List.map`, `List.append`, ...) makes output, not a search, and is left +# alone. A def of this file walks, when it calls itself, its first live +# parameter that some self-call does not pass back unchanged (the one it +# shrinks), unless that parameter is a `Nat` or a `String` (a count, such as +# fuel, or a text); and each parameter its body, anywhere, passes as the lone +# name of an argument a call walks, of a Base search or of a def listed +# before it. A def of another module is not seen. A call reports when it is +# not a self-call and an argument it walks is exactly the lone name of a +# carried parameter: anything else there (a literal table, an expression, a +# name the step binds) is left alone. The step is what hoist reads as hot: +# the def's body, a case arm's body only when it calls the def, never a case +# pattern, and never the rest of a chain after `=>` (a lambda's body, a +# `Lazy` thunk, runs when it is called). Laws and proofs do not run (a def +# with no type at all fills a law: it is a proof), and a law file is skipped +# whole. One finding per call, on its callee. +import Base +import ../../src.bend as Src +import ../../paths.bend as Paths +import ../../finding.bend as F +import ../../syntax/lex.bend as Lex +import ../../syntax/tree.bend as Tree +import ../calls.bend as Calls +import ../../lazy/lazy.bend as Lazy +import ./hoist.bend as Hoist + +# a def of this file, and one argument it walks +type Walk is Data: + Walk{name: String, at: Nat} + +# the answer as a list: none or one +def opt(mm: Maybe<&2, Nat>) -> List<&2, Nat>: + match mm: + case None{}: + Nil{} + case Some{at}: + [at] + +# the list argument of a Base list search +def base_at(+tt: String) -> List<&2, Nat>: + +two = List.contains(~String, ~String.eq, ["List.contains", "List.find", "List.filter", "List.length"], tt) + +three = List.contains(~String, ~String.eq, ["List.any", "List.all"], tt) + +four = List.contains(~String, ~String.eq, ["List.foldl", "List.foldr"], tt) + Bool.pick(List<&2, Nat>, two, [2n], Bool.pick(List<&2, Nat>, three, [3n], Bool.pick(List<&2, Nat>, four, [4n], []))) + +# the arguments the defs of this file named tt walk +def file_at(ws: List<&2, Walk>, +tt: String) -> List<&2, Nat>: + match ws: + case Nil{}: + Nil{} + case Con{Walk{+nm, +at}, rest}: + +more = file_at(rest, tt) + Bool.pick(List<&2, Nat>, String.eq(nm, tt), at <> more, more) + +# the arguments a callee walks: a Base walk's list, and those the defs of this file record +def slots(+tt: String, +ws: List<&2, Walk>) -> List<&2, Nat>: + List.append(&2, Nat, base_at(tt), file_at(ws, tt)) + +# a leaf that is a plain name: its text +def name_tok(tok: Lex.Tok) -> Maybe<&2, String>: + match tok: + case Lex.Tok{Lex.TName{}, t, l, c}: + Some{t} + case other: + None{} + +# the argument, when it is exactly one plain name +def name_of(nn: Tree.Node) -> Maybe<&2, String>: + match nn: + case Tree.NCons{Tree.Leaf{tok}, Tree.NNil{}}: + name_tok(tok) + case other: + None{} + +# the name, when the list holds it +def keep_in(mm: Maybe<&2, String>, +names: List<&2, String>) -> Maybe<&2, String>: + match mm: + case None{}: + None{} + case Some{+nm}: + Bool.pick(Maybe<&2, String>, List.contains(~String, ~String.eq, names, nm), Some{nm}, None{}) + +# the first of two answers that has one +def first(aa: Maybe<&2, String>, bb: Maybe<&2, String>) -> Maybe<&2, String>: + match aa: + case None{}: + bb + case Some{nm}: + Some{nm} + +# the first walked argument that is the lone name of one of the names +def found(ss: List<&2, Nat>, +as: List<&2, Tree.Node>, +names: List<&2, String>) -> Maybe<&2, String>: + match ss: + case Nil{}: + 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 + +# where a name sits among the parameter names +def index_of(ps: List<&2, String>, +nm: String, +ii: Nat) -> Maybe<&2, Nat>: + match ps: + case Nil{}: + None{} + case Con{+p, rest}: + Lazy.stop(Maybe<&2, Nat>, String.eq(p, nm), Some{ii}, _u => index_of(rest, nm, 1n+ii)) + +# where the name sits among the parameter names, when there is a name +def index_in(mm: Maybe<&2, String>, +ps: List<&2, String>) -> Maybe<&2, Nat>: + match mm: + case None{}: + None{} + case Some{+nm}: + index_of(ps, nm, 0n) + +# the parameters that sit, as lone names, at walked arguments +def params_at(ss: List<&2, Nat>, +as: List<&2, Tree.Node>, +ps: List<&2, String>) -> List<&2, Nat>: + match ss: + case Nil{}: + 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 + +# a call's walked parameters, when its callee is a name and it is a call +def pass_hit( + kk: Lex.TokKind, + +open: Bool, + +tt: String, + kids: Tree.Node, + +ps: List<&2, String>, + +ws: List<&2, Walk> +) -> List<&2, Nat>: + match kk: + case Lex.TName{}: + Lazy.stop(List<&2, Nat>, Bool.not(open), [], _u => params_at(slots(tt, ws), Calls.args(kids), ps)) + case Lex.TDotted{}: + Lazy.stop(List<&2, Nat>, Bool.not(open), [], _u => params_at(slots(tt, ws), Calls.args(kids), ps)) + case other: + Nil{} + +# the parameters a body passes, anywhere, as an argument some call walks +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 + 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)]) + case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}: + List.concat(&2, Nat, [passes(kids, ps, ws), passes(body, ps, ws), passes(rest, ps, ws)]) + case Tree.NCons{h, rest}: + passes(rest, ps, ws) + case other: + Nil{} + +# a live parameter that some self-call does not pass back unchanged +def moves(+pp: Tree.Node, +carried: List<&2, String>) -> Bool: + Bool.and(Calls.is_live(pp), Bool.not(List.contains(~String, ~String.eq, carried, Calls.param_name(pp)))) + +# a count or a text: a loop down one scans no list +def scalar(+pp: Tree.Node) -> Bool: + +hh = Calls.type_head(pp, False{}) + Bool.or(String.eq(hh, "Nat"), String.eq(hh, "String")) + +# where the parameter a def shrinks sits, unless it is a count or a text +def place(+pp: Tree.Node, +ii: Nat) -> Maybe<&2, Nat>: + Bool.pick(Maybe<&2, Nat>, scalar(pp), None{}, Some{ii}) + +def own.go(ps: List<&2, Tree.Node>, +carried: List<&2, String>, +ii: Nat) -> Maybe<&2, Nat>: + match ps: + case Nil{}: + None{} + case Con{+p, rest}: + +here = moves(p, carried) # noqa: U013 a def's parameters + 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 +def own(+sig: Tree.Node, +body: Tree.Node, +name: String) -> Maybe<&2, Nat>: + Lazy.stop(Maybe<&2, Nat>, Bool.not(Calls.calls(body, name)), None{}, + _u => own.go(Calls.params(sig), Hoist.carried(sig, body, name), 0n)) + +# one walk of the def for each argument +def tag(ns: List<&2, Nat>, +name: String, +ws: List<&2, Walk>) -> List<&2, Walk>: + match ns: + case Nil{}: + ws + case Con{at, rest}: + Walk{name, at} <> tag(rest, name, ws) + +def walks.go(ds: List<&2, Calls.Def>, +ws: List<&2, Walk>) -> List<&2, Walk>: + match ds: + case Nil{}: + ws + case Con{Calls.Def{+name, +sig, +body}, rest}: + +mine = List.append(&2, Nat, opt(own(sig, body, name)), passes(body, Calls.names(sig), ws)) + walks.go(rest, tag(mine, name, ws)) + +# the defs of this file that walk, each with an argument it walks, in order +def walks(ds: List<&2, Calls.Def>) -> List<&2, Walk>: + walks.go(ds, []) + +# the name of the parameter a def shrinks, "" for none +def lead.go(ps: List<&2, Tree.Node>, +carried: List<&2, String>) -> String: + match ps: + case Nil{}: + "" + case Con{+p, rest}: + +here = moves(p, carried) # noqa: U013 a def's parameters + Lazy.stop(String, here, Calls.param_name(p), _u => lead.go(rest, carried)) + +# a finding on the callee, naming the carried list +def cite( + mm: Maybe<&2, String>, + +tt: String, + +line: U32, + +col: U32, + +self: String, + +lead: String, + +path: String +) -> List<&2, F.Finding>: + match mm: + case None{}: + Nil{} + case Some{+pp}: + [F.Finding{path, line, col, U32.from_nat(String.length(tt)), "scan", + tt ++ " walks " ++ pp ++ " on every step of " ++ self ++ ", which carries it unchanged: that is O(|" ++ lead + ++ "| * |" ++ pp ++ "|). Index it once outside the loop, or merge two sorted walks."}] + +# a hot call of a walk other than the def, a walked argument carried +def on_name( + +hot: Bool, + +open: Bool, + +tt: String, + +line: U32, + +col: U32, + kids: Tree.Node, + +self: String, + +ws: List<&2, Walk>, + +carried: List<&2, String>, + +lead: String, + +path: String +) -> List<&2, F.Finding>: + Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(hot, Bool.and(open, Bool.not(String.eq(tt, self))))), [], + _u => cite(found(slots(tt, ws), Calls.args(kids), carried), tt, line, col, self, lead, path)) + +# a call's finding, when its callee is a name +def call_hit( + kk: Lex.TokKind, + +hot: Bool, + +open: Bool, + +tt: String, + +line: U32, + +col: U32, + kids: Tree.Node, + +self: String, + +ws: List<&2, Walk>, + +carried: List<&2, String>, + +lead: String, + +path: String +) -> List<&2, F.Finding>: + match kk: + case Lex.TName{}: + on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path) + case Lex.TDotted{}: + on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path) + case other: + Nil{} + +# the walks of carried lists on a hot path +def walk( + nn: Tree.Node, + +self: String, + +ws: List<&2, Walk>, + +carried: List<&2, String>, + +lead: String, + +path: String, + +hot: Bool +) -> 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}}: + +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 + +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]) + case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}: + walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k)) + case Tree.NCons{Tree.Group{open, +kids, close}, rest}: + List.concat(&2, F.Finding, + [walk(kids, self, ws, carried, lead, path, hot), walk(rest, self, ws, carried, lead, path, hot)]) + case Tree.NCons{Tree.Stmt{Tree.SCase{}, kids, +body}, rest}: + +arm = Bool.and(hot, Calls.calls(body, self)) + List.concat(&2, F.Finding, [walk(kids, self, ws, carried, lead, path, False{}), + walk(body, self, ws, carried, lead, path, arm), walk(rest, self, ws, carried, lead, path, hot)]) + case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}: + List.concat(&2, F.Finding, [walk(kids, self, ws, carried, lead, path, hot), + walk(body, self, ws, carried, lead, path, hot), walk(rest, self, ws, carried, lead, path, hot)]) + case Tree.NCons{h, rest}: + walk(rest, self, ws, carried, lead, path, hot) + case other: + Nil{} + +# one def's walk, its carried parameters and the one it shrinks read once +def run(+sig: Tree.Node, +body: Tree.Node, +name: String, +ws: List<&2, Walk>, +path: String) -> List<&2, F.Finding>: + +carried = Hoist.carried(sig, body, name) + walk(body, name, ws, carried, lead.go(Calls.params(sig), carried), path, True{}) + +def check.go( + ds: List<&2, Calls.Def>, + +ws: List<&2, Walk>, + +path: String, + acc: List<&2, List<&2, F.Finding>> +) -> List<&2, F.Finding>: + match ds: + case Nil{}: + List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc)) + case Con{Calls.Def{+name, +sig, +body}, rest}: + check.go(rest, ws, path, + Lazy.stop(List<&2, F.Finding>, + Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), [], + _u => run(sig, body, name, ws, path)) <> acc) + +# the findings over a file's defs, their walks read once +def check.on(+ds: List<&2, Calls.Def>, +path: String) -> List<&2, F.Finding>: + check.go(ds, walks(ds), path, []) + +# the rule; a law file is skipped whole, before its walks are read +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 => check.on(Calls.defs(tree), path)) diff --git a/src/rules/suspicious/table.bend b/src/rules/suspicious/table.bend index 6a2ffdf..e51e772 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) + +own = hit(String.eq(o, "("), t, kids, fixed, path, l, c) # noqa: U013 fixed holds the file's table defs 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/thunk.bend b/src/rules/suspicious/thunk.bend new file mode 100644 index 0000000..7adc10e --- /dev/null +++ b/src/rules/suspicious/thunk.bend @@ -0,0 +1,145 @@ +# 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 +# `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. +import Base +import ../../src.bend as Src +import ../../finding.bend as F +import ../../syntax/lex.bend as Lex +import ../../syntax/tree.bend as Tree +import ../calls.bend as Calls +import ../../lazy/lazy.bend as Lazy + +# does a name leaf under the node read the parameter: its text, or its text +# then a dot? +def reads(nn: Tree.Node, +pp: String) -> Bool: + match nn: + case Tree.Leaf{Lex.Tok{k, +t, _l, _c}}: + Bool.and(Lex.is_name(k), Bool.or(String.eq(t, pp), String.starts_with(t, pp ++ "."))) + case Tree.Group{_o, kids, _cl}: + reads(kids, pp) + case Tree.Stmt{_k, kids, body}: + +a = reads(kids, pp) + +b = reads(body, pp) + Bool.or(a, b) + case Tree.NCons{h, t}: + +a = reads(h, pp) + +b = reads(t, pp) + Bool.or(a, b) + case Tree.NNil{}: + False{} + +# does the lambda's body end after the call: the chain ends, or a comma? +def ends(nn: Tree.Node) -> Bool: + match nn: + case Tree.NCons{Tree.Leaf{Lex.Tok{k, _t, _l, _c}}, _rest}: + Lex.is_comma(k) + case Tree.NCons{_h, _rest}: + False{} + case _other: + True{} + +# are the parts a thunk of a self-call: the lead (a name parameter the call +# does not read), `=>`, the def's name, a `(` group, then the body's end? +def hit(+lead: Bool, +arrow: Bool, +own: Bool, +call: Bool, +end: Bool) -> Bool: + Bool.and(lead, Bool.and(arrow, Bool.and(own, Bool.and(call, end)))) + +# the finding at the self-call's name +def cite(+ll: U32, +cc: U32, +name: String, +path: String) -> F.Finding: + F.Finding{path, ll, cc, U32.from_nat(String.length(name)), "thunk", + name ++ " calls itself inside a thunk, which allocates a closure and leaves the loop on every step; carry the test as a Bool into the next call (`go(rest, k, test(h))`) and match on it first, so the search stays a loop."} + +# after the parameter, `=>`, the name and its `(` group: the finding when +# they make a thunk of a self-call +def site.group( + kp: Lex.TokKind, + +pp: String, + +aa: String, + +nm: String, + +ll: U32, + +cc: U32, + r3: Tree.Node, + +name: String, + +path: String +) -> List<&2, F.Finding>: + match r3: + case Tree.NCons{Tree.Group{Lex.Tok{_ko, +o, _lo, _co}, kids, _cl}, after}: + +lead = Bool.and(Lex.is_name(kp), Bool.not(reads(kids, pp))) + Bool.pick(List<&2, F.Finding>, + hit(lead, String.eq(aa, "=>"), String.eq(nm, name), String.eq(o, "("), ends(after)), + [cite(ll, cc, name, path)], []) + case _other: + [] + +# after the parameter and `=>`: the leaf that names the call +def site.name( + kp: Lex.TokKind, + +pp: String, + +aa: String, + r2: Tree.Node, + +name: String, + +path: String +) -> List<&2, F.Finding>: + match r2: + case Tree.NCons{Tree.Leaf{Lex.Tok{_kn, +n, +l, +c}}, r3}: + site.group(kp, pp, aa, n, l, c, r3, name, path) + case _other: + [] + +# after the parameter: the leaf that should be `=>` +def site.lam(kp: Lex.TokKind, +pp: String, rest: Tree.Node, +name: String, +path: String) -> List<&2, F.Finding>: + match rest: + case Tree.NCons{Tree.Leaf{Lex.Tok{_ka, +a, _la, _ca}}, r2}: + site.name(kp, pp, a, r2, name, path) + case _other: + [] + +# the finding when a node and the chain after it open a thunk of a self-call +def site(hh: Tree.Node, rest: Tree.Node, +name: String, +path: String) -> List<&2, F.Finding>: + match hh: + case Tree.Leaf{Lex.Tok{kp, +p, _l, _c}}: + site.lam(kp, p, rest, name, path) + 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>: + 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) + case Tree.Stmt{_k, kids, body}: + List.concat(&2, F.Finding, [walk(kids, name, path), walk(body, name, path)]) + case _other: + Nil{} + +def check.go(ds: List<&2, Calls.Def>, +path: String, acc: List<&2, List<&2, F.Finding>>) -> List<&2, F.Finding>: + match ds: + case Nil{}: + 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) + +# the rule +def check(ss: Src.Src) -> List<&2, F.Finding>: + Src.Src{path, text, toks, tree, bound, items} = ss + check.go(Calls.defs(tree), path, []) diff --git a/src/rules/suspicious/unused.bend b/src/rules/suspicious/unused.bend index eefb229..d43460e 100644 --- a/src/rules/suspicious/unused.bend +++ b/src/rules/suspicious/unused.bend @@ -192,7 +192,8 @@ def check.go( Nil{} case Con{Bind.Bind{+name, +line, +col, +kind, note}, rest}: +more = check.go(rest, hh, uses, fl, path) - +hit = Bool.and(reportable(kind, note, line, fl), Bool.not(String.starts_with(name, "_"))) + +shown = reportable(kind, note, line, fl) # noqa: U013 the file's foreign lines + +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", what(kind) ++ " " ++ name ++ " is never used."} <> more, more) diff --git a/src/syntax/bind.bend b/src/syntax/bind.bend index 1b95cde..2e683f0 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) + noted(binder(binds, l, c), Bind{name, l, c, kind, note}) <> refresh(rest, binds) # noqa: U013 annotated binders # the names in scope at a line: those of the statement on it, else of the # nearest statement above