src/rules/correctness/hole.bend
bolt@1.11.0.0 · 50 lines · 0 definitions
1# rule hole: a TODO hole left in code, the one bend counts in "N TODO found":
2# a `?` and then the name `TODO`, with any spaces, newlines or comments
3# between them (`?TODO`, `? TODO`). `?todo`, `?TODO_later` and `?TODO.x` are
4# other names, which bend reports as a type error, not as a TODO, and they are
5# not reported here. The finding spans `?` through `TODO` when both sit on one
6# line, and the `?` alone when `TODO` is on a later line. LAWS.bend is exempt:
7# by convention its laws are open claims, filled by PROOF.bend beside it.
8import Base
9import bolt@1.11.0.0/src/paths.bend as Paths
10import bolt@1.11.0.0/src/src.bend as Src
11import bolt@1.11.0.0/src/finding.bend as F
12import bolt@1.11.0.0/src/syntax/lex.bend as Lex
13import bolt@1.11.0.0/src/lazy/lazy.bend as Lazy
14import bolt@1.11.0.0/src/rules/calls.bend as Calls
15
16# True when the first token past spaces, newlines and comments is `TODO`
17def check.todo(toks: List<&2, Lex.Tok>) -> Bool:
18 match toks:
19 case Con{Lex.Tok{+k, +t, l, c}, rest}:
20 Lazy.stop(Bool, Lex.significant(k), Bool.and(Calls.kind.upper(k), String.eq(t, "TODO")), _u => check.todo(rest))
21 case Nil{}:
22 False{}
23
24# the width of the hole a `?` at line, col starts: through the next token
25# past spaces, newlines and comments when it sits on the same line, else 1
26def check.width(toks: List<&2, Lex.Tok>, +line: U32, +col: U32) -> U32:
27 match toks:
28 case Con{Lex.Tok{k, t, +l, +c}, rest}:
29 Lazy.stop(U32, Lex.significant(k), Bool.pick(U32, U32.is_eq(l, line), U32.add(U32.sub(c, col), 4), 1),
30 _u => check.width(rest, line, col))
31 case Nil{}:
32 1
33
34def check.go(toks: List<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>:
35 match toks:
36 case Con{Lex.Tok{k, +q, +l, +c}, +rest}:
37 +more = check.go(rest, path)
38 Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(Calls.kind.oper(k), Lazy.and_then(String.eq(q, "?"),
39 _u => check.todo(rest)))), more,
40 _u => F.Finding{path, l, c, check.width(rest, l, c), "hole", "This ?TODO hole is still unfilled."} <> more)
41 case Nil{}:
42 Nil{}
43
44def check.on(toks: List<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>:
45 Lazy.stop(List<&2, F.Finding>, Paths.is_laws(path), [], _u => check.go(toks, path))
46
47# the rule
48def check(ss: Src.Src) -> List<&2, F.Finding>:
49 Src.Src{path, text, toks, tree, bound, items} = ss
50 check.on(toks, path)