src/lsp/checker/argv.bend

bolt@1.22.0.0 · 41 lines · 0 definitions

1# checker/argv: the runs of bend the real checker makes, as data. Pure: the
2# effect (bend.bend) only performs them, so LAWS.bend states over every path
3# and every first report that each run carries `--check-only`, the flag that
4# makes bend check the file and never run its main (laws/LspCheckerNeverRunsMain.bend; that bend
5# honours it is trusted in src/lsp/report.bend).
6import Base
7import bolt@1.22.0.0/src/paths.bend as Paths
8import bolt@1.22.0.0/src/lsp/report.bend as Rep
9
10# a run of bend: the file it is given and the flag after it
11type Run is Data:
12  Run{path: String, flag: String}
13
14# the flag of a run
15def flag(rr: Run) -> String:
16  Run{path, ff} = rr
17  ff
18
19# the run that checks a file: `bend <path> --check-only`
20def run_of(path: String) -> Run:
21  Run{path, "--check-only"}
22
23# only the open-laws report ("1 TODO found", "N TODOs found"), and nothing
24# else
25def only_todos(ds: List<&2, Rep.Diag>) -> Bool:
26  match ds:
27    case Con{Rep.Diag{line, +msg}, Nil{}}:
28      Bool.or(String.contains(msg, "TODO found"), String.contains(msg, "TODOs found"))
29    case other:
30      False{}
31
32# the PROOF.bend beside a LAWS.bend
33def proof_path(+path: String) -> String:
34  String.take(path, Nat.sub(String.length(path), 9n)) ++ "PROOF.bend"
35
36# By convention LAWS.bend states its laws as open claims and PROOF.bend, beside
37# it, fills them: alone, LAWS.bend always has TODOs. They are an error only
38# while PROOF.bend does not check clean, so a first report that is only the
39# open laws of a LAWS.bend is followed by a run on that PROOF.bend
40def followup(+ds: List<&2, Rep.Diag>, +path: String) -> Maybe<&2, Run>:
41  Bool.pick(Maybe<&2, Run>, Bool.and(only_todos(ds), Paths.is_laws(path)), Some{run_of(proof_path(path))}, None{})