1	# rule hole: a TODO hole left in code, the one bend counts when it prints
2	# `SOME PROOFS FAIL` then "Error: 1 TODO found." or "Error: N TODOs found."
3	# and exits 1 (bend 2.0.34): a `?` and then the name `TODO`, with any spaces, newlines or comments
4	# between them (`?TODO`, `? TODO`). `?todo`, `?TODO_later` and `?TODO.x` are
5	# other names, which bend reports as a type error, not as a TODO, and they are
6	# not reported here. The finding spans `?` through `TODO` when both sit on one
7	# line, and the `?` alone when `TODO` is on a later line. LAWS.bend is exempt:
8	# by convention its laws are open claims, filled by PROOF.bend beside it.
9	import Base
10	import ../../paths.bend as Paths
11	import ../../role.bend as Role
12	import ../../src.bend as Src
13	import ../../finding.bend as F
14	import ../../syntax/lex.bend as Lex
15	import ../../lazy/lazy.bend as Lazy
16	import ../calls.bend as Calls
17	
18	# True when the first token past spaces, newlines and comments is `TODO`
19	def check.todo(toks: List<&2, Lex.Tok>) -> Bool:
20	  match toks:
21	    case Con{Lex.Tok{+k, +t, l, c}, rest}:
22	      Lazy.stop(Bool, Lex.significant(k), Bool.and(Calls.kind.upper(k), String.eq(t, "TODO")), _u => check.todo(rest))
23	    case Nil{}:
24	      False{}
25	
26	# the width of the hole a `?` at line, col starts: through the next token
27	# past spaces, newlines and comments when it sits on the same line, else 1
28	def check.width(toks: List<&2, Lex.Tok>, +line: U32, +col: U32) -> U32:
29	  match toks:
30	    case Con{Lex.Tok{k, t, +l, +c}, rest}:
31	      Lazy.stop(U32, Lex.significant(k), Bool.pick(U32, U32.is_eq(l, line), U32.add(U32.sub(c, col), 4), 1),
32	        _u => check.width(rest, line, col))
33	    case Nil{}:
34	      1
35	
36	def check.go(toks: List<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>:
37	  match toks:
38	    case Con{Lex.Tok{k, +q, +l, +c}, +rest}:
39	      +more = check.go(rest, path)
40	      Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(Calls.kind.oper(k), Lazy.and_then(String.eq(q, "?"),
41	        _u => check.todo(rest)))), more,
42	        _u => F.Finding{path, l, c, check.width(rest, l, c), "hole", "This ?TODO hole is still unfilled."} <> more)
43	    case Nil{}:
44	      Nil{}
45	
46	def check.on(toks: List<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>:
47	  Lazy.stop(List<&2, F.Finding>, Paths.is_laws(path), [], _u => check.go(toks, path))
48	
49	# the rule, told the file's role (src/role.bend): a law file is skipped
50	def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>:
51	  Src.Src{path, text, toks, tree, bound, items} = ss
52	  Lazy.stop(List<&2, F.Finding>, Role.is_laws(rr), [], _u => check.go(toks, path))
53	
54	# the rule
55	def check(ss: Src.Src) -> List<&2, F.Finding>:
56	  Src.Src{path, text, toks, tree, bound, items} = ss
57	  check.on(toks, path)