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