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.
7	import Base
8	import ./answer.bend as S
9	import ./argv.bend as Argv
10	import ../report.bend as Rep
11	import ./names.bend as Names
12	import ../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)
20	def 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
26	def 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
32	def 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
42	def 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
46	def 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)
55	def 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)
62	def service() -> S.Checker:  # noqa: L001 checker effect
63	  S.Checker{p => check(p)}