src/lsp/checker/bend.bend
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.27.0.0/src/lsp/checker/answer.bend as S
9import bolt@1.27.0.0/src/lsp/checker/argv.bend as Argv
10import bolt@1.27.0.0/src/lsp/report.bend as Rep
11import bolt@1.27.0.0/src/lsp/checker/names.bend as Names
12import bolt@1.27.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)}