language/decreasing_call.bend
bend-lint-rules@0.2.2.0 · 320 lines · 0 definitions
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.
10import Base
11import bend-lint-api@0.2.2.0/linter/lint.bend as Lint
12import bend-lint-api@0.2.2.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.
18type 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.
22type 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.
27type 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.
35type Loop is Data:
36 Loop{params: List<&2, Param>, lets: List<&2, U32>, text: String}
37
38# Functions
39# =========
40def 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
47def 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.
65def 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
72def 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
79def 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.
88def 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.
114def 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.
132def 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
143def 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.
154def 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`.
166def 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
201def ordinal(n: Nat) -> String:
202 U32.show(U32.from_nat(1n+n))
203
204def 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
219def 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`.
235def 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`).
260def 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
272def 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`.
276def 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.
287def 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
316def run(+here: Lint.Here) -> Lint.Ask(List<&2, Lint.Finding>):
317 Lint.done(defs(Lint.Here.nodes(here), Lint.Here.text(here), []))
318
319def rule() -> Lint.Rule:
320 Lint.Rule{Lint.Needs{False{}, False{}}, [], Lint.OnFile{run}}