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.
10	import Base
11	import bend-lint-api@0.2.2.0/linter/lint.bend as Lint
12	import bend-lint-api@0.2.2.0/shared/lists.bend as Lists
13	
14	# Types
15	# =====
16	
17	# A binder that can be used once: its number, and its name.
18	type 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.
23	type Seen is Data:
24	  Seen{first: Maybe<&2, Lint.Span>, second: Maybe<&2, Lint.Span>}
25	
26	# Functions
27	# =========
28	def 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.
38	def 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.
52	def 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`.
64	def 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	
79	def is_match(syntax: Lint.Syntax) -> Bool:
80	  match syntax:
81	    case Lint.Match{}:
82	      True{}
83	    case _:
84	      False{}
85	
86	def 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.
94	def 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.
102	def 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.
114	def 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	
156	def 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`).
162	def 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.
171	def 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	
193	def 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	
211	def run(+here: Lint.Here) -> Lint.Ask(List<&2, Lint.Finding>):
212	  Lint.done(defs(Lint.Here.nodes(here), []))
213	
214	def rule() -> Lint.Rule:
215	  Lint.Rule{Lint.Needs{False{}, False{}}, [], Lint.OnFile{run}}