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.
8	import Base
9	import ./status.bend as Status
10	import ./lsp/report.bend as Rep
11	import ./lsp/checker/answer.bend as Checker
12	
13	# a message's lines after the first, indented
14	def 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
22	def 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
30	def message(msg: String) -> String:
31	  message.of(String.lines(msg))
32	
33	# each diagnostic as a line
34	def 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
43	type 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
48	type Out is Data:
49	  Out{lines: List<&2, String>, code: U32}
50	
51	# every run's error lines, in order
52	def 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
63	def 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
73	def 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
78	def 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
88	def 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
96	def 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
107	def 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)
115	def 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))