src/rules/suspicious/unit.bend
bolt@1.25.0.0 · 227 lines · 0 definitions
1# rule unit: a multiply or divide by the literal one (`1`, `1n`, `1.0`) on a
2# step that actually recurses. `*` and `/` inside `(e : T)` are `T.mul` and
3# `T.div`; bare, they are `Nat`. Either form, and a direct `Nat.mul` /
4# `U32.mul` / `F32.mul` or `.div`, does nothing when an operand is one
5# (`/` only when the divisor is). Drop the operation. Any other factor or
6# divisor is left alone, and so is a base case or a def that does not call
7# itself. A base case is a case arm that does not call the def; the arms are
8# judged per `case` only, so a `Bool.pick` branch beside a self-call is still
9# the recursive step, and so is a lambda body inside it (a `Lazy.stop`
10# thunk or a `List.map` callback runs on the step). One finding per
11# operation, on the literal: `Nat.mul(1n, 1n)` is one. Laws and proofs do not
12# run (a def with no type at all fills a law: it is a proof).
13import Base
14import bolt@1.25.0.0/src/src.bend as Src
15import bolt@1.25.0.0/src/finding.bend as F
16import bolt@1.25.0.0/src/syntax/lex.bend as Lex
17import bolt@1.25.0.0/src/syntax/tree.bend as Tree
18import bolt@1.25.0.0/src/rules/calls.bend as Calls
19import bolt@1.25.0.0/src/lazy/lazy.bend as Lazy
20
21# is the text the literal one?
22def one_text(+tt: String) -> Bool:
23 Bool.or(String.eq(tt, "1"), Bool.or(String.eq(tt, "1n"), String.eq(tt, "1.0")))
24
25# is the kind a number token?
26def num_kind(kk: Lex.TokKind) -> Bool:
27 match kk:
28 case Lex.TNum{}:
29 True{}
30 case other:
31 False{}
32
33# a token that is the literal one
34def one_tok(tok: Lex.Tok) -> Bool:
35 Lex.Tok{+k, +t, l, c} = tok
36 Bool.and(num_kind(k), one_text(t))
37
38# is the kind an operator's?
39def op_kind(kk: Lex.TokKind) -> Bool:
40 match kk:
41 case Lex.TOp{}:
42 True{}
43 case other:
44 False{}
45
46# the maybe, when it holds the literal one
47def one_of(mm: Maybe<&2, Lex.Tok>) -> Maybe<&2, Lex.Tok>:
48 match mm:
49 case None{}:
50 None{}
51 case Some{+tok}:
52 Bool.pick(Maybe<&2, Lex.Tok>, one_tok(tok), Some{tok}, None{})
53
54# the first maybe when it holds a token, else the second
55def either(aa: Maybe<&2, Lex.Tok>, bb: Maybe<&2, Lex.Tok>) -> Maybe<&2, Lex.Tok>:
56 match aa:
57 case None{}:
58 bb
59 case Some{tok}:
60 Some{tok}
61
62# the literal an operator's finding points at: for `*` the factor after it
63# when it is one, else the one before; for `/` the divisor when it is one
64def which(+op: String, prev: Maybe<&2, Lex.Tok>, +nxt: Maybe<&2, Lex.Tok>) -> Maybe<&2, Lex.Tok>:
65 +right = one_of(nxt)
66 Bool.pick(Maybe<&2, Lex.Tok>, String.eq(op, "*"), either(right, one_of(prev)),
67 Bool.pick(Maybe<&2, Lex.Tok>, String.eq(op, "/"), right, None{}))
68
69# a finding on that literal
70def cite(mm: Maybe<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>:
71 match mm:
72 case None{}:
73 Nil{}
74 case Some{Lex.Tok{k, +t, l, c}}:
75 [F.Finding{path, l, c, U32.from_nat(String.length(t)), "unit",
76 "Multiplying or dividing by " ++ t ++ " has no effect; drop the operation."}]
77
78# an argument that is exactly the literal one
79def arg_one(aa: Tree.Node) -> Maybe<&2, Lex.Tok>:
80 match aa:
81 case Tree.NCons{Tree.Leaf{tok}, Tree.NNil{}}:
82 one_of(Some{tok})
83 case other:
84 None{}
85
86# the last argument, when it is the literal one
87def last_one(as: List<&2, Tree.Node>) -> Maybe<&2, Lex.Tok>:
88 match as:
89 case Nil{}:
90 None{}
91 case Con{h, Nil{}}:
92 arg_one(h)
93 case Con{h, rest}:
94 last_one(rest)
95
96# the last argument that is the literal one
97def any_one(as: List<&2, Tree.Node>) -> Maybe<&2, Lex.Tok>:
98 match as:
99 case Nil{}:
100 None{}
101 case Con{h, rest}:
102 +more = any_one(rest)
103 either(more, arg_one(h))
104
105# a divide's divisor, when the call is a divide
106def on_div_is(+div: Bool, +as: List<&2, Tree.Node>, +path: String) -> List<&2, F.Finding>:
107 match div:
108 case True{}:
109 cite(last_one(as), path)
110 case False{}:
111 Nil{}
112
113# a divide's divisor, when the call is a divide
114def on_div(+tt: String, +as: List<&2, Tree.Node>, +path: String) -> List<&2, F.Finding>:
115 on_div_is(List.contains(~String, ~String.eq, ["Nat.div", "U32.div", "F32.div"], tt), as, path)
116
117# a multiply (either factor) or a divide (the divisor only)
118def on_op_is(+mul: Bool, +tt: String, +as: List<&2, Tree.Node>, +path: String) -> List<&2, F.Finding>:
119 match mul:
120 case True{}:
121 cite(any_one(as), path)
122 case False{}:
123 on_div(tt, as, path)
124
125# a multiply (either factor) or a divide (the divisor only)
126def on_op(+tt: String, +as: List<&2, Tree.Node>, +path: String) -> List<&2, F.Finding>:
127 on_op_is(List.contains(~String, ~String.eq, ["Nat.mul", "U32.mul", "F32.mul"], tt), tt, as, path)
128
129# the call's own identity operands, when this step recurses
130def on_hot(hot: Bool, +tt: String, +as: List<&2, Tree.Node>, +path: String) -> List<&2, F.Finding>:
131 match hot:
132 case False{}:
133 Nil{}
134 case True{}:
135 on_op(tt, as, path)
136
137# the call's own identity operands, when this step recurses
138def on_call(+tt: String, kids: Tree.Node, +path: String, +hot: Bool) -> List<&2, F.Finding>:
139 on_hot(hot, tt, Calls.args(kids), path)
140
141# the call's findings when the group is an application
142def own_of(
143 call: Bool,
144 +tt: String,
145 +kids: Tree.Node,
146 +path: String,
147 +hot: Bool
148) -> List<&2, F.Finding>:
149 match call:
150 case True{}:
151 on_call(tt, kids, path, hot)
152 case False{}:
153 Nil{}
154
155# the first leaf, when the chain starts with one
156def first_tok(nn: Tree.Node) -> Maybe<&2, Lex.Tok>:
157 match nn:
158 case Tree.NCons{Tree.Leaf{tok}, rest}:
159 Some{tok}
160 case other:
161 None{}
162
163# the token a leaf leaves behind for what follows it: none past an operator
164def after(tok: Lex.Tok) -> Maybe<&2, Lex.Tok>:
165 match tok:
166 case Lex.Tok{+k, +t, +l, +c}:
167 Bool.pick(Maybe<&2, Lex.Tok>, op_kind(k), None{}, Some{Lex.Tok{k, t, l, c}})
168
169# a leaf's own finding: an operator by one, in a hot region
170def op_hit(
171 tok: Lex.Tok,
172 +prev: Maybe<&2, Lex.Tok>,
173 +nxt: Maybe<&2, Lex.Tok>,
174 +path: String,
175 +hot: Bool
176) -> List<&2, F.Finding>:
177 match tok:
178 case Lex.Tok{k, +t, l, c}:
179 Bool.pick(List<&2, F.Finding>, Bool.and(hot, op_kind(k)), cite(which(t, prev, nxt), path), [])
180
181# the name a group is called by: the token right before it ("" for none)
182def callee(mm: Maybe<&2, Lex.Tok>) -> String:
183 match mm:
184 case None{}:
185 ""
186 case Some{Lex.Tok{k, t, l, c}}:
187 t
188
189# `*` / `/` by one, and the same through calls, in a hot region. prev is the
190# leaf right before, none past an operator, a group or a statement; a `(`
191# group right after a leaf is a call of it
192def walk(nn: Tree.Node, +prev: Maybe<&2, Lex.Tok>, +self: String, +path: String, +hot: Bool) -> List<&2, F.Finding>:
193 match nn:
194 case Tree.NCons{Tree.Leaf{+tok}, +rest}:
195 +more = walk(rest, after(tok), self, path, hot)
196 List.append(&2, F.Finding, op_hit(tok, prev, first_tok(rest), path, hot), more)
197 case Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, +kids, _}, rest}:
198 +own = own_of(String.eq(o, "("), callee(prev), kids, path, hot)
199 +inner = walk(kids, None{}, self, path, hot)
200 +later = walk(rest, None{}, self, path, hot)
201 List.concat(&2, F.Finding, [inner, own, later])
202 case Tree.NCons{Tree.Stmt{Tree.SCase{}, kids, +body}, rest}:
203 +arm = Bool.and(hot, Calls.calls(body, self))
204 List.concat(&2, F.Finding, [walk(kids, None{}, self, path, False{}),
205 walk(body, None{}, self, path, arm), walk(rest, None{}, self, path, hot)])
206 case Tree.NCons{Tree.Stmt{kind, kids, body}, rest}:
207 List.concat(&2, F.Finding, [walk(kids, None{}, self, path, hot),
208 walk(body, None{}, self, path, hot), walk(rest, None{}, self, path, hot)])
209 case Tree.NCons{h, rest}:
210 walk(rest, prev, self, path, hot)
211 case other:
212 Nil{}
213
214def check.go(ds: List<&2, Calls.Def>, +path: String, acc: List<&2, List<&2, F.Finding>>) -> List<&2, F.Finding>:
215 match ds:
216 case Nil{}:
217 List.concat(&2, F.Finding, List.reverse(&2, List<&2, F.Finding>, acc))
218 case Con{Calls.Def{+name, +sig, +body}, rest}:
219 check.go(rest, path,
220 Lazy.stop(List<&2, F.Finding>,
221 Bool.not(Bool.and(Calls.calls(body, name), Bool.not(Calls.exempt(path, sig)))), [],
222 _u => walk(body, None{}, name, path, True{})) <> acc)
223
224# the rule
225def check(ss: Src.Src) -> List<&2, F.Finding>:
226 Src.Src{path, text, toks, tree, bound, items} = ss
227 check.go(Calls.defs(tree), path, [])