src/lsp/checker/answer.bend

bolt@1.23.0.0 · 67 lines · 0 definitions

1# checker/answer: pure: what a run of the checker (bend.bend) gave for a file,
2# read from the text bend.bend's exec returns, and the checker as a service.
3import Base
4import bolt@1.23.0.0/src/lsp/report.bend as Rep
5
6# a checker's answer for a file: the diagnostics bend reported, or that bend
7# could not be run on it at all
8type Answer is Data:
9  Checked{ds: List<&2, Rep.Diag>}
10  Unrun{}
11
12# an answer's diagnostics: none when bend could not be run
13def errors(aa: Answer) -> List<&2, Rep.Diag>:
14  match aa:
15    case Checked{ds}:
16      ds
17    case Unrun{}:
18      []
19
20# a run a signal cut short: what bend reported before it died, or, when that
21# is nothing, no check at all
22def died(ds: List<&2, Rep.Diag>) -> Answer:
23  match ds:
24    case Nil{}:
25      Unrun{}
26    case Con{dd, rest}:
27      Checked{dd <> rest}
28
29# the answer a tag gives: bend ran (`r`), a signal killed it (`s`), or
30# neither, and it could not be run; each error placed by the checked file's
31# names, when they are known
32def answer.tag(ran: Bool, killed: Bool, names: Maybe<&2, List<&2, String>>, text: String) -> Answer:
33  match ran killed:
34    case True{} _k:
35      Checked{Rep.parse_in(names, text)}
36    case False{} True{}:
37      died(Rep.parse_in(names, text))
38    case False{} False{}:
39      Unrun{}
40
41# exec's text read: its tag, then what bend printed, as diagnostics placed by
42# the checked file's names
43def answer(names: Maybe<&2, List<&2, String>>, ss: String) -> Answer:
44  match ss:
45    case SNil{}:
46      Unrun{}
47    case SCon{+cc, text}:
48      answer.tag(Char.is_eq(cc, 'r'), Char.is_eq(cc, 's'), names, text)
49
50# a LAWS.bend's errors, settled by its PROOF.bend's answer: none when that
51# checks clean, and no check at all when bend could not be run on it
52def proved(aa: Answer, ds: List<&2, Rep.Diag>) -> Answer:
53  match aa:
54    case Checked{pds}:
55      Checked{Bool.pick(List<&2, Rep.Diag>, List.is_empty(&2, Rep.Diag, pds), [], ds)}
56    case Unrun{}:
57      Unrun{}
58
59# effect service: the checker's answer for the file at a path (bend.bend's
60# service is the real one)
61type Checker is Type:  # noqa: L001 effect service
62  Checker{run: String -> IO(Answer)}
63
64# the checker's answer for the file at a path, from a checker service
65def check(cc: Checker, path: String) -> IO(Answer):  # noqa: L001 effect accessor
66  Checker{r} = cc
67  r(path)