src/check.bend
bolt@1.17.0.0 · 118 lines · 0 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.17.0.0/src/status.bend as Status
10import bolt@1.17.0.0/src/lsp/report.bend as Rep
11import bolt@1.17.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 (BOLT-TRUST-9): 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))