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