1	# rule prefix: a String.take compared to a literal of its length:
2	# `String.eq(String.take(s, k), "..")` or `String.eq("..", String.take(s,
3	# k))`. Among the significant tokens (spaces, newlines and comments dropped):
4	# a dotted name `String.eq`, `(`, `String.take` and `(`, then the take's
5	# first argument s, any tokens up to the first comma outside the brackets
6	# they open (a call such as `String.drop(m, 4n)` is one argument), then a
7	# Nat literal k, `)`, `,`, a string literal and `)`; or the dotted name
8	# `String.eq`, `(`, the string literal, `,`, `String.take`, `(`, s, the
9	# comma, k, `)` and `)`. Only when k's text is the literal's length (an
10	# escape, `\n` or `\u{1B}`, one char) written in decimal with an `n`, as
11	# `4n` for `"ERR "`. A bracket that closes the take before any such comma
12	# ends the scan with no finding. One finding, on the `String.eq` token, for
13	# each such run, and nothing else: a take of another length is another bug.
14	# String.take copies k chars into a new String only to compare them;
15	# `String.starts_with(s, "ERR ")` (Base) walks s in place and gives the same
16	# answer for every s, False when s is shorter, s any expression. A LAWS.bend
17	# or a PROOF.bend, which never runs, is exempt. A comment is never read, and
18	# a string literal is one token, so the shape written inside either is not
19	# the shape.
20	import Base
21	import ../../src.bend as Src
22	import ../../paths.bend as Paths
23	import ../../role.bend as Role
24	import ../../lazy/lazy.bend as Lazy
25	import ../../finding.bend as F
26	import ../../syntax/lex.bend as Lex
27	import ../tokens.bend as T
28	
29	# where the length of a string literal's text is: before its opening
30	# quote, in plain text, just after a backslash, inside a `\u{..}`, or past
31	# its closing quote
32	type Mode is Data:
33	  MOpen{}
34	  MPlain{}
35	  MEsc{}
36	  MUni{}
37	  MDone{}
38	
39	# is the char the code point?
40	def is_cp(+cc: Char, +xx: U32) -> Bool:
41	  U32.is_eq(Char.to_u32(cc), xx)
42	
43	# what the char adds to the length: one in plain text, but not the closing
44	# quote; nothing anywhere else
45	def len.add(mm: Mode, +cc: Char) -> Nat:
46	  match mm:
47	    case MPlain{}:
48	      Bool.pick(Nat, is_cp(cc, 34), 0n, 1n)
49	    case other:
50	      0n
51	
52	# where the char leaves the length: a backslash starts an escape, a quote
53	# closes the literal, `u` after a backslash opens a `\u{..}` and `}` closes
54	# it
55	def len.next(mm: Mode, +cc: Char) -> Mode:
56	  match mm:
57	    case MOpen{}:
58	      MPlain{}
59	    case MPlain{}:
60	      Bool.pick(Mode, is_cp(cc, 92), MEsc{}, Bool.pick(Mode, is_cp(cc, 34), MDone{}, MPlain{}))
61	    case MEsc{}:
62	      Bool.pick(Mode, is_cp(cc, 117), MUni{}, MPlain{})
63	    case MUni{}:
64	      Bool.pick(Mode, is_cp(cc, 125), MPlain{}, MUni{})
65	    case MDone{}:
66	      MDone{}
67	
68	# the length of the rest of a literal's text, from where it is
69	def len.go(tt: String, +mm: Mode) -> Nat:
70	  match tt:
71	    case SNil{}:
72	      0n
73	    case SCon{+cc, rest}:
74	      Nat.add(len.add(mm, cc), len.go(rest, len.next(mm, cc)))
75	
76	# the length of a string literal, its text as the lexer keeps it (quotes
77	# and escapes as written): each escape one char
78	def len(tt: String) -> Nat:
79	  len.go(tt, MOpen{})
80	
81	# is the Nat literal's text the literal's length?
82	def fits(+kk: String, lit: String) -> Bool:
83	  String.eq(kk, Nat.show(len(lit)) ++ "n")
84	
85	# what the finding says: the take, and the starts_with that replaces it
86	def say(+ss: String, +kk: String, +lit: String) -> String:
87	  "String.eq(String.take(" ++ ss ++ ", " ++ kk ++ "), " ++ lit ++ ") copies " ++ kk
88	    ++ " chars only to compare them; String.starts_with(" ++ ss ++ ", " ++ lit ++ ") gives the same answer in place."
89	
90	# where the scan of a take's first argument stands: inside it at a depth of
91	# brackets it opened, just past the comma that ends it, or at the bracket
92	# that closes the take before any such comma
93	type Skip is Data:
94	  SGo{depth: Nat}
95	  SComma{}
96	  SClose{}
97	
98	# the argument as the finding writes it, and the tokens after its comma
99	type Arg is Data:
100	  Arg{text: String, rest: List<&2, Lex.Tok>}
101	
102	# a comma at the depth: the argument's end at depth zero, else inside it
103	def skip.comma(dd: Nat) -> Skip:
104	  match dd:
105	    case 0n:
106	      SComma{}
107	    case 1n+p:
108	      SGo{1n+p}
109	
110	# a closing bracket at the depth: the take's own at depth zero, else one
111	# bracket the argument opened
112	def skip.close(dd: Nat) -> Skip:
113	  match dd:
114	    case 0n:
115	      SClose{}
116	    case 1n+p:
117	      SGo{p}
118	
119	# where a token of the kind leaves the scan at the depth
120	def skip.step(kk: Lex.TokKind, dd: Nat) -> Skip:
121	  match kk:
122	    case Lex.TComma{}:
123	      skip.comma(dd)
124	    case Lex.TOpen{}:
125	      SGo{1n+dd}
126	    case Lex.TClose{}:
127	      skip.close(dd)
128	    case other:
129	      SGo{dd}
130	
131	# a token as the finding writes it: a comma with a space after it, an
132	# operator with one on each side
133	def piece(kk: Lex.TokKind, +tt: String) -> String:
134	  match kk:
135	    case Lex.TComma{}:
136	      ", "
137	    case Lex.TOp{}:
138	      " " ++ tt ++ " "
139	    case other:
140	      tt
141	
142	# what a token adds to the argument's text, given where it leaves the scan:
143	# nothing for the comma that ends the argument
144	def skip.piece(sk: Skip, kk: Lex.TokKind, +tt: String) -> String:
145	  match sk:
146	    case SComma{}:
147	      ""
148	    case other:
149	      piece(kk, tt)
150	
151	# the take's first argument, scanned from where the scan stands: what it
152	# says (acc: its pieces so far, last first) and the tokens after the comma
153	# that ends it; none when the take
154	# closes first or the tokens run out
155	def skip(toks: List<&2, Lex.Tok>, sk: Skip, +acc: List<&2, String>) -> Maybe<&2, Arg>:
156	  match toks:
157	    case Nil{}:
158	      None{}
159	    case Con{Lex.Tok{+k, +t, l, c}, rest}:
160	      match sk:
161	        case SComma{}:
162	          Some{Arg{String.join(List.reverse(&2, String, acc), ""), Lex.Tok{k, t, l, c} <> rest}}
163	        case SClose{}:
164	          None{}
165	        case SGo{dd}:
166	          +nx = skip.step(k, dd)
167	          skip(rest, nx, skip.piece(nx, k, t) <> acc)
168	
169	# a dotted name: what `String.eq` is
170	def dotted(kk: Lex.TokKind) -> Bool:
171	  match kk:
172	    case Lex.TDotted{}:
173	      True{}
174	    case other:
175	      False{}
176	
177	# after the argument's comma, k, `)`, `,`, a string literal and `)`: is k
178	# the literal's length?
179	def tail_a.ok(+kk: String, +t7: String, +t8: String, k9: Lex.TokKind, +t9: String, +t10: String) -> Bool:
180	  Bool.and(String.eq(t7, ")"), Bool.and(String.eq(t8, ","), Bool.and(Lex.is_str(k9),
181	    Bool.and(String.eq(t10, ")"), fits(kk, t9)))))
182	
183	# the take-first shape's end, after the argument: what the finding says
184	def tail_a(ma: Maybe<&2, Arg>) -> Maybe<&2, String>:
185	  match ma:
186	    case None{}:
187	      None{}
188	    case Some{Arg{+ss, r}}:
189	      match r:
190	        case Con{Lex.Tok{k6, +t6, l6, c6}, Con{Lex.Tok{k7, +t7, l7, c7}, Con{Lex.Tok{k8, +t8, l8, c8},
191	          Con{Lex.Tok{k9, +t9, l9, c9}, Con{Lex.Tok{k10, +t10, l10, c10}, rest}}}}}:
192	          Bool.pick(Maybe<&2, String>, tail_a.ok(t6, t7, t8, k9, t9, t10), Some{say(ss, t6, t9)}, None{})
193	        case other:
194	          None{}
195	
196	# after the argument's comma, k, `)` and `)`: is k the literal's length?
197	def tail_b.ok(+kk: String, +t9: String, +t10: String, +lit: String) -> Bool:
198	  Bool.and(String.eq(t9, ")"), Bool.and(String.eq(t10, ")"), fits(kk, lit)))
199	
200	# the literal-first shape's end, after the argument: what the finding says
201	def tail_b(ma: Maybe<&2, Arg>, +lit: String) -> Maybe<&2, String>:
202	  match ma:
203	    case None{}:
204	      None{}
205	    case Some{Arg{+ss, r}}:
206	      match r:
207	        case Con{Lex.Tok{k8, +t8, l8, c8}, Con{Lex.Tok{k9, +t9, l9, c9}, Con{Lex.Tok{k10, +t10, l10, c10}, rest}}}:
208	          Bool.pick(Maybe<&2, String>, tail_b.ok(t8, t9, t10, lit), Some{say(ss, t8, lit)}, None{})
209	        case other:
210	          None{}
211	
212	# a dotted `String.eq`, `(`, `String.take` and `(`?
213	def head_a(k0: Lex.TokKind, +t0: String, +t1: String, +t2: String, +t3: String) -> Bool:
214	  Bool.and(dotted(k0), Bool.and(String.eq(t0, "String.eq"), Bool.and(String.eq(t1, "("),
215	    Bool.and(String.eq(t3, "("), String.eq(t2, "String.take")))))
216	
217	# the take-first shape, its head read: the end, after the argument
218	def at_a.go(ok: Bool, r3: List<&2, Lex.Tok>) -> Maybe<&2, String>:
219	  match ok:
220	    case True{}:
221	      tail_a(skip(r3, SGo{0n}, []))
222	    case False{}:
223	      None{}
224	
225	# a token of kind k0 and text t0, then these: the take-first shape?
226	def at_a(k0: Lex.TokKind, +t0: String, toks: List<&2, Lex.Tok>) -> Maybe<&2, String>:
227	  match toks:
228	    case Con{Lex.Tok{k1, +t1, l1, c1}, Con{Lex.Tok{k2, +t2, l2, c2}, Con{Lex.Tok{k3, +t3, l3, c3}, r3}}}:
229	      at_a.go(head_a(k0, t0, t1, t2, t3), r3)
230	    case other:
231	      None{}
232	
233	# a dotted `String.eq`, `(`, a string literal, `,`, `String.take` and `(`?
234	def head_b(k0: Lex.TokKind, +t0: String, +t1: String, k2: Lex.TokKind, +t3: String, +t4: String, +t5: String) -> Bool:
235	  Bool.and(dotted(k0), Bool.and(String.eq(t0, "String.eq"), Bool.and(String.eq(t1, "("), Bool.and(Lex.is_str(k2),
236	    Bool.and(String.eq(t3, ","), Bool.and(String.eq(t4, "String.take"), String.eq(t5, "(")))))))
237	
238	# the literal-first shape, its head read: the end, after the argument
239	def at_b.go(ok: Bool, r5: List<&2, Lex.Tok>, +lit: String) -> Maybe<&2, String>:
240	  match ok:
241	    case True{}:
242	      tail_b(skip(r5, SGo{0n}, []), lit)
243	    case False{}:
244	      None{}
245	
246	# a token of kind k0 and text t0, then these: the literal-first shape?
247	def at_b(k0: Lex.TokKind, +t0: String, toks: List<&2, Lex.Tok>) -> Maybe<&2, String>:
248	  match toks:
249	    case Con{Lex.Tok{k1, +t1, l1, c1}, Con{Lex.Tok{k2, +t2, l2, c2}, Con{Lex.Tok{k3, +t3, l3, c3},
250	      Con{Lex.Tok{k4, +t4, l4, c4}, Con{Lex.Tok{k5, +t5, l5, c5}, r5}}}}}:
251	      at_b.go(head_b(k0, t0, t1, k2, t3, t4, t5), r5, t2)
252	    case other:
253	      None{}
254	
255	# the first message, else the second
256	def either(ma: Maybe<&2, String>, mb: Maybe<&2, String>) -> Maybe<&2, String>:
257	  match ma:
258	    case None{}:
259	      mb
260	    case Some{x}:
261	      Some{x}
262	
263	# a token of kind k0 and text t0, then these: either shape? what the finding
264	# says when they make one
265	def at(+k0: Lex.TokKind, +t0: String, +toks: List<&2, Lex.Tok>) -> Maybe<&2, String>:
266	  either(at_a(k0, t0, toks), at_b(k0, t0, toks))
267	
268	# the finding a run makes, if any, before the rest
269	def hit(mm: Maybe<&2, String>, +path: String, +ll: U32, +cc: U32, more: List<&2, F.Finding>) -> List<&2, F.Finding>:
270	  match mm:
271	    case None{}:
272	      more
273	    case Some{msg}:
274	      F.Finding{path, ll, cc, 9, "prefix", msg} <> more
275	
276	# every run of either shape among the tokens, in order
277	def walk(toks: List<&2, Lex.Tok>, +path: String) -> List<&2, F.Finding>:
278	  match toks:
279	    case Nil{}:
280	      Nil{}
281	    case Con{Lex.Tok{+k, +t, +l, +c}, +rest}:
282	      hit(at(k, t, rest), path, l, c, walk(rest, path))
283	
284	# the rule
285	def check(ss: Src.Src) -> List<&2, F.Finding>:
286	  Src.Src{+path, text, toks, tree, bound, items} = ss
287	  Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => walk(T.sig(toks), path))
288	
289	# the rule, told the file's role (src/role.bend): a law or proof file is
290	# skipped
291	def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>:
292	  Src.Src{path, text, toks, tree, bound, items} = ss
293	  Lazy.stop(List<&2, F.Finding>, Role.is_law_file(rr), [], _u => walk(T.sig(toks), path))