src/rules/style/doc.bend

bolt@1.27.0.0 · 99 lines · 11 definitions

1# rule doc: every top-level def, type and law has a comment block right above
2# it: one or more column-0 `#` lines with no blank line between them and the
3# item, save a run of column-0 `@` lines (attributes such as `@unsafe`) that
4# may sit between the block and the item. A block of bare `#` lines counts,
5# though its text is empty; a line that starts inside a multi-line string
6# literal is text, never a comment line. Helpers
7# (dotted names like `show.go`) ride on their parent's doc, `main` needs none,
8# PROOF.bend fills laws that LAWS.bend already documents, and a test (under
9# tests/) is documented by its header and its check names.
10import Base
11import bolt@1.27.0.0/src/src.bend as Src
12import bolt@1.27.0.0/src/finding.bend as F
13import bolt@1.27.0.0/src/syntax/outline.bend as Outline
14import bolt@1.27.0.0/src/lazy/lazy.bend as Lazy
15import bolt@1.27.0.0/src/paths.bend as Paths
16import bolt@1.27.0.0/src/role.bend as Role
17import bolt@1.27.0.0/src/syntax/lex.bend as Lex
18
19# does an item of this kind need a comment?
20def needs(kk: Outline.ItemKind) -> Bool:
21  match kk:
22    case Outline.IDef{}:
23      True{}
24    case Outline.IType{}:
25      True{}
26    case Outline.ILaw{}:
27      True{}
28    case other:
29      False{}
30
31# `main`, and helpers named `x.go`
32def exempt(+name: String) -> Bool:
33  Bool.or(String.eq(name, "main"), String.contains(name, "."))
34
35# an item's kind, for the message
36def what(kk: Outline.ItemKind) -> String:
37  match kk:
38    case Outline.IType{}:
39      "Type"
40    case Outline.ILaw{}:
41      "Law"
42    case other:
43      "Def"
44
45# reading down, does a comment block end right above the next line? After a
46# comment line (its first char `#`) it does; an attribute line (`@unsafe`)
47# keeps what was above it; any other line ends it
48def check.after(+hh: String, ok: Bool) -> Bool:
49  Bool.or(String.starts_with(hh, "#"), Bool.and(String.starts_with(hh, "@"), ok))
50
51# reading lines 0 to nn - 1 down from ok: does a comment block end right
52# above line nn, past a run of attribute lines?
53def check.lead(lines: List<&2, String>, +nn: U32, +ok: Bool) -> Bool:
54  match lines:
55    case Nil{}:
56      Bool.and(U32.is_eq(nn, 0), ok)
57    case Con{hh, tt}:
58      Lazy.stop(Bool, U32.is_eq(nn, 0), ok, _u => check.lead(tt, U32.sub(nn, 1), check.after(hh, ok)))
59
60# is there a comment line right above line nn, or right above the attribute
61# lines right above it? A block of bare `#` lines counts, though its doc text
62# is empty. An item's comment block always ends there, so this test alone
63# decides: the doc text, what the comments say, is never read
64def check.above(+lines: List<&2, String>, +nn: U32) -> Bool:
65  check.lead(lines, nn, False{})
66
67def check.go(items: List<&2, Outline.Item>, +path: String, +lines: List<&2, String>) -> List<&2, F.Finding>:
68  match items:
69    case Nil{}:
70      Nil{}
71    case Con{Outline.Item{+k, +name, +line, _sig, _doc, _p}, rest}:
72      +more = check.go(rest, path, lines)
73      Bool.pick(List<&2, F.Finding>,
74        Lazy.and_then(Bool.and(needs(k), Bool.not(exempt(name))), _u => Bool.not(check.above(lines, line))),
75        F.Finding{path, line, 0, 0, "doc", what(k) ++ " " ++ name ++ " has no comment above it."} <> more, more)
76
77def lines.go(ls: List<&2, String>, +ins: List<&2, Bool>) -> List<&2, String>:
78  match ls:
79    case Nil{}:
80      Nil{}
81    case Con{hh, tt}:
82      Bool.pick(String, Outline.inside.hit(ins), "", hh) <> lines.go(tt, Outline.inside.rest(ins))
83
84# the lines of a source, each one that starts inside a string literal read
85# as empty: it is text, never a comment line
86def lines(text: String, toks: List<&2, Lex.Tok>) -> List<&2, String>:
87  lines.go(String.lines(text), Outline.inside(toks))
88
89# the rule
90def check(ss: Src.Src) -> List<&2, F.Finding>:
91  Src.Src{+path, text, toks, tree, bound, items} = ss
92  Lazy.stop(List<&2, F.Finding>, Bool.or(Paths.is_proof(path), Paths.is_test(path)),
93    [], _u => check.go(items, path, lines(text, toks)))
94
95# the rule, told the file's role (src/role.bend): a proof file is skipped
96def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>:
97  Src.Src{+path, text, toks, tree, bound, items} = ss
98  Lazy.stop(List<&2, F.Finding>, Bool.or(Role.is_proof(rr), Paths.is_test(path)),
99    [], _u => check.go(items, path, lines(text, toks)))