src/check.bend source

src/check.bend on the hub · documented module

# src/check: `bolt check file..`: the checker (`bend`) on each file, its# errors in bolt's shape, `path:line:1: error: message` (bend reports no# column; a message's further lines are indented under it), then the count.# A file bend could not be run on is one error, `path:1:1: error: could not# run bend`, and never `clean`.# What a check prints and how it exits is `out`'s decision over what bend# reported (src/LAWS.bend proves it); `run` only does it.import Baseimport ./status.bend as Statusimport ./lsp/report.bend as Repimport ./lsp/checker/answer.bend as Checker# a message's lines after the first, indenteddef rest_lines(ls: List<&2, String>) -> String:  match ls:    case Nil{}:      ""    case Con{l, t}:      "\n  " ++ l ++ rest_lines(t)# a message's lines: the first, then the rest indenteddef message.of(ls: List<&2, String>) -> String:  match ls:    case Nil{}:      ""    case Con{h, t}:      h ++ rest_lines(t)# a message: its first line, the rest indenteddef message(msg: String) -> String:  message.of(String.lines(msg))# each diagnostic as a linedef show_all(ds: List<&2, Rep.Diag>, +path: String) -> List<&2, String>:  match ds:    case Nil{}:      Nil{}    case Con{Rep.Diag{line, msg}, rest}:      (path ++ ":" ++ U32.show((line + 1 : U32)) ++ ":1: error: " ++ message(msg)) <> show_all(rest, path)# a file checked: its path and the diagnostics bend reported for it, or a# file bend could not be run ontype Run is Data:  Run{path: String, ds: List<&2, Rep.Diag>}  Failed{path: String}# what a check prints, line by line, and the code it exits withtype Out is Data:  Out{lines: List<&2, String>, code: U32}# every run's error lines, in orderdef lines_of(runs: List<&2, Run>) -> List<&2, String>:  match runs:    case Nil{}:      Nil{}    case Con{Run{path, ds}, rest}:      List.append(&2, String, show_all(ds, path), lines_of(rest))    case Con{Failed{path}, rest}:      (path ++ ":1:1: error: could not run bend") <> lines_of(rest)# the error lines, then `clean` or the count, and the exit code: 1 when# there is any errordef out.at(ls: List<&2, String>, count: Nat) -> Out:  match count:    case 0n:      Out{List.append(&2, String, ls, ["clean"]), 0}    case 1n:      Out{List.append(&2, String, ls, ["1 error, 0 warnings"]), 1}    case 2n+more:      Out{List.append(&2, String, ls, [U32.show(U32.from_nat(2n+more)) ++ " errors, 0 warnings"]), 1}# what a check prints and how it exits, from what bend reported for each filedef out(runs: List<&2, Run>) -> Out:  +ls = lines_of(runs)  out.at(ls, List.length(&2, String, ls))# each line printeddef print_all(lines: List<&2, String>) -> IO(Unit):  # noqa: L001 IO driver  match lines:    case Nil{}:      IO.pure(Unit, Unit{})    case Con{l, t}:      do IO<Unit>:        IO.print(l)        print_all(t)# a file's run, from the checker's answer for itdef run_of(path: String, aa: Checker.Answer) -> Run:  match aa:    case Checker.Checked{ds}:      Run{path, ds}    case Checker.Unrun{}:      Failed{path}# every file checked, in order: what bend reported for eachdef check_all(~ck: Checker.Checker, paths: List<&2, String>) -> IO(List<&2, Run>):  # noqa: L001 IO driver  match paths:    case Nil{}:      IO.pure(List<&2, Run>, [])    case Con{+path, rest}:      do IO<List<&2, Run>>:        aa : Checker.Answer <- Checker.check(ck, path)        more : List<&2, Run> <- check_all(~ck, rest)        return run_of(path, aa) <> more# what out decided, done (BOLT-TRUST-9): its lines printed, then its codedef perform(oo: Out) -> IO(Unit):  # noqa: L001 IO driver  Out{lines, code} = oo  do IO<Unit>:    print_all(lines)    Status.stop(U32.is_gt(code, 0))# the checker over the files given, exiting 1 when any of them had an error# (main passes checker/bend.bend's service)def run(~ck: Checker.Checker, paths: List<&2, String>) -> IO(Unit):  # noqa: L001 IO driver  do IO<Unit>:    runs : List<&2, Run> <- check_all(~ck, paths)    perform(out(runs))