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).
6	import Base
7	import ../../paths.bend as Paths
8	import ../report.bend as Rep
9	
10	# a run of bend: the file it is given and the flag after it
11	type Run is Data:
12	  Run{path: String, flag: String}
13	
14	# the flag of a run
15	def flag(rr: Run) -> String:
16	  Run{path, ff} = rr
17	  ff
18	
19	# the run that checks a file: `bend <path> --check-only`
20	def 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
25	def 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
33	def 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
40	def 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{})