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