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.
3	import Base
4	import ../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
8	type 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
13	def 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
22	def 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
32	def 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
43	def 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
52	def 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)
61	type 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
65	def check(cc: Checker, path: String) -> IO(Answer):  # noqa: L001 effect accessor
66	  Checker{r} = cc
67	  r(path)