language/decreasing_call.bend

bend-lint-rules@0.2.0.0 · 320 lines · 25 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.0.0/linter/lint.bend as Lint
12import bend-lint-api@0.2.0.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}}