1	# rule wrap: how a def header breaks. A one-line header wider than 120 must
2	# break; the width is the header through its `:`, counted the way `space`
3	# counts a line (a string literal is two characters), a comment counting
4	# none. A header breaks when a newline token of its own sits in it: a line
5	# break inside a string literal is the string's. A one-line header that
6	# fits stays one line however many parameters it has. A header that breaks
7	# puts `(` at the end of the first line and one parameter on each following
8	# line, then `)` and the return type on a line of their own after the last
9	# parameter. Several parameters on a line, a parameter left on the `(`
10	# line, a parameter split across lines, a `)` on the last parameter's line
11	# (`bb: U32) -> U32:`), a `)` with no `->` right after it on its line (the
12	# return type on a line of its own, `)` then `-> U32:`; a def that fills a
13	# law has no return type, and `):` is its end), or a parameter list
14	# with no parameter in it (`def none(` then `) -> U32:`, which fits on one
15	# line), is a finding. A comment after the header's `:` is not part of the
16	# header: `def u(aa: U32) -> U32: # note` is a one-line header.
17	import Base
18	import ../../src.bend as Src
19	import ../../finding.bend as F
20	import ../../syntax/lex.bend as Lex
21	import ../../syntax/outline.bend as Outline
22	import ../../lazy/lazy.bend as Lazy
23	import ./space.bend as Space
24	
25	# where one parameter sits in the header: its first line, its last, its column
26	type Span is Data:
27	  Span{line: U32, end: U32, col: U32}
28	
29	# seeking the parameter list, inside it, just past its `)`, past a `->`
30	# right after it on its line, or past anything else after it
31	type Phase is Data:
32	  Seek{}
33	  Args{}
34	  Past{}
35	  Shut{}
36	  Loose{}
37	
38	# what a token does to the bracket depths
39	type Act is Data:
40	  AOpen{}
41	  AParen{}
42	  AEnd{}
43	  AUnparen{}
44	  ABrack{}
45	  AUnbrack{}
46	  ABrace{}
47	  AUnbrace{}
48	  AAngle{}
49	  AUnangle{}
50	  AComma{}
51	  AArrow{}
52	  AStray{}
53	  ANone{}
54	
55	# the walk: depths, where the list's `)` sat, the `(` line, and the parameter
56	# open so far (spans reversed)
57	type Walk is Data:
58	  Walk{mode: Phase, paren: U32, bracket: U32, brace: U32, angle: U32, shut: Span, open: U32,
59	    on: Bool, pline: U32, pend: U32, pcol: U32, spans: List<&2, Span>}
60	
61	# the header already breaks across lines: some token of it is a newline
62	def check.broken(toks: List<&2, Lex.Tok>) -> Bool:
63	  match toks:
64	    case Nil{}:
65	      False{}
66	    case Con{Lex.Tok{kk, _tx, _ln, _cl}, rest}:
67	      Lazy.or_else(Lex.is_nl(kk), _u => check.broken(rest))
68	
69	# one token's share of the header's width: a comment has none
70	def check.cost(kd: Lex.TokKind, +tx: String) -> U32:
71	  match kd:
72	    case Lex.TComment{}:
73	      0
74	    case other:
75	      Space.width_of(other, tx)
76	
77	# the width so far, with one token's share added
78	def check.add(+acc: U32, kd: Lex.TokKind, +tx: String) -> U32:
79	  (acc + check.cost(kd, tx) : U32)
80	
81	# a `:` token?
82	def check.is_colon(kk: Lex.TokKind) -> Bool:
83	  match kk:
84	    case Lex.TColon{}:
85	      True{}
86	    case other:
87	      False{}
88	
89	# the header's width through its last `:` (upto, once seen says there was
90	# one), else its whole width, a string literal counting as two and a
91	# comment none
92	def check.width.go(toks: List<&2, Lex.Tok>, +acc: U32, +upto: U32, +seen: Bool) -> U32:
93	  match toks:
94	    case Nil{}:
95	      Bool.pick(U32, seen, upto, acc)
96	    case Con{Lex.Tok{+kd, tx, _ln, _cl}, rest}:
97	      +next = check.add(acc, kd, tx)
98	      +colon = check.is_colon(kd)
99	      check.width.go(rest, next, Bool.pick(U32, colon, next, upto), Bool.or(colon, seen))
100	
101	# the header's width, through its `:`: a comment after it does not count
102	def check.width(toks: List<&2, Lex.Tok>) -> U32:
103	  check.width.go(toks, 0, 0, False{})
104	
105	# a fresh walk, before the parameter list
106	def check.start() -> Walk:
107	  Walk{Seek{}, 0, 0, 0, 0, Span{0, 0, 0}, 0, False{}, 0, 0, 0, []}
108	
109	# `(`
110	def check.is_oparen(kk: Lex.TokKind, +tx: String) -> Bool:
111	  match kk:
112	    case Lex.TOpen{}:
113	      String.eq(tx, "(")
114	    case other:
115	      False{}
116	
117	# `)`
118	def check.is_cparen(kk: Lex.TokKind, +tx: String) -> Bool:
119	  match kk:
120	    case Lex.TClose{}:
121	      String.eq(tx, ")")
122	    case other:
123	      False{}
124	
125	# an opening bracket, as the depth it raises; ANone when it is not one
126	def check.open_text(+tx: String) -> Act:
127	  Bool.pick(Act, String.eq(tx, "("), AParen{},
128	    Bool.pick(Act, String.eq(tx, "["), ABrack{},
129	      Bool.pick(Act, String.eq(tx, "{"), ABrace{}, ANone{})))
130	
131	# an opening bracket, as the depth it raises
132	def check.on_open(kk: Lex.TokKind, +tx: String) -> Act:
133	  match kk:
134	    case Lex.TOpen{}:
135	      check.open_text(tx)
136	    case other:
137	      ANone{}
138	
139	# a closing bracket, as the depth it lowers; ANone when it is not one
140	def check.close_text(+tx: String) -> Act:
141	  Bool.pick(Act, String.eq(tx, ")"), AUnparen{},
142	    Bool.pick(Act, String.eq(tx, "]"), AUnbrack{},
143	      Bool.pick(Act, String.eq(tx, "}"), AUnbrace{}, ANone{})))
144	
145	# a closing bracket, as the depth it lowers
146	def check.on_close(kk: Lex.TokKind, +tx: String) -> Act:
147	  match kk:
148	    case Lex.TClose{}:
149	      check.close_text(tx)
150	    case other:
151	      ANone{}
152	
153	# an operator token
154	def check.is_op(kk: Lex.TokKind) -> Bool:
155	  match kk:
156	    case Lex.TOp{}:
157	      True{}
158	    case other:
159	      False{}
160	
161	# every char a `>`
162	def check.gt_chars(cs: List<&2, Char>) -> Bool:
163	  match cs:
164	    case Nil{}:
165	      True{}
166	    case Con{+c, t}:
167	      Lazy.and_then(Char.is_eq(c, '>'), _u => check.gt_chars(t))
168	
169	# the text is a non-empty run of `>`
170	def check.all_gt(+tx: String) -> Bool:
171	  Bool.and(Bool.not(String.is_empty(tx)), check.gt_chars(String.to_list(tx)))
172	
173	# how many `>` a run holds
174	def check.gt_count(cs: List<&2, Char>) -> Nat:
175	  match cs:
176	    case Nil{}:
177	      0n
178	    case Con{+c, t}:
179	      +more = check.gt_count(t)
180	      Bool.pick(Nat, Char.is_eq(c, '>'), Succ{more}, more)
181	
182	# the angle-closes in the text, else none
183	def check.ticks_of(+tx: String) -> Nat:
184	  Lazy.stop(Nat, Bool.not(check.all_gt(tx)), 0n, _u => check.gt_count(String.to_list(tx)))
185	
186	# `<` or `<&` glued to a name opens type arguments
187	def check.opens_angle(glued: Bool, +tx: String) -> Bool:
188	  Bool.and(glued, Bool.or(String.eq(tx, "<"), String.eq(tx, "<&")))
189	
190	# an angle close, discarded when an angle open already won
191	def check.drop_close(_closed: Act) -> Act:
192	  AAngle{}
193	
194	# an angle open wins over a close; otherwise the close stands
195	def check.prefer_open(opens: Bool, closed: Act) -> Act:
196	  match opens:
197	    case True{}:
198	      check.drop_close(closed)
199	    case False{}:
200	      closed
201	
202	# `>` runs close angles; `<` glued to a name opens one
203	def check.op_angle(+tx: String, glued: Bool) -> Act:
204	  check.prefer_open(check.opens_angle(glued, tx),
205	    Bool.pick(Act, check.all_gt(tx), AUnangle{}, ANone{}))
206	
207	# not an operator: no angle motion
208	def check.no_angle(_tx: String, _glued: Bool) -> Act:
209	  ANone{}
210	
211	# an operator's angle motion
212	def check.angle_op(is_op: Bool, +tx: String, glued: Bool) -> Act:
213	  match is_op:
214	    case True{}:
215	      check.op_angle(tx, glued)
216	    case False{}:
217	      check.no_angle(tx, glued)
218	
219	# angle motion, when the token is an operator
220	def check.angle_act(kk: Lex.TokKind, +tx: String, glued: Bool) -> Act:
221	  check.angle_op(check.is_op(kk), tx, glued)
222	
223	# a value used only so a branch can name it
224	def check.keep(act: Act, _kk: Lex.TokKind, _tx: String, _glued: Bool) -> Act:
225	  act
226	
227	# angle motion when the token was not a bracket, else that bracket
228	def check.or_angle(closed: Act, kk: Lex.TokKind, +tx: String, glued: Bool) -> Act:
229	  match closed:
230	    case ANone{}:
231	      check.angle_act(kk, tx, glued)
232	    case other:
233	      check.keep(other, kk, tx, glued)
234	
235	# a close bracket, else angle motion
236	def check.or_close(opened: Act, +kk: Lex.TokKind, +tx: String, glued: Bool) -> Act:
237	  match opened:
238	    case ANone{}:
239	      check.or_angle(check.on_close(kk, tx), kk, tx, glued)
240	    case other:
241	      check.keep(other, kk, tx, glued)
242	
243	# the bracket or angle motion of a token, not the parameter list's own breaks
244	def check.brackets(+kk: Lex.TokKind, +tx: String, glued: Bool) -> Act:
245	  check.or_close(check.on_open(kk, tx), kk, tx, glued)
246	
247	# no depth is open
248	def check.zero(+paren: U32, +angle: U32, +brace: U32, +bracket: U32) -> Bool:
249	  Bool.and(U32.is_eq(paren, 0),
250	    Bool.and(U32.is_eq(angle, 0),
251	      Bool.and(U32.is_eq(brace, 0), U32.is_eq(bracket, 0))))
252	
253	# the top of the parameter list: one `(`, nothing nested
254	def check.top(+paren: U32, +angle: U32, +brace: U32, +bracket: U32) -> Bool:
255	  Bool.and(U32.is_eq(paren, 1),
256	    Bool.and(U32.is_eq(angle, 0),
257	      Bool.and(U32.is_eq(brace, 0), U32.is_eq(bracket, 0))))
258	
259	# `(` at depth zero opens the parameter list; a nested one is just a paren
260	def check.pick_open(zero: Bool, rest: Act) -> Act:
261	  match zero:
262	    case True{}:
263	      AOpen{}
264	    case False{}:
265	      rest
266	
267	# the parameter list's `(`, else the token's ordinary motion
268	def check.seek_open(is_open: Bool, zero: Bool, rest: Act) -> Act:
269	  match is_open:
270	    case True{}:
271	      check.pick_open(zero, rest)
272	    case False{}:
273	      rest
274	
275	# motion while still seeking the parameter list
276	def check.act_seek(
277	  +kk: Lex.TokKind,
278	  +tx: String,
279	  glued: Bool,
280	  +paren: U32,
281	  +angle: U32,
282	  +brace: U32,
283	  +bracket: U32
284	) -> Act:
285	  check.seek_open(check.is_oparen(kk, tx), check.zero(paren, angle, brace, bracket),
286	    check.brackets(kk, tx, glued))
287	
288	# `)` at the top of the list ends it; a nested one is just a paren
289	def check.end_or(flat: Bool, rest: Act) -> Act:
290	  match flat:
291	    case True{}:
292	      AEnd{}
293	    case False{}:
294	      rest
295	
296	# the parameter list's `)`, else the token's ordinary motion
297	def check.args_end(is_close: Bool, flat: Bool, rest: Act) -> Act:
298	  match is_close:
299	    case True{}:
300	      check.end_or(flat, rest)
301	    case False{}:
302	      rest
303	
304	# a comma at the top of the list separates parameters
305	def check.comma_or(flat: Bool, rest: Act) -> Act:
306	  match flat:
307	    case True{}:
308	      AComma{}
309	    case False{}:
310	      rest
311	
312	# a separating comma, else the token's ordinary motion
313	def check.args_comma(is_comma: Bool, flat: Bool, rest: Act) -> Act:
314	  match is_comma:
315	    case True{}:
316	      check.comma_or(flat, rest)
317	    case False{}:
318	      rest
319	
320	# motion inside the parameter list
321	def check.act_args(
322	  +kk: Lex.TokKind,
323	  +tx: String,
324	  glued: Bool,
325	  +paren: U32,
326	  +angle: U32,
327	  +brace: U32,
328	  +bracket: U32
329	) -> Act:
330	  check.args_end(check.is_cparen(kk, tx), check.top(paren, angle, brace, bracket),
331	    check.args_comma(Lex.is_comma(kk), check.top(paren, angle, brace, bracket),
332	      check.brackets(kk, tx, glued)))
333	
334	# past the parameter list nothing moves
335	def check.act_done(
336	  _kk: Lex.TokKind,
337	  _tx: String,
338	  _glued: Bool,
339	  _paren: U32,
340	  _angle: U32,
341	  _brace: U32,
342	  _bracket: U32
343	) -> Act:
344	  ANone{}
345	
346	# `->`
347	def check.is_arrow(kk: Lex.TokKind) -> Bool:
348	  match kk:
349	    case Lex.TArrow{}:
350	      True{}
351	    case other:
352	      False{}
353	
354	# right after the list's `)`, a `->`, or the `:` of a header with no return
355	# type (a def that fills a law), or anything else
356	def check.act_shut(
357	  +kk: Lex.TokKind,
358	  _tx: String,
359	  _glued: Bool,
360	  _paren: U32,
361	  _angle: U32,
362	  _brace: U32,
363	  _bracket: U32
364	) -> Act:
365	  Bool.pick(Act, Bool.or(check.is_arrow(kk), check.is_colon(kk)), AArrow{}, AStray{})
366	
367	# the motion of one token
368	def check.act(
369	  ph: Phase,
370	  kk: Lex.TokKind,
371	  +tx: String,
372	  glued: Bool,
373	  +paren: U32,
374	  +angle: U32,
375	  +brace: U32,
376	  +bracket: U32
377	) -> Act:
378	  match ph:
379	    case Past{}:
380	      check.act_done(kk, tx, glued, paren, angle, brace, bracket)
381	    case Shut{}:
382	      check.act_shut(kk, tx, glued, paren, angle, brace, bracket)
383	    case Loose{}:
384	      check.act_done(kk, tx, glued, paren, angle, brace, bracket)
385	    case Seek{}:
386	      check.act_seek(kk, tx, glued, paren, angle, brace, bracket)
387	    case Args{}:
388	      check.act_args(kk, tx, glued, paren, angle, brace, bracket)
389	
390	# the parameter list's own `(`, `)` and commas are not part of a parameter
391	def check.is_sep(act: Act) -> Bool:
392	  match act:
393	    case AOpen{}:
394	      True{}
395	    case AEnd{}:
396	      True{}
397	    case AComma{}:
398	      True{}
399	    case other:
400	      False{}
401	
402	# one less, and not below zero
403	def check.dec_u(+nn: U32) -> U32:
404	  Lazy.stop(U32, U32.is_eq(nn, 0), 0, _u => (nn - 1 : U32))
405	
406	# `left` angle-closes applied to the depth, and not below zero
407	def check.sub(left: Nat, +angle: U32) -> U32:
408	  match left:
409	    case Zero{}:
410	      angle
411	    case Succ{p}:
412	      Lazy.stop(U32, U32.is_eq(angle, 0), angle, _u => check.sub(p, (angle - 1 : U32)))
413	
414	# a parameter that did start, onto the list
415	def check.no_span(_pline: U32, _pend: U32, _pcol: U32, spans: List<&2, Span>) -> List<&2, Span>:
416	  spans
417	
418	# the open parameter, closed onto the list
419	def check.cons(on: Bool, +pline: U32, +pend: U32, +pcol: U32, spans: List<&2, Span>) -> List<&2, Span>:
420	  match on:
421	    case True{}:
422	      Span{pline, pend, pcol} <> spans
423	    case False{}:
424	      check.no_span(pline, pend, pcol, spans)
425	
426	# the walk rebuilt; angle-closes are applied by the caller
427	def check.rebuild(
428	  _ticks: Nat,
429	  mode: Phase,
430	  paren: U32,
431	  bracket: U32,
432	  brace: U32,
433	  angle: U32,
434	  shut: Span,
435	  open: U32,
436	  on: Bool,
437	  pline: U32,
438	  pend: U32,
439	  pcol: U32,
440	  spans: List<&2, Span>
441	) -> Walk:
442	  Walk{mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans}
443	
444	# `(` opens the parameter list
445	def check.opened(
446	  ticks: Nat,
447	  bracket: U32,
448	  brace: U32,
449	  angle: U32,
450	  spans: List<&2, Span>,
451	  +ln: U32,
452	  _mode: Phase,
453	  _paren: U32,
454	  _shut: Span,
455	  _open: U32,
456	  _on: Bool,
457	  _pline: U32,
458	  _pend: U32,
459	  _pcol: U32
460	) -> Walk:
461	  check.rebuild(ticks, Args{}, 1, bracket, brace, angle, Span{0, 0, 0}, ln, False{}, 0, 0, 0, spans)
462	
463	# `)` ends the parameter list, and notes where it sits
464	def check.ended(
465	  ticks: Nat,
466	  _mode: Phase,
467	  paren: U32,
468	  bracket: U32,
469	  brace: U32,
470	  angle: U32,
471	  _shut: Span,
472	  open: U32,
473	  on: Bool,
474	  pline: U32,
475	  pend: U32,
476	  pcol: U32,
477	  spans: List<&2, Span>,
478	  +ln: U32,
479	  cl: U32
480	) -> Walk:
481	  check.rebuild(ticks, Shut{}, check.dec_u(paren), bracket, brace, angle, Span{ln, ln, cl}, open, False{},
482	    0, 0, 0, check.cons(on, pline, pend, pcol, spans))
483	
484	# a comma closes the parameter that was open
485	def check.commaed(
486	  ticks: Nat,
487	  mode: Phase,
488	  paren: U32,
489	  bracket: U32,
490	  brace: U32,
491	  angle: U32,
492	  shut: Span,
493	  open: U32,
494	  on: Bool,
495	  pline: U32,
496	  pend: U32,
497	  pcol: U32,
498	  spans: List<&2, Span>
499	) -> Walk:
500	  check.rebuild(ticks, mode, paren, bracket, brace, angle, shut, open, False{}, 0, 0, 0,
501	    check.cons(on, pline, pend, pcol, spans))
502	
503	# a run of `>` lowers the angle depth
504	def check.unangled(
505	  ticks: Nat,
506	  mode: Phase,
507	  paren: U32,
508	  bracket: U32,
509	  brace: U32,
510	  angle: U32,
511	  shut: Span,
512	  open: U32,
513	  on: Bool,
514	  pline: U32,
515	  pend: U32,
516	  pcol: U32,
517	  spans: List<&2, Span>
518	) -> Walk:
519	  check.rebuild(0n, mode, paren, bracket, brace, check.sub(ticks, angle), shut, open, on, pline, pend, pcol, spans)
520	
521	# a `->` on the `)` line puts the return type there; on a later line it does not
522	def check.turn(+ln: U32, shut: Span) -> Phase:
523	  Span{+line, _end, _col} = shut
524	  Bool.pick(Phase, U32.is_eq(ln, line), Past{}, Loose{})
525	
526	# the token's motion applied to fields already taken off the walk
527	def check.apply_on(
528	  motion: Act,
529	  mode: Phase,
530	  paren: U32,
531	  bracket: U32,
532	  brace: U32,
533	  angle: U32,
534	  +shut: Span,
535	  open: U32,
536	  on: Bool,
537	  pline: U32,
538	  pend: U32,
539	  pcol: U32,
540	  spans: List<&2, Span>,
541	  +ln: U32,
542	  cl: U32,
543	  ticks: Nat
544	) -> Walk:
545	  match motion:
546	    case AOpen{}:
547	      check.opened(ticks, bracket, brace, angle, spans, ln, mode, paren, shut, open, on, pline, pend, pcol)
548	    case AParen{}:
549	      check.rebuild(ticks, mode, (paren + 1 : U32), bracket, brace, angle, shut, open, on, pline, pend, pcol, spans)
550	    case AEnd{}:
551	      check.ended(ticks, mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans, ln, cl)
552	    case AUnparen{}:
553	      check.rebuild(ticks, mode, check.dec_u(paren), bracket, brace, angle, shut, open, on, pline, pend, pcol, spans)
554	    case ABrack{}:
555	      check.rebuild(ticks, mode, paren, (bracket + 1 : U32), brace, angle, shut, open, on, pline, pend, pcol, spans)
556	    case AUnbrack{}:
557	      check.rebuild(ticks, mode, paren, check.dec_u(bracket), brace, angle, shut, open, on, pline, pend, pcol, spans)
558	    case ABrace{}:
559	      check.rebuild(ticks, mode, paren, bracket, (brace + 1 : U32), angle, shut, open, on, pline, pend, pcol, spans)
560	    case AUnbrace{}:
561	      check.rebuild(ticks, mode, paren, bracket, check.dec_u(brace), angle, shut, open, on, pline, pend, pcol, spans)
562	    case AAngle{}:
563	      check.rebuild(ticks, mode, paren, bracket, brace, (angle + 1 : U32), shut, open, on, pline, pend, pcol, spans)
564	    case AUnangle{}:
565	      check.unangled(ticks, mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans)
566	    case AComma{}:
567	      check.commaed(ticks, mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans)
568	    case AArrow{}:
569	      check.rebuild(ticks, check.turn(ln, shut), paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans)
570	    case AStray{}:
571	      check.rebuild(ticks, Loose{}, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans)
572	    case ANone{}:
573	      check.rebuild(ticks, mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans)
574	
575	# the token's motion applied to the walk
576	def check.apply(motion: Act, wk: Walk, +ln: U32, cl: U32, ticks: Nat) -> Walk:
577	  Walk{mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans} = wk
578	  check.apply_on(motion, mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans, ln, cl, ticks)
579	
580	# the same parameter, extended to this line
581	def check.note_extend(
582	  +pline: U32,
583	  _pend: U32,
584	  +pcol: U32,
585	  +ln: U32,
586	  _cl: U32,
587	  mode: Phase,
588	  paren: U32,
589	  bracket: U32,
590	  brace: U32,
591	  angle: U32,
592	  shut: Span,
593	  open: U32,
594	  spans: List<&2, Span>
595	) -> Walk:
596	  Walk{mode, paren, bracket, brace, angle, shut, open, True{}, pline, ln, pcol, spans}
597	
598	# a parameter starting here
599	def check.note_begin(
600	  _pline: U32,
601	  _pend: U32,
602	  _pcol: U32,
603	  +ln: U32,
604	  +cl: U32,
605	  mode: Phase,
606	  paren: U32,
607	  bracket: U32,
608	  brace: U32,
609	  angle: U32,
610	  shut: Span,
611	  open: U32,
612	  spans: List<&2, Span>
613	) -> Walk:
614	  Walk{mode, paren, bracket, brace, angle, shut, open, True{}, ln, ln, cl, spans}
615	
616	# the token continues the open parameter, or starts one
617	def check.note_on(
618	  on: Bool,
619	  mode: Phase,
620	  paren: U32,
621	  bracket: U32,
622	  brace: U32,
623	  angle: U32,
624	  shut: Span,
625	  open: U32,
626	  pline: U32,
627	  pend: U32,
628	  pcol: U32,
629	  spans: List<&2, Span>,
630	  +ln: U32,
631	  +cl: U32
632	) -> Walk:
633	  match on:
634	    case True{}:
635	      check.note_extend(pline, pend, pcol, ln, cl, mode, paren, bracket, brace, angle, shut, open, spans)
636	    case False{}:
637	      check.note_begin(pline, pend, pcol, ln, cl, mode, paren, bracket, brace, angle, shut, open, spans)
638	
639	# outside the parameter list the token starts nothing
640	def check.note_skip(
641	  on: Bool,
642	  mode: Phase,
643	  paren: U32,
644	  bracket: U32,
645	  brace: U32,
646	  angle: U32,
647	  shut: Span,
648	  open: U32,
649	  pline: U32,
650	  pend: U32,
651	  pcol: U32,
652	  spans: List<&2, Span>,
653	  _tok: Lex.Tok
654	) -> Walk:
655	  Walk{mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans}
656	
657	# inside the parameter list, the token's position joins the open parameter
658	def check.note_here(
659	  on: Bool,
660	  mode: Phase,
661	  paren: U32,
662	  bracket: U32,
663	  brace: U32,
664	  angle: U32,
665	  shut: Span,
666	  open: U32,
667	  pline: U32,
668	  pend: U32,
669	  pcol: U32,
670	  spans: List<&2, Span>,
671	  tok: Lex.Tok
672	) -> Walk:
673	  Lex.Tok{_kk, _tx, +ln, +cl} = tok
674	  check.note_on(on, mode, paren, bracket, brace, angle, shut, open, pline, pend, pcol, spans, ln, cl)
675	
676	# inside the list the token is part of a parameter; outside it is not
677	def check.note_phase(
678	  mode: Phase,
679	  on: Bool,
680	  paren: U32,
681	  bracket: U32,
682	  brace: U32,
683	  angle: U32,
684	  shut: Span,
685	  open: U32,
686	  pline: U32,
687	  pend: U32,
688	  pcol: U32,
689	  spans: List<&2, Span>,
690	  tok: Lex.Tok
691	) -> Walk:
692	  match mode:
693	    case Args{}:
694	      check.note_here(on, Args{}, paren, bracket, brace, angle, shut, open, pline, pend, pcol, spans, tok)
695	    case other:
696	      check.note_skip(on, other, paren, bracket, brace, angle, shut, open, pline, pend, pcol, spans, tok)
697	
698	# a token that belongs to a parameter notes where that parameter sits
699	def check.note_args(wk: Walk, tok: Lex.Tok) -> Walk:
700	  Walk{mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans} = wk
701	  check.note_phase(mode, on, paren, bracket, brace, angle, shut, open, pline, pend, pcol, spans, tok)
702	
703	# a token the parameter list itself consumed
704	def check.drop_tok(_tok: Lex.Tok, wk: Walk) -> Walk:
705	  wk
706	
707	# note the token when it is part of a parameter
708	def check.maybe_note(sep: Bool, wk: Walk, tok: Lex.Tok) -> Walk:
709	  match sep:
710	    case True{}:
711	      check.drop_tok(tok, wk)
712	    case False{}:
713	      check.note_args(wk, tok)
714	
715	# one significant token
716	def check.step_hit(+wk: Walk, +tok: Lex.Tok, glued: Bool) -> Walk:
717	  Walk{+mode, +paren, +bracket, +brace, +angle, _shut, _open, _on, _pline, _pend, _pcol, _spans} = wk
718	  Lex.Tok{+kk, +tx, +ln, cl} = tok
719	  +motion = check.act(mode, kk, tx, glued, paren, angle, brace, bracket)
720	  check.maybe_note(check.is_sep(motion), check.apply(motion, wk, ln, cl, check.ticks_of(tx)), tok)
721	
722	# a space, a newline or a comment changes nothing
723	def check.step_skip(_tok: Lex.Tok, wk: Walk, _glued: Bool) -> Walk:
724	  wk
725	
726	# a significant token is read; a space, a newline or a comment is not
727	def check.step_on(sig: Bool, +tok: Lex.Tok, wk: Walk, glued: Bool) -> Walk:
728	  match sig:
729	    case True{}:
730	      check.step_hit(wk, tok, glued)
731	    case False{}:
732	      check.step_skip(tok, wk, glued)
733	
734	# one token of the header
735	def check.step(+tok: Lex.Tok, wk: Walk, glued: Bool) -> Walk:
736	  Lex.Tok{+kk, _tx, _ln, _cl} = tok
737	  check.step_on(Lex.significant(kk), tok, wk, glued)
738	
739	# the parameter still open at the end of the header
740	def check.seal(wk: Walk) -> Walk:
741	  Walk{mode, paren, bracket, brace, angle, shut, open, on, pline, pend, pcol, spans} = wk
742	  Walk{mode, paren, bracket, brace, angle, shut, open, False{}, 0, 0, 0, check.cons(on, pline, pend, pcol, spans)}
743	
744	# a name glues a following `<`
745	def check.glue_of(tok: Lex.Tok) -> Bool:
746	  Lex.Tok{kk, _tx, _ln, _cl} = tok
747	  Lex.is_name(kk)
748	
749	# every token of the header
750	def check.walk(toks: List<&2, Lex.Tok>, wk: Walk, glued: Bool) -> Walk:
751	  match toks:
752	    case Nil{}:
753	      check.seal(wk)
754	    case Con{+tok, rest}:
755	      check.walk(rest, check.step(tok, wk, glued), check.glue_of(tok))
756	
757	# another parameter already sits on this line
758	def check.shares(spans: List<&2, Span>, +ln: U32) -> Bool:
759	  match spans:
760	    case Nil{}:
761	      False{}
762	    case Con{Span{+line, _end, _col}, rest}:
763	      Lazy.or_else(U32.is_eq(line, ln), _u => check.shares(rest, ln))
764	
765	# split across lines, sitting on the `(` line, or sharing its line
766	def check.bad(sp: Span, +open: U32, spans: List<&2, Span>) -> Bool:
767	  Span{+line, +end, _col} = sp
768	  Lazy.or_else(Bool.not(U32.is_eq(line, end)),
769	    _u => Lazy.or_else(U32.is_eq(line, open), _u2 => check.shares(spans, line)))
770	
771	# the first parameter that is not alone on its own line
772	def check.judge(spans: List<&2, Span>, +open: U32) -> Maybe<&2, Span>:
773	  match spans:
774	    case Nil{}:
775	      None{}
776	    case Con{+sp, +rest}:
777	      Lazy.stop(Maybe<&2, Span>, check.bad(sp, open, rest), Some{sp}, _u => check.judge(rest, open))
778	
779	# the first parameter that breaks the shape, in source order
780	def check.jam_span(wk: Walk) -> Maybe<&2, Span>:
781	  Walk{_mode, _paren, _bracket, _brace, _angle, _shut, +open, _on, _pline, _pend, _pcol, spans} = wk
782	  check.judge(List.reverse(&2, Span, spans), open)
783	
784	# the last parameter (the head: spans are reversed) runs onto the `)` line
785	def check.tight(spans: List<&2, Span>, +close: U32) -> Bool:
786	  match spans:
787	    case Nil{}:
788	      False{}
789	    case Con{Span{_line, +end, _col}, _rest}:
790	      Bool.not(U32.is_lt(end, close))
791	
792	# the `)`, when it shares the last parameter's line
793	def check.shut_at(shut: Span, spans: List<&2, Span>) -> Maybe<&2, Span>:
794	  Span{+line, end, +col} = shut
795	  Bool.pick(Maybe<&2, Span>, check.tight(spans, line), Some{Span{line, end, col}}, None{})
796	
797	# the `)` of a list that did close, when it is not on a line after the last
798	# parameter
799	def check.shut_span(wk: Walk) -> Maybe<&2, Span>:
800	  Walk{mode, _paren, _bracket, _brace, _angle, shut, _open, _on, _pline, _pend, _pcol, spans} = wk
801	  match mode:
802	    case Seek{}:
803	      None{}
804	    case Args{}:
805	      None{}
806	    case other:
807	      check.shut_at(shut, spans)
808	
809	# the `)` with no `->` right after it on its line
810	def check.loose_span(wk: Walk) -> Maybe<&2, Span>:
811	  Walk{mode, _paren, _bracket, _brace, _angle, shut, _open, _on, _pline, _pend, _pcol, _spans} = wk
812	  match mode:
813	    case Shut{}:
814	      Some{shut}
815	    case Loose{}:
816	      Some{shut}
817	    case other:
818	      None{}
819	
820	# the `(` line, when the list holds no parameter
821	def check.none_at(spans: List<&2, Span>, +open: U32) -> Maybe<&2, Span>:
822	  match spans:
823	    case Nil{}:
824	      Some{Span{open, open, 0}}
825	    case Con{_sp, _rest}:
826	      None{}
827	
828	# a parameter list that opened and holds no parameter
829	def check.empty_span(wk: Walk) -> Maybe<&2, Span>:
830	  Walk{mode, _paren, _bracket, _brace, _angle, _shut, +open, _on, _pline, _pend, _pcol, spans} = wk
831	  match mode:
832	    case Seek{}:
833	      None{}
834	    case other:
835	      check.none_at(spans, open)
836	
837	# the return type off the `)` line, as a finding
838	def check.place_loose(
839	  mm: Maybe<&2, Span>,
840	  +base: U32,
841	  +path: String,
842	  +more: List<&2, F.Finding>
843	) -> List<&2, F.Finding>:
844	  match mm:
845	    case None{}:
846	      more
847	    case Some{Span{+line, _end, +col}}:
848	      F.Finding{path, (base + line : U32), col, 0, "wrap",
849	        "The return type is not on the `)` line; write `) -> T` on one line."}
850	        <> more
851	
852	# the `)` on the last parameter's line, as a finding, else the return type
853	# off the `)` line
854	def check.place_shut(
855	  mm: Maybe<&2, Span>,
856	  loose: Maybe<&2, Span>,
857	  +base: U32,
858	  +path: String,
859	  +more: List<&2, F.Finding>
860	) -> List<&2, F.Finding>:
861	  match mm:
862	    case None{}:
863	      check.place_loose(loose, base, path, more)
864	    case Some{Span{+line, _end, +col}}:
865	      F.Finding{path, (base + line : U32), col, 0, "wrap",
866	        "The `)` shares a line with the last parameter; put `)` and the return type on a line of their own."}
867	        <> more
868	
869	# an empty parameter list across lines, as a finding, else a misplaced `)`
870	def check.place_empty(
871	  mm: Maybe<&2, Span>,
872	  shut: Maybe<&2, Span>,
873	  loose: Maybe<&2, Span>,
874	  +base: U32,
875	  +path: String,
876	  +more: List<&2, F.Finding>
877	) -> List<&2, F.Finding>:
878	  match mm:
879	    case None{}:
880	      check.place_shut(shut, loose, base, path, more)
881	    case Some{Span{+line, _end, +col}}:
882	      F.Finding{path, (base + line : U32), col, 0, "wrap",
883	        "This def header has no parameters but spans several lines; put it on one line."}
884	        <> more
885	
886	# the parameter that breaks the shape, else an empty list, a misplaced `)` or
887	# a return type off its line, as a finding on the header's lines
888	def check.place(
889	  mm: Maybe<&2, Span>,
890	  empty: Maybe<&2, Span>,
891	  shut: Maybe<&2, Span>,
892	  loose: Maybe<&2, Span>,
893	  +base: U32,
894	  +path: String,
895	  +more: List<&2, F.Finding>
896	) -> List<&2, F.Finding>:
897	  match mm:
898	    case None{}:
899	      check.place_empty(empty, shut, loose, base, path, more)
900	    case Some{Span{+line, _end, +col}}:
901	      F.Finding{path, (base + line : U32), col, 0, "wrap",
902	        "This wrapped def header does not have one parameter per line; put each parameter on its own line."}
903	        <> more
904	
905	# a multi-line header that is not one parameter per line, holds no parameter,
906	# or whose `)` shares the last parameter's line or has no `->` after it
907	def check.jam(+line: U32, toks: List<&2, Lex.Tok>, +path: String, +more: List<&2, F.Finding>) -> List<&2, F.Finding>:
908	  +wk = check.walk(toks, check.start(), False{})
909	  check.place(check.jam_span(wk), check.empty_span(wk), check.shut_span(wk), check.loose_span(wk), line, path, more)
910	
911	# a one-line header past 120
912	def check.wide(+line: U32, toks: List<&2, Lex.Tok>, +path: String, +more: List<&2, F.Finding>) -> List<&2, F.Finding>:
913	  Lazy.stop(List<&2, F.Finding>, U32.is_gt(check.width(toks), 120),
914	    F.Finding{path, line, 120, 0, "wrap",
915	      "This def header is longer than 120 characters; wrap it with one parameter per line."} <> more, _u => more)
916	
917	# a broken header is judged by its shape; a one-line header by its width
918	def check.header(
919	  multi: Bool,
920	  +line: U32,
921	  toks: List<&2, Lex.Tok>,
922	  +path: String,
923	  +more: List<&2, F.Finding>
924	) -> List<&2, F.Finding>:
925	  match multi:
926	    case True{}:
927	      check.jam(line, toks, path, more)
928	    case False{}:
929	      check.wide(line, toks, path, more)
930	
931	# a def header's tokens, judged
932	def check.lexed(+line: U32, +toks: List<&2, Lex.Tok>, +path: String, +more: List<&2, F.Finding>) -> List<&2, F.Finding>:
933	  check.header(check.broken(toks), line, toks, path, more)
934	
935	# a def header; anything else is not this rule's
936	def check.one(
937	  kk: Outline.ItemKind,
938	  +line: U32,
939	  +sig: String,
940	  +path: String,
941	  +more: List<&2, F.Finding>
942	) -> List<&2, F.Finding>:
943	  Lazy.stop(List<&2, F.Finding>, Bool.not(Outline.is_def(kk)), more,
944	    _u => check.lexed(line, Lex.tokens(sig), path, more))
945	
946	# every def header of the file
947	def check.go(items: List<&2, Outline.Item>, +path: String) -> List<&2, F.Finding>:
948	  match items:
949	    case Nil{}:
950	      Nil{}
951	    case Con{Outline.Item{+kk, _name, +line, +sig, _doc, _pp}, rest}:
952	      +more = check.go(rest, path)
953	      check.one(kk, line, sig, path, more)
954	
955	# the rule
956	def check(ss: Src.Src) -> List<&2, F.Finding>:
957	  Src.Src{+path, _text, _toks, _tree, _bound, items} = ss
958	  check.go(items, path)