1	# rule pick: a def calls itself in a branch of a `Bool.pick`. Bool.pick is a
2	# function, so both branches are evaluated whatever the condition. In both
3	# branches, two recursive calls a step is 2^n work where one was meant (a
4	# per-token scan that took 20 s this way took 20 ms as one pass): bind the
5	# call once above the pick (`+more = go(rest)`) and pick between `x <> more`
6	# and `more`. In one branch, the recursion runs even when the other branch
7	# was the answer: a search never stops early and walks the whole input
8	# (portal-bend's `get`, bendoom's sorted insert). Match on the Bool instead,
9	# in a helper that takes it as a parameter. A self-call is the def's name
10	# followed by `(..)`: a parameter or a value named like the def is not one. A
11	# pick nested in a branch of one already reported is not reported again; one
12	# nested in its condition is. A
13	# law file, a proof file and a def that is a proof never run, so they are
14	# exempt: a def that returns a proof, or one written with no type at all
15	# (`def f(x, y):`), which fills the law named f.
16	import Base
17	import ../../src.bend as Src
18	import ../../finding.bend as F
19	import ../../syntax/lex.bend as Lex
20	import ../../syntax/tree.bend as Tree
21	import ../calls.bend as Calls
22	import ../../lazy/lazy.bend as Lazy
23	
24	# do both branches (the third and fourth arguments) call the def?
25	def both(+as: List<&2, Tree.Node>, +name: String) -> Bool:
26	  Bool.and(Calls.calls(Calls.arg(as, 2n), name), Calls.calls(Calls.arg(as, 3n), name))
27	
28	# does either branch call the def?
29	def once(+as: List<&2, Tree.Node>, +name: String) -> Bool:
30	  Bool.or(Calls.calls(Calls.arg(as, 2n), name), Calls.calls(Calls.arg(as, 3n), name))
31	
32	# is argument nth of a group quiet: the group's own quiet, or, in a branch
33	# (the third or fourth argument) of a reported pick, hushed
34	def mute(+quiet: Bool, +hush: Bool, nth: Nat) -> Bool:
35	  match nth:
36	    case 0n:
37	      quiet
38	    case 1n:
39	      quiet
40	    case 2n:
41	      Bool.or(quiet, hush)
42	    case 3n:
43	      Bool.or(quiet, hush)
44	    case 4n+p:
45	      quiet
46	
47	# the argument a token leaves the walk in: one further past a top-level comma
48	def next(kk: Lex.TokKind, nth: Nat) -> Nat:
49	  match kk:
50	    case Lex.TComma{}:
51	      1n+nth
52	    case other:
53	      nth
54	
55	# every `Bool.pick(..)` in a chain, at any depth, that recurses in both
56	# branches or in one. The chain is argument nth of a group with quiet
57	# (inside a branch of a reported pick) and hush (the group is a reported
58	# pick, so its branches are quiet); a pick in the condition still counts.
59	def walk(nn: Tree.Node, +name: String, +path: String, +quiet: Bool, +hush: Bool, +nth: Nat) -> List<&2, F.Finding>:
60	  match nn:
61	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, +l, +c}}, Tree.NCons{Tree.Group{open, +kids, close}, rest}}:
62	      +at = next(k, nth)
63	      +q = mute(quiet, hush, at)
64	      +as = Calls.args(kids)
65	      +ispick = String.eq(t, "Bool.pick")
66	      +two = Bool.and(Bool.and(ispick, Bool.not(q)), both(as, name))
67	      +one = Bool.and(Bool.and(ispick, Bool.not(two)), Bool.and(Bool.not(q), once(as, name)))
68	      +more = List.concat(&2, F.Finding, [walk(kids, name, path, q, Bool.or(two, one), 0n),
69	        walk(rest, name, path, quiet, hush, at)])
70	      Bool.pick(List<&2, F.Finding>, two,
71	        F.Finding{path, l, c, 9, "pick",
72	          name ++ " calls itself in both branches of Bool.pick, which evaluates both, so both calls run; bind the call once above the pick."}
73	          <> more,
74	        Bool.pick(List<&2, F.Finding>, one,
75	          F.Finding{path, l, c, 9, "pick",
76	            name ++ " calls itself in one branch of Bool.pick, which evaluates both, so the call always runs and never exits early; branch with `match` on the condition instead."}
77	            <> more,
78	          more))
79	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}:
80	      walk(rest, name, path, quiet, hush, next(k, nth))
81	    case Tree.NCons{Tree.Group{open, kids, close}, rest}:
82	      List.concat(&2, F.Finding, [walk(kids, name, path, mute(quiet, hush, nth), False{}, 0n),
83	        walk(rest, name, path, quiet, hush, nth)])
84	    case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}:
85	      List.concat(&2, F.Finding, [walk(kids, name, path, mute(quiet, hush, nth), False{}, 0n),
86	        walk(body, name, path, mute(quiet, hush, nth), False{}, 0n), walk(rest, name, path, quiet, hush, nth)])
87	    case Tree.NCons{h, rest}:
88	      walk(rest, name, path, quiet, hush, nth)
89	    case other:
90	      Nil{}
91	
92	# every reported pick in a chain walked at quiet, outside any pick's arguments
93	def picks(nn: Tree.Node, +name: String, +path: String, +quiet: Bool) -> List<&2, F.Finding>:
94	  walk(nn, name, path, quiet, False{}, 0n)
95	
96	def check.go(ds: List<&2, Calls.Def>, +path: String, acc: List<&2, List<&2, F.Finding>>) -> List<&2, F.Finding>:
97	  match ds:
98	    case Nil{}:
99	      List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc))
100	    case Con{Calls.Def{+name, +sig, body}, rest}:
101	      check.go(rest, path,
102	        Lazy.stop(List<&2, F.Finding>, Calls.exempt(path, sig), [],
103	          _u => picks(body, name, path, False{})) <> acc)
104	
105	# the rule
106	def check(ss: Src.Src) -> List<&2, F.Finding>:
107	  Src.Src{path, text, toks, tree, bound, items} = ss
108	  check.go(Calls.defs(tree), path, [])