1	# language/unneeded_plus: a binder written with `+` that its body uses at most once on each path, so the
2	# `+` claims a reuse that never happens.
3	# Heuristics: it reads how often the checker found each binder used, the most over its branches. A
4	# binder that a match or a let takes apart is skipped: its `+` also makes its fields reusable. So is a
5	# parameter of a definition used as a value (`OnFile{run}`): the type it must have can ask for the `+`.
6	# The `+` costs no speed: the compiler counts references from the uses, not from the `+`. Removing
7	# 1,049 such `+` from Bend's slash boss demo, three-bodies and a raytracer left their C unchanged.
8	import Base
9	import bend-lint-api@0.2.2.0/linter/lint.bend as Lint
10	import bend-lint-api@0.2.2.0/shared/lists.bend as Lists
11	
12	# Types
13	# =====
14	
15	# What judging the binders of one definition reads: the definitions of the file used as values (named, not called), as
16	# the check names them; the definition, as the check names it; and its binders that a match or a let takes apart.
17	type Owner is Data:
18	  Owner{values: List<&2, String>, target: String, matched: List<&2, U32>}
19	
20	# Functions
21	# =========
22	
23	# The definition a reference below `path` names, if it is used as a value: not as the function of an application.
24	def value.visit(+u: Unit, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, String>:
25	  match path node:
26	    case Con{
27	      Lint.Above{Lint.Node{Lint.Application{}, n, s, k, f}, at},
28	      up
29	    } Lint.Node{Lint.Reference{t}, rn, rs, rk, rf}:
30	      Bool.pick(List<&2, String>, U32.is_eq(at, 0), [], [t])
31	    case _ Lint.Node{Lint.Reference{t}, rn, rs, rk, rf}:
32	      [t]
33	    case _ _:
34	      []
35	
36	def is_constructed(nodes: List<&2, Lint.Node>) -> Bool:
37	  match nodes:
38	    case Con{Lint.Node{Lint.PatternConstructor{t}, n, s, k, f}, rest}:
39	      True{}
40	    case _:
41	      False{}
42	
43	# The binder a variable below `path` uses, if it is taken apart there: it is a match's scrutinee, or the value of a let
44	# with a constructor pattern (`Vert{x, y} = v`).
45	def matched.visit(+u: Unit, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, U32>:
46	  match path node:
47	    case Con{
48	      Lint.Above{Lint.Node{Lint.Match{}, n, s, k, f}, at},
49	      up
50	    } Lint.Node{Lint.Variable{b}, vn, vs, vk, vf}:
51	      [b]
52	    case Con{
53	      Lint.Above{Lint.Node{Lint.Destructure{q}, n, s, +kids, f}, +at},
54	      up
55	    } Lint.Node{Lint.Variable{b}, vn, vs, vk, vf}:
56	      Bool.pick(
57	        List<&2, U32>,
58	        Bool.not(
59	          U32.is_eq((at + 1: U32), U32.from_nat(Lists.length(&2, Lint.Node, kids)))
60	        )
61	          && is_constructed(kids),
62	        [b],
63	        []
64	      )
65	    case _ _:
66	      []
67	
68	# Whether a binder used `used` times needs no `+`: none or one use.
69	def is_once(used: Maybe<&2, Lint.Quantity>) -> Bool:
70	  match used:
71	    case Some{Lint.Erased{}}:
72	      True{}
73	    case Some{Lint.Once{}}:
74	      True{}
75	    case _:
76	      False{}
77	
78	# The binder a node of this kind declares with `+`, if it does.
79	def plus(syntax: Lint.Syntax) -> Maybe<&2, U32>:
80	  match syntax:
81	    case Lint.Parameter{b, Lint.Many{}}:
82	      Some{b}
83	    case Lint.Field{b, Lint.Many{}}:
84	      Some{b}
85	    case Lint.Binding{b, Lint.Many{}}:
86	      Some{b}
87	    case Lint.Forall{b, Lint.Many{}}:
88	      Some{b}
89	    case Lint.Lambda{b, Some{Lint.Many{}}}:
90	      Some{b}
91	    case Lint.PatternVariable{b, Lint.Many{}}:
92	      Some{b}
93	    case _:
94	      None{}
95	
96	def is_parameter(syntax: Lint.Syntax) -> Bool:
97	  match syntax:
98	    case Lint.Parameter{b, q}:
99	      True{}
100	    case _:
101	      False{}
102	
103	def message(+name: String) -> String:
104	  "+"
105	    ++ name
106	    ++ " is used at most once on each path, so it needs no `+`. Write "
107	    ++ name
108	    ++ " without it. Speed does not change: Bend counts references from the uses, not from the `+`."
109	
110	# Whether a `+` binder its body uses at most once (`once`) needs no `+`: not if a match takes it apart, nor if it is a
111	# parameter of a definition used as a value: the type it must have can ask for the `+`.
112	def is_needless(once: Bool, parameter: Bool, owner: Owner, b: U32) -> Bool:
113	  match once parameter owner:
114	    case True{} True{} Owner{values, target, matched}:
115	      Bool.not(
116	        List.contains(~String, ~String.eq, values, target)
117	      )
118	        && Bool.not(List.contains(~U32, ~U32.is_eq, matched, b))
119	    case True{} False{} Owner{values, target, matched}:
120	      Bool.not(List.contains(~U32, ~U32.is_eq, matched, b))
121	    case _ _ _:
122	      False{}
123	
124	# The findings about a `+` binder (`binder`, if the node declares one) that its facts say its body uses at most once.
125	def judged(
126	  binder: Maybe<&2, U32>,
127	  +parameter: Bool,
128	  +owner: Owner,
129	  +span: Maybe<&2, Lint.Span>,
130	  +name: String,
131	  facts: List<&2, Lint.Fact>,
132	  out: List<&2, Lint.Finding>
133	) -> List<&2, Lint.Finding>:
134	  match binder facts:
135	    case Some{+b} Con{Lint.Fact{Lint.OfBinder{}, q, used, t}, rest}:
136	      judged(
137	        Some{b},
138	        parameter,
139	        owner,
140	        span,
141	        name,
142	        rest,
143	        Lists.onto(
144	          &2,
145	          Lint.Finding,
146	          Lint.finding(
147	            Lint.Hint{},
148	            is_needless(is_once(used), parameter, owner, b),
149	            span,
150	            message(name)
151	          ),
152	          out
153	        )
154	      )
155	    case Some{+b} Con{f, rest}:
156	      judged(Some{b}, parameter, owner, span, name, rest, out)
157	    case _ _:
158	      List.reverse(&2, Lint.Finding, out)
159	
160	def visit(+owner: Owner, +path: List<&2, Lint.Above>, +node: Lint.Node) -> List<&2, Lint.Finding>:
161	  match node:
162	    case Lint.Node{+syntax, name, span, k, fs}:
163	      judged(plus(syntax), is_parameter(syntax), owner, span, name, fs, [])
164	
165	def defs(
166	  nodes: List<&2, Lint.Node>,
167	  +values: List<&2, String>,
168	  out: List<&2, Lint.Finding>
169	) -> List<&2, Lint.Finding>:
170	  match nodes:
171	    case Nil{}:
172	      List.reverse(&2, Lint.Finding, out)
173	    case Con{Lint.Node{Lint.Definition{+t, u}, n, s, k, f}, rest}:
174	      +owner = {Lint.Node{Lint.Definition{t, u}, n, s, k, f}: Lint.Node}
175	      defs(
176	        rest,
177	        values,
178	        Lists.onto(
179	          &2,
180	          Lint.Finding,
181	          Lint.visit(
182	            ~Owner,
183	            ~Lint.Finding,
184	            ~visit,
185	            Owner{values, t, Lint.visit(~Unit, ~U32, ~matched.visit, Unit{}, [owner])},
186	            [owner]
187	          ),
188	          out
189	        )
190	      )
191	    case Con{node, rest}:
192	      defs(rest, values, out)
193	
194	def run(+here: Lint.Here) -> Lint.Ask(List<&2, Lint.Finding>):
195	  +nodes = Lint.Here.nodes(here)
196	  Lint.done(defs(nodes, Lint.visit(~Unit, ~String, ~value.visit, Unit{}, nodes), []))
197	
198	def rule() -> Lint.Rule:
199	  Lint.Rule{Lint.Needs{True{}, False{}}, [], Lint.OnFile{run}}