Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,8 @@ Design specs and plans are not kept in this repo; they live under
the loop on every miss (bend 2.0.34, 500 misses over 100k cells: JS 2.40 s
against 0.28 s carried, native `--gpu off` 1.18 s against 0.76 s; bend's
self-hosted compiler, PR #1207, gained 5.8 to 6.7% per site). `bolt`'s
`thunk` rule (U015, opt-in) reports that shape. The early exits of
`thunk` rule (U015, opt-in) reports that shape, a lone thunk (a dispatch
of two or more lambdas is left alone). The early exits of
`src/lazy/lazy.bend` (`Lazy.stop`, `Lazy.or_else`, `Lazy.and_then`: the
last argument is a `Unit -> T` thunk, applied only on the branch that needs
it) stay right for expensive work that does not recurse. The same goes for
Expand Down
16 changes: 8 additions & 8 deletions SPEC.md

Large diffs are not rendered by default.

9 changes: 0 additions & 9 deletions bolt.bend
Original file line number Diff line number Diff line change
Expand Up @@ -32,12 +32,3 @@ def unsafe() -> String:
# SPEC.md's rows and the laws' tags agree
def trace() -> String:
"error"

# a loop that walks a list it carries unchanged, on every step
def scan() -> String:
"error"

# 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"
9 changes: 0 additions & 9 deletions src/LAWS.bend
Original file line number Diff line number Diff line change
Expand Up @@ -159,15 +159,6 @@ law opt_in_off:
for h_rule: {Config.set_level(sets, rule) == None{} : Maybe<&2, Config.Level>}
{Config.level(Config.Config{sets}, group, rule) == Config.Off{} : Config.Level}

# LAW: argv is opt-in: with no setting of its own it is off, whatever its
# group says, so it reports on no project that did not name it
# BOLT-RULE-U014
law argv_opt_in:
for +sets: List<&2, Config.LevelSet>
for +group: String
for h_rule: {Config.set_level(sets, "argv") == None{} : Maybe<&2, Config.Level>}
{Config.level(Config.Config{sets}, group, "argv") == Config.Off{} : Config.Level}

# Unknown names (BOLT-CFG-7). The specs below are strict folds over the code
# table, written apart from config.bend's lookups.

Expand Down
3 changes: 0 additions & 3 deletions src/PROOF.bend
Original file line number Diff line number Diff line change
Expand Up @@ -148,9 +148,6 @@ def Laws.opt_in_off(sets, group, rule, h_opt, h_rule):
== Config.Off{} : Config.Level}
{==}

def Laws.argv_opt_in(sets, group, h_rule):
Laws.opt_in_off(sets, group, "argv", {==}, h_rule)

# Unknown names (BOLT-CFG-7). config.bend looks a slug up with Codes.find and
# a group with an early-exit fold; the spec folds both strictly. Each step
# lemma takes the comparison it branches on as a variable and cases on it.
Expand Down
91 changes: 61 additions & 30 deletions src/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ unset group has its default. The groups:
| group | rules | default |
|---------------|----------------------------------------------------------------------------------|---------|
| `correctness` | `hole` `pick` `put` `arms` `escape` `twice` `strings` `chars` `foreign` `setting` | error |
| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` (`scan`, `argv`, `thunk`: opt-in) | warn |
| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` `fromrev` (`scan`, `thunk`: opt-in) | warn |
| `style` | `doc` `space` `wrap` `param` `noqa` | warn |
| `laws` | `coverage` `closed` `unsafe` (`trace`: opt-in) | warn |
| `pedantic` | `tail` | off |
Expand All @@ -73,14 +73,18 @@ The stable codes, assigned once (do not renumber):
| C011 | `setting` | U011 | `rewalk` | P001 | `tail` |
| | | U012 | `unit` | | |
| | | U013 | `scan` | | |
| | | U014 | `argv` | | |
| | | U014 | retired | | |
| | | U015 | `thunk` | | |
| | | U016 | `fromrev` | | |

Letters: `C` correctness, `U` suspicious, `S` style, `L` laws, `P` pedantic.

`pedantic` is advice that is noisy on idiomatic code: off until a project
asks for it. L004 was `quantify`, the opt-in strict mode of `closed`;
`closed` is strict itself now, and L004 is never reused. `trace` is opt-in:
`closed` is strict itself now, and L004 is never reused. U014 was `argv`,
a check on `IO.args()` readers, retired before its first release: every
reader already drops the program, and it could not tell one that does from
one that does not. U014 is never reused either. `trace` is opt-in:
it is in `laws`, but no group setting reaches it; only `def trace()` in a
bolt.bend turns it on. `scan` and `thunk` are opt-in the same way, in `suspicious`: only
`def scan()` or `def thunk()` turns each on. An unknown level word grades as an error, so a typo shows. A `bolt.bend` is
Expand Down Expand Up @@ -146,17 +150,19 @@ or one written with no type at all (`def f(x, y):`, no `:` among its
parameters and no `->`), which is how Bend fills the law named `f`.

- `doc` — every top-level def, type and law has a comment block right above
it: column-0 `#` lines with no blank line before the item. A block of bare
`#` lines counts. Helpers (dotted names like `show.go`) ride on their
it: column-0 `#` lines with no blank line before the item, or before a run
of column-0 `@` lines (`@unsafe`) right above it. A block of bare `#` lines
counts. Helpers (dotted names like `show.go`) ride on their
parent's, `main` needs none, PROOF.bend fills laws that LAWS.bend
documents, and a test (under `tests/`) is documented by its header and its
check names.
- `unused` — a name bound by a let, a do-bind, a lambda or as a parameter is
never used. Exempt: pattern binders (naming every field of `Tok{k, t, l, c}`
reads better than `_`), names starting with `_`, erased parameters (`-x`),
a law's `for` names, and every parameter of a foreign def, one whose body
starts with `import` (its C and JS read them), however its header is
wrapped.
a law's `for` names, and every parameter of a foreign def, one whose body's
first statement is `import` (its C and JS read them), wherever its
header's `->` and return type fall. A name read in a dependent arrow's
types (`@+x: U32 -> S`) is a use.
- `hole` — a TODO hole left in code, the one bend counts in "1 TODO found." /
"N TODOs found." (under `SOME PROOFS FAIL`, exit 1):
`?` and then `TODO`, with spaces, newlines or comments allowed between
Expand Down Expand Up @@ -244,7 +250,8 @@ parameters and no `->`), which is how Bend fills the law named `f`.
(one sort phase went 39 s -> 0.9 s). A get anywhere in the def is
reported, one in a base arm that runs once included. A literal index of
any size is exempt. A `List.get` on a fixed table is `table`'s; a
`String.get` always stays here.
`String.get` always stays here. A get that is the def's own self-call (the
step of a def named `List.get` or `String.get`, as Base's are) is exempt.
- `table` — `List.get` or `List.set` at a computed index inside a def that
calls itself, when the list is a fixed table (a literal, a sized array, or
`List.replicate` / `Array.new` / `List.range` with a constant count),
Expand Down Expand Up @@ -293,28 +300,48 @@ parameters and no `->`), which is how Bend fills the law named `f`.
recurse, a Base walk that rebuilds the list (`List.map`, `List.append`),
and a def of another module are left alone. One finding per call, on its
callee.
- `argv` (opt-in) — a call `IO.args(`: an `IO.args` token with a `(` right
after it. Since bend 2.0.32 `IO.args()` starts with the program as
invoked, as C's argv does, so a program that parses it as it comes takes
its own path for its first argument. Read the arguments through shake's
`Shake.argv()`, or drop the first word before parsing. The rule cannot
tell the reader that drops it from one that does not: give that one
reader `# noqa: U014`. No path is exempt.
- `thunk` (opt-in) — a lambda whose body is exactly a self-call and whose
parameter the call does not read: a `Unit -> T` thunk such as
`Lazy.or_else(hit, _u => go(rest, k))`. The closure is allocated on every
step and the call in it is not a tail call of the def, so the search leaves
the loop each time round (bend 2.0.34, 500 misses over 100k cells: JS
2.40 s against 0.28 s, native 1.18 s against 0.76 s). Carry the test as a
Bool into the next call, `go(rest, k, test(h))`, and match on it first: the
step is then a tail call and compiles to a loop. `Lazy.*` stays right for
guarding work that does not recurse. Exactly: a name leaf (the parameter),
`=>`, the def's name and its `(` group, with the chain ending there or
going on with a comma, and no name leaf in the group spelling the
parameter or the parameter then a dot. A body that does more than the call
(`_u => Some{go(t)}`), or a continuation that reads its parameter
(`a => go(f, a)`), is left alone; `_ => loop(n)` is not, since the rule
parameter the call does not read, passed as the one lambda of a call: a
`Unit -> T` thunk such as `Lazy.or_else(hit, _u => go(rest, k))`. The
closure is allocated on every step and the call in it is not a tail call of
the def, so the search leaves the loop each time round (bend 2.0.34, 500
misses over 100k cells: JS 2.40 s against 0.28 s, native 1.18 s against
0.76 s). Carry the test as a Bool into the next call, `go(rest, k,
test(h))`, and match on it first: the step is then a tail call and compiles
to a loop. `Lazy.*` stays right for guarding work that does not recurse.
A dispatch, a call given two or more lambdas (`Lazy.either(T, c, _u =>
go(a), _v => go(b))`), is left alone: one carried Bool does not replace it.
Exactly: in the kids of a `(` group whose arguments (split at their commas)
hold exactly one with a `=>` leaf of its own (not inside a bracket), a name
leaf (the parameter), `=>`, the def's name and its `(` group, with the kids
ending there or going on with a comma, and no name leaf in the group
spelling the parameter or the parameter then a dot. A body that does more
than the call (`_u => Some{go(t)}`), a continuation that reads its
parameter (`a => go(f, a)`), or a lambda that is no call's argument
(`x = _u => go(t)`) is left alone; `_ => loop(n)` is not, since the rule
reads the shape and not the type.
- `fromrev` — `String.from_list(List.reverse(..))`: among the significant
tokens, `String.from_list`, `(`, `List.reverse` and `(` right after one
another, one finding on the first. A buffer of chars consed on the front
and then reversed and read into a String walks the buffer twice and builds
a list only to throw it away; `String.from_list` is not a tail call either,
so a long buffer runs the JS lane out of stack. Fold the buffer onto a
String with `SCon` in one pass (`src/rchars.bend`, bolt's own):

```bend
def text.go(buf: List<&2, Char>, acc: String) -> String:
match buf:
case Nil{}:
acc
case Con{h, t}:
text.go(t, SCon{h, acc})
```

Called as `text.go(buf, SNil{})` (bend 2.0.34, a 100k-char buffer 200
times: native 0.35 s against 0.17 s; JS at 20k chars 4.6 s against 3.1 s,
and at 50k the two-pass form overflows). Anything between the four tokens,
another `(` included, is not the shape, and neither is `List.reverse.go`.
A LAWS.bend or a PROOF.bend is exempt.
- `put` — `Map.put`. It is Base's internal helper: at a leaf it keeps the old
key and replaces the value without comparing, so a new key silently
overwrites another entry. `Map.set` compares. A file that defines
Expand Down Expand Up @@ -369,7 +396,11 @@ parameters and no `->`), which is how Bend fills the law named `f`.
overflows the checker's stack (bend 2.0.33/2.0.34). A literal of any size
counts, `3n` included. Only an argument that is the literal alone, or
`U32.to_nat(` it `)`, counts, so a let-bound literal and `(7n)` are not
seen. A def's own calls are exempt.
seen. A def's own calls are exempt, and so is a def that returns an
effect: a header with `->` then the name `IO` (`-> IO(Unit):`), or one
that ends in `->` with `IO(..):` on the next line. Its fuel bounds reads,
frames or retries the outside world sets (a drain of 256 datagrams a
tick, a read of 100000 chunks), not the size of an input it was given.
- `tail` (pedantic) — a self-call that is not a tail call, in a def whose
first live parameter is a `List` or a `String`. On a long one the JS lane
overflows its stack (a 48 KB header crashed a server; ~4,900 entries and
Expand Down
2 changes: 1 addition & 1 deletion src/args.bend
Original file line number Diff line number Diff line change
Expand Up @@ -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<List<&2, String>>:
ss : List<&1, String> <- IO.args() # noqa: U014 the one reader: args_of drops the program
ss : List<&1, String> <- IO.args()
return args_of(ss)

# whether a word names a subcommand
Expand Down
5 changes: 3 additions & 2 deletions src/codes.bend
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@
# source `bolt(group:slug)`. Numbers are assigned once, in the group order
# of src/README.md: do not renumber a rule, and do not reuse a retired code
# (L004 was `quantify`, now `closed` itself; C001 was `shadow` and U005 was
# `nat`, whose failures bend 2.0.25 no longer has).
# `nat`, whose failures bend 2.0.25 no longer has; U014 was `argv`, retired
# before its first release, since every reader already drops the program).
import Base
import ./lazy/lazy.bend as Lazy

Expand Down Expand Up @@ -36,8 +37,8 @@ def table() -> List<&2, Entry>:
Entry{"rewalk", "U011", "suspicious"},
Entry{"unit", "U012", "suspicious"},
Entry{"scan", "U013", "suspicious"},
Entry{"argv", "U014", "suspicious"},
Entry{"thunk", "U015", "suspicious"},
Entry{"fromrev", "U016", "suspicious"},
Entry{"doc", "S001", "style"},
Entry{"space", "S002", "style"},
Entry{"wrap", "S003", "style"},
Expand Down
14 changes: 7 additions & 7 deletions src/config.bend
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@
import Base
import ./lazy/lazy.bend as Lazy
import ./syntax/lex.bend as Lex
import ./rchars.bend as Rchars
import ./syntax/tree.bend as Tree
import ./syntax/bind.bend as Bind
import ./codes.bend as Codes
Expand Down Expand Up @@ -158,7 +159,7 @@ def unknown.in(ss: List<&2, Setting>, +rows: List<&2, Codes.Entry>) -> List<&2,
Nil{}
case Con{Setting{+n, w, line}, rest}:
+more = unknown.in(rest, rows)
Bool.pick(List<&2, Setting>, known.in(rows, n), # noqa: U013 the fixed code table
Bool.pick(List<&2, Setting>, known.in(rows, n),
more, Setting{n, w, line} <> more)

# the settings, in order, whose name is neither a rule's slug nor a group of
Expand All @@ -170,7 +171,7 @@ def unknown(ss: List<&2, Setting>) -> List<&2, Setting>:
def dir_of.go(cs: List<&2, Char>, +acc: List<&2, Char>, best: List<&2, Char>) -> String:
match cs:
case Nil{}:
String.from_list(List.reverse(&2, Char, best))
Rchars.text(best)
case Con{'/', t}:
dir_of.go(t, '/' <> acc, '/' <> acc)
case Con{c, t}:
Expand Down Expand Up @@ -215,9 +216,9 @@ def home.step(+seg: String, +above: List<&2, String>) -> List<&2, String>:
def home.segs(cs: List<&2, Char>, seg: List<&2, Char>, above: List<&2, String>) -> List<&2, String>:
match cs:
case Nil{}:
home.step(String.from_list(List.reverse(&2, Char, seg)), above)
home.step(Rchars.text(seg), above)
case Con{'/', t}:
home.segs(t, [], home.step(String.from_list(List.reverse(&2, Char, seg)), above))
home.segs(t, [], home.step(Rchars.text(seg), above))
case Con{c, t}:
home.segs(t, c <> seg, above)

Expand Down Expand Up @@ -274,10 +275,9 @@ def default(+group: String) -> Level:

# a rule only its own setting turns on: a group setting, or the group's
# default, would put new findings on projects that never asked for it
# (`trace`, and `argv`, which cannot tell the one reader that drops the
# program from the rest)
# (`trace`, `thunk` and `scan`)
def opt_in(+rule: String) -> Bool:
List.contains(~String, ~String.eq, ["trace", "argv", "thunk", "scan"], rule)
List.contains(~String, ~String.eq, ["trace", "thunk", "scan"], rule)

# the rule's own setting, else its group's, else the group's default; an
# opt-in rule's own setting, else off
Expand Down
2 changes: 1 addition & 1 deletion src/lint/plan.bend
Original file line number Diff line number Diff line change
Expand Up @@ -424,7 +424,7 @@ def grade(+cs: List<&2, Conf>, +world: W.World, fs: List<&2, F.Finding>) -> List
case Nil{}:
Nil{}
case Con{F.Finding{+path, line, col, len, rule, msg}, rest}:
cfg = config.at(cs, world, path) # noqa: U013 one config per directory
cfg = config.at(cs, world, path)
List.append(&2, F.Graded, Rules.graded(cfg, [F.Finding{path, line, col, len, rule, msg}]), grade(cs, world, rest))

# ---------------------------------------------------------------------------
Expand Down
2 changes: 1 addition & 1 deletion src/lsp/files/disk.bend
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ def read.opened(rr: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>)
case Fail{e}:
IO.pure(Maybe<&2, String>, None{})
case Done{file}:
slurp(U32.to_nat(100000), file, []) # noqa: U006 100000 reads of 64 KiB, past any source
slurp(U32.to_nat(100000), file, [])

# a file's text, or None when it cannot be opened
def read(path: String) -> IO(Maybe<&2, String>): # noqa: L001 disk effect
Expand Down
3 changes: 2 additions & 1 deletion src/lsp/frame.bend
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
# N bytes of UTF-8. Framing counts bytes and a read may end inside a char, so
# the transport reads bytes, cuts on bytes, and only then decodes.
import Base
import ../rchars.bend as Rchars

# UTF-8, bytes to chars
# ---------------------
Expand Down Expand Up @@ -49,7 +50,7 @@ def decode.run(bs: List<&2, U32>, st: Dec) -> Dec:

def decode.end(st: Dec) -> String:
Dec{need, acc, out} = st
String.from_list(List.reverse(&2, Char, out))
Rchars.text(out)

# UTF-8 bytes as a string (a bad byte is skipped)
def decode(bs: List<&2, U32>) -> String:
Expand Down
2 changes: 1 addition & 1 deletion src/lsp/transport/stdio.bend
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ def recv.loop(fuel: Nat, h2: Stdio) -> IO(Stdio & Maybe<&2, String>):

# the fuel bounds the reads one message may take
def recv(h2: Stdio) -> IO(Stdio & Maybe<&2, String>): # noqa: L001 transport effect
recv.loop(U32.to_nat(1000000), h2) # noqa: U006 a million reads for one message
recv.loop(U32.to_nat(1000000), h2)

def send.done(ww: File & Result<&1, &1, U32 & String, Unit>, inp: File, buf: List<&2, U32>) -> IO(Stdio):
(out, r) = ww
Expand Down
5 changes: 3 additions & 2 deletions src/noqa.bend
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
import Base
import ./lazy/lazy.bend as Lazy
import ./syntax/lex.bend as Lex
import ./rchars.bend as Rchars
import ./finding.bend as F
import ./codes.bend as Codes
import ./src.bend as Src
Expand Down Expand Up @@ -60,7 +61,7 @@ type Rd is Data:

# the chars read, the last first, as a code
def word(buf: List<&2, Char>) -> String:
String.from_list(List.reverse(&2, Char, buf))
Rchars.text(buf)

# before a code: a space waits, a letter or digit starts one, anything else
# ends the list
Expand Down Expand Up @@ -247,5 +248,5 @@ def keep(+ms: List<&2, Marks>, gs: List<&2, F.Graded>) -> List<&2, F.Graded>:
Nil{}
case Con{F.Graded{ll, F.Finding{+path, +line, col, len, +rule, msg}}, rest}:
+more = keep(ms, rest)
Bool.pick(List<&2, F.Graded>, silenced(ms, path, line, Codes.code(rule)), more, # noqa: U013 files with marks
Bool.pick(List<&2, F.Graded>, silenced(ms, path, line, Codes.code(rule)), more,
F.Graded{ll, F.Finding{path, line, col, len, rule, msg}} <> more)
17 changes: 17 additions & 0 deletions src/rchars.bend
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
# src/rchars: a buffer of chars read one at a time and consed on the front
# (the last read first) as the String it spells, in one pass: each char goes
# onto the String built so far, with no reversed list in between (the shape
# `fromrev`, U016, reports). Pure.
import Base

# the buffer's chars, first read first, then acc
def onto(buf: List<&2, Char>, acc: String) -> String:
match buf:
case Nil{}:
acc
case Con{h, t}:
onto(t, SCon{h, acc})

# the buffer's chars, first read first
def text(buf: List<&2, Char>) -> String:
onto(buf, SNil{})
4 changes: 2 additions & 2 deletions src/rules.bend
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,8 @@ import ./rules/suspicious/ring.bend as Ring
import ./rules/suspicious/rewalk.bend as Rewalk
import ./rules/suspicious/unit.bend as Unit
import ./rules/suspicious/scan.bend as Scan
import ./rules/suspicious/argv.bend as Argv
import ./rules/suspicious/thunk.bend as Thunk
import ./rules/suspicious/fromrev.bend as Fromrev
import ./rules/correctness/put.bend as Put
import ./rules/correctness/escape.bend as Escape
import ./rules/correctness/strings.bend as Strings
Expand Down Expand Up @@ -87,8 +87,8 @@ def on.rules(+ss: Src.Src) -> List<&2, F.Finding>:
Rewalk.check(ss),
Unit.check(ss),
Scan.check(ss),
Argv.check(ss),
Thunk.check(ss),
Fromrev.check(ss),
Put.check(ss),
Escape.check(ss),
Strings.check(ss),
Expand Down
Loading
Loading