1	# shake/cli: the parser behind main.bend, internal. `parse` reads argv
2	# against a Cli; `help` writes usage for a command path, and `help` is the
3	# subcommand that asks for it (`--help` too, unless the command declares its
4	# own long `help`). A `--` that reaches `parse` ends option parsing; in a
5	# compiled program the runtime takes the first `--` itself.
6	import Base
7	
8	# a flag, a valued option, an option that may repeat, a positional, or a rest
9	# positional
10	type ArgKind is Data:
11	  Flag{}
12	  Opt{}
13	  Pos{}
14	  Rest{}
15	  Many{}
16	
17	# what an argument the words leave unbound falls back to: the value of its
18	# env var, when `parse_env` is given one, else its default
19	type Fallback is Data:
20	  Fallback{env: Maybe<&2, String>, default: Maybe<&2, String>}
21	
22	# one argument: name is the binding key; short/long are the CLI spellings
23	type Arg is Data:
24	  Arg{
25	    name: String,
26	    short: Maybe<&2, String>,
27	    long: Maybe<&2, String>,
28	    kind: ArgKind,
29	    help: String,
30	    required: Bool,
31	    fallback: Fallback,
32	    choices: List<&2, String>
33	  }
34	
35	# a nested command
36	type Sub is Data:
37	  Sub{
38	    name: String,
39	    about: String,
40	    args: List<&2, Arg>,
41	    subcommands: List<&2, Sub>
42	  }
43	
44	# the program: name, about, optional version, top-level args and commands
45	type Cli is Data:
46	  Cli{
47	    name: String,
48	    about: String,
49	    version: Maybe<&2, String>,
50	    args: List<&2, Arg>,
51	    subcommands: List<&2, Sub>
52	  }
53	
54	# an env var's name and its value, as `parse_env` is given them
55	def Var() -> Data:
56	  Sigma<&2, &2, String, _ => String>
57	
58	# one bound name and its text
59	type Bind is Data:
60	  Bind{name: String, value: String}
61	
62	# one command above the current one: its arguments and the bindings made
63	# while it was current
64	type Level is Data:
65	  Level{args: List<&2, Arg>, binds: List<&2, Bind>}
66	
67	# a successful parse, read one command at a time, as clap's ArgMatches: the
68	# bindings the command made, in binding order, and, when a subcommand was
69	# selected under it, that subcommand's name and Matched
70	type Matched is Data:
71	  Leaf{+binds: List<&2, Bind>}
72	  Node{+binds: List<&2, Bind>, +name: String, +sub: Matched}
73	
74	# a failed parse. NeedHelp is `help` / `help <path>` (or `--help`, `-h`),
75	# NeedVersion `--version` (or `-V`); NoValue is an option whose value never
76	# came, Missing a required argument nothing bound. Every error but NeedHelp
77	# and NeedVersion carries `at`, the command path selected where it failed
78	type ParseErr is Data:
79	  UnknownFlag{at: List<&2, String>, flag: String}
80	  Missing{at: List<&2, String>, name: String}
81	  NoValue{at: List<&2, String>, name: String}
82	  BadValue{at: List<&2, String>, name: String, value: String}
83	  NeedHelp{path: List<&2, String>}
84	  Unexpected{at: List<&2, String>, arg: String}
85	  Repeated{at: List<&2, String>, name: String}
86	  NeedVersion{}
87	
88	# how the next token is read
89	type Mode is Data:
90	  Free{}
91	  Need{name: String}
92	  Help{}
93	  Dead{err: ParseErr}
94	
95	# the walker: the current command's arguments, the commands above it (the
96	# nearest first, one per name of the selected path), its subcommands, the
97	# selected path, and the current command's own bindings
98	type St is Data:
99	  St{
100	    mode: Mode,
101	    args: List<&2, Arg>,
102	    up: List<&2, Level>,
103	    subs: List<&2, Sub>,
104	    path: List<&2, String>,
105	    binds: List<&2, Bind>,
106	    pos: List<&2, Arg>,
107	    raw: Bool,
108	    seen: Bool
109	  }
110	
111	# the page a help walk has reached
112	type How is Data:
113	  How{
114	    bin: String,
115	    about: String,
116	    version: Maybe<&2, String>,
117	    args: List<&2, Arg>,
118	    subs: List<&2, Sub>,
119	    usage: String
120	  }
121	
122	# a program spec
123	def app(
124	  +name: String,
125	  +about: String,
126	  version: Maybe<&2, String>,
127	  args: List<&2, Arg>,
128	  subs: List<&2, Sub>
129	) -> Cli:
130	  Cli{name, about, version, args, subs}
131	
132	# a nested command
133	def sub(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
134	  +name: String,
135	  +about: String,
136	  args: List<&2, Arg>,
137	  subs: List<&2, Sub>
138	) -> Sub:
139	  Sub{name, about, args, subs}
140	
141	# a boolean flag
142	def flag(
143	  +name: String,
144	  short: Maybe<&2, String>,
145	  long: Maybe<&2, String>,
146	  +help: String
147	) -> Arg:
148	  Arg{name, short, long, Flag{}, help, False{}, Fallback{None{}, None{}}, []}
149	
150	# a valued option
151	def opt(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
152	  +name: String,
153	  short: Maybe<&2, String>,
154	  long: Maybe<&2, String>,
155	  +help: String,
156	  required: Bool,
157	  default: Maybe<&2, String>,
158	  choices: List<&2, String>
159	) -> Arg:
160	  Arg{name, short, long, Opt{}, help, required, Fallback{None{}, default}, choices}
161	
162	# an option that may be given more than once; `get_all` reads every value
163	def many(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
164	  +name: String,
165	  short: Maybe<&2, String>,
166	  long: Maybe<&2, String>,
167	  +help: String,
168	  required: Bool,
169	  default: Maybe<&2, String>,
170	  choices: List<&2, String>
171	) -> Arg:
172	  Arg{name, short, long, Many{}, help, required, Fallback{None{}, default}, choices}
173	
174	# a positional
175	def pos(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
176	  +name: String,
177	  +help: String,
178	  required: Bool,
179	  default: Maybe<&2, String>,
180	  choices: List<&2, String>
181	) -> Arg:
182	  Arg{name, None{}, None{}, Pos{}, help, required, Fallback{None{}, default}, choices}
183	
184	# a rest positional: every leftover word, as one name
185	def rest(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
186	  +name: String,
187	  +help: String,
188	  required: Bool,
189	  default: Maybe<&2, String>,
190	  choices: List<&2, String>
191	) -> Arg:
192	  Arg{name, None{}, None{}, Rest{}, help, required, Fallback{None{}, default}, choices}
193	
194	# this argument, falling back to the env var `var` (clap's `.env`)
195	def env(aa: Arg, +var: String) -> Arg:
196	  Arg{+n, +s, +l, kk, +h, +r, Fallback{_e, dd}, cs} = aa
197	  Arg{n, s, l, kk, h, r, Fallback{Some{var}, dd}, cs}
198	
199	# the larger of two Nats
200	def help.max(+aa: Nat, +bb: Nat) -> Nat:
201	  Bool.pick(Nat, Nat.is_le(aa, bb), bb, aa)
202	
203	# n spaces
204	def help.spaces(nn: Nat) -> String:
205	  match nn:
206	    case 0n:
207	      ""
208	    case 1n+p:
209	      " " ++ help.spaces(p)
210	
211	# s padded on the right to width n
212	def help.pad(+ss: String, nn: Nat) -> String:
213	  ss ++ help.spaces(Nat.sub(nn, String.length(ss)))
214	
215	# a Maybe string's text, or the default
216	def text.of(mm: Maybe<&2, String>, +dd: String) -> String:
217	  Maybe.default(&2, String, mm, dd)
218	
219	# whether a string is a flag token (`-` alone is not)
220	def looks_flag(+ss: String) -> Bool:
221	  Bool.and(String.starts_with(ss, "-"), Bool.not(String.eq(ss, "-")))
222	
223	# a buffer of chars consed on the front (the last read first), folded onto acc
224	def from.rev.go(cs: List<&2, Char>, acc: String) -> String:
225	  match cs:
226	    case Nil{}:
227	      acc
228	    case Con{+h, t}:
229	      from.rev.go(t, SCon{h, acc})
230	
231	# chars reversed into a string
232	def from.rev(cs: List<&2, Char>) -> String:
233	  from.rev.go(cs, SNil{})
234	
235	# `name` and an optional `=value`, once the next char is known
236	def cut_eq.pick(
237	  eq: Bool,
238	  acc: List<&2, Char>,
239	  tt: List<&2, Char>,
240	  rest: String & Maybe<&2, String>
241	) -> String & Maybe<&2, String>:
242	  match eq:
243	    case True{}:
244	      (from.rev(acc), Some{String.from_list(tt)})
245	    case False{}:
246	      rest
247	
248	# one char of a `name=value` cut
249	def cut_eq.chr(
250	  +cc: Char,
251	  tt: List<&2, Char>,
252	  acc: List<&2, Char>,
253	  rest: String & Maybe<&2, String>
254	) -> String & Maybe<&2, String>:
255	  cut_eq.pick(Char.is_eq(cc, '='), acc, tt, rest)
256	
257	# `name` and an optional `=value` from the body after `--`
258	def cut_eq.go(
259	  cs: List<&2, Char>,
260	  +acc: List<&2, Char>
261	) -> String & Maybe<&2, String>:
262	  match cs:
263	    case Nil{}:
264	      (from.rev(acc), None{})
265	    case Con{+c, +t}:
266	      cut_eq.chr(c, t, acc, cut_eq.go(t, c <> acc))
267	
268	# `name` and an optional `=value`
269	def cut_eq(ss: String) -> String & Maybe<&2, String>:
270	  cut_eq.go(String.to_list(ss), [])
271	
272	# the value glued after a short letter: what follows one `=` when the rest
273	# starts with it (possibly empty, as `--name=` is), else the rest when there
274	# is any
275	def short_of.val(eq: Bool, +rest: String) -> Maybe<&2, String>:
276	  match eq:
277	    case True{}:
278	      Some{String.drop(rest, 1n)}
279	    case False{}:
280	      Bool.pick(Maybe<&2, String>, String.is_empty(rest), None{}, Some{rest})
281	
282	# whether this Arg's long spelling is `name`
283	def by_long.hit(aa: Arg, +name: String) -> Bool:
284	  Arg{_n, _s, long, _k, _h, _r, _d, _c} = aa
285	  String.eq(text.of(long, ""), name)
286	
287	# this Arg when the long spelling matches, else the rest
288	def by_long.at(hit: Bool, hh: Arg, rest: Maybe<&2, Arg>) -> Maybe<&2, Arg>:
289	  match hit:
290	    case True{}:
291	      Some{hh}
292	    case False{}:
293	      rest
294	
295	# the Arg with this long spelling, if any
296	def by_long(args: List<&2, Arg>, +name: String) -> Maybe<&2, Arg>:
297	  match args:
298	    case Nil{}:
299	      None{}
300	    case Con{+h, t}:
301	      by_long.at(by_long.hit(h, name), h, by_long(t, name))
302	
303	# whether this Arg's short spelling is `name`
304	def by_short.hit(aa: Arg, +name: String) -> Bool:
305	  Arg{_n, short, _l, _k, _h, _r, _d, _c} = aa
306	  String.eq(text.of(short, ""), name)
307	
308	# this Arg when the short spelling matches, else the rest
309	def by_short.at(hit: Bool, hh: Arg, rest: Maybe<&2, Arg>) -> Maybe<&2, Arg>:
310	  match hit:
311	    case True{}:
312	      Some{hh}
313	    case False{}:
314	      rest
315	
316	# the Arg with this short spelling, if any
317	def by_short(args: List<&2, Arg>, +name: String) -> Maybe<&2, Arg>:
318	  match args:
319	    case Nil{}:
320	      None{}
321	    case Con{+h, t}:
322	      by_short.at(by_short.hit(h, name), h, by_short(t, name))
323	
324	# whether this Arg's name is `name`
325	def by_name.hit(aa: Arg, +name: String) -> Bool:
326	  Arg{+n, _s, _l, _k, _h, _r, _d, _c} = aa
327	  String.eq(n, name)
328	
329	# this Arg when the binding name matches, else the rest
330	def by_name.at(hit: Bool, hh: Arg, rest: Maybe<&2, Arg>) -> Maybe<&2, Arg>:
331	  match hit:
332	    case True{}:
333	      Some{hh}
334	    case False{}:
335	      rest
336	
337	# the Arg with this binding name, if any
338	def by_name(args: List<&2, Arg>, +name: String) -> Maybe<&2, Arg>:
339	  match args:
340	    case Nil{}:
341	      None{}
342	    case Con{+h, t}:
343	      by_name.at(by_name.hit(h, name), h, by_name(t, name))
344	
345	# this Sub when its name matches, else the rest
346	def find_sub.at(ss: Sub, rest: Maybe<&2, Sub>, +name: String) -> Maybe<&2, Sub>:
347	  Sub{+n, _a, _g, _c} = ss
348	  Bool.pick(Maybe<&2, Sub>, String.eq(n, name), Some{ss}, rest)
349	
350	# the Sub with this name, if any
351	def find_sub(subs: List<&2, Sub>, +name: String) -> Maybe<&2, Sub>:
352	  match subs:
353	    case Nil{}:
354	      None{}
355	    case Con{+h, t}:
356	      find_sub.at(h, find_sub(t, name), name)
357	
358	# whether this Arg is a positional
359	def pos.is.kind(kk: ArgKind) -> Bool:
360	  match kk:
361	    case Pos{}:
362	      True{}
363	    case Rest{}:
364	      True{}
365	    case Flag{}:
366	      False{}
367	    case Opt{}:
368	      False{}
369	    case Many{}:
370	      False{}
371	
372	# whether this ArgKind is rest
373	def rest.is.kind(kk: ArgKind) -> Bool:
374	  match kk:
375	    case Rest{}:
376	      True{}
377	    case Pos{}:
378	      False{}
379	    case Flag{}:
380	      False{}
381	    case Opt{}:
382	      False{}
383	    case Many{}:
384	      False{}
385	
386	# whether this Arg is a positional
387	def pos.is(aa: Arg) -> Bool:
388	  Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
389	  pos.is.kind(kind)
390	
391	# whether this Arg is a rest positional
392	def rest.is(aa: Arg) -> Bool:
393	  Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
394	  rest.is.kind(kind)
395	
396	# this Arg kept when it is a positional
397	def pos_of.put(keep: Bool, hh: Arg, rest: List<&2, Arg>) -> List<&2, Arg>:
398	  match keep:
399	    case True{}:
400	      hh <> rest
401	    case False{}:
402	      rest
403	
404	# the positionals of a spec, in order
405	def pos_of(args: List<&2, Arg>) -> List<&2, Arg>:
406	  match args:
407	    case Nil{}:
408	      Nil{}
409	    case Con{+h, t}:
410	      pos_of.put(pos.is(h), h, pos_of(t))
411	
412	# whether `v` is among the choices; an empty list accepts any value
413	def allowed.ok.at(hit: Bool, rest: Bool) -> Bool:
414	  match hit:
415	    case True{}:
416	      True{}
417	    case False{}:
418	      rest
419	
420	# whether `v` is listed; the empty list answers no
421	def allowed.ok(cs: List<&2, String>, +vv: String) -> Bool:
422	  match cs:
423	    case Nil{}:
424	      False{}
425	    case Con{+h, t}:
426	      allowed.ok.at(String.eq(h, vv), allowed.ok(t, vv))
427	
428	# empty choices accept any value; otherwise `v` must be listed
429	def allowed(+cs: List<&2, String>, +vv: String) -> Bool:
430	  Bool.or(List.is_empty(&2, String, cs), allowed.ok(cs, vv))
431	
432	# whether this bind's name is `name`
433	def bound.hit(bb: Bind, +name: String) -> Bool:
434	  Bind{+n, _v} = bb
435	  String.eq(n, name)
436	
437	# True when the head matches, else the rest
438	def bound.at(hit: Bool, rest: Bool) -> Bool:
439	  match hit:
440	    case True{}:
441	      True{}
442	    case False{}:
443	      rest
444	
445	# whether `name` is already bound
446	def bound(bs: List<&2, Bind>, +name: String) -> Bool:
447	  match bs:
448	    case Nil{}:
449	      False{}
450	    case Con{+h, t}:
451	      bound.at(bound.hit(h, name), bound(t, name))
452	
453	# this bind's value when the name matches, else the rest
454	def get_all.bind.hit(
455	  hit: Bool,
456	  +vv: String,
457	  more: List<&2, String>
458	) -> List<&2, String>:
459	  match hit:
460	    case True{}:
461	      vv <> more
462	    case False{}:
463	      more
464	
465	# this bind's value when the name matches, else the rest
466	def get_all.bind.at(
467	  bb: Bind,
468	  more: List<&2, String>,
469	  +name: String
470	) -> List<&2, String>:
471	  Bind{+n, v} = bb
472	  get_all.bind.hit(String.eq(n, name), v, more)
473	
474	# every value bound to `name`
475	def get_all.bind(bs: List<&2, Bind>, +name: String) -> List<&2, String>:
476	  match bs:
477	    case Nil{}:
478	      []
479	    case Con{+h, t}:
480	      get_all.bind.at(h, get_all.bind(t, name), name)
481	
482	# the bindings this command made, in binding order
483	def own(mm: Matched) -> List<&2, Bind>:
484	  match mm:
485	    case Leaf{bs}:
486	      bs
487	    case Node{bs, _n, _s}:
488	      bs
489	
490	# every value this command bound to `name`
491	def get_all(mm: Matched, +name: String) -> List<&2, String>:
492	  get_all.bind(own(mm), name)
493	
494	# the last of a list of values, or `dflt` when it is empty
495	def get.last(vs: List<&2, String>, dflt: Maybe<&2, String>) -> Maybe<&2, String>:
496	  match vs:
497	    case Nil{}:
498	      dflt
499	    case Con{hh, tt}:
500	      get.last(tt, Some{hh})
501	
502	# the value bound to `name` last, or None when nothing bound it
503	def get(mm: Matched, +name: String) -> Maybe<&2, String>:
504	  get.last(get_all(mm, name), None{})
505	
506	# whether a value is `true`
507	def on.of(mv: Maybe<&2, String>) -> Bool:
508	  match mv:
509	    case None{}:
510	      False{}
511	    case Some{vv}:
512	      String.eq(vv, "true")
513	
514	# whether a flag named `name` was set
515	def on(mm: Matched, +name: String) -> Bool:
516	  on.of(get(mm, name))
517	
518	# the names of the subcommands selected below this command, in order
519	def path_of(mm: Matched) -> List<&2, String>:
520	  match mm:
521	    case Leaf{_b}:
522	      []
523	    case Node{_b, +name, next}:
524	      name <> path_of(next)
525	
526	# the name of the subcommand selected under this command
527	def sub_name(mm: Matched) -> Maybe<&2, String>:
528	  match mm:
529	    case Leaf{_b}:
530	      None{}
531	    case Node{_b, name, _s}:
532	      Some{name}
533	
534	# a subcommand's Matched when it is the one asked for
535	def sub_of.pick(hit: Bool, next: Matched) -> Maybe<&2, Matched>:
536	  match hit:
537	    case True{}:
538	      Some{next}
539	    case False{}:
540	      None{}
541	
542	# the Matched of subcommand `name`, when it is the one selected
543	def sub_of(mm: Matched, +name: String) -> Maybe<&2, Matched>:
544	  match mm:
545	    case Leaf{_b}:
546	      None{}
547	    case Node{_b, nn, next}:
548	      sub_of.pick(String.eq(nn, name), next)
549	
550	# one name further down, when there is still a Matched to go down from
551	def at.step(cur: Maybe<&2, Matched>, +name: String) -> Maybe<&2, Matched>:
552	  match cur:
553	    case None{}:
554	      None{}
555	    case Some{mm}:
556	      sub_of(mm, name)
557	
558	# the rest of a path, followed from where the walk down stands
559	def at.go(path: List<&2, String>, cur: Maybe<&2, Matched>) -> Maybe<&2, Matched>:
560	  match path:
561	    case Nil{}:
562	      cur
563	    case Con{+hh, tt}:
564	      at.go(tt, at.step(cur, hh))
565	
566	# the Matched of the command `path` names below this one, name by name, or
567	# None where a name is not the subcommand selected
568	def at(mm: Matched, path: List<&2, String>) -> Maybe<&2, Matched>:
569	  at.go(path, Some{mm})
570	
571	# the starting walker for a Cli
572	def parse.start(app: Cli) -> St:
573	  Cli{_n, _a, _v, +args, subs} = app
574	  St{Free{}, args, [], subs, [], [], pos_of(args), False{}, False{}}
575	
576	# a failed walker that keeps the rest of the state
577	def parse.dead(
578	  ee: ParseErr,
579	  +args: List<&2, Arg>,
580	  +up: List<&2, Level>,
581	  +subs: List<&2, Sub>,
582	  +path: List<&2, String>,
583	  +binds: List<&2, Bind>,
584	  pos: List<&2, Arg>,
585	  +raw: Bool,
586	  +seen: Bool
587	) -> St:
588	  St{Dead{ee}, args, up, subs, path, binds, pos, raw, seen}
589	
590	# a successful bind of `name` to `val`
591	def parse.put(
592	  +name: String,
593	  +val: String,
594	  +args: List<&2, Arg>,
595	  +up: List<&2, Level>,
596	  +subs: List<&2, Sub>,
597	  +path: List<&2, String>,
598	  +binds: List<&2, Bind>,
599	  +pos: List<&2, Arg>,
600	  +raw: Bool,
601	  +seen: Bool
602	) -> St:
603	  St{Free{}, args, up, subs, path, Bind{name, val} <> binds, pos, raw, seen}
604	
605	# the choices of a found Arg, or none
606	def parse.choices(mm: Maybe<&2, Arg>) -> List<&2, String>:
607	  match mm:
608	    case None{}:
609	      []
610	    case Some{a}:
611	      Arg{_n, _s, _l, _k, _h, _r, _d, cs} = a
612	      cs
613	
614	# bind `name` to `val` when the value is allowed
615	def parse.take_choice(
616	  ok: Bool,
617	  +name: String,
618	  +val: String,
619	  +args: List<&2, Arg>,
620	  +up: List<&2, Level>,
621	  +subs: List<&2, Sub>,
622	  +path: List<&2, String>,
623	  +binds: List<&2, Bind>,
624	  +pos: List<&2, Arg>,
625	  +raw: Bool,
626	  +seen: Bool
627	) -> St:
628	  match ok:
629	    case True{}:
630	      parse.put(name, val, args, up, subs, path, binds, pos, raw, seen)
631	    case False{}:
632	      parse.dead(BadValue{path, name, val}, args, up, subs, path, binds, pos, raw, seen)
633	
634	# bind an option that already has its value, checked against the choices of
635	# the current command's argument of that name: a parent's argument of the same
636	# name has its own
637	def parse.take_opt_val(
638	  +name: String,
639	  +val: String,
640	  +args: List<&2, Arg>,
641	  +up: List<&2, Level>,
642	  +subs: List<&2, Sub>,
643	  +path: List<&2, String>,
644	  +binds: List<&2, Bind>,
645	  +pos: List<&2, Arg>,
646	  +raw: Bool,
647	  +seen: Bool
648	) -> St:
649	  parse.take_choice(allowed(parse.choices(by_name(args, name)), val), name, val,
650	    args, up, subs, path, binds, pos, raw, seen)
651	
652	# a flag with no glued value is set; a glued value is unexpected
653	def parse.take_flag(
654	  val: Maybe<&2, String>,
655	  +name: String,
656	  +orig: String,
657	  +args: List<&2, Arg>,
658	  +up: List<&2, Level>,
659	  +subs: List<&2, Sub>,
660	  +path: List<&2, String>,
661	  +binds: List<&2, Bind>,
662	  pos: List<&2, Arg>,
663	  +raw: Bool,
664	  +seen: Bool
665	) -> St:
666	  match val:
667	    case None{}:
668	      parse.put(name, "true", args, up, subs, path, binds, pos, raw, seen)
669	    case Some{_v}:
670	      parse.dead(Unexpected{path, orig}, args, up, subs, path, binds, pos, raw, seen)
671	
672	# an option: glued value now, or the next token
673	def parse.take_opt(
674	  val: Maybe<&2, String>,
675	  +name: String,
676	  +args: List<&2, Arg>,
677	  +up: List<&2, Level>,
678	  +subs: List<&2, Sub>,
679	  +path: List<&2, String>,
680	  +binds: List<&2, Bind>,
681	  +pos: List<&2, Arg>,
682	  +raw: Bool,
683	  +seen: Bool
684	) -> St:
685	  match val:
686	    case None{}:
687	      St{Need{name}, args, up, subs, path, binds, pos, raw, seen}
688	    case Some{v}:
689	      parse.take_opt_val(name, v, args, up, subs, path, binds, pos, raw, seen)
690	
691	# a flag or single-valued option given again is refused, whatever the walk
692	# would have done with it; the walker keeps the rest of its state
693	def parse.once(again: Bool, st: St, +name: String, +path: List<&2, String>) -> St:
694	  match again:
695	    case True{}:
696	      St{_m, +args, +up, +subs, _p, +binds, +pos, +raw, +seen} = st
697	      St{Dead{Repeated{path, name}}, args, up, subs, path, binds, pos, raw, seen}
698	    case False{}:
699	      st
700	
701	# dispatch on the found Arg's kind
702	def parse.take_arg.kind(
703	  kk: ArgKind,
704	  +name: String,
705	  val: Maybe<&2, String>,
706	  +orig: String,
707	  +args: List<&2, Arg>,
708	  +up: List<&2, Level>,
709	  +subs: List<&2, Sub>,
710	  +path: List<&2, String>,
711	  +binds: List<&2, Bind>,
712	  +pos: List<&2, Arg>,
713	  +raw: Bool,
714	  +seen: Bool
715	) -> St:
716	  match kk:
717	    case Flag{}:
718	      parse.once(bound(binds, name), parse.take_flag(val, name, orig, args, up, subs, path,
719	        binds, pos, raw, seen), name, path)
720	    case Opt{}:
721	      parse.once(bound(binds, name), parse.take_opt(val, name, args, up, subs, path, binds, pos,
722	        raw, seen), name, path)
723	    case Many{}:
724	      parse.take_opt(val, name, args, up, subs, path, binds, pos, raw, seen)
725	    case Pos{}:
726	      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
727	    case Rest{}:
728	      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
729	
730	# a found Arg, or an unknown flag
731	def parse.take_arg(
732	  found: Maybe<&2, Arg>,
733	  val: Maybe<&2, String>,
734	  +orig: String,
735	  +args: List<&2, Arg>,
736	  +up: List<&2, Level>,
737	  +subs: List<&2, Sub>,
738	  +path: List<&2, String>,
739	  +binds: List<&2, Bind>,
740	  pos: List<&2, Arg>,
741	  +raw: Bool,
742	  +seen: Bool
743	) -> St:
744	  match found:
745	    case None{}:
746	      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
747	    case Some{a}:
748	      Arg{+name, _s, _l, kind, _h, _r, _d, _c} = a
749	      parse.take_arg.kind(kind, name, val, orig, args, up, subs, path, binds, pos,
750	        raw, seen)
751	
752	# whether an unknown long option is a request for help: a bare `--help`,
753	# with no `=` value, before any positional of the current command is bound
754	def long_help(+name: String, val: Maybe<&2, String>, seen: Bool) -> Bool:
755	  match val:
756	    case None{}:
757	      Bool.and(String.eq(name, "help"), Bool.not(seen))
758	    case Some{_v}:
759	      False{}
760	
761	# an unknown long option: a request for help (`--help`, as `help`), or an
762	# unknown flag
763	def parse.take_long.help(
764	  hit: Bool,
765	  +orig: String,
766	  +args: List<&2, Arg>,
767	  +up: List<&2, Level>,
768	  +subs: List<&2, Sub>,
769	  +path: List<&2, String>,
770	  +binds: List<&2, Bind>,
771	  +pos: List<&2, Arg>,
772	  +raw: Bool,
773	  +seen: Bool
774	) -> St:
775	  match hit:
776	    case True{}:
777	      St{Help{}, args, up, subs, path, binds, pos, raw, seen}
778	    case False{}:
779	      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
780	
781	# a long option the current command spells, or an unknown one
782	def parse.take_long.found(
783	  found: Maybe<&2, Arg>,
784	  +name: String,
785	  val: Maybe<&2, String>,
786	  +orig: String,
787	  +args: List<&2, Arg>,
788	  +up: List<&2, Level>,
789	  +subs: List<&2, Sub>,
790	  +path: List<&2, String>,
791	  +binds: List<&2, Bind>,
792	  +pos: List<&2, Arg>,
793	  +raw: Bool,
794	  +seen: Bool
795	) -> St:
796	  match found:
797	    case None{}:
798	      parse.take_long.help(long_help(name, val, seen), orig, args, up, subs, path,
799	        binds, pos, raw, seen)
800	    case Some{a}:
801	      parse.take_arg(Some{a}, val, orig, args, up, subs, path, binds, pos, raw, seen)
802	
803	# a long option with a name, or `--=...`
804	def parse.take_long.named(
805	  empty: Bool,
806	  +name: String,
807	  val: Maybe<&2, String>,
808	  +orig: String,
809	  +args: List<&2, Arg>,
810	  +up: List<&2, Level>,
811	  +subs: List<&2, Sub>,
812	  +path: List<&2, String>,
813	  +binds: List<&2, Bind>,
814	  +pos: List<&2, Arg>,
815	  +raw: Bool,
816	  +seen: Bool
817	) -> St:
818	  match empty:
819	    case True{}:
820	      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
821	    case False{}:
822	      parse.take_long.found(by_long(args, name), name, val, orig, args, up, subs,
823	        path, binds, pos, raw, seen)
824	
825	# a long option after the `=` cut
826	def parse.take_long.cut(
827	  nv: String & Maybe<&2, String>,
828	  +orig: String,
829	  +args: List<&2, Arg>,
830	  +up: List<&2, Level>,
831	  +subs: List<&2, Sub>,
832	  +path: List<&2, String>,
833	  +binds: List<&2, Bind>,
834	  pos: List<&2, Arg>,
835	  +raw: Bool,
836	  +seen: Bool
837	) -> St:
838	  (+name, val) = nv
839	  parse.take_long.named(String.is_empty(name), name, val, orig, args, up, subs,
840	    path, binds, pos, raw, seen)
841	
842	# a long option body after `--`
843	def parse.take_long(
844	  body: String,
845	  +orig: String,
846	  +args: List<&2, Arg>,
847	  +up: List<&2, Level>,
848	  +subs: List<&2, Sub>,
849	  +path: List<&2, String>,
850	  +binds: List<&2, Bind>,
851	  +pos: List<&2, Arg>,
852	  +raw: Bool,
853	  +seen: Bool
854	) -> St:
855	  parse.take_long.cut(cut_eq(body), orig, args, up, subs, path, binds, pos, raw,
856	    seen)
857	
858	# a flag's value in a cluster: the rest when it starts with `=` (which
859	# `take_arg` refuses), else none, so the next letter goes on
860	def cluster.val.flag(eq: Bool, +rest: String) -> Maybe<&2, String>:
861	  match eq:
862	    case True{}:
863	      Some{rest}
864	    case False{}:
865	      None{}
866	
867	# the value a letter of this kind gives its argument: an option takes the
868	# rest of the word, after one `=`
869	def cluster.val.kind(kk: ArgKind, +rest: String) -> Maybe<&2, String>:
870	  match kk:
871	    case Flag{}:
872	      cluster.val.flag(String.starts_with(rest, "="), rest)
873	    case Opt{}:
874	      short_of.val(String.starts_with(rest, "="), rest)
875	    case Many{}:
876	      short_of.val(String.starts_with(rest, "="), rest)
877	    case Pos{}:
878	      None{}
879	    case Rest{}:
880	      None{}
881	
882	# the value the letter's argument gets, or none when no argument has it
883	def cluster.val(found: Maybe<&2, Arg>, +rest: String) -> Maybe<&2, String>:
884	  match found:
885	    case None{}:
886	      None{}
887	    case Some{aa}:
888	      Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
889	      cluster.val.kind(kind, rest)
890	
891	# whether a letter of this kind ends the cluster: every kind but a flag that
892	# is not followed by `=`
893	def cluster.ends.kind(kk: ArgKind, +rest: String) -> Bool:
894	  match kk:
895	    case Flag{}:
896	      String.starts_with(rest, "=")
897	    case Opt{}:
898	      True{}
899	    case Many{}:
900	      True{}
901	    case Pos{}:
902	      True{}
903	    case Rest{}:
904	      True{}
905	
906	# whether the letters after this one are no longer read as letters: an
907	# unknown letter, an option (they are its value) or a flag given `=`
908	def cluster.ends(found: Maybe<&2, Arg>, +rest: String) -> Bool:
909	  match found:
910	    case None{}:
911	      True{}
912	    case Some{aa}:
913	      Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
914	      cluster.ends.kind(kind, rest)
915	
916	# one letter against a walker an earlier letter failed changes nothing;
917	# otherwise it goes through `take_arg`
918	def cluster.apply.mode(
919	  mode: Mode,
920	  +cc: Char,
921	  +rest: String,
922	  +orig: String,
923	  +args: List<&2, Arg>,
924	  +up: List<&2, Level>,
925	  +subs: List<&2, Sub>,
926	  +path: List<&2, String>,
927	  +binds: List<&2, Bind>,
928	  +pos: List<&2, Arg>,
929	  +raw: Bool,
930	  +seen: Bool
931	) -> St:
932	  match mode:
933	    case Dead{e}:
934	      St{Dead{e}, args, up, subs, path, binds, pos, raw, seen}
935	    case _other:
936	      +found = by_short(args, SCon{cc, SNil{}})
937	      parse.take_arg(found, cluster.val(found, rest), orig, args, up, subs, path, binds, pos,
938	        raw, seen)
939	
940	# one letter against the walker
941	def cluster.apply(st: St, +cc: Char, +rest: String, +orig: String) -> St:
942	  St{mode, +args, +up, +subs, +path, +binds, +pos, +raw, +seen} = st
943	  cluster.apply.mode(mode, cc, rest, orig, args, up, subs, path, binds, pos, raw, seen)
944	
945	# one letter of a cluster, unless an earlier one ended it
946	def cluster.letter(done: Bool, +cc: Char, +rest: String, +orig: String, st: St) -> St:
947	  match done:
948	    case True{}:
949	      st
950	    case False{}:
951	      cluster.apply(st, cc, rest, orig)
952	
953	# whether the cluster has ended after this letter
954	def cluster.done(done: Bool, +cc: Char, +rest: String, st: St) -> Bool:
955	  match done:
956	    case True{}:
957	      True{}
958	    case False{}:
959	      St{_m, +args, _g, _s, _p, _b, _o, _r, _n} = st
960	      cluster.ends(by_short(args, SCon{cc, SNil{}}), rest)
961	
962	# every letter of a short cluster `-abc`, in order: a flag binds and the next
963	# letter goes on; an option takes the rest of the word, after one `=`, or the
964	# next word when nothing is left; an unknown letter, or a flag given `=`,
965	# refuses the whole word
966	def cluster(body: String, +orig: String, +st: St, +done: Bool) -> St:
967	  match body:
968	    case SNil{}:
969	      st
970	    case SCon{+cc, +rest}:
971	      cluster(rest, orig, cluster.letter(done, cc, rest, orig, st), cluster.done(done, cc, rest, st))
972	
973	# whether a short option word is a request for help: `-h` alone, before any
974	# positional of the current command is bound, when the command spells
975	# neither `-h` nor `--help`
976	def short_help(+body: String, +args: List<&2, Arg>, seen: Bool) -> Bool:
977	  Bool.and(String.eq(body, "h"),
978	    Bool.and(Bool.not(seen),
979	      Bool.and(Maybe.is_none(&2, Arg, by_short(args, "h")), Maybe.is_none(&2, Arg, by_long(args, "help")))))
980	
981	# a request for help (`-h`, as `help`), or a cluster of short options
982	def parse.take_short.go(
983	  hit: Bool,
984	  body: String,
985	  +orig: String,
986	  +args: List<&2, Arg>,
987	  +up: List<&2, Level>,
988	  +subs: List<&2, Sub>,
989	  +path: List<&2, String>,
990	  +binds: List<&2, Bind>,
991	  +pos: List<&2, Arg>,
992	  +raw: Bool,
993	  +seen: Bool
994	) -> St:
995	  match hit:
996	    case True{}:
997	      St{Help{}, args, up, subs, path, binds, pos, raw, seen}
998	    case False{}:
999	      cluster(body, orig, St{Free{}, args, up, subs, path, binds, pos, raw, seen}, False{})
1000	
1001	# a short option body after `-`
1002	def parse.take_short(
1003	  +body: String,
1004	  +orig: String,
1005	  +args: List<&2, Arg>,
1006	  +up: List<&2, Level>,
1007	  +subs: List<&2, Sub>,
1008	  +path: List<&2, String>,
1009	  +binds: List<&2, Bind>,
1010	  +pos: List<&2, Arg>,
1011	  +raw: Bool,
1012	  +seen: Bool
1013	) -> St:
1014	  parse.take_short.go(short_help(body, args, seen), body, orig, args, up, subs, path, binds, pos, raw, seen)
1015	
1016	# a rest positional stays; a plain one is consumed
1017	def parse.take_pos.keep(keep: Bool, hh: Arg, tt: List<&2, Arg>) -> List<&2, Arg>:
1018	  match keep:
1019	    case True{}:
1020	      hh <> tt
1021	    case False{}:
1022	      tt
1023	
1024	# the next remaining positional, or an unexpected word
1025	def parse.take_pos(
1026	  +tok: String,
1027	  +args: List<&2, Arg>,
1028	  +up: List<&2, Level>,
1029	  subs: List<&2, Sub>,
1030	  +path: List<&2, String>,
1031	  +binds: List<&2, Bind>,
1032	  pos: List<&2, Arg>,
1033	  raw: Bool
1034	) -> St:
1035	  match pos:
1036	    case Nil{}:
1037	      parse.dead(Unexpected{path, tok}, args, up, subs, path, binds, pos, raw, True{})
1038	    case Con{+h, t}:
1039	      Arg{+name, _s, _l, _k, _h, _r, _d, +cs} = h
1040	      parse.take_choice(allowed(cs, tok), name, tok, args, up, subs, path, binds,
1041	        parse.take_pos.keep(rest.is(h), h, t), raw, True{})
1042	
1043	# this Sub's arguments become current, with no bindings of its own; the
1044	# command it leaves keeps its arguments and bindings above it
1045	def parse.enter(
1046	  ss: Sub,
1047	  +args: List<&2, Arg>,
1048	  +up: List<&2, Level>,
1049	  +path: List<&2, String>,
1050	  binds: List<&2, Bind>
1051	) -> St:
1052	  Sub{+name, _a, +next, next_subs} = ss
1053	  St{Free{}, next, Level{args, binds} <> up, next_subs,
1054	    List.append(&2, String, path, [name]), [], pos_of(next), False{},
1055	    False{}}
1056	
1057	# required and no default → Some{name}
1058	def parse.req.go(req: Bool, bare: Bool, +nn: String) -> Maybe<&2, String>:
1059	  Bool.pick(Maybe<&2, String>, Bool.and(req, bare), Some{nn}, None{})
1060	
1061	# a required Arg without a default, as a missing name
1062	def parse.req(aa: Arg) -> Maybe<&2, String>:
1063	  Arg{+n, _s, _l, _k, _h, +req, Fallback{_e, default}, _c} = aa
1064	  parse.req.go(req, Maybe.is_none(&2, String, default), n)
1065	
1066	# this missing name, else the rest
1067	def parse.first_req.at(
1068	  here: Maybe<&2, String>,
1069	  rest: Maybe<&2, String>
1070	) -> Maybe<&2, String>:
1071	  match here:
1072	    case Some{n}:
1073	      Some{n}
1074	    case None{}:
1075	      rest
1076	
1077	# a rest stays in the list, so it does not block a subcommand
1078	def parse.first_req.skip(skip: Bool, aa: Arg) -> Maybe<&2, String>:
1079	  match skip:
1080	    case True{}:
1081	      None{}
1082	    case False{}:
1083	      parse.req(aa)
1084	
1085	# the first leftover required positional
1086	def parse.first_req(pos: List<&2, Arg>) -> Maybe<&2, String>:
1087	  match pos:
1088	    case Nil{}:
1089	      None{}
1090	    case Con{+h, t}:
1091	      parse.first_req.at(parse.first_req.skip(rest.is(h), h), parse.first_req(t))
1092	
1093	# a leftover required positional blocks entering a subcommand
1094	def parse.enter_or(
1095	  miss: Maybe<&2, String>,
1096	  ss: Sub,
1097	  +args: List<&2, Arg>,
1098	  +up: List<&2, Level>,
1099	  +subs: List<&2, Sub>,
1100	  +path: List<&2, String>,
1101	  +binds: List<&2, Bind>,
1102	  +pos: List<&2, Arg>,
1103	  +raw: Bool,
1104	  +seen: Bool
1105	) -> St:
1106	  match miss:
1107	    case None{}:
1108	      parse.enter(ss, args, up, path, binds)
1109	    case Some{n}:
1110	      parse.dead(Missing{path, n}, args, up, subs, path, binds, pos, raw, seen)
1111	
1112	# a found subcommand, or a positional
1113	def parse.word.go(
1114	  found: Maybe<&2, Sub>,
1115	  +tok: String,
1116	  +args: List<&2, Arg>,
1117	  +up: List<&2, Level>,
1118	  +subs: List<&2, Sub>,
1119	  +path: List<&2, String>,
1120	  +binds: List<&2, Bind>,
1121	  +pos: List<&2, Arg>,
1122	  +raw: Bool,
1123	  +seen: Bool
1124	) -> St:
1125	  match found:
1126	    case None{}:
1127	      parse.take_pos(tok, args, up, subs, path, binds, pos, raw)
1128	    case Some{s}:
1129	      parse.enter_or(parse.first_req(pos), s, args, up, subs, path, binds, pos, raw,
1130	        seen)
1131	
1132	# a word: a subcommand, or a positional
1133	def parse.word(
1134	  +tok: String,
1135	  +args: List<&2, Arg>,
1136	  +up: List<&2, Level>,
1137	  +subs: List<&2, Sub>,
1138	  +path: List<&2, String>,
1139	  +binds: List<&2, Bind>,
1140	  +pos: List<&2, Arg>,
1141	  +raw: Bool,
1142	  +seen: Bool
1143	) -> St:
1144	  parse.word.go(find_sub(subs, tok), tok, args, up, subs, path, binds, pos,
1145	    raw, seen)
1146	
1147	# `-` as a word, or a short option
1148	def parse.step.short.go(
1149	  alone: Bool,
1150	  +tok: String,
1151	  +args: List<&2, Arg>,
1152	  +up: List<&2, Level>,
1153	  +subs: List<&2, Sub>,
1154	  +path: List<&2, String>,
1155	  +binds: List<&2, Bind>,
1156	  +pos: List<&2, Arg>,
1157	  +seen: Bool
1158	) -> St:
1159	  match alone:
1160	    case True{}:
1161	      parse.word(tok, args, up, subs, path, binds, pos, False{}, seen)
1162	    case False{}:
1163	      parse.take_short(String.drop(tok, 1n), tok, args, up, subs, path, binds, pos,
1164	        False{}, seen)
1165	
1166	# `-` alone is a positional; otherwise a short option
1167	def parse.step.short(
1168	  dash: Bool,
1169	  +tok: String,
1170	  +args: List<&2, Arg>,
1171	  +up: List<&2, Level>,
1172	  +subs: List<&2, Sub>,
1173	  +path: List<&2, String>,
1174	  +binds: List<&2, Bind>,
1175	  +pos: List<&2, Arg>,
1176	  +seen: Bool
1177	) -> St:
1178	  match dash:
1179	    case True{}:
1180	      parse.step.short.go(String.is_empty(String.drop(tok, 1n)), tok, args, up, subs, path, binds,
1181	        pos, seen)
1182	    case False{}:
1183	      parse.word(tok, args, up, subs, path, binds, pos, False{}, seen)
1184	
1185	# `--long` first, then `-s`, then a word
1186	def parse.step.kind.go(
1187	  long: Bool,
1188	  dash: Bool,
1189	  +tok: String,
1190	  +args: List<&2, Arg>,
1191	  +up: List<&2, Level>,
1192	  +subs: List<&2, Sub>,
1193	  +path: List<&2, String>,
1194	  +binds: List<&2, Bind>,
1195	  +pos: List<&2, Arg>,
1196	  +seen: Bool
1197	) -> St:
1198	  match long:
1199	    case True{}:
1200	      parse.take_long(String.drop(tok, 2n), tok, args, up, subs, path, binds, pos,
1201	        False{}, seen)
1202	    case False{}:
1203	      parse.step.short(dash, tok, args, up, subs, path, binds, pos, seen)
1204	
1205	# a long option, a short option, or a word
1206	def parse.step.kind(
1207	  +tok: String,
1208	  +args: List<&2, Arg>,
1209	  +up: List<&2, Level>,
1210	  subs: List<&2, Sub>,
1211	  +path: List<&2, String>,
1212	  +binds: List<&2, Bind>,
1213	  +pos: List<&2, Arg>,
1214	  +seen: Bool
1215	) -> St:
1216	  parse.step.kind.go(String.starts_with(tok, "--"), String.starts_with(tok, "-"), tok,
1217	    args, up, subs, path, binds, pos, seen)
1218	
1219	# `help` in command position collects the rest of argv as a path
1220	def parse.step.help(
1221	  hit: Bool,
1222	  +tok: String,
1223	  +args: List<&2, Arg>,
1224	  +up: List<&2, Level>,
1225	  +subs: List<&2, Sub>,
1226	  +path: List<&2, String>,
1227	  +binds: List<&2, Bind>,
1228	  +pos: List<&2, Arg>,
1229	  +seen: Bool
1230	) -> St:
1231	  match hit:
1232	    case True{}:
1233	      St{Help{}, args, up, subs, path, binds, pos, False{}, seen}
1234	    case False{}:
1235	      parse.step.kind(tok, args, up, subs, path, binds, pos, seen)
1236	
1237	# `--` ends option parsing
1238	def parse.step.end(
1239	  end: Bool,
1240	  +tok: String,
1241	  +args: List<&2, Arg>,
1242	  +up: List<&2, Level>,
1243	  +subs: List<&2, Sub>,
1244	  +path: List<&2, String>,
1245	  +binds: List<&2, Bind>,
1246	  +pos: List<&2, Arg>,
1247	  +seen: Bool
1248	) -> St:
1249	  match end:
1250	    case True{}:
1251	      St{Free{}, args, up, subs, path, binds, pos, True{}, seen}
1252	    case False{}:
1253	      parse.step.help(Bool.and(String.eq(tok, "help"), Bool.not(seen)), tok, args,
1254	        up, subs, path, binds, pos, seen)
1255	
1256	# after `--`, every token is a positional
1257	def parse.step.raw(
1258	  raw: Bool,
1259	  +tok: String,
1260	  +args: List<&2, Arg>,
1261	  +up: List<&2, Level>,
1262	  +subs: List<&2, Sub>,
1263	  +path: List<&2, String>,
1264	  +binds: List<&2, Bind>,
1265	  +pos: List<&2, Arg>,
1266	  +seen: Bool
1267	) -> St:
1268	  match raw:
1269	    case True{}:
1270	      parse.take_pos(tok, args, up, subs, path, binds, pos, True{})
1271	    case False{}:
1272	      parse.step.end(String.eq(tok, "--"), tok, args, up, subs, path, binds, pos,
1273	        seen)
1274	
1275	# a pending option value: a flag-shaped token is a missing value
1276	def parse.step.need(
1277	  flag: Bool,
1278	  +name: String,
1279	  +tok: String,
1280	  +args: List<&2, Arg>,
1281	  +up: List<&2, Level>,
1282	  +subs: List<&2, Sub>,
1283	  +path: List<&2, String>,
1284	  +binds: List<&2, Bind>,
1285	  +pos: List<&2, Arg>,
1286	  +raw: Bool,
1287	  +seen: Bool
1288	) -> St:
1289	  match flag:
1290	    case True{}:
1291	      parse.dead(NoValue{path, name}, args, up, subs, path, binds, pos, raw, seen)
1292	    case False{}:
1293	      parse.take_opt_val(name, tok, args, up, subs, path, binds, pos, raw, seen)
1294	
1295	# a word after `help`: the subcommand it names, whose own subcommands the
1296	# next word is looked up in, or an unexpected word
1297	def parse.step.help_path(
1298	  found: Maybe<&2, Sub>,
1299	  +tok: String,
1300	  +args: List<&2, Arg>,
1301	  +up: List<&2, Level>,
1302	  +subs: List<&2, Sub>,
1303	  +path: List<&2, String>,
1304	  +binds: List<&2, Bind>,
1305	  +pos: List<&2, Arg>,
1306	  +raw: Bool,
1307	  +seen: Bool
1308	) -> St:
1309	  match found:
1310	    case None{}:
1311	      parse.dead(Unexpected{path, tok}, args, up, subs, path, binds, pos, raw, seen)
1312	    case Some{ss}:
1313	      Sub{_n, _a, _g, next_subs} = ss
1314	      St{Help{}, args, up, next_subs, List.append(&2, String, path, [tok]), binds,
1315	        pos, raw, seen}
1316	
1317	# one token against the walker
1318	def parse.step.mode(
1319	  mode: Mode,
1320	  +tok: String,
1321	  +args: List<&2, Arg>,
1322	  +up: List<&2, Level>,
1323	  +subs: List<&2, Sub>,
1324	  +path: List<&2, String>,
1325	  +binds: List<&2, Bind>,
1326	  +pos: List<&2, Arg>,
1327	  +raw: Bool,
1328	  +seen: Bool
1329	) -> St:
1330	  match mode:
1331	    case Dead{e}:
1332	      St{Dead{e}, args, up, subs, path, binds, pos, raw, seen}
1333	    case Need{name}:
1334	      parse.step.need(looks_flag(tok), name, tok, args, up, subs, path, binds, pos,
1335	        raw, seen)
1336	    case Help{}:
1337	      parse.step.help_path(find_sub(subs, tok), tok, args, up, subs, path, binds, pos, raw,
1338	        seen)
1339	    case Free{}:
1340	      parse.step.raw(raw, tok, args, up, subs, path, binds, pos, seen)
1341	
1342	# one token
1343	def parse.step(+tok: String, st: St) -> St:
1344	  St{mode, args, up, subs, path, binds, pending, raw, seen} = st
1345	  parse.step.mode(mode, tok, args, up, subs, path, binds, pending, raw, seen)
1346	
1347	# every token, in order
1348	def parse.walk(argv: List<&2, String>, st: St) -> St:
1349	  match argv:
1350	    case Nil{}:
1351	      st
1352	    case Con{+h, t}:
1353	      parse.walk(t, parse.step(h, st))
1354	
1355	# a default value kept when the name is not already bound
1356	def fill.one(
1357	  skip: Bool,
1358	  +name: String,
1359	  +val: String,
1360	  rest: List<&2, Bind>
1361	) -> List<&2, Bind>:
1362	  match skip:
1363	    case True{}:
1364	      rest
1365	    case False{}:
1366	      Bind{name, val} <> rest
1367	
1368	# a Some default is filled when unbound
1369	def fill.arg.go(
1370	  dd: Maybe<&2, String>,
1371	  +name: String,
1372	  +binds: List<&2, Bind>
1373	) -> List<&2, Bind>:
1374	  match dd:
1375	    case None{}:
1376	      binds
1377	    case Some{v}:
1378	      fill.one(bound(binds, name), name, v, binds)
1379	
1380	# this Arg's default, when it has one and is not bound
1381	def fill.arg(aa: Arg, +binds: List<&2, Bind>) -> List<&2, Bind>:
1382	  Arg{+n, _s, _l, _k, _h, _r, Fallback{_e, default}, _c} = aa
1383	  fill.arg.go(default, n, binds)
1384	
1385	# defaults of every spec Arg
1386	def fill.args(args: List<&2, Arg>, +binds: List<&2, Bind>) -> List<&2, Bind>:
1387	  match args:
1388	    case Nil{}:
1389	      binds
1390	    case Con{+h, t}:
1391	      fill.arg(h, fill.args(t, binds))
1392	
1393	# a required name that is not bound
1394	def miss.one(
1395	  need: Bool,
1396	  +name: String,
1397	  rest: Maybe<&2, String>
1398	) -> Maybe<&2, String>:
1399	  match need:
1400	    case True{}:
1401	      Some{name}
1402	    case False{}:
1403	      rest
1404	
1405	# whether this Arg is required and unbound
1406	def miss.arg(
1407	  aa: Arg,
1408	  +binds: List<&2, Bind>,
1409	  rest: Maybe<&2, String>
1410	) -> Maybe<&2, String>:
1411	  Arg{+n, _s, _l, _k, _h, +req, _d, _c} = aa
1412	  miss.one(Bool.and(req, Bool.not(bound(binds, n))), n, rest)
1413	
1414	# the first required name that is not bound
1415	def miss.args(args: List<&2, Arg>, +binds: List<&2, Bind>) -> Maybe<&2, String>:
1416	  match args:
1417	    case Nil{}:
1418	      None{}
1419	    case Con{+h, t}:
1420	      miss.arg(h, binds, miss.args(t, binds))
1421	
1422	# each command's defaults, filled in among its own bindings
1423	def fill.levels(lvs: List<&2, Level>) -> List<&2, Level>:
1424	  match lvs:
1425	    case Nil{}:
1426	      []
1427	    case Con{hh, tt}:
1428	      Level{+args, binds} = hh
1429	      Level{args, fill.args(args, binds)} <> fill.levels(tt)
1430	
1431	# the first required argument a command left unbound, in list order
1432	def miss.levels(lvs: List<&2, Level>) -> Maybe<&2, String>:
1433	  match lvs:
1434	    case Nil{}:
1435	      None{}
1436	    case Con{hh, tt}:
1437	      Level{+args, +binds} = hh
1438	      parse.first_req.at(miss.args(args, binds), miss.levels(tt))
1439	
1440	# the bindings a command made
1441	def level.binds(lv: Level) -> List<&2, Bind>:
1442	  Level{_a, binds} = lv
1443	  binds
1444	
1445	# each command's Matched, root first, with the name selected under it
1446	def matched.build(lvs: List<&2, Level>, names: List<&2, String>) -> Matched:
1447	  match lvs:
1448	    case Nil{}:
1449	      Leaf{[]}
1450	    case Con{hh, tt}:
1451	      match names:
1452	        case Nil{}:
1453	          Leaf{List.reverse(&2, Bind, level.binds(hh))}
1454	        case Con{nn, ns}:
1455	          Node{List.reverse(&2, Bind, level.binds(hh)), nn, matched.build(tt, ns)}
1456	
1457	# a missing required name, or the matched result
1458	def parse.finish.miss(
1459	  mm: Maybe<&2, String>,
1460	  path: List<&2, String>,
1461	  +lvs: List<&2, Level>
1462	) -> Result<&2, &2, ParseErr, Matched>:
1463	  match mm:
1464	    case Some{n}:
1465	      Fail{Missing{path, n}}
1466	    case None{}:
1467	      Done{matched.build(lvs, path)}
1468	
1469	# every command's defaults, then its required arguments, root first
1470	def parse.finish.ok(+path: List<&2, String>, +lvs: List<&2, Level>) -> Result<&2, &2, ParseErr, Matched>:
1471	  parse.finish.miss(miss.levels(lvs), path, lvs)
1472	
1473	# a finished walker: help, a pending value, an error, or defaults + required
1474	def parse.finish.mode(
1475	  mode: Mode,
1476	  +args: List<&2, Arg>,
1477	  +up: List<&2, Level>,
1478	  +path: List<&2, String>,
1479	  +binds: List<&2, Bind>
1480	) -> Result<&2, &2, ParseErr, Matched>:
1481	  match mode:
1482	    case Dead{e}:
1483	      Fail{e}
1484	    case Need{name}:
1485	      Fail{NoValue{path, name}}
1486	    case Help{}:
1487	      Fail{NeedHelp{path}}
1488	    case Free{}:
1489	      parse.finish.ok(path, List.reverse(&2, Level, fill.levels(Level{args, binds} <> up)))
1490	
1491	# the walker, finished
1492	def parse.finish(st: St) -> Result<&2, &2, ParseErr, Matched>:
1493	  St{mode, args, up, _s, path, binds, _p, _r, _n} = st
1494	  parse.finish.mode(mode, args, up, path, binds)
1495	
1496	# whether a word refused at `at` asks for the version: `--version`, or `-V`
1497	# when the root does not spell `--version`, refused at the root of a spec
1498	# with a version
1499	def version.asks(+app: Cli, +at: List<&2, String>, +word: String) -> Bool:
1500	  Cli{_n, _a, version, args, _s} = app
1501	  Bool.and(Bool.or(String.eq(word, "--version"),
1502	      Bool.and(String.eq(word, "-V"), Maybe.is_none(&2, Arg, by_long(args, "version")))),
1503	    Bool.and(List.is_empty(&2, String, at), Maybe.is_some(&2, String, version)))
1504	
1505	# an error, or a request for the version when it is one
1506	def version.err(+app: Cli, ee: ParseErr) -> ParseErr:
1507	  match ee:
1508	    case UnknownFlag{+at, +word}:
1509	      Bool.pick(ParseErr, version.asks(app, at, word), NeedVersion{}, UnknownFlag{at, word})
1510	    case other:
1511	      other
1512	
1513	# a parse's answer, its failure read as a request for the version when it is
1514	# one
1515	def version.res(+app: Cli, rr: Result<&2, &2, ParseErr, Matched>) -> Result<&2, &2, ParseErr, Matched>:
1516	  match rr:
1517	    case Done{mm}:
1518	      Done{mm}
1519	    case Fail{ee}:
1520	      Fail{version.err(app, ee)}
1521	
1522	# argv against a Cli
1523	def parse(+app: Cli, argv: List<&2, String>) -> Result<&2, &2, ParseErr, Matched>:
1524	  version.res(app, parse.finish(parse.walk(argv, parse.start(app))))
1525	
1526	# `name version`, when there is a version
1527	def version_of.text(+name: String, version: Maybe<&2, String>) -> Maybe<&2, String>:
1528	  match version:
1529	    case None{}:
1530	      None{}
1531	    case Some{vv}:
1532	      Some{name ++ " " ++ vv}
1533	
1534	# a spec's `name version`, when it has a version
1535	def version_of.cli(app: Cli) -> Maybe<&2, String>:
1536	  Cli{+name, _a, version, _g, _s} = app
1537	  version_of.text(name, version)
1538	
1539	# `name version` for a request for the version, of a spec that has one
1540	def version_of(+app: Cli, ee: ParseErr) -> Maybe<&2, String>:
1541	  match ee:
1542	    case NeedVersion{}:
1543	      version_of.cli(app)
1544	    case _other:
1545	      None{}
1546	
1547	# this pair's value when its name matches, else the rest
1548	def env.get.at(hit: Bool, +vv: String, rest: Maybe<&2, String>) -> Maybe<&2, String>:
1549	  match hit:
1550	    case True{}:
1551	      Some{vv}
1552	    case False{}:
1553	      rest
1554	
1555	# the value of the first pair named `name`
1556	def env.get(vars: List<&2, Var>, +name: String) -> Maybe<&2, String>:
1557	  match vars:
1558	    case Nil{}:
1559	      None{}
1560	    case Con{hh, tt}:
1561	      (+nn, +vv) = hh
1562	      env.get.at(String.eq(nn, name), vv, env.get(tt, name))
1563	
1564	# a value that is not empty
1565	def env.full(mv: Maybe<&2, String>) -> Maybe<&2, String>:
1566	  match mv:
1567	    case None{}:
1568	      None{}
1569	    case Some{+vv}:
1570	      Bool.pick(Maybe<&2, String>, String.is_empty(vv), None{}, Some{vv})
1571	
1572	# the env value of an env var: its first pair's value, when that is not empty
1573	def env.of(ev: Maybe<&2, String>, vars: List<&2, Var>) -> Maybe<&2, String>:
1574	  match ev:
1575	    case None{}:
1576	      None{}
1577	    case Some{+var}:
1578	      env.full(env.get(vars, var))
1579	
1580	# whether an env value turns a flag off, as clap's `SetTrue` reads it
1581	def env.off(+vv: String) -> Bool:
1582	  allowed.ok(["0", "false", "no", "off", "n", "f"], String.to_lower(vv))
1583	
1584	# the default an env value gives an argument of this kind: a flag is set
1585	# unless the value turns it off; every other kind takes the value
1586	def env.kind(kk: ArgKind, +vv: String) -> Maybe<&2, String>:
1587	  match kk:
1588	    case Flag{}:
1589	      Bool.pick(Maybe<&2, String>, env.off(vv), None{}, Some{"true"})
1590	    case Opt{}:
1591	      Some{vv}
1592	    case Many{}:
1593	      Some{vv}
1594	    case Pos{}:
1595	      Some{vv}
1596	    case Rest{}:
1597	      Some{vv}
1598	
1599	# a fallback with its default replaced by what the env value gives, when
1600	# there is one
1601	def resolve.with(
1602	  found: Maybe<&2, String>,
1603	  kk: ArgKind,
1604	  ev: Maybe<&2, String>,
1605	  dd: Maybe<&2, String>
1606	) -> Fallback:
1607	  match found:
1608	    case None{}:
1609	      Fallback{ev, dd}
1610	    case Some{+vv}:
1611	      Fallback{ev, env.kind(kk, vv)}
1612	
1613	# an argument whose default is its fallback under `vars`
1614	def resolve.arg(aa: Arg, vars: List<&2, Var>) -> Arg:
1615	  Arg{+n, +s, +l, +kk, +h, +r, Fallback{+ev, dd}, +cs} = aa
1616	  Arg{n, s, l, kk, h, r, resolve.with(env.of(ev, vars), kk, ev, dd), cs}
1617	
1618	# every argument's default is its fallback
1619	def resolve.args(args: List<&2, Arg>, +vars: List<&2, Var>) -> List<&2, Arg>:
1620	  match args:
1621	    case Nil{}:
1622	      []
1623	    case Con{hh, tt}:
1624	      resolve.arg(hh, vars) <> resolve.args(tt, vars)
1625	
1626	# every argument of every subcommand, its default its fallback
1627	def resolve.subs(subs: List<&2, Sub>, +vars: List<&2, Var>) -> List<&2, Sub>:
1628	  match subs:
1629	    case Nil{}:
1630	      []
1631	    case Con{hh, tt}:
1632	      Sub{+n, +a, args, kids} = hh
1633	      Sub{n, a, resolve.args(args, vars), resolve.subs(kids, vars)} <> resolve.subs(tt, vars)
1634	
1635	# the spec whose every argument's default is its fallback under `vars`
1636	def resolve(app: Cli, +vars: List<&2, Var>) -> Cli:
1637	  Cli{+n, +a, +v, args, subs} = app
1638	  Cli{n, a, v, resolve.args(args, vars), resolve.subs(subs, vars)}
1639	
1640	# whether this kind is a flag
1641	def env.flag.is(kk: ArgKind) -> Bool:
1642	  match kk:
1643	    case Flag{}:
1644	      True{}
1645	    case Opt{}:
1646	      False{}
1647	    case Many{}:
1648	      False{}
1649	    case Pos{}:
1650	      False{}
1651	    case Rest{}:
1652	      False{}
1653	
1654	# an argument bound to an env value outside its choices: never a flag, and
1655	# only for a value its command's bindings hold
1656	def env.bad.val(
1657	  found: Maybe<&2, String>,
1658	  kk: ArgKind,
1659	  +name: String,
1660	  +cs: List<&2, String>,
1661	  +binds: List<&2, Bind>
1662	) -> Maybe<&2, Var>:
1663	  match found:
1664	    case None{}:
1665	      None{}
1666	    case Some{+vv}:
1667	      Bool.pick(Maybe<&2, Var>,
1668	        Bool.and(Bool.not(env.flag.is(kk)), Bool.and(Bool.not(allowed(cs, vv)),
1669	          List.contains(~String, ~String.eq, get_all.bind(binds, name), vv))),
1670	        Some{(name, vv)}, None{})
1671	
1672	# this argument's name and env value, when its command's bindings hold that
1673	# value and its choices do not
1674	def env.bad.arg(aa: Arg, vars: List<&2, Var>, +binds: List<&2, Bind>) -> Maybe<&2, Var>:
1675	  Arg{+n, _s, _l, kk, _h, _r, Fallback{ev, _d}, +cs} = aa
1676	  env.bad.val(env.of(ev, vars), kk, n, cs, binds)
1677	
1678	# the first of two answers that is one
1679	def env.first(here: Maybe<&2, Var>, rest: Maybe<&2, Var>) -> Maybe<&2, Var>:
1680	  match here:
1681	    case None{}:
1682	      rest
1683	    case Some{pp}:
1684	      Some{pp}
1685	
1686	# the first argument of a command bound to an env value outside its choices
1687	def env.bad.args(
1688	  args: List<&2, Arg>,
1689	  +vars: List<&2, Var>,
1690	  +binds: List<&2, Bind>
1691	) -> Maybe<&2, Var>:
1692	  match args:
1693	    case Nil{}:
1694	      None{}
1695	    case Con{hh, tt}:
1696	      env.first(env.bad.arg(hh, vars, binds), env.bad.args(tt, vars, binds))
1697	
1698	# the arguments of a found subcommand, or none
1699	def env.sub.args(found: Maybe<&2, Sub>) -> List<&2, Arg>:
1700	  match found:
1701	    case None{}:
1702	      []
1703	    case Some{ss}:
1704	      Sub{_n, _a, args, _k} = ss
1705	      args
1706	
1707	# the subcommands of a found subcommand, or none
1708	def env.sub.kids(found: Maybe<&2, Sub>) -> List<&2, Sub>:
1709	  match found:
1710	    case None{}:
1711	      []
1712	    case Some{ss}:
1713	      Sub{_n, _a, _g, kids} = ss
1714	      kids
1715	
1716	# the first argument bound to an env value outside its choices, the command
1717	# first, then down the selected path
1718	def env.bad.go(
1719	  mm: Matched,
1720	  +args: List<&2, Arg>,
1721	  +subs: List<&2, Sub>,
1722	  +vars: List<&2, Var>
1723	) -> Maybe<&2, Var>:
1724	  match mm:
1725	    case Leaf{+bs}:
1726	      env.bad.args(args, vars, bs)
1727	    case Node{+bs, +name, next}:
1728	      env.first(env.bad.args(args, vars, bs),
1729	        env.bad.go(next, env.sub.args(find_sub(subs, name)), env.sub.kids(find_sub(subs, name)), vars))
1730	
1731	# a success, or the first env value outside its choices that it bound
1732	def env.check.done(bad: Maybe<&2, Var>, +mm: Matched) -> Result<&2, &2, ParseErr, Matched>:
1733	  match bad:
1734	    case None{}:
1735	      Done{mm}
1736	    case Some{pp}:
1737	      (+name, +vv) = pp
1738	      Fail{BadValue{path_of(mm), name, vv}}
1739	
1740	# a successful parse checked for env values outside their choices
1741	def env.check.ok(app: Cli, +vars: List<&2, Var>, +mm: Matched) -> Result<&2, &2, ParseErr, Matched>:
1742	  Cli{_n, _a, _v, +args, subs} = app
1743	  env.check.done(env.bad.go(mm, args, subs, vars), mm)
1744	
1745	# a failed parse as it is; a successful one checked for env values outside
1746	# their choices
1747	def env.check(
1748	  app: Cli,
1749	  +vars: List<&2, Var>,
1750	  got: Result<&2, &2, ParseErr, Matched>
1751	) -> Result<&2, &2, ParseErr, Matched>:
1752	  match got:
1753	    case Fail{ee}:
1754	      Fail{ee}
1755	    case Done{+mm}:
1756	      env.check.ok(app, vars, mm)
1757	
1758	# argv against a Cli, every argument falling back to its env value under
1759	# `vars`, then to its default
1760	def parse_env(
1761	  +app: Cli,
1762	  argv: List<&2, String>,
1763	  +vars: List<&2, Var>
1764	) -> Result<&2, &2, ParseErr, Matched>:
1765	  env.check(app, vars, parse(resolve(app, vars), argv))
1766	
1767	# an env var in front of the names, when there is one
1768	def env.names.put(ev: Maybe<&2, String>, rest: List<&2, String>) -> List<&2, String>:
1769	  match ev:
1770	    case None{}:
1771	      rest
1772	    case Some{var}:
1773	      var <> rest
1774	
1775	# the env vars of a command's arguments, in order
1776	def env.names.args(args: List<&2, Arg>) -> List<&2, String>:
1777	  match args:
1778	    case Nil{}:
1779	      []
1780	    case Con{hh, tt}:
1781	      Arg{_n, _s, _l, _k, _h, _r, Fallback{ev, _d}, _c} = hh
1782	      env.names.put(ev, env.names.args(tt))
1783	
1784	# the env vars of every subcommand's arguments, depth first
1785	def env.names.forest(subs: List<&2, Sub>) -> List<&2, String>:
1786	  match subs:
1787	    case Nil{}:
1788	      []
1789	    case Con{hh, tt}:
1790	      Sub{_n, _a, args, kids} = hh
1791	      List.append(&2, String, env.names.args(args),
1792	        List.append(&2, String, env.names.forest(kids), env.names.forest(tt)))
1793	
1794	# the env vars of a spec: the root's arguments', then every subcommand's
1795	def env.names(app: Cli) -> List<&2, String>:
1796	  Cli{_n, _a, _v, args, subs} = app
1797	  List.append(&2, String, env.names.args(args), env.names.forest(subs))
1798	
1799	# the short/long label of an option, plus a metavar for Opt
1800	def help.label.kind(kk: ArgKind, +name: String, +label: String) -> String:
1801	  match kk:
1802	    case Flag{}:
1803	      label
1804	    case Opt{}:
1805	      label ++ " <" ++ String.to_upper(name) ++ ">"
1806	    case Many{}:
1807	      label ++ " <" ++ String.to_upper(name) ++ ">..."
1808	    case Pos{}:
1809	      label
1810	    case Rest{}:
1811	      label
1812	
1813	# `-s, --long` or one of them
1814	def help.label.pair(+short: String, +long: String) -> String:
1815	  Bool.pick(String, String.is_empty(short),
1816	    Bool.pick(String, String.is_empty(long), "", "    --" ++ long),
1817	    Bool.pick(String, String.is_empty(long), "  -" ++ short,
1818	      "  -" ++ short ++ ", --" ++ long))
1819	
1820	# the usage label of an option
1821	def help.label(aa: Arg) -> String:
1822	  Arg{+name, short, long, kind, _h, _r, _d, _c} = aa
1823	  help.label.kind(kind, name, help.label.pair(text.of(short, ""), text.of(long, "")))
1824	
1825	# extras after the help string: default and choices
1826	def help.extra.go(+dd: String, +cs: List<&2, String>) -> String:
1827	  Bool.pick(String, String.is_empty(dd),
1828	    Bool.pick(String, List.is_empty(&2, String, cs), "",
1829	      " [possible values: " ++ String.join(cs, ", ") ++ "]"),
1830	    Bool.pick(String, List.is_empty(&2, String, cs),
1831	      " [default: " ++ dd ++ "]",
1832	      " [default: " ++ dd ++ "] [possible values: " ++ String.join(cs, ", ") ++
1833	        "]"))
1834	
1835	# the env var after the help string, before the default
1836	def help.env(ev: Maybe<&2, String>) -> String:
1837	  match ev:
1838	    case None{}:
1839	      ""
1840	    case Some{var}:
1841	      " [env: " ++ var ++ "]"
1842	
1843	# extras after the help string: env var, default and choices
1844	def help.extra(aa: Arg) -> String:
1845	  Arg{_n, _s, _l, _k, _h, _r, Fallback{ev, default}, cs} = aa
1846	  help.env(ev) ++ help.extra.go(text.of(default, ""), cs)
1847	
1848	# one option line, given the label width
1849	def help.opt_line(+aa: Arg, ww: Nat) -> String:
1850	  Arg{_n, _s, _l, _k, +h, _r, _d, _c} = aa
1851	  help.pad(help.label(aa), ww) ++ "  " ++ h ++ help.extra(aa)
1852	
1853	# the max option-label width
1854	def help.opt_width(args: List<&2, Arg>, nn: Nat) -> Nat:
1855	  match args:
1856	    case Nil{}:
1857	      nn
1858	    case Con{+h, t}:
1859	      help.opt_width(t, help.max(nn, String.length(help.label(h))))
1860	
1861	# a non-positional option line
1862	def help.opt_lines.at(skip: Bool, hh: Arg, rest: String, ww: Nat) -> String:
1863	  match skip:
1864	    case True{}:
1865	      rest
1866	    case False{}:
1867	      help.opt_line(hh, ww) ++ "\n" ++ rest
1868	
1869	# option lines, skipping positionals
1870	def help.opt_lines(args: List<&2, Arg>, +ww: Nat) -> String:
1871	  match args:
1872	    case Nil{}:
1873	      ""
1874	    case Con{+h, t}:
1875	      help.opt_lines.at(pos.is(h), h, help.opt_lines(t, ww), ww)
1876	
1877	# wrap option lines in a heading
1878	def help.opts.go(+body: String) -> String:
1879	  Bool.pick(String, String.is_empty(body), "", "Options:\n" ++ body ++ "\n")
1880	
1881	# the Options block, or empty when there are none
1882	def help.opts(+args: List<&2, Arg>) -> String:
1883	  help.opts.go(help.opt_lines(args, help.opt_width(args, 0n)))
1884	
1885	# a command's name
1886	def help.sub_name(ss: Sub) -> String:
1887	  Sub{n, _a, _g, _c} = ss
1888	  n
1889	
1890	# a command's about
1891	def help.sub_about(ss: Sub) -> String:
1892	  Sub{_n, a, _g, _c} = ss
1893	  a
1894	
1895	# max command-name width, including `help`
1896	def help.cmd_width(subs: List<&2, Sub>, nn: Nat) -> Nat:
1897	  match subs:
1898	    case Nil{}:
1899	      help.max(nn, String.length("help"))
1900	    case Con{+h, t}:
1901	      help.cmd_width(t, help.max(nn, String.length(help.sub_name(h))))
1902	
1903	# one command line
1904	def help.cmd_line(+name: String, +about: String, ww: Nat) -> String:
1905	  "  " ++ help.pad(name, ww) ++ "  " ++ about ++ "\n"
1906	
1907	# command lines, then `help`
1908	def help.cmd_lines(subs: List<&2, Sub>, +ww: Nat) -> String:
1909	  match subs:
1910	    case Nil{}:
1911	      help.cmd_line("help",
1912	        "Print this message or the help of the given subcommand(s)", ww)
1913	    case Con{+h, t}:
1914	      help.cmd_line(help.sub_name(h), help.sub_about(h), ww) ++ help.cmd_lines(t, ww)
1915	
1916	# the Commands block
1917	def help.cmds(+subs: List<&2, Sub>) -> String:
1918	  "Commands:\n" ++ help.cmd_lines(subs, help.cmd_width(subs, 0n)) ++ "\n"
1919	
1920	# a rest mark: `...`, or empty
1921	def help.pos.dots(many: Bool) -> String:
1922	  Bool.pick(String, many, "...", "")
1923	
1924	# a positional in a usage line: `<NAME>` or `[NAME]`
1925	def help.pos.wrap(req: Bool, +nn: String) -> String:
1926	  Bool.pick(String, req, " <" ++ nn ++ ">", " [" ++ nn ++ "]")
1927	
1928	# a positional in a usage line: `<NAME>` or `[NAME]`, plus `...` when rest
1929	def help.pos.one(aa: Arg) -> String:
1930	  Arg{+n, _s, _l, kind, _h, +req, _d, _c} = aa
1931	  help.pos.wrap(req, String.to_upper(n)) ++ help.pos.dots(rest.is.kind(kind))
1932	
1933	# this positional's hint, else the rest
1934	def help.pos.at(keep: Bool, hh: Arg, rest: String) -> String:
1935	  match keep:
1936	    case True{}:
1937	      help.pos.one(hh) ++ rest
1938	    case False{}:
1939	      rest
1940	
1941	# every positional in a usage line
1942	def help.pos(args: List<&2, Arg>) -> String:
1943	  match args:
1944	    case Nil{}:
1945	      ""
1946	    case Con{+h, t}:
1947	      help.pos.at(pos.is(h), h, help.pos(t))
1948	
1949	# a positional's label in the Arguments block: its usage mark without the
1950	# space before it
1951	def help.pos.label(aa: Arg) -> String:
1952	  String.drop(help.pos.one(aa), 1n)
1953	
1954	# one Arguments line, given the label width
1955	def help.arg_line(+aa: Arg, ww: Nat) -> String:
1956	  Arg{_n, _s, _l, _k, +h, _r, _d, _c} = aa
1957	  "  " ++ help.pad(help.pos.label(aa), ww) ++ "  " ++ h ++ help.extra(aa)
1958	
1959	# the max positional-label width
1960	def help.arg_width(args: List<&2, Arg>, nn: Nat) -> Nat:
1961	  match args:
1962	    case Nil{}:
1963	      nn
1964	    case Con{+h, t}:
1965	      help.arg_width(t, help.max(nn, String.length(help.pos.label(h))))
1966	
1967	# a positional's Arguments line
1968	def help.arg_lines.at(keep: Bool, hh: Arg, rest: String, ww: Nat) -> String:
1969	  match keep:
1970	    case True{}:
1971	      help.arg_line(hh, ww) ++ "\n" ++ rest
1972	    case False{}:
1973	      rest
1974	
1975	# Arguments lines, skipping flags and options
1976	def help.arg_lines(args: List<&2, Arg>, +ww: Nat) -> String:
1977	  match args:
1978	    case Nil{}:
1979	      ""
1980	    case Con{+h, t}:
1981	      help.arg_lines.at(pos.is(h), h, help.arg_lines(t, ww), ww)
1982	
1983	# wrap Arguments lines in a heading
1984	def help.args.go(+body: String) -> String:
1985	  Bool.pick(String, String.is_empty(body), "", "Arguments:\n" ++ body ++ "\n")
1986	
1987	# the Arguments block, or empty when there are no positionals
1988	def help.args(+args: List<&2, Arg>) -> String:
1989	  help.args.go(help.arg_lines(args, help.arg_width(pos_of(args), 0n)))
1990	
1991	# the bracketed options word when the spec has a flag or option
1992	def help.opts_hint.go(has: Bool) -> String:
1993	  Bool.pick(String, has, " [" ++ String.to_upper("options") ++ "]", "")
1994	
1995	# True when this Arg is a flag or option, else the rest
1996	def help.has_opt.at(is_pos: Bool, rest: Bool) -> Bool:
1997	  match is_pos:
1998	    case True{}:
1999	      rest
2000	    case False{}:
Lines 1-2000 of 2470. More: https://jend.leeeet.dev/read.txt?path=shake@0.7.0.0/src/cli.bend&start_line=2001