language/reused_binder.bend

bend-lint-rules@0.2.0.0 · 215 lines · 17 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.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 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}}