1	# rule ring: a self-call replaces a binder with `List.append` of `List.drop`
2	# (or `String.append` / `++`, or `tail`) by a constant count, passing it back
3	# in the binder's own parameter position. Each step copies that fixed window.
4	# Keep it in an Array and advance an index. A list the def matches and walks
5	# (as any scrutinee of a match) is variable-length input, a window dropped
6	# into another parameter's slot is not carried, and a one-shot trim is not a
7	# loop: all stay quiet. Growing an accumulator by append, with no drop of
8	# that same value, is `concat`. Laws and proofs do not run (a def with no
9	# type at all fills a law: it is a proof).
10	import Base
11	import ../../src.bend as Src
12	import ../../finding.bend as F
13	import ../../syntax/lex.bend as Lex
14	import ../../syntax/tree.bend as Tree
15	import ../calls.bend as Calls
16	import ../../lazy/lazy.bend as Lazy
17	
18	# the first of two maybes
19	def or_tok(aa: Maybe<&2, Lex.Tok>, +bb: Maybe<&2, Lex.Tok>) -> Maybe<&2, Lex.Tok>:
20	  match aa:
21	    case Some{+t}:
22	      Some{t}
23	    case None{}:
24	      bb
25	
26	# is the chain exactly one number?
27	def is_num(nn: Tree.Node) -> Bool:
28	  match nn:
29	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, t, l, c}}, Tree.NNil{}}:
30	      True{}
31	    case other:
32	      False{}
33	
34	# the chain is exactly one lowercase name; its text, or empty
35	def name_text(nn: Tree.Node) -> String:
36	  match nn:
37	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, +t, l, c}}, Tree.NNil{}}:
38	      t
39	    case other:
40	      ""
41	
42	# this argument is a window binder
43	def win_name(nn: Tree.Node, +wins: List<&2, String>) -> Bool:
44	  +tt = name_text(nn)
45	  Bool.and(Bool.not(String.is_empty(tt)), List.contains(~String, ~String.eq, wins, tt))
46	
47	# does any argument name the window?
48	def has_name(as: List<&2, Tree.Node>, +wins: List<&2, String>) -> Bool:
49	  match as:
50	    case Nil{}:
51	      False{}
52	    case Con{h, rest}:
53	      +more = has_name(rest, wins)
54	      Bool.or(win_name(h, wins), more)
55	
56	# is the last argument a number?
57	def last_num(as: List<&2, Tree.Node>) -> Bool:
58	  match as:
59	    case Nil{}:
60	      False{}
61	    case Con{h, Nil{}}:
62	      is_num(h)
63	    case Con{h, rest}:
64	      last_num(rest)
65	
66	# a fixed drop or tail of a named window
67	def drop_ok(+tt: String, +as: List<&2, Tree.Node>, +wins: List<&2, String>) -> Bool:
68	  +kind = List.contains(~String, ~String.eq, ["List.drop", "String.drop", "List.tail", "String.tail"], tt)
69	  +tail = Bool.or(String.eq(tt, "List.tail"), String.eq(tt, "String.tail"))
70	  Bool.and(kind, Bool.and(has_name(as, wins), Bool.or(tail, last_num(as))))
71	
72	# the callee token when this call is a fixed drop
73	def drop_tok(
74	  kk: Lex.TokKind,
75	  +tt: String,
76	  +line: U32,
77	  +col: U32,
78	  kids: Tree.Node,
79	  +wins: List<&2, String>
80	) -> Maybe<&2, Lex.Tok>:
81	  Bool.pick(Maybe<&2, Lex.Tok>, drop_ok(tt, Calls.args(kids), wins), Some{Lex.Tok{kk, tt, line, col}}, None{})
82	
83	# the drop this call is, when the group is an application
84	def here_of(
85	  +open: Bool,
86	  kk: Lex.TokKind,
87	  +tt: String,
88	  +line: U32,
89	  +col: U32,
90	  kids: Tree.Node,
91	  +wins: List<&2, String>
92	) -> Maybe<&2, Lex.Tok>:
93	  match open:
94	    case False{}:
95	      None{}
96	    case True{}:
97	      drop_tok(kk, tt, line, col, kids, wins)
98	
99	# a drop anywhere under the node
100	def drop_in(nn: Tree.Node, +wins: List<&2, String>) -> Maybe<&2, Lex.Tok>:
101	  match nn:
102	    case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
103	      +here = here_of(String.eq(o, "("), k, t, l, c, kids, wins)
104	      +inn = drop_in(kids, wins)
105	      +aft = drop_in(rest, wins)
106	      or_tok(here, or_tok(inn, aft))
107	    case Tree.NCons{Tree.Group{open, +kids, close}, rest}:
108	      or_tok(drop_in(kids, wins), drop_in(rest, wins))
109	    case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
110	      or_tok(drop_in(kids, wins), or_tok(drop_in(body, wins), drop_in(rest, wins)))
111	    case Tree.NCons{h, rest}:
112	      drop_in(rest, wins)
113	    case other:
114	      None{}
115	
116	# which list an append extends
117	def receiver_is(+list: Bool, +str: Bool, +as: List<&2, Tree.Node>, +wins: List<&2, String>) -> Maybe<&2, Lex.Tok>:
118	  match list str:
119	    case True{} b:
120	      drop_in(Calls.arg(as, 2n), wins)
121	    case False{} True{}:
122	      drop_in(Calls.arg(as, 0n), wins)
123	    case False{} False{}:
124	      None{}
125	
126	# the drop an append copies onto, when this call is List.append or String.append
127	def receiver(+tt: String, kids: Tree.Node, +wins: List<&2, String>) -> Maybe<&2, Lex.Tok>:
128	  receiver_is(String.eq(tt, "List.append"), String.eq(tt, "String.append"), Calls.args(kids), wins)
129	
130	# a `++` whose left already dropped: that drop; otherwise nothing
131	def pp_found(+is_pp: Bool, seen: Maybe<&2, Lex.Tok>) -> Maybe<&2, Lex.Tok>:
132	  match is_pp seen:
133	    case True{} Some{+t}:
134	      Some{t}
135	    case True{} None{}:
136	      None{}
137	    case False{} s:
138	      None{}
139	
140	# the drop still in play after this operator (`++` starts a new left side)
141	def pp_seen(+is_pp: Bool, +seen: Maybe<&2, Lex.Tok>) -> Maybe<&2, Lex.Tok>:
142	  match is_pp:
143	    case True{}:
144	      None{}
145	    case False{}:
146	      seen
147	
148	# an application's append-receiver drop; a bracket is not an application
149	def call_recv(+open: Bool, +tt: String, kids: Tree.Node, +wins: List<&2, String>) -> Maybe<&2, Lex.Tok>:
150	  match open:
151	    case False{}:
152	      None{}
153	    case True{}:
154	      receiver(tt, kids, wins)
155	
156	# a drop this node itself is: the call when it is an application, else under a bracket
157	def call_drop(
158	  +open: Bool,
159	  +kk: Lex.TokKind,
160	  +tt: String,
161	  +line: U32,
162	  +col: U32,
163	  +kids: Tree.Node,
164	  +wins: List<&2, String>
165	) -> Maybe<&2, Lex.Tok>:
166	  match open:
167	    case False{}:
168	      drop_in(kids, wins)
169	    case True{}:
170	      drop_tok(kk, tt, line, col, kids, wins)
171	
172	# a drop then `++`, or an append onto a drop, in this chain
173	def plus_scan(nn: Tree.Node, +seen: Maybe<&2, Lex.Tok>, +wins: List<&2, String>) -> Maybe<&2, Lex.Tok>:
174	  match nn:
175	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TOp{}, +op, l, c}}, rest}:
176	      +is_pp = String.eq(op, "++")
177	      or_tok(pp_found(is_pp, seen), plus_scan(rest, pp_seen(is_pp, seen), wins))
178	    case Tree.NCons{Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
179	      +open = String.eq(o, "(")
180	      +recv = call_recv(open, t, kids, wins)
181	      +inn = plus_scan(kids, None{}, wins)
182	      +drop = call_drop(open, k, t, l, c, kids, wins)
183	      +aft = plus_scan(rest, or_tok(seen, drop), wins)
184	      or_tok(recv, or_tok(inn, aft))
185	    case Tree.NCons{Tree.Group{open, +kids, close}, rest}:
186	      +inn = plus_scan(kids, None{}, wins)
187	      +aft = plus_scan(rest, or_tok(seen, drop_in(kids, wins)), wins)
188	      or_tok(inn, aft)
189	    case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
190	      or_tok(plus_scan(kids, None{}, wins), or_tok(plus_scan(body, None{}, wins), plus_scan(rest, seen, wins)))
191	    case Tree.NCons{h, rest}:
192	      plus_scan(rest, seen, wins)
193	    case other:
194	      None{}
195	
196	# a finding at the drop the scan found
197	def slide_at(mm: Maybe<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>:
198	  match mm:
199	    case None{}:
200	      Nil{}
201	    case Some{Lex.Tok{k, +t, l, c}}:
202	      [F.Finding{path, l, c, U32.from_nat(String.length(t)), "ring",
203	        "Each step drops from and appends to a fixed-size window, which copies it; keep the window in an Array and advance an index."}]
204	
205	# a finding at the drop, when the argument slides a window
206	def slide(aa: Tree.Node, +path: String, +wins: List<&2, String>) -> List<&2, F.Finding>:
207	  slide_at(plus_scan(aa, None{}, wins), path)
208	
209	# the windows an argument in this parameter's slot may slide: the parameter
210	# itself when it is a window, else none
211	def slot_wins(+slot: String, +wins: List<&2, String>) -> List<&2, String>:
212	  Bool.pick(List<&2, String>, List.contains(~String, ~String.eq, wins, slot), [slot], [])
213	
214	# every self-call argument that slides the window of its own slot (params,
215	# from the argument's position on)
216	def slides(
217	  as: List<&2, Tree.Node>,
218	  +params: List<&2, String>,
219	  +path: String,
220	  +wins: List<&2, String>
221	) -> List<&2, F.Finding>:
222	  match as:
223	    case Nil{}:
224	      Nil{}
225	    case Con{h, rest}:
226	      +slot = Maybe.default(&2, String, List.head(&2, String, params), "")
227	      List.append(&2, F.Finding, slide(h, path, slot_wins(slot, wins)),
228	        slides(rest, List.tail(&2, String, params), path, wins))
229	
230	# every self-call's sliding arguments
231	def walk(
232	  nn: Tree.Node,
233	  +self: String,
234	  +params: List<&2, String>,
235	  +path: String,
236	  +wins: List<&2, String>
237	) -> List<&2, F.Finding>:
238	  match nn:
239	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}}:
240	      +me = Bool.and(String.eq(o, "("), String.eq(t, self))
241	      +own = Lazy.stop(List<&2, F.Finding>, Bool.not(me), [], _u => slides(Calls.args(kids), params, path, wins))
242	      List.concat(&2, F.Finding, [own, walk(kids, self, params, path, wins), walk(rest, self, params, path, wins)])
243	    case Tree.NCons{Tree.Group{open, +kids, close}, rest}:
244	      List.concat(&2, F.Finding, [walk(kids, self, params, path, wins), walk(rest, self, params, path, wins)])
245	    case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
246	      List.concat(&2, F.Finding, [walk(kids, self, params, path, wins), walk(body, self, params, path, wins),
247	        walk(rest, self, params, path, wins)])
248	    case Tree.NCons{h, rest}:
249	      walk(rest, self, params, path, wins)
250	    case other:
251	      Nil{}
252	
253	# the top-level names of a chain, onto acc
254	def names_in(nn: Tree.Node, acc: List<&2, String>) -> List<&2, String>:
255	  match nn:
256	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, t, l, c}}, rest}:
257	      t <> names_in(rest, acc)
258	    case Tree.NCons{h, rest}:
259	      names_in(rest, acc)
260	    case other:
261	      acc
262	
263	# every scrutinee of `match a b ..:`, onto acc (acc alone for any other chain)
264	def match_names(kids: Tree.Node, +acc: List<&2, String>) -> List<&2, String>:
265	  match kids:
266	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TKey{}, +kw, l, c}}, +rest}:
267	      Lazy.stop(List<&2, String>, Bool.not(String.eq(kw, "match")), acc, _u => names_in(rest, acc))
268	    case other:
269	      acc
270	
271	# names the def matches, as any scrutinee: variable-length input, not a window
272	def matched(nn: Tree.Node, +acc: List<&2, String>) -> List<&2, String>:
273	  match nn:
274	    case Tree.NCons{Tree.Stmt{Tree.STerm{}, +kids, body}, rest}:
275	      +here = match_names(kids, acc)
276	      matched(rest, matched(body, matched(kids, here)))
277	    case Tree.NCons{Tree.Stmt{kind, +kids, body}, rest}:
278	      matched(rest, matched(body, matched(kids, acc)))
279	    case Tree.NCons{Tree.Group{open, +kids, close}, rest}:
280	      matched(rest, matched(kids, acc))
281	    case Tree.NCons{h, rest}:
282	      matched(rest, acc)
283	    case other:
284	      acc
285	
286	# parameters that are not matched as input
287	def windows.go(ps: List<&2, String>, +bad: List<&2, String>, +acc: List<&2, String>) -> List<&2, String>:
288	  match ps:
289	    case Nil{}:
290	      List.reverse(&2, String, acc)
291	    case Con{+p, rest}:
292	      +keep = Bool.and(Bool.not(String.is_empty(p)), Bool.not(List.contains(~String, ~String.eq, bad, p)))
293	      windows.go(rest, bad, Bool.pick(List<&2, String>, keep, p <> acc, acc))
294	
295	# parameters that are not matched as input
296	def windows(sig: Tree.Node, body: Tree.Node) -> List<&2, String>:
297	  windows.go(Calls.names(sig), matched(body, []), [])
298	
299	def check.go(ds: List<&2, Calls.Def>, +path: String, acc: List<&2, List<&2, F.Finding>>) -> List<&2, F.Finding>:
300	  match ds:
301	    case Nil{}:
302	      List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc))
303	    case Con{Calls.Def{+name, +sig, +body}, rest}:
304	      check.go(rest, path,
305	        Lazy.stop(List<&2, F.Finding>,
306	          Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), [],
307	          _u => walk(body, name, Calls.names(sig), path, windows(sig, body))) <> acc)
308	
309	# the rule
310	def check(ss: Src.Src) -> List<&2, F.Finding>:
311	  Src.Src{path, text, toks, tree, bound, items} = ss
312	  check.go(Calls.defs(tree), path, [])