1	# language/decreasing_call: a call of a definition to itself that Bend cannot prove smaller, so the check
2	# fails ("a decreasing self-call").
3	# Heuristics: as Bend's checker does, it reads the arguments left to right against the parameters:
4	# each must be passed unchanged until one is smaller, a field that a `match` on that parameter took
5	# apart (`p` of `case 1n+p:`). Erased parameters do not count. An argument that is a call, or another
6	# variable, is not smaller. One that is a literal or a constructor is left to the checker: the rule
7	# does not report it. Bend's checker stops at its first error; this rule reports every such call at
8	# once. An @unsafe definition (`def f?`) may call itself freely, and a call in a type (a pair type
9	# `A & B`, a type's arguments, an equality) is not checked.
10	import Base
11	import bend-lint-api@0.2.1.0/linter/lint.bend as Lint
12	import bend-lint-api@0.2.1.0/shared/lists.bend as Lists
13	
14	# Types
15	# =====
16	
17	# A parameter: its binder, whether it is erased (it does not count), and its name.
18	type Param is Data:
19	  Param{binder: U32, erased: Bool, name: String}
20	
21	# A binder known smaller than the parameter or field `root`: a field a match took apart from it.
22	type Smaller is Data:
23	  Smaller{root: U32, field: U32}
24	
25	# What the arguments of a call say: it decreases; it does not, at the argument numbered `at` (from 0)
26	# for the parameter `param`, or with every argument unchanged; or the rule cannot tell.
27	type Verdict is Data:
28	  Decreases{}
29	  Fails{at: Nat, param: String}
30	  Unchanged{}
31	  Unknown{}
32	
33	# What judging a definition's calls of itself reads: its parameters, the binders its lets bind (an argument that is one
34	# stands for its value, which the rule does not follow), and the file's text.
35	type Loop is Data:
36	  Loop{params: List<&2, Param>, lets: List<&2, U32>, text: String}
37	
38	# Functions
39	# =========
40	def Param.is_erased(bare: Bool, quantity: Lint.Quantity) -> Bool:
41	  match bare quantity:
42	    case False{} Lint.Erased{}:
43	      True{}
44	    case _ _:
45	      False{}
46	
47	def Param.all(nodes: List<&2, Lint.Node>, out: List<&2, Param>) -> List<&2, Param>:
48	  match nodes:
49	    case Nil{}:
50	      List.reverse(&2, Param, out)
51	    case Con{Lint.Node{Lint.Parameter{+b, +q}, +n, s, k, f}, rest}:
52	      Param.all(
53	        rest,
54	        Param{
55	          b,
56	          Param.is_erased(Lint.Node.is_bare(Lint.Node{Lint.Parameter{b, q}, n, s, k, f}), q),
57	          n
58	        }
59	          <> out
60	      )
61	    case Con{node, rest}:
62	      Param.all(rest, out)
63	
64	# The roots that `binder` is smaller than, with `binder` itself.
65	def roots(smaller: List<&2, Smaller>, +binder: U32, out: List<&2, U32>) -> List<&2, U32>:
66	  match smaller:
67	    case Nil{}:
68	      binder <> out
69	    case Con{Smaller{r, f}, rest}:
70	      roots(rest, binder, Lists.push(U32, Lists.when(U32, U32.is_eq(f, binder), r), out))
71	
72	def pairs.of(+r: U32, fs: List<&2, U32>, out: List<&2, Smaller>) -> List<&2, Smaller>:
73	  match fs:
74	    case Nil{}:
75	      out
76	    case Con{f, rest}:
77	      pairs.of(r, rest, Smaller{r, f} <> out)
78	
79	def pairs(rs: List<&2, U32>, +fs: List<&2, U32>, out: List<&2, Smaller>) -> List<&2, Smaller>:
80	  match rs:
81	    case Nil{}:
82	      out
83	    case Con{r, rest}:
84	      pairs(rest, fs, pairs.of(r, fs, out))
85	
86	# What a case's patterns take apart: each pattern, a constructor, makes its variables smaller than its
87	# scrutinee, and than all that scrutinee is smaller than.
88	def taken(
89	  scrutinees: List<&2, Lint.Node>,
90	  patterns: List<&2, Lint.Node>,
91	  +smaller: List<&2, Smaller>
92	) -> List<&2, Smaller>:
93	  match scrutinees patterns:
94	    case Con{
95	      Lint.Node{Lint.Variable{s}, n, sp, k, f},
96	      more
97	    } Con{Lint.Node{Lint.PatternConstructor{t}, pn, ps, kids, pf}, rest}:
98	      taken(
99	        more,
100	        rest,
101	        Lists.onto(
102	          &2,
103	          Smaller,
104	          pairs(roots(smaller, s, []), Lint.Node.bound(kids, []), []),
105	          smaller
106	        )
107	      )
108	    case Con{x, more} Con{y, rest}:
109	      taken(more, rest, smaller)
110	    case _ _:
111	      smaller
112	
113	# What a case below `parent` takes apart, if `node` is one and `parent` its match.
114	def known.at(
115	  parent: Maybe<&2, Lint.Node>,
116	  node: Lint.Node,
117	  smaller: List<&2, Smaller>
118	) -> List<&2, Smaller>:
119	  match parent node:
120	    case Some{
121	      Lint.Node{Lint.Match{}, mn, ms, scrutinees, mf}
122	    } Lint.Node{Lint.Case{}, n, s, patterns, f}:
123	      taken(
124	        Lint.Node.scrutinees(Lint.Node{Lint.Match{}, mn, ms, scrutinees, mf}),
125	        patterns,
126	        smaller
127	      )
128	    case _ _:
129	      smaller
130	
131	# What the cases above a call (`chain`, outermost first; `parent` is the node above the first) take apart.
132	def known(
133	  chain: List<&2, Lint.Above>,
134	  parent: Maybe<&2, Lint.Node>,
135	  smaller: List<&2, Smaller>
136	) -> List<&2, Smaller>:
137	  match chain:
138	    case Nil{}:
139	      smaller
140	    case Con{Lint.Above{+node, at}, rest}:
141	      known(rest, Some{node}, known.at(parent, node, smaller))
142	
143	def is_smaller(smaller: List<&2, Smaller>, hit: Bool, +root: U32, +field: U32) -> Bool:
144	  match smaller hit:
145	    case _ True{}:
146	      True{}
147	    case Nil{} False{}:
148	      False{}
149	    case Con{Smaller{r, f}, rest} False{}:
150	      is_smaller(rest, U32.is_eq(r, root) && U32.is_eq(f, field), root, field)
151	
152	# What one argument, a variable, says: none to read on (it is the parameter, unchanged), else the
153	# verdict: it decreases (a field a match took apart), the rule cannot tell (a let's name), or it fails.
154	def step(same: Bool, smaller: Bool, local: Bool, at: Nat, param: String) -> Maybe<&2, Verdict>:
155	  match same smaller local:
156	    case True{} _ _:
157	      None{}
158	    case False{} True{} _:
159	      Some{Decreases{}}
160	    case False{} False{} True{}:
161	      Some{Unknown{}}
162	    case False{} False{} False{}:
163	      Some{Fails{at, param}}
164	
165	# The verdict on a call's arguments against the parameters, from the one numbered `at`.
166	def verdict(
167	  params: List<&2, Param>,
168	  args: List<&2, Lint.Node>,
169	  told: Maybe<&2, Verdict>,
170	  +smaller: List<&2, Smaller>,
171	  +lets: List<&2, U32>,
172	  +at: Nat
173	) -> Verdict:
174	  match params args told:
175	    case _ _ Some{v}:
176	      v
177	    case Con{Param{b, True{}, n}, ps} Con{arg, rest} None{}:
178	      verdict(ps, rest, None{}, smaller, lets, 1n+at)
179	    case Con{Param{+b, False{}, +n}, ps} Con{Lint.Node{Lint.Variable{+a}, x, s, k, f}, rest} None{}:
180	      verdict(
181	        ps,
182	        rest,
183	        step(
184	          U32.is_eq(a, b),
185	          is_smaller(smaller, False{}, b, a),
186	          List.contains(~U32, ~U32.is_eq, lets, a),
187	          at,
188	          n
189	        ),
190	        smaller,
191	        lets,
192	        1n+at
193	      )
194	    case Con{Param{b, False{}, n}, ps} Con{Lint.Node{Lint.Application{}, x, s, k, f}, rest} None{}:
195	      Fails{at, n}
196	    case Nil{} Nil{} None{}:
197	      Unchanged{}
198	    case _ _ None{}:
199	      Unknown{}
200	
201	def ordinal(n: Nat) -> String:
202	  U32.show(U32.from_nat(1n+n))
203	
204	def message(verdict: Verdict, loop: String, source: String, args: List<&2, Lint.Node>) -> String:
205	  match verdict:
206	    case Fails{+at, param}:
207	      loop
208	        ++ " calls itself here, but argument "
209	        ++ ordinal(at)
210	        ++ " (`"
211	        ++ Lint.Span.text(source, Lint.Node.span(List.get(&2, Lint.Node, args, at)))
212	        ++ "`) is neither the parameter "
213	        ++ param
214	        ++ " unchanged nor a part of it that a match took apart, and the arguments before it are unchanged. Bend reads the arguments left to right, so it cannot prove the loop ends, and the check fails (\"a decreasing self-call\"). Put the parameter that shrinks first, pass the ones before it unchanged, and pass a part of it that a match took apart (`p` of `case 1n+p:`)."
215	    case _:
216	      loop
217	        ++ " calls itself here with every argument unchanged, so the loop would never end, and the check fails (\"a decreasing self-call\"). Pass a part of the parameter that shrinks, one that a match took apart (`p` of `case 1n+p:`)."
218	
219	def finding(
220	  verdict: Verdict,
221	  span: Maybe<&2, Lint.Span>,
222	  loop: String,
223	  source: String,
224	  args: List<&2, Lint.Node>
225	) -> List<&2, Lint.Finding>:
226	  match verdict span:
227	    case Fails{at, param} Some{s}:
228	      [Lint.Finding{Lint.Warning{}, s, message(Fails{at, param}, loop, source, args), []}]
229	    case Unchanged{} Some{s}:
230	      [Lint.Finding{Lint.Warning{}, s, message(Unchanged{}, loop, source, args), []}]
231	    case _ _:
232	      []
233	
234	# The findings about a call of its definition to itself, below `path`.
235	def call(+loop: Loop, path: List<&2, Lint.Above>, node: Lint.Node) -> List<&2, Lint.Finding>:
236	  match loop node:
237	    case Loop{
238	      params,
239	      lets,
240	      text
241	    } Lint.Node{syntax, name, span, Con{Lint.Node{hs, callee, hp, hk, hf}, +args}, facts}:
242	      finding(
243	        verdict(
244	          params,
245	          args,
246	          None{},
247	          known(List.reverse(&2, Lint.Above, path), None{}, []),
248	          lets,
249	          0n
250	        ),
251	        span,
252	        callee,
253	        text,
254	        args
255	      )
256	    case _ _:
257	      []
258	
259	# The same, if `node` is a live call of its definition to itself (`recursive`).
260	def calls(
261	  recursive: Bool,
262	  loop: Loop,
263	  path: List<&2, Lint.Above>,
264	  node: Lint.Node
265	) -> List<&2, Lint.Finding>:
266	  match recursive:
267	    case True{}:
268	      call(loop, path, node)
269	    case False{}:
270	      []
271	
272	def visit(+loop: Loop, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, Lint.Finding>:
273	  calls(Lint.is_recursive(path, node) && Lint.is_live(path), loop, path, node)
274	
275	# The binders the lets of a definition bind, below `path`.
276	def let(+u: Unit, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, U32>:
277	  match path node:
278	    case Con{
279	      Lint.Above{Lint.Node{Lint.Destructure{q}, n, s, k, f}, at},
280	      up
281	    } Lint.Node{Lint.PatternVariable{b, pq}, pn, ps, pk, pf}:
282	      [b]
283	    case _ _:
284	      []
285	
286	# The findings in each definition among `nodes`, onto `out`. An @unsafe definition (`def f?`) may call itself freely.
287	def defs(
288	  nodes: List<&2, Lint.Node>,
289	  +text: String,
290	  out: List<&2, Lint.Finding>
291	) -> List<&2, Lint.Finding>:
292	  match nodes:
293	    case Nil{}:
294	      List.reverse(&2, Lint.Finding, out)
295	    case Con{Lint.Node{Lint.Definition{t, False{}}, n, s, +k, f}, rest}:
296	      +owner = {Lint.Node{Lint.Definition{t, False{}}, n, s, k, f}: Lint.Node}
297	      defs(
298	        rest,
299	        text,
300	        Lists.onto(
301	          &2,
302	          Lint.Finding,
303	          Lint.visit(
304	            ~Loop,
305	            ~Lint.Finding,
306	            ~visit,
307	            Loop{Param.all(k, []), Lint.visit(~Unit, ~U32, ~let, Unit{}, [owner]), text},
308	            [owner]
309	          ),
310	          out
311	        )
312	      )
313	    case Con{node, rest}:
314	      defs(rest, text, out)
315	
316	def run(+here: Lint.Here) -> Lint.Ask(List<&2, Lint.Finding>):
317	  Lint.done(defs(Lint.Here.nodes(here), Lint.Here.text(here), []))
318	
319	def rule() -> Lint.Rule:
320	  Lint.Rule{Lint.Needs{False{}, False{}}, [], Lint.OnFile{run}}