src/check.bend

bolt@1.26.0.0 · 118 lines · 14 definitions

1# src/check: `bolt check file..`: the checker (`bend`) on each file, its
2# errors in bolt's shape, `path:line:1: error: message` (bend reports no
3# column; a message's further lines are indented under it), then the count.
4# A file bend could not be run on is one error, `path:1:1: error: could not
5# run bend`, and never `clean`.
6# What a check prints and how it exits is `out`'s decision over what bend
7# reported (src/LAWS.bend proves it); `run` only does it.
8import Base
9import bolt@1.26.0.0/src/status.bend as Status
10import bolt@1.26.0.0/src/lsp/report.bend as Rep
11import bolt@1.26.0.0/src/lsp/checker/answer.bend as Checker
12
13# a message's lines after the first, indented
14def rest_lines(ls: List<&2, String>) -> String:
15  match ls:
16    case Nil{}:
17      ""
18    case Con{l, t}:
19      "\n  " ++ l ++ rest_lines(t)
20
21# a message's lines: the first, then the rest indented
22def message.of(ls: List<&2, String>) -> String:
23  match ls:
24    case Nil{}:
25      ""
26    case Con{h, t}:
27      h ++ rest_lines(t)
28
29# a message: its first line, the rest indented
30def message(msg: String) -> String:
31  message.of(String.lines(msg))
32
33# each diagnostic as a line
34def show_all(ds: List<&2, Rep.Diag>, +path: String) -> List<&2, String>:
35  match ds:
36    case Nil{}:
37      Nil{}
38    case Con{Rep.Diag{line, msg}, rest}:
39      (path ++ ":" ++ U32.show((line + 1 : U32)) ++ ":1: error: " ++ message(msg)) <> show_all(rest, path)
40
41# a file checked: its path and the diagnostics bend reported for it, or a
42# file bend could not be run on
43type Run is Data:
44  Run{path: String, ds: List<&2, Rep.Diag>}
45  Failed{path: String}
46
47# what a check prints, line by line, and the code it exits with
48type Out is Data:
49  Out{lines: List<&2, String>, code: U32}
50
51# every run's error lines, in order
52def lines_of(runs: List<&2, Run>) -> List<&2, String>:
53  match runs:
54    case Nil{}:
55      Nil{}
56    case Con{Run{path, ds}, rest}:
57      List.append(&2, String, show_all(ds, path), lines_of(rest))
58    case Con{Failed{path}, rest}:
59      (path ++ ":1:1: error: could not run bend") <> lines_of(rest)
60
61# the error lines, then `clean` or the count, and the exit code: 1 when
62# there is any error
63def out.at(ls: List<&2, String>, count: Nat) -> Out:
64  match count:
65    case 0n:
66      Out{List.append(&2, String, ls, ["clean"]), 0}
67    case 1n:
68      Out{List.append(&2, String, ls, ["1 error, 0 warnings"]), 1}
69    case 2n+more:
70      Out{List.append(&2, String, ls, [U32.show(U32.from_nat(2n+more)) ++ " errors, 0 warnings"]), 1}
71
72# what a check prints and how it exits, from what bend reported for each file
73def out(runs: List<&2, Run>) -> Out:
74  +ls = lines_of(runs)
75  out.at(ls, List.length(&2, String, ls))
76
77# each line printed
78def print_all(lines: List<&2, String>) -> IO(Unit):  # noqa: L001 IO driver
79  match lines:
80    case Nil{}:
81      IO.pure(Unit, Unit{})
82    case Con{l, t}:
83      do IO<Unit>:
84        IO.print(l)
85        print_all(t)
86
87# a file's run, from the checker's answer for it
88def run_of(path: String, aa: Checker.Answer) -> Run:
89  match aa:
90    case Checker.Checked{ds}:
91      Run{path, ds}
92    case Checker.Unrun{}:
93      Failed{path}
94
95# every file checked, in order: what bend reported for each
96def check_all(~ck: Checker.Checker, paths: List<&2, String>) -> IO(List<&2, Run>):  # noqa: L001 IO driver
97  match paths:
98    case Nil{}:
99      IO.pure(List<&2, Run>, [])
100    case Con{+path, rest}:
101      do IO<List<&2, Run>>:
102        aa : Checker.Answer <- Checker.check(ck, path)
103        more : List<&2, Run> <- check_all(~ck, rest)
104        return run_of(path, aa) <> more
105
106# what out decided, done (trusted in src/lint.bend): its lines printed, then its code
107def perform(oo: Out) -> IO(Unit):  # noqa: L001 IO driver
108  Out{lines, code} = oo
109  do IO<Unit>:
110    print_all(lines)
111    Status.stop(U32.is_gt(code, 0))
112
113# the checker over the files given, exiting 1 when any of them had an error
114# (main passes checker/bend.bend's service)
115def run(~ck: Checker.Checker, paths: List<&2, String>) -> IO(Unit):  # noqa: L001 IO driver
116  do IO<Unit>:
117    runs : List<&2, Run> <- check_all(~ck, paths)
118    perform(out(runs))