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).
13	import Base
14	import ../../src.bend as Src
15	import ../../finding.bend as F
16	import ../../syntax/lex.bend as Lex
17	import ../../syntax/tree.bend as Tree
18	import ../calls.bend as Calls
19	import ../../lazy/lazy.bend as Lazy
20	
21	# is the text the literal one?
22	def 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?
26	def 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
34	def 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?
39	def 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
47	def 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
55	def 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
64	def 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
70	def 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
79	def 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
87	def 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
97	def 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
106	def 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
114	def 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)
118	def 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)
126	def 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
130	def 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
138	def 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
142	def 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
156	def 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
164	def 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
170	def 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)
182	def 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
192	def 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	
214	def 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
225	def 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, [])