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