1	# rule scan: a def that calls itself and, on the same step, hands a
2	# parameter it carries unchanged to a walk. Every step walks that list again:
3	# O(|A| * |B|), A what the def walks and B what it carries. Index it once
4	# outside the loop, or merge two sorted walks. A parameter is carried when
5	# every self-call passes it back as that same lone name in its own position
6	# (hoist's notion). A call is a name token (plain or dotted), then a `(`
7	# group, and what it walks is some of its arguments, counted from 0. A Base
8	# list search walks its list: argument 2 of `List.contains`, `List.find`,
9	# `List.filter` and `List.length`, 3 of `List.any` and `List.all`, 4 of
10	# `List.foldl` and `List.foldr`; a Base walk that rebuilds the list
11	# (`List.map`, `List.append`, ...) makes output, not a search, and is left
12	# alone. A def of this file walks, when it calls itself, its first live
13	# parameter that some self-call does not pass back unchanged (the one it
14	# shrinks), unless that parameter is a `Nat` or a `String` (a count, such as
15	# fuel, or a text); and each parameter its body, anywhere, passes as the lone
16	# name of an argument a call walks, of a Base search or of a def listed
17	# before it. A def of another module is not seen. A call reports when it is
18	# not a self-call and an argument it walks is exactly the lone name of a
19	# carried parameter: anything else there (a literal table, an expression, a
20	# name the step binds) is left alone. The step is what hoist reads as hot:
21	# the def's body, a case arm's body only when it calls the def, never a case
22	# pattern, and never the rest of a chain after `=>` (a lambda's body, a
23	# `Lazy` thunk, runs when it is called). Laws and proofs do not run (a def
24	# with no type at all fills a law: it is a proof), and a law file is skipped
25	# whole. One finding per call, on its callee.
26	import Base
27	import ../../src.bend as Src
28	import ../../paths.bend as Paths
29	import ../../role.bend as Role
30	import ../../finding.bend as F
31	import ../../syntax/lex.bend as Lex
32	import ../../syntax/tree.bend as Tree
33	import ../calls.bend as Calls
34	import ../../lazy/lazy.bend as Lazy
35	import ./hoist.bend as Hoist
36	
37	# a def of this file, and one argument it walks
38	type Walk is Data:
39	  Walk{name: String, at: Nat}
40	
41	# the answer as a list: none or one
42	def opt(mm: Maybe<&2, Nat>) -> List<&2, Nat>:
43	  match mm:
44	    case None{}:
45	      Nil{}
46	    case Some{at}:
47	      [at]
48	
49	# the list argument of a Base list search
50	def base_at(+tt: String) -> List<&2, Nat>:
51	  +two = List.contains(~String, ~String.eq, ["List.contains", "List.find", "List.filter", "List.length"], tt)
52	  +three = List.contains(~String, ~String.eq, ["List.any", "List.all"], tt)
53	  +four = List.contains(~String, ~String.eq, ["List.foldl", "List.foldr"], tt)
54	  Bool.pick(List<&2, Nat>, two, [2n], Bool.pick(List<&2, Nat>, three, [3n], Bool.pick(List<&2, Nat>, four, [4n], [])))
55	
56	# the arguments the defs of this file named tt walk
57	def file_at(ws: List<&2, Walk>, +tt: String) -> List<&2, Nat>:
58	  match ws:
59	    case Nil{}:
60	      Nil{}
61	    case Con{Walk{+nm, +at}, rest}:
62	      +more = file_at(rest, tt)
63	      Bool.pick(List<&2, Nat>, String.eq(nm, tt), at <> more, more)
64	
65	# the arguments a callee walks: a Base walk's list, and those the defs of this file record
66	def slots(+tt: String, +ws: List<&2, Walk>) -> List<&2, Nat>:
67	  List.append(&2, Nat, base_at(tt), file_at(ws, tt))
68	
69	# a leaf that is a plain name: its text
70	def name_tok(tok: Lex.Tok) -> Maybe<&2, String>:
71	  match tok:
72	    case Lex.Tok{Lex.TName{}, t, l, c}:
73	      Some{t}
74	    case other:
75	      None{}
76	
77	# the argument, when it is exactly one plain name
78	def name_of(nn: Tree.Node) -> Maybe<&2, String>:
79	  match nn:
80	    case Tree.NCons{Tree.Leaf{tok}, Tree.NNil{}}:
81	      name_tok(tok)
82	    case other:
83	      None{}
84	
85	# the name, when the list holds it
86	def keep_in(mm: Maybe<&2, String>, +names: List<&2, String>) -> Maybe<&2, String>:
87	  match mm:
88	    case None{}:
89	      None{}
90	    case Some{+nm}:
91	      Bool.pick(Maybe<&2, String>, List.contains(~String, ~String.eq, names, nm), Some{nm}, None{})
92	
93	# the first of two answers that has one
94	def first(aa: Maybe<&2, String>, bb: Maybe<&2, String>) -> Maybe<&2, String>:
95	  match aa:
96	    case None{}:
97	      bb
98	    case Some{nm}:
99	      Some{nm}
100	
101	# the first walked argument that is the lone name of one of the names
102	def found(ss: List<&2, Nat>, +as: List<&2, Tree.Node>, +names: List<&2, String>) -> Maybe<&2, String>:
103	  match ss:
104	    case Nil{}:
105	      None{}
106	    case Con{at, rest}:
107	      +more = found(rest, as, names)
108	      first(keep_in(name_of(Calls.arg(as, at)), names), more)
109	
110	# where a name sits among the parameter names
111	def index_of(ps: List<&2, String>, +nm: String, +ii: Nat) -> Maybe<&2, Nat>:
112	  match ps:
113	    case Nil{}:
114	      None{}
115	    case Con{+p, rest}:
116	      Lazy.stop(Maybe<&2, Nat>, String.eq(p, nm), Some{ii}, _u => index_of(rest, nm, 1n+ii))
117	
118	# where the name sits among the parameter names, when there is a name
119	def index_in(mm: Maybe<&2, String>, +ps: List<&2, String>) -> Maybe<&2, Nat>:
120	  match mm:
121	    case None{}:
122	      None{}
123	    case Some{+nm}:
124	      index_of(ps, nm, 0n)
125	
126	# the parameters that sit, as lone names, at walked arguments
127	def params_at(ss: List<&2, Nat>, +as: List<&2, Tree.Node>, +ps: List<&2, String>) -> List<&2, Nat>:
128	  match ss:
129	    case Nil{}:
130	      Nil{}
131	    case Con{at, rest}:
132	      +more = params_at(rest, as, ps)
133	      List.append(&2, Nat, opt(index_in(name_of(Calls.arg(as, at)), ps)), more)
134	
135	# a call's walked parameters, when its callee is a name and it is a call
136	def pass_hit(
137	  kk: Lex.TokKind,
138	  +open: Bool,
139	  +tt: String,
140	  kids: Tree.Node,
141	  +ps: List<&2, String>,
142	  +ws: List<&2, Walk>
143	) -> List<&2, Nat>:
144	  match kk:
145	    case Lex.TName{}:
146	      Lazy.stop(List<&2, Nat>, Bool.not(open), [], _u => params_at(slots(tt, ws), Calls.args(kids), ps))
147	    case Lex.TDotted{}:
148	      Lazy.stop(List<&2, Nat>, Bool.not(open), [], _u => params_at(slots(tt, ws), Calls.args(kids), ps))
149	    case other:
150	      Nil{}
151	
152	# the parameters a body passes, anywhere, as an argument some call walks
153	def passes(nn: Tree.Node, +ps: List<&2, String>, +ws: List<&2, Walk>) -> List<&2, Nat>:
154	  match nn:
155	    case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
156	      +own = pass_hit(k, String.eq(o, "("), t, kids, ps, ws)
157	      List.concat(&2, Nat, [own, passes(kids, ps, ws), passes(rest, ps, ws)])
158	    case Tree.NCons{Tree.Group{open, +kids, close}, rest}:
159	      List.concat(&2, Nat, [passes(kids, ps, ws), passes(rest, ps, ws)])
160	    case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
161	      List.concat(&2, Nat, [passes(kids, ps, ws), passes(body, ps, ws), passes(rest, ps, ws)])
162	    case Tree.NCons{h, rest}:
163	      passes(rest, ps, ws)
164	    case other:
165	      Nil{}
166	
167	# a live parameter that some self-call does not pass back unchanged
168	def moves(+pp: Tree.Node, +carried: List<&2, String>) -> Bool:
169	  Bool.and(Calls.is_live(pp), Bool.not(List.contains(~String, ~String.eq, carried, Calls.param_name(pp))))
170	
171	# a count or a text: a loop down one scans no list
172	def scalar(+pp: Tree.Node) -> Bool:
173	  +hh = Calls.type_head(pp, False{})
174	  Bool.or(String.eq(hh, "Nat"), String.eq(hh, "String"))
175	
176	# where the parameter a def shrinks sits, unless it is a count or a text
177	def place(+pp: Tree.Node, +ii: Nat) -> Maybe<&2, Nat>:
178	  Bool.pick(Maybe<&2, Nat>, scalar(pp), None{}, Some{ii})
179	
180	def own.go(ps: List<&2, Tree.Node>, +carried: List<&2, String>, +ii: Nat) -> Maybe<&2, Nat>:
181	  match ps:
182	    case Nil{}:
183	      None{}
184	    case Con{+p, rest}:
185	      +here = moves(p, carried)
186	      Lazy.stop(Maybe<&2, Nat>, here, place(p, ii), _u => own.go(rest, carried, 1n+ii))
187	
188	# where the parameter a def shrinks sits, when it calls itself and it is no count or text
189	def own(+sig: Tree.Node, +body: Tree.Node, +name: String) -> Maybe<&2, Nat>:
190	  Lazy.stop(Maybe<&2, Nat>, Bool.not(Calls.calls(body, name)), None{},
191	    _u => own.go(Calls.params(sig), Hoist.carried(sig, body, name), 0n))
192	
193	# one walk of the def for each argument
194	def tag(ns: List<&2, Nat>, +name: String, +ws: List<&2, Walk>) -> List<&2, Walk>:
195	  match ns:
196	    case Nil{}:
197	      ws
198	    case Con{at, rest}:
199	      Walk{name, at} <> tag(rest, name, ws)
200	
201	def walks.go(ds: List<&2, Calls.Def>, +ws: List<&2, Walk>) -> List<&2, Walk>:
202	  match ds:
203	    case Nil{}:
204	      ws
205	    case Con{Calls.Def{+name, +sig, +body}, rest}:
206	      +mine = List.append(&2, Nat, opt(own(sig, body, name)), passes(body, Calls.names(sig), ws))
207	      walks.go(rest, tag(mine, name, ws))
208	
209	# the defs of this file that walk, each with an argument it walks, in order
210	def walks(ds: List<&2, Calls.Def>) -> List<&2, Walk>:
211	  walks.go(ds, [])
212	
213	# the name of the parameter a def shrinks, "" for none
214	def lead.go(ps: List<&2, Tree.Node>, +carried: List<&2, String>) -> String:
215	  match ps:
216	    case Nil{}:
217	      ""
218	    case Con{+p, rest}:
219	      +here = moves(p, carried)
220	      Lazy.stop(String, here, Calls.param_name(p), _u => lead.go(rest, carried))
221	
222	# a finding on the callee, naming the carried list
223	def cite(
224	  mm: Maybe<&2, String>,
225	  +tt: String,
226	  +line: U32,
227	  +col: U32,
228	  +self: String,
229	  +lead: String,
230	  +path: String
231	) -> List<&2, F.Finding>:
232	  match mm:
233	    case None{}:
234	      Nil{}
235	    case Some{+pp}:
236	      [F.Finding{path, line, col, U32.from_nat(String.length(tt)), "scan",
237	        tt ++ " walks " ++ pp ++ " on every step of " ++ self ++ ", which carries it unchanged: that is O(|" ++ lead
238	          ++ "| * |" ++ pp ++ "|). Index it once outside the loop, or merge two sorted walks."}]
239	
240	# a hot call of a walk other than the def, a walked argument carried
241	def on_name(
242	  +hot: Bool,
243	  +open: Bool,
244	  +tt: String,
245	  +line: U32,
246	  +col: U32,
247	  kids: Tree.Node,
248	  +self: String,
249	  +ws: List<&2, Walk>,
250	  +carried: List<&2, String>,
251	  +lead: String,
252	  +path: String
253	) -> List<&2, F.Finding>:
254	  Lazy.stop(List<&2, F.Finding>, Bool.not(Bool.and(hot, Bool.and(open, Bool.not(String.eq(tt, self))))), [],
255	    _u => cite(found(slots(tt, ws), Calls.args(kids), carried), tt, line, col, self, lead, path))
256	
257	# a call's finding, when its callee is a name
258	def call_hit(
259	  kk: Lex.TokKind,
260	  +hot: Bool,
261	  +open: Bool,
262	  +tt: String,
263	  +line: U32,
264	  +col: U32,
265	  kids: Tree.Node,
266	  +self: String,
267	  +ws: List<&2, Walk>,
268	  +carried: List<&2, String>,
269	  +lead: String,
270	  +path: String
271	) -> List<&2, F.Finding>:
272	  match kk:
273	    case Lex.TName{}:
274	      on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path)
275	    case Lex.TDotted{}:
276	      on_name(hot, open, tt, line, col, kids, self, ws, carried, lead, path)
277	    case other:
278	      Nil{}
279	
280	# the walks of carried lists on a hot path
281	def walk(
282	  nn: Tree.Node,
283	  +self: String,
284	  +ws: List<&2, Walk>,
285	  +carried: List<&2, String>,
286	  +lead: String,
287	  +path: String,
288	  +hot: Bool
289	) -> List<&2, F.Finding>:
290	  match nn:
291	    case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
292	      +heat = Hoist.warm(hot, k)
293	      +own = call_hit(k, heat, String.eq(o, "("), t, l, c, kids, self, ws, carried, lead, path)
294	      +inn = walk(kids, self, ws, carried, lead, path, heat)
295	      +aft = walk(rest, self, ws, carried, lead, path, heat)
296	      List.concat(&2, F.Finding, [own, inn, aft])
297	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}:
298	      walk(rest, self, ws, carried, lead, path, Hoist.warm(hot, k))
299	    case Tree.NCons{Tree.Group{open, +kids, close}, rest}:
300	      List.concat(&2, F.Finding,
301	        [walk(kids, self, ws, carried, lead, path, hot), walk(rest, self, ws, carried, lead, path, hot)])
302	    case Tree.NCons{Tree.Stmt{Tree.SCase{}, kids, +body}, rest}:
303	      +arm = Bool.and(hot, Calls.calls(body, self))
304	      List.concat(&2, F.Finding, [walk(kids, self, ws, carried, lead, path, False{}),
305	        walk(body, self, ws, carried, lead, path, arm), walk(rest, self, ws, carried, lead, path, hot)])
306	    case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}:
307	      List.concat(&2, F.Finding, [walk(kids, self, ws, carried, lead, path, hot),
308	        walk(body, self, ws, carried, lead, path, hot), walk(rest, self, ws, carried, lead, path, hot)])
309	    case Tree.NCons{h, rest}:
310	      walk(rest, self, ws, carried, lead, path, hot)
311	    case other:
312	      Nil{}
313	
314	# one def's walk, its carried parameters and the one it shrinks read once
315	def run(+sig: Tree.Node, +body: Tree.Node, +name: String, +ws: List<&2, Walk>, +path: String) -> List<&2, F.Finding>:
316	  +carried = Hoist.carried(sig, body, name)
317	  walk(body, name, ws, carried, lead.go(Calls.params(sig), carried), path, True{})
318	
319	def check.go(
320	  ds: List<&2, Calls.Def>,
321	  +ws: List<&2, Walk>,
322	  +path: String,
323	  acc: List<&2, List<&2, F.Finding>>
324	) -> List<&2, F.Finding>:
325	  match ds:
326	    case Nil{}:
327	      List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc))
328	    case Con{Calls.Def{+name, +sig, +body}, rest}:
329	      check.go(rest, ws, path,
330	        Lazy.stop(List<&2, F.Finding>,
331	          Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), [],
332	          _u => run(sig, body, name, ws, path)) <> acc)
333	
334	# the findings over a file's defs, their walks read once
335	def check.on(+ds: List<&2, Calls.Def>, +path: String) -> List<&2, F.Finding>:
336	  check.go(ds, walks(ds), path, [])
337	
338	# the rule; a law file is skipped whole, before its walks are read
339	def check(ss: Src.Src) -> List<&2, F.Finding>:
340	  Src.Src{+path, text, toks, tree, bound, items} = ss
341	  Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => check.on(Calls.defs(tree), path))
342	
343	# the rule, told the file's role (src/role.bend): a law or proof file is
344	# skipped whole
345	def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>:
346	  Src.Src{path, text, toks, tree, bound, items} = ss
347	  Lazy.stop(List<&2, F.Finding>, Role.is_law_file(rr), [], _u => check.on(Calls.defs(tree), path))