src/lsp/checker/bend.bend

bolt@1.17.0.0 · 63 lines · 0 definitions

1# checker/bend: an effect (CPU event loop only): the diagnostics of the file
2# at a path. It runs `bend` on the file and reads its report. Which runs it
3# makes is argv.bend's, and what its output answers is answer.bend's, both
4# pure; this file only performs them. `service` hands it to the server and
5# to `bolt check`, which take the checker as a service and never import this
6# file, so their proofs reach no foreign code.
7import Base
8import bolt@1.17.0.0/src/lsp/checker/answer.bend as S
9import bolt@1.17.0.0/src/lsp/checker/argv.bend as Argv
10import bolt@1.17.0.0/src/lsp/report.bend as Rep
11import bolt@1.17.0.0/src/lsp/checker/names.bend as Names
12import bolt@1.17.0.0/src/lsp/files/disk.bend as Disk
13
14# how `bend <path> <flag>` went, one tag char, then everything it printed.
15# The flag is argv.bend's, `--check-only`: it checks, and never runs main.
16# The tag is `r` when bend ran and exited, `s` when a signal killed it, and
17# `x` when it could not be run: no pipe, no fork, or an exit with 127, the
18# code a failed exec exits with (as a shell does for a command it cannot
19# find)
20def bendcheck.exec(path: String, flag: String) -> IO(String):
21  import "./exec.c"
22  import "./exec.js"
23
24# what a run of bend answered, tag first; every run is argv.bend's, so it
25# checks and never runs main
26def launch(rr: Argv.Run) -> IO(String):  # noqa: L001 checker effect
27  Argv.Run{path, flag} = rr
28  bendcheck.exec(path, flag)
29
30# the first report, settled by the run that follows it (a LAWS.bend's
31# PROOF.bend), when argv.bend gives one
32def settle(mr: Maybe<&2, Argv.Run>, +ds: List<&2, Rep.Diag>) -> IO(S.Answer):  # noqa: L001 checker effect
33  match mr:
34    case None{}:
35      IO.pure(S.Answer, S.Checked{ds})
36    case Some{rr}:
37      do IO<S.Answer>:
38        text : String <- launch(rr)
39        return S.proved(S.answer(None{}, text), ds)
40
41# the diagnostics of a run, settled by the run that follows it
42def checked(+ds: List<&2, Rep.Diag>, +path: String) -> IO(S.Answer):  # noqa: L001 checker effect
43  settle(Argv.followup(ds, path), ds)
44
45# a run's answer: its diagnostics settled when bend ran, else no check
46def settled(aa: S.Answer, +path: String) -> IO(S.Answer):  # noqa: L001 checker effect
47  match aa:
48    case S.Checked{ds}:
49      checked(ds, path)
50    case S.Unrun{}:
51      IO.pure(S.Answer, S.Unrun{})
52
53# bend's report on the file, its errors placed by the names of the file's
54# items (read from the file bend read; unknown when it cannot be read)
55def check(+path: String) -> IO(S.Answer):  # noqa: L001 checker effect
56  do IO<S.Answer>:
57    text : String <- launch(Argv.run_of(path))
58    src : Maybe<&2, String> <- Disk.read(path)
59    settled(S.answer(Names.of(src), text), path)
60
61# the checker as a service (answer.bend's Checker)
62def service() -> S.Checker:  # noqa: L001 checker effect
63  S.Checker{p => check(p)}