language/reused_binder.bend
bend-lint-rules@0.1.1.0 · 215 lines · 0 definitions
1# language/reused_binder: a binder written without `+` that live code uses twice on one path, so the
2# check fails ("consumed more than once").
3# Heuristics: it checks only the binders whose quantity the syntax gives for sure: a parameter or a
4# let's name written without `+`, which can be used once on each path. It leaves out a pattern's
5# field, whose quantity also comes from its scrutinee's type, and a law's bare parameter. Two uses are
6# on one path unless they are in different cases of one `match`. Both values of a call count, so
7# `Bool.pick(T, c, x, x)` uses x twice. Uses in types are dead and do not count. A binder that a
8# `match` takes apart is skipped: in a case, it stands for the matched constructor. Bend's checker
9# stops at its first error; this rule reports every such binder at once.
10import Base
11import bend-lint-api@0.1.1.0/linter/lint.bend as Lint
12import bend-lint-api@0.1.1.0/shared/lists.bend as Lists
13
14# Types
15# =====
16
17# A binder that can be used once: its number, and its name.
18type Once is Data:
19 Once{binder: U32, name: String}
20
21# The live uses of one binder among some nodes: the first, and the first that an earlier one on its path precedes, if
22# any. Two uses are on one path unless a match parts them: its cases, and its scrutinees, are each a path of their own.
23type Seen is Data:
24 Seen{first: Maybe<&2, Lint.Span>, second: Maybe<&2, Lint.Span>}
25
26# Functions
27# =========
28def message(+name: String) -> String:
29 name
30 ++ " is used again here, on the same path as an earlier use, but it is declared without `+`, so it can be used once on each path, and the check fails (\"consumed more than once\"). If its type is Data, write `+"
31 ++ name
32 ++ "` where it is declared (it then carries a reference count at run time); else use it once: a function, an array or an IO handle can never be copied. This is a false positive if one of the uses is an argument for an erased parameter (`-x`, as a proof's motive often is): that is dead code."
33
34# The binders a definition declares that can be used once, as their syntax says for sure: a parameter written without
35# `+` (unless one is `bare`: its quantity is its law's), and a let's name written without `+`. A pattern's field is left
36# out: its quantity also comes from its scrutinee's type (a field of a `List<&2, A>` is reusable), which the rule cannot
37# see.
38def Once.of(+bare: Bool, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, Once>:
39 match path node:
40 case _ Lint.Node{Lint.Parameter{b, Lint.Once{}}, name, s, k, f}:
41 Bool.pick(List<&2, Once>, bare, [], [Once{b, name}])
42 case Con{
43 Lint.Above{Lint.Node{Lint.Destructure{q}, pn, ps, pk, pf}, at},
44 up
45 } Lint.Node{Lint.PatternVariable{b, Lint.Once{}}, name, s, k, f}:
46 [Once{b, name}]
47 case _ _:
48 []
49
50# The binders a match takes apart: the variables right under it, its scrutinees. In a case, they stand for the matched
51# constructor.
52def scrutinee(+u: Unit, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, U32>:
53 match path node:
54 case Con{
55 Lint.Above{Lint.Node{Lint.Match{}, mn, ms, mk, mf}, at},
56 up
57 } Lint.Node{Lint.Variable{b}, n, s, k, f}:
58 [b]
59 case _ _:
60 []
61
62# Whether the nodes under `node`, which is live if `live`, are: a body is; a type is not (an equality, a function or
63# pair type, a type's arguments). An annotation's type is not either: see `scan`.
64def is_live_inside(+node: Lint.Node, live: Bool) -> Bool:
65 match node:
66 case Lint.Node{Lint.Body{}, n, s, k, f}:
67 True{}
68 case Lint.Node{Lint.Equality{}, n, s, k, f}:
69 False{}
70 case Lint.Node{Lint.Forall{b, q}, n, s, k, f}:
71 False{}
72 case Lint.Node{Lint.TypeApplication{t}, n, s, k, f}:
73 False{}
74 case Lint.Node{Lint.Application{}, n, s, kids, f}:
75 live && Bool.not(Lint.is_pair(kids))
76 case _:
77 live
78
79def is_match(syntax: Lint.Syntax) -> Bool:
80 match syntax:
81 case Lint.Match{}:
82 True{}
83 case _:
84 False{}
85
86def is_annotation(syntax: Lint.Syntax) -> Bool:
87 match syntax:
88 case Lint.Annotation{}:
89 True{}
90 case _:
91 False{}
92
93# What a node's uses of `b` are: its own, if it is a live use, else `under`'s, those under it.
94def Seen.of(+node: Lint.Node, b: U32, live: Bool, under: Seen) -> Seen:
95 match node live:
96 case Lint.Node{Lint.Variable{v}, n, Some{span}, k, f} True{}:
97 Bool.pick(Seen, U32.is_eq(v, b), Seen{Some{span}, None{}}, under)
98 case _ _:
99 under
100
101# The uses of `seen`, then those of `next`, the nodes after them: on one path, or, if `apart`, on paths of their own.
102def Seen.then(apart: Bool, seen: Seen, next: Seen) -> Seen:
103 match apart seen next:
104 case True{} Seen{f, s} Seen{g, t}:
105 Seen{Maybe.or(&2, Lint.Span, f, g), Maybe.or(&2, Lint.Span, s, t)}
106 case False{} Seen{Some{f}, s} Seen{g, t}:
107 Seen{Some{f}, Maybe.or(&2, Lint.Span, s, g)}
108 case False{} Seen{None{}, s} Seen{g, t}:
109 Seen{g, Maybe.or(&2, Lint.Span, s, t)}
110
111# The live uses of `b` among `nodes`, the nodes under one, after `seen`: `live` says whether they are live, `apart`
112# whether each is a path of its own (a match's), and `typed` whether only the first is live (an annotation's: the
113# second is a type); `at` counts the nodes.
114def scan(
115 nodes: List<&2, Lint.Node>,
116 +b: U32,
117 +live: Bool,
118 +apart: Bool,
119 +typed: Bool,
120 +at: U32,
121 seen: Seen
122) -> Seen:
123 match nodes:
124 case Nil{}:
125 seen
126 case Con{Lint.Node{+syntax, name, span, +kids, facts}, rest}:
127 +node = {Lint.Node{syntax, name, span, kids, facts}: Lint.Node}
128 +here = live && Bool.not(typed && U32.is_gt(at, 0))
129 scan(
130 rest,
131 b,
132 live,
133 apart,
134 typed,
135 (at + 1: U32),
136 Seen.then(
137 apart,
138 seen,
139 Seen.of(
140 node,
141 b,
142 here,
143 scan(
144 kids,
145 b,
146 is_live_inside(node, here),
147 is_match(syntax),
148 is_annotation(syntax),
149 0,
150 Seen{None{}, None{}}
151 )
152 )
153 )
154 )
155
156def finding(second: Seen, name: String) -> List<&2, Lint.Finding>:
157 match second:
158 case Seen{f, s}:
159 Lint.finding(Lint.Warning{}, True{}, s, message(name))
160
161# The finding about a binder of `owner` used twice on one path, unless a match takes it apart (`matched`).
162def judged(matched: Bool, owner: Lint.Node, b: U32, name: String) -> List<&2, Lint.Finding>:
163 match matched:
164 case True{}:
165 []
166 case False{}:
167 finding(scan([owner], b, False{}, False{}, False{}, 0, Seen{None{}, None{}}), name)
168
169# The finding about each of `onces`, binders of `owner`, used twice on one path, onto `out`; a binder a match takes
170# apart (`matched`) is skipped.
171def judge(
172 +owner: Lint.Node,
173 onces: List<&2, Once>,
174 +matched: List<&2, U32>,
175 out: List<&2, Lint.Finding>
176) -> List<&2, Lint.Finding>:
177 match onces:
178 case Nil{}:
179 out
180 case Con{Once{+b, name}, rest}:
181 judge(
182 owner,
183 rest,
184 matched,
185 Lists.onto(
186 &2,
187 Lint.Finding,
188 judged(List.contains(~U32, ~U32.is_eq, matched, b), owner, b, name),
189 out
190 )
191 )
192
193def defs(nodes: List<&2, Lint.Node>, out: List<&2, Lint.Finding>) -> List<&2, Lint.Finding>:
194 match nodes:
195 case Nil{}:
196 List.reverse(&2, Lint.Finding, out)
197 case Con{Lint.Node{Lint.Definition{t, u}, n, s, +k, f}, rest}:
198 +owner = {Lint.Node{Lint.Definition{t, u}, n, s, k, f}: Lint.Node}
199 defs(
200 rest,
201 judge(
202 owner,
203 Lint.visit(~Bool, ~Once, ~Once.of, Lists.any(~Lint.Node, ~Lint.Node.is_bare, k), [owner]),
204 Lint.visit(~Unit, ~U32, ~scrutinee, Unit{}, [owner]),
205 out
206 )
207 )
208 case Con{node, rest}:
209 defs(rest, out)
210
211def run(+here: Lint.Here) -> Lint.Ask(List<&2, Lint.Finding>):
212 Lint.done(defs(Lint.Here.nodes(here), []))
213
214def rule() -> Lint.Rule:
215 Lint.Rule{Lint.Needs{False{}, False{}}, [], Lint.OnFile{run}}