src/rules/style/wrap.bend

bolt@1.27.0.0 · 958 lines · 97 definitions

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.
17import Base
18import bolt@1.27.0.0/src/src.bend as Src
19import bolt@1.27.0.0/src/finding.bend as F
20import bolt@1.27.0.0/src/syntax/lex.bend as Lex
21import bolt@1.27.0.0/src/syntax/outline.bend as Outline
22import bolt@1.27.0.0/src/lazy/lazy.bend as Lazy
23import bolt@1.27.0.0/src/rules/style/space.bend as Space
24
25# where one parameter sits in the header: its first line, its last, its column
26type 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
31type Phase is Data:
32  Seek{}
33  Args{}
34  Past{}
35  Shut{}
36  Loose{}
37
38# what a token does to the bracket depths
39type 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)
57type 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
62def 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
70def 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
78def check.add(+acc: U32, kd: Lex.TokKind, +tx: String) -> U32:
79  (acc + check.cost(kd, tx) : U32)
80
81# a `:` token?
82def 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
92def 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
102def 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
106def check.start() -> Walk:
107  Walk{Seek{}, 0, 0, 0, 0, Span{0, 0, 0}, 0, False{}, 0, 0, 0, []}
108
109# `(`
110def 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# `)`
118def 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
126def 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
132def 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
140def 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
146def 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
154def 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 `>`
162def 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 `>`
170def 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
174def 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
183def 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
187def 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
191def check.drop_close(_closed: Act) -> Act:
192  AAngle{}
193
194# an angle open wins over a close; otherwise the close stands
195def 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
203def 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
208def check.no_angle(_tx: String, _glued: Bool) -> Act:
209  ANone{}
210
211# an operator's angle motion
212def 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
220def 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
224def 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
228def 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
236def 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
244def 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
248def 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
254def 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
260def 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
268def 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
276def 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
289def 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
297def 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
305def 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
313def 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
321def 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
335def 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# `->`
347def 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
356def 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
368def 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
391def 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
403def 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
407def 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
415def 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
419def 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
427def 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
445def 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
464def 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
485def 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
504def 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
522def 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
527def 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
576def 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
581def 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
599def 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
617def 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
640def 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
658def 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
677def 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
699def 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
704def check.drop_tok(_tok: Lex.Tok, wk: Walk) -> Walk:
705  wk
706
707# note the token when it is part of a parameter
708def 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
716def 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
723def 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
727def 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
735def 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
740def 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 `<`
745def 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
750def 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
758def 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
766def 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
772def 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
780def 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
785def 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
793def 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
799def 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
810def 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
821def 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
829def 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
838def 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
854def 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 `)`
870def 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
888def 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
907def 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
912def 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
918def 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
932def 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
936def 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
947def 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
956def check(ss: Src.Src) -> List<&2, F.Finding>:
957  Src.Src{+path, _text, _toks, _tree, _bound, items} = ss
958  check.go(items, path)