src/cli.bend

shake@0.7.0.0 · 2,470 lines · 262 definitions

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.
6import Base
7
8# a flag, a valued option, an option that may repeat, a positional, or a rest
9# positional
10type 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
19type 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
23type 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
36type 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
45type 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
55def Var() -> Data:
56  Sigma<&2, &2, String, _ => String>
57
58# one bound name and its text
59type 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
64type 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
70type Matched is Data:
71  Leaf{+binds: List<&2, Bind>}
72  Node{+binds: List<&2, Bind>, +name: String, +sub: Matched}
73
74# a failed parse. NeedHelp is `help` / `help <path>` (or `--help`, `-h`),
75# NeedVersion `--version` (or `-V`); NoValue is an option whose value never
76# came, Missing a required argument nothing bound. Every error but NeedHelp
77# and NeedVersion carries `at`, the command path selected where it failed
78type ParseErr is Data:
79  UnknownFlag{at: List<&2, String>, flag: String}
80  Missing{at: List<&2, String>, name: String}
81  NoValue{at: List<&2, String>, name: String}
82  BadValue{at: List<&2, String>, name: String, value: String}
83  NeedHelp{path: List<&2, String>}
84  Unexpected{at: List<&2, String>, arg: String}
85  Repeated{at: List<&2, String>, name: String}
86  NeedVersion{}
87
88# how the next token is read
89type Mode is Data:
90  Free{}
91  Need{name: String}
92  Help{}
93  Dead{err: ParseErr}
94
95# the walker: the current command's arguments, the commands above it (the
96# nearest first, one per name of the selected path), its subcommands, the
97# selected path, and the current command's own bindings
98type St is Data:
99  St{
100    mode: Mode,
101    args: List<&2, Arg>,
102    up: List<&2, Level>,
103    subs: List<&2, Sub>,
104    path: List<&2, String>,
105    binds: List<&2, Bind>,
106    pos: List<&2, Arg>,
107    raw: Bool,
108    seen: Bool
109  }
110
111# the page a help walk has reached
112type How is Data:
113  How{
114    bin: String,
115    about: String,
116    version: Maybe<&2, String>,
117    args: List<&2, Arg>,
118    subs: List<&2, Sub>,
119    usage: String
120  }
121
122# a program spec
123def app(
124  +name: String,
125  +about: String,
126  version: Maybe<&2, String>,
127  args: List<&2, Arg>,
128  subs: List<&2, Sub>
129) -> Cli:
130  Cli{name, about, version, args, subs}
131
132# a nested command
133def sub(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
134  +name: String,
135  +about: String,
136  args: List<&2, Arg>,
137  subs: List<&2, Sub>
138) -> Sub:
139  Sub{name, about, args, subs}
140
141# a boolean flag
142def flag(
143  +name: String,
144  short: Maybe<&2, String>,
145  long: Maybe<&2, String>,
146  +help: String
147) -> Arg:
148  Arg{name, short, long, Flag{}, help, False{}, Fallback{None{}, None{}}, []}
149
150# a valued option
151def opt(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
152  +name: String,
153  short: Maybe<&2, String>,
154  long: Maybe<&2, String>,
155  +help: String,
156  required: Bool,
157  default: Maybe<&2, String>,
158  choices: List<&2, String>
159) -> Arg:
160  Arg{name, short, long, Opt{}, help, required, Fallback{None{}, default}, choices}
161
162# an option that may be given more than once; `get_all` reads every value
163def many(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
164  +name: String,
165  short: Maybe<&2, String>,
166  long: Maybe<&2, String>,
167  +help: String,
168  required: Bool,
169  default: Maybe<&2, String>,
170  choices: List<&2, String>
171) -> Arg:
172  Arg{name, short, long, Many{}, help, required, Fallback{None{}, default}, choices}
173
174# a positional
175def pos(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
176  +name: String,
177  +help: String,
178  required: Bool,
179  default: Maybe<&2, String>,
180  choices: List<&2, String>
181) -> Arg:
182  Arg{name, None{}, None{}, Pos{}, help, required, Fallback{None{}, default}, choices}
183
184# a rest positional: every leftover word, as one name
185def rest(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
186  +name: String,
187  +help: String,
188  required: Bool,
189  default: Maybe<&2, String>,
190  choices: List<&2, String>
191) -> Arg:
192  Arg{name, None{}, None{}, Rest{}, help, required, Fallback{None{}, default}, choices}
193
194# this argument, falling back to the env var `var` (clap's `.env`)
195def env(aa: Arg, +var: String) -> Arg:
196  Arg{+n, +s, +l, kk, +h, +r, Fallback{_e, dd}, cs} = aa
197  Arg{n, s, l, kk, h, r, Fallback{Some{var}, dd}, cs}
198
199# the larger of two Nats
200def help.max(+aa: Nat, +bb: Nat) -> Nat:
201  Bool.pick(Nat, Nat.is_le(aa, bb), bb, aa)
202
203# n spaces
204def help.spaces(nn: Nat) -> String:
205  match nn:
206    case 0n:
207      ""
208    case 1n+p:
209      " " ++ help.spaces(p)
210
211# s padded on the right to width n
212def help.pad(+ss: String, nn: Nat) -> String:
213  ss ++ help.spaces(Nat.sub(nn, String.length(ss)))
214
215# a Maybe string's text, or the default
216def text.of(mm: Maybe<&2, String>, +dd: String) -> String:
217  Maybe.default(&2, String, mm, dd)
218
219# whether a string is a flag token (`-` alone is not)
220def looks_flag(+ss: String) -> Bool:
221  Bool.and(String.starts_with(ss, "-"), Bool.not(String.eq(ss, "-")))
222
223# a buffer of chars consed on the front (the last read first), folded onto acc
224def from.rev.go(cs: List<&2, Char>, acc: String) -> String:
225  match cs:
226    case Nil{}:
227      acc
228    case Con{+h, t}:
229      from.rev.go(t, SCon{h, acc})
230
231# chars reversed into a string
232def from.rev(cs: List<&2, Char>) -> String:
233  from.rev.go(cs, SNil{})
234
235# `name` and an optional `=value`, once the next char is known
236def cut_eq.pick(
237  eq: Bool,
238  acc: List<&2, Char>,
239  tt: List<&2, Char>,
240  rest: String & Maybe<&2, String>
241) -> String & Maybe<&2, String>:
242  match eq:
243    case True{}:
244      (from.rev(acc), Some{String.from_list(tt)})
245    case False{}:
246      rest
247
248# one char of a `name=value` cut
249def cut_eq.chr(
250  +cc: Char,
251  tt: List<&2, Char>,
252  acc: List<&2, Char>,
253  rest: String & Maybe<&2, String>
254) -> String & Maybe<&2, String>:
255  cut_eq.pick(Char.is_eq(cc, '='), acc, tt, rest)
256
257# `name` and an optional `=value` from the body after `--`
258def cut_eq.go(
259  cs: List<&2, Char>,
260  +acc: List<&2, Char>
261) -> String & Maybe<&2, String>:
262  match cs:
263    case Nil{}:
264      (from.rev(acc), None{})
265    case Con{+c, +t}:
266      cut_eq.chr(c, t, acc, cut_eq.go(t, c <> acc))
267
268# `name` and an optional `=value`
269def cut_eq(ss: String) -> String & Maybe<&2, String>:
270  cut_eq.go(String.to_list(ss), [])
271
272# the value glued after a short letter: what follows one `=` when the rest
273# starts with it (possibly empty, as `--name=` is), else the rest when there
274# is any
275def short_of.val(eq: Bool, +rest: String) -> Maybe<&2, String>:
276  match eq:
277    case True{}:
278      Some{String.drop(rest, 1n)}
279    case False{}:
280      Bool.pick(Maybe<&2, String>, String.is_empty(rest), None{}, Some{rest})
281
282# whether this Arg's long spelling is `name`
283def by_long.hit(aa: Arg, +name: String) -> Bool:
284  Arg{_n, _s, long, _k, _h, _r, _d, _c} = aa
285  String.eq(text.of(long, ""), name)
286
287# this Arg when the long spelling matches, else the rest
288def by_long.at(hit: Bool, hh: Arg, rest: Maybe<&2, Arg>) -> Maybe<&2, Arg>:
289  match hit:
290    case True{}:
291      Some{hh}
292    case False{}:
293      rest
294
295# the Arg with this long spelling, if any
296def by_long(args: List<&2, Arg>, +name: String) -> Maybe<&2, Arg>:
297  match args:
298    case Nil{}:
299      None{}
300    case Con{+h, t}:
301      by_long.at(by_long.hit(h, name), h, by_long(t, name))
302
303# whether this Arg's short spelling is `name`
304def by_short.hit(aa: Arg, +name: String) -> Bool:
305  Arg{_n, short, _l, _k, _h, _r, _d, _c} = aa
306  String.eq(text.of(short, ""), name)
307
308# this Arg when the short spelling matches, else the rest
309def by_short.at(hit: Bool, hh: Arg, rest: Maybe<&2, Arg>) -> Maybe<&2, Arg>:
310  match hit:
311    case True{}:
312      Some{hh}
313    case False{}:
314      rest
315
316# the Arg with this short spelling, if any
317def by_short(args: List<&2, Arg>, +name: String) -> Maybe<&2, Arg>:
318  match args:
319    case Nil{}:
320      None{}
321    case Con{+h, t}:
322      by_short.at(by_short.hit(h, name), h, by_short(t, name))
323
324# whether this Arg's name is `name`
325def by_name.hit(aa: Arg, +name: String) -> Bool:
326  Arg{+n, _s, _l, _k, _h, _r, _d, _c} = aa
327  String.eq(n, name)
328
329# this Arg when the binding name matches, else the rest
330def by_name.at(hit: Bool, hh: Arg, rest: Maybe<&2, Arg>) -> Maybe<&2, Arg>:
331  match hit:
332    case True{}:
333      Some{hh}
334    case False{}:
335      rest
336
337# the Arg with this binding name, if any
338def by_name(args: List<&2, Arg>, +name: String) -> Maybe<&2, Arg>:
339  match args:
340    case Nil{}:
341      None{}
342    case Con{+h, t}:
343      by_name.at(by_name.hit(h, name), h, by_name(t, name))
344
345# this Sub when its name matches, else the rest
346def find_sub.at(ss: Sub, rest: Maybe<&2, Sub>, +name: String) -> Maybe<&2, Sub>:
347  Sub{+n, _a, _g, _c} = ss
348  Bool.pick(Maybe<&2, Sub>, String.eq(n, name), Some{ss}, rest)
349
350# the Sub with this name, if any
351def find_sub(subs: List<&2, Sub>, +name: String) -> Maybe<&2, Sub>:
352  match subs:
353    case Nil{}:
354      None{}
355    case Con{+h, t}:
356      find_sub.at(h, find_sub(t, name), name)
357
358# whether this Arg is a positional
359def pos.is.kind(kk: ArgKind) -> Bool:
360  match kk:
361    case Pos{}:
362      True{}
363    case Rest{}:
364      True{}
365    case Flag{}:
366      False{}
367    case Opt{}:
368      False{}
369    case Many{}:
370      False{}
371
372# whether this ArgKind is rest
373def rest.is.kind(kk: ArgKind) -> Bool:
374  match kk:
375    case Rest{}:
376      True{}
377    case Pos{}:
378      False{}
379    case Flag{}:
380      False{}
381    case Opt{}:
382      False{}
383    case Many{}:
384      False{}
385
386# whether this Arg is a positional
387def pos.is(aa: Arg) -> Bool:
388  Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
389  pos.is.kind(kind)
390
391# whether this Arg is a rest positional
392def rest.is(aa: Arg) -> Bool:
393  Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
394  rest.is.kind(kind)
395
396# this Arg kept when it is a positional
397def pos_of.put(keep: Bool, hh: Arg, rest: List<&2, Arg>) -> List<&2, Arg>:
398  match keep:
399    case True{}:
400      hh <> rest
401    case False{}:
402      rest
403
404# the positionals of a spec, in order
405def pos_of(args: List<&2, Arg>) -> List<&2, Arg>:
406  match args:
407    case Nil{}:
408      Nil{}
409    case Con{+h, t}:
410      pos_of.put(pos.is(h), h, pos_of(t))
411
412# whether `v` is among the choices; an empty list accepts any value
413def allowed.ok.at(hit: Bool, rest: Bool) -> Bool:
414  match hit:
415    case True{}:
416      True{}
417    case False{}:
418      rest
419
420# whether `v` is listed; the empty list answers no
421def allowed.ok(cs: List<&2, String>, +vv: String) -> Bool:
422  match cs:
423    case Nil{}:
424      False{}
425    case Con{+h, t}:
426      allowed.ok.at(String.eq(h, vv), allowed.ok(t, vv))
427
428# empty choices accept any value; otherwise `v` must be listed
429def allowed(+cs: List<&2, String>, +vv: String) -> Bool:
430  Bool.or(List.is_empty(&2, String, cs), allowed.ok(cs, vv))
431
432# whether this bind's name is `name`
433def bound.hit(bb: Bind, +name: String) -> Bool:
434  Bind{+n, _v} = bb
435  String.eq(n, name)
436
437# True when the head matches, else the rest
438def bound.at(hit: Bool, rest: Bool) -> Bool:
439  match hit:
440    case True{}:
441      True{}
442    case False{}:
443      rest
444
445# whether `name` is already bound
446def bound(bs: List<&2, Bind>, +name: String) -> Bool:
447  match bs:
448    case Nil{}:
449      False{}
450    case Con{+h, t}:
451      bound.at(bound.hit(h, name), bound(t, name))
452
453# this bind's value when the name matches, else the rest
454def get_all.bind.hit(
455  hit: Bool,
456  +vv: String,
457  more: List<&2, String>
458) -> List<&2, String>:
459  match hit:
460    case True{}:
461      vv <> more
462    case False{}:
463      more
464
465# this bind's value when the name matches, else the rest
466def get_all.bind.at(
467  bb: Bind,
468  more: List<&2, String>,
469  +name: String
470) -> List<&2, String>:
471  Bind{+n, v} = bb
472  get_all.bind.hit(String.eq(n, name), v, more)
473
474# every value bound to `name`
475def get_all.bind(bs: List<&2, Bind>, +name: String) -> List<&2, String>:
476  match bs:
477    case Nil{}:
478      []
479    case Con{+h, t}:
480      get_all.bind.at(h, get_all.bind(t, name), name)
481
482# the bindings this command made, in binding order
483def own(mm: Matched) -> List<&2, Bind>:
484  match mm:
485    case Leaf{bs}:
486      bs
487    case Node{bs, _n, _s}:
488      bs
489
490# every value this command bound to `name`
491def get_all(mm: Matched, +name: String) -> List<&2, String>:
492  get_all.bind(own(mm), name)
493
494# the last of a list of values, or `dflt` when it is empty
495def get.last(vs: List<&2, String>, dflt: Maybe<&2, String>) -> Maybe<&2, String>:
496  match vs:
497    case Nil{}:
498      dflt
499    case Con{hh, tt}:
500      get.last(tt, Some{hh})
501
502# the value bound to `name` last, or None when nothing bound it
503def get(mm: Matched, +name: String) -> Maybe<&2, String>:
504  get.last(get_all(mm, name), None{})
505
506# whether a value is `true`
507def on.of(mv: Maybe<&2, String>) -> Bool:
508  match mv:
509    case None{}:
510      False{}
511    case Some{vv}:
512      String.eq(vv, "true")
513
514# whether a flag named `name` was set
515def on(mm: Matched, +name: String) -> Bool:
516  on.of(get(mm, name))
517
518# the names of the subcommands selected below this command, in order
519def path_of(mm: Matched) -> List<&2, String>:
520  match mm:
521    case Leaf{_b}:
522      []
523    case Node{_b, +name, next}:
524      name <> path_of(next)
525
526# the name of the subcommand selected under this command
527def sub_name(mm: Matched) -> Maybe<&2, String>:
528  match mm:
529    case Leaf{_b}:
530      None{}
531    case Node{_b, name, _s}:
532      Some{name}
533
534# a subcommand's Matched when it is the one asked for
535def sub_of.pick(hit: Bool, next: Matched) -> Maybe<&2, Matched>:
536  match hit:
537    case True{}:
538      Some{next}
539    case False{}:
540      None{}
541
542# the Matched of subcommand `name`, when it is the one selected
543def sub_of(mm: Matched, +name: String) -> Maybe<&2, Matched>:
544  match mm:
545    case Leaf{_b}:
546      None{}
547    case Node{_b, nn, next}:
548      sub_of.pick(String.eq(nn, name), next)
549
550# one name further down, when there is still a Matched to go down from
551def at.step(cur: Maybe<&2, Matched>, +name: String) -> Maybe<&2, Matched>:
552  match cur:
553    case None{}:
554      None{}
555    case Some{mm}:
556      sub_of(mm, name)
557
558# the rest of a path, followed from where the walk down stands
559def at.go(path: List<&2, String>, cur: Maybe<&2, Matched>) -> Maybe<&2, Matched>:
560  match path:
561    case Nil{}:
562      cur
563    case Con{+hh, tt}:
564      at.go(tt, at.step(cur, hh))
565
566# the Matched of the command `path` names below this one, name by name, or
567# None where a name is not the subcommand selected
568def at(mm: Matched, path: List<&2, String>) -> Maybe<&2, Matched>:
569  at.go(path, Some{mm})
570
571# the starting walker for a Cli
572def parse.start(app: Cli) -> St:
573  Cli{_n, _a, _v, +args, subs} = app
574  St{Free{}, args, [], subs, [], [], pos_of(args), False{}, False{}}
575
576# a failed walker that keeps the rest of the state
577def parse.dead(
578  ee: ParseErr,
579  +args: List<&2, Arg>,
580  +up: List<&2, Level>,
581  +subs: List<&2, Sub>,
582  +path: List<&2, String>,
583  +binds: List<&2, Bind>,
584  pos: List<&2, Arg>,
585  +raw: Bool,
586  +seen: Bool
587) -> St:
588  St{Dead{ee}, args, up, subs, path, binds, pos, raw, seen}
589
590# a successful bind of `name` to `val`
591def parse.put(
592  +name: String,
593  +val: String,
594  +args: List<&2, Arg>,
595  +up: List<&2, Level>,
596  +subs: List<&2, Sub>,
597  +path: List<&2, String>,
598  +binds: List<&2, Bind>,
599  +pos: List<&2, Arg>,
600  +raw: Bool,
601  +seen: Bool
602) -> St:
603  St{Free{}, args, up, subs, path, Bind{name, val} <> binds, pos, raw, seen}
604
605# the choices of a found Arg, or none
606def parse.choices(mm: Maybe<&2, Arg>) -> List<&2, String>:
607  match mm:
608    case None{}:
609      []
610    case Some{a}:
611      Arg{_n, _s, _l, _k, _h, _r, _d, cs} = a
612      cs
613
614# bind `name` to `val` when the value is allowed
615def parse.take_choice(
616  ok: Bool,
617  +name: String,
618  +val: String,
619  +args: List<&2, Arg>,
620  +up: List<&2, Level>,
621  +subs: List<&2, Sub>,
622  +path: List<&2, String>,
623  +binds: List<&2, Bind>,
624  +pos: List<&2, Arg>,
625  +raw: Bool,
626  +seen: Bool
627) -> St:
628  match ok:
629    case True{}:
630      parse.put(name, val, args, up, subs, path, binds, pos, raw, seen)
631    case False{}:
632      parse.dead(BadValue{path, name, val}, args, up, subs, path, binds, pos, raw, seen)
633
634# bind an option that already has its value, checked against the choices of
635# the current command's argument of that name: a parent's argument of the same
636# name has its own
637def parse.take_opt_val(
638  +name: String,
639  +val: String,
640  +args: List<&2, Arg>,
641  +up: List<&2, Level>,
642  +subs: List<&2, Sub>,
643  +path: List<&2, String>,
644  +binds: List<&2, Bind>,
645  +pos: List<&2, Arg>,
646  +raw: Bool,
647  +seen: Bool
648) -> St:
649  parse.take_choice(allowed(parse.choices(by_name(args, name)), val), name, val,
650    args, up, subs, path, binds, pos, raw, seen)
651
652# a flag with no glued value is set; a glued value is unexpected
653def parse.take_flag(
654  val: Maybe<&2, String>,
655  +name: String,
656  +orig: String,
657  +args: List<&2, Arg>,
658  +up: List<&2, Level>,
659  +subs: List<&2, Sub>,
660  +path: List<&2, String>,
661  +binds: List<&2, Bind>,
662  pos: List<&2, Arg>,
663  +raw: Bool,
664  +seen: Bool
665) -> St:
666  match val:
667    case None{}:
668      parse.put(name, "true", args, up, subs, path, binds, pos, raw, seen)
669    case Some{_v}:
670      parse.dead(Unexpected{path, orig}, args, up, subs, path, binds, pos, raw, seen)
671
672# an option: glued value now, or the next token
673def parse.take_opt(
674  val: Maybe<&2, String>,
675  +name: String,
676  +args: List<&2, Arg>,
677  +up: List<&2, Level>,
678  +subs: List<&2, Sub>,
679  +path: List<&2, String>,
680  +binds: List<&2, Bind>,
681  +pos: List<&2, Arg>,
682  +raw: Bool,
683  +seen: Bool
684) -> St:
685  match val:
686    case None{}:
687      St{Need{name}, args, up, subs, path, binds, pos, raw, seen}
688    case Some{v}:
689      parse.take_opt_val(name, v, args, up, subs, path, binds, pos, raw, seen)
690
691# a flag or single-valued option given again is refused, whatever the walk
692# would have done with it; the walker keeps the rest of its state
693def parse.once(again: Bool, st: St, +name: String, +path: List<&2, String>) -> St:
694  match again:
695    case True{}:
696      St{_m, +args, +up, +subs, _p, +binds, +pos, +raw, +seen} = st
697      St{Dead{Repeated{path, name}}, args, up, subs, path, binds, pos, raw, seen}
698    case False{}:
699      st
700
701# dispatch on the found Arg's kind
702def parse.take_arg.kind(
703  kk: ArgKind,
704  +name: String,
705  val: Maybe<&2, String>,
706  +orig: String,
707  +args: List<&2, Arg>,
708  +up: List<&2, Level>,
709  +subs: List<&2, Sub>,
710  +path: List<&2, String>,
711  +binds: List<&2, Bind>,
712  +pos: List<&2, Arg>,
713  +raw: Bool,
714  +seen: Bool
715) -> St:
716  match kk:
717    case Flag{}:
718      parse.once(bound(binds, name), parse.take_flag(val, name, orig, args, up, subs, path,
719        binds, pos, raw, seen), name, path)
720    case Opt{}:
721      parse.once(bound(binds, name), parse.take_opt(val, name, args, up, subs, path, binds, pos,
722        raw, seen), name, path)
723    case Many{}:
724      parse.take_opt(val, name, args, up, subs, path, binds, pos, raw, seen)
725    case Pos{}:
726      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
727    case Rest{}:
728      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
729
730# a found Arg, or an unknown flag
731def parse.take_arg(
732  found: Maybe<&2, Arg>,
733  val: Maybe<&2, String>,
734  +orig: String,
735  +args: List<&2, Arg>,
736  +up: List<&2, Level>,
737  +subs: List<&2, Sub>,
738  +path: List<&2, String>,
739  +binds: List<&2, Bind>,
740  pos: List<&2, Arg>,
741  +raw: Bool,
742  +seen: Bool
743) -> St:
744  match found:
745    case None{}:
746      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
747    case Some{a}:
748      Arg{+name, _s, _l, kind, _h, _r, _d, _c} = a
749      parse.take_arg.kind(kind, name, val, orig, args, up, subs, path, binds, pos,
750        raw, seen)
751
752# whether an unknown long option is a request for help: a bare `--help`,
753# with no `=` value, before any positional of the current command is bound
754def long_help(+name: String, val: Maybe<&2, String>, seen: Bool) -> Bool:
755  match val:
756    case None{}:
757      Bool.and(String.eq(name, "help"), Bool.not(seen))
758    case Some{_v}:
759      False{}
760
761# an unknown long option: a request for help (`--help`, as `help`), or an
762# unknown flag
763def parse.take_long.help(
764  hit: Bool,
765  +orig: String,
766  +args: List<&2, Arg>,
767  +up: List<&2, Level>,
768  +subs: List<&2, Sub>,
769  +path: List<&2, String>,
770  +binds: List<&2, Bind>,
771  +pos: List<&2, Arg>,
772  +raw: Bool,
773  +seen: Bool
774) -> St:
775  match hit:
776    case True{}:
777      St{Help{}, args, up, subs, path, binds, pos, raw, seen}
778    case False{}:
779      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
780
781# a long option the current command spells, or an unknown one
782def parse.take_long.found(
783  found: Maybe<&2, Arg>,
784  +name: String,
785  val: Maybe<&2, String>,
786  +orig: String,
787  +args: List<&2, Arg>,
788  +up: List<&2, Level>,
789  +subs: List<&2, Sub>,
790  +path: List<&2, String>,
791  +binds: List<&2, Bind>,
792  +pos: List<&2, Arg>,
793  +raw: Bool,
794  +seen: Bool
795) -> St:
796  match found:
797    case None{}:
798      parse.take_long.help(long_help(name, val, seen), orig, args, up, subs, path,
799        binds, pos, raw, seen)
800    case Some{a}:
801      parse.take_arg(Some{a}, val, orig, args, up, subs, path, binds, pos, raw, seen)
802
803# a long option with a name, or `--=...`
804def parse.take_long.named(
805  empty: Bool,
806  +name: String,
807  val: Maybe<&2, String>,
808  +orig: String,
809  +args: List<&2, Arg>,
810  +up: List<&2, Level>,
811  +subs: List<&2, Sub>,
812  +path: List<&2, String>,
813  +binds: List<&2, Bind>,
814  +pos: List<&2, Arg>,
815  +raw: Bool,
816  +seen: Bool
817) -> St:
818  match empty:
819    case True{}:
820      parse.dead(UnknownFlag{path, orig}, args, up, subs, path, binds, pos, raw, seen)
821    case False{}:
822      parse.take_long.found(by_long(args, name), name, val, orig, args, up, subs,
823        path, binds, pos, raw, seen)
824
825# a long option after the `=` cut
826def parse.take_long.cut(
827  nv: String & Maybe<&2, String>,
828  +orig: String,
829  +args: List<&2, Arg>,
830  +up: List<&2, Level>,
831  +subs: List<&2, Sub>,
832  +path: List<&2, String>,
833  +binds: List<&2, Bind>,
834  pos: List<&2, Arg>,
835  +raw: Bool,
836  +seen: Bool
837) -> St:
838  (+name, val) = nv
839  parse.take_long.named(String.is_empty(name), name, val, orig, args, up, subs,
840    path, binds, pos, raw, seen)
841
842# a long option body after `--`
843def parse.take_long(
844  body: String,
845  +orig: String,
846  +args: List<&2, Arg>,
847  +up: List<&2, Level>,
848  +subs: List<&2, Sub>,
849  +path: List<&2, String>,
850  +binds: List<&2, Bind>,
851  +pos: List<&2, Arg>,
852  +raw: Bool,
853  +seen: Bool
854) -> St:
855  parse.take_long.cut(cut_eq(body), orig, args, up, subs, path, binds, pos, raw,
856    seen)
857
858# a flag's value in a cluster: the rest when it starts with `=` (which
859# `take_arg` refuses), else none, so the next letter goes on
860def cluster.val.flag(eq: Bool, +rest: String) -> Maybe<&2, String>:
861  match eq:
862    case True{}:
863      Some{rest}
864    case False{}:
865      None{}
866
867# the value a letter of this kind gives its argument: an option takes the
868# rest of the word, after one `=`
869def cluster.val.kind(kk: ArgKind, +rest: String) -> Maybe<&2, String>:
870  match kk:
871    case Flag{}:
872      cluster.val.flag(String.starts_with(rest, "="), rest)
873    case Opt{}:
874      short_of.val(String.starts_with(rest, "="), rest)
875    case Many{}:
876      short_of.val(String.starts_with(rest, "="), rest)
877    case Pos{}:
878      None{}
879    case Rest{}:
880      None{}
881
882# the value the letter's argument gets, or none when no argument has it
883def cluster.val(found: Maybe<&2, Arg>, +rest: String) -> Maybe<&2, String>:
884  match found:
885    case None{}:
886      None{}
887    case Some{aa}:
888      Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
889      cluster.val.kind(kind, rest)
890
891# whether a letter of this kind ends the cluster: every kind but a flag that
892# is not followed by `=`
893def cluster.ends.kind(kk: ArgKind, +rest: String) -> Bool:
894  match kk:
895    case Flag{}:
896      String.starts_with(rest, "=")
897    case Opt{}:
898      True{}
899    case Many{}:
900      True{}
901    case Pos{}:
902      True{}
903    case Rest{}:
904      True{}
905
906# whether the letters after this one are no longer read as letters: an
907# unknown letter, an option (they are its value) or a flag given `=`
908def cluster.ends(found: Maybe<&2, Arg>, +rest: String) -> Bool:
909  match found:
910    case None{}:
911      True{}
912    case Some{aa}:
913      Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
914      cluster.ends.kind(kind, rest)
915
916# one letter against a walker an earlier letter failed changes nothing;
917# otherwise it goes through `take_arg`
918def cluster.apply.mode(
919  mode: Mode,
920  +cc: Char,
921  +rest: String,
922  +orig: String,
923  +args: List<&2, Arg>,
924  +up: List<&2, Level>,
925  +subs: List<&2, Sub>,
926  +path: List<&2, String>,
927  +binds: List<&2, Bind>,
928  +pos: List<&2, Arg>,
929  +raw: Bool,
930  +seen: Bool
931) -> St:
932  match mode:
933    case Dead{e}:
934      St{Dead{e}, args, up, subs, path, binds, pos, raw, seen}
935    case _other:
936      +found = by_short(args, SCon{cc, SNil{}})
937      parse.take_arg(found, cluster.val(found, rest), orig, args, up, subs, path, binds, pos,
938        raw, seen)
939
940# one letter against the walker
941def cluster.apply(st: St, +cc: Char, +rest: String, +orig: String) -> St:
942  St{mode, +args, +up, +subs, +path, +binds, +pos, +raw, +seen} = st
943  cluster.apply.mode(mode, cc, rest, orig, args, up, subs, path, binds, pos, raw, seen)
944
945# one letter of a cluster, unless an earlier one ended it
946def cluster.letter(done: Bool, +cc: Char, +rest: String, +orig: String, st: St) -> St:
947  match done:
948    case True{}:
949      st
950    case False{}:
951      cluster.apply(st, cc, rest, orig)
952
953# whether the cluster has ended after this letter
954def cluster.done(done: Bool, +cc: Char, +rest: String, st: St) -> Bool:
955  match done:
956    case True{}:
957      True{}
958    case False{}:
959      St{_m, +args, _g, _s, _p, _b, _o, _r, _n} = st
960      cluster.ends(by_short(args, SCon{cc, SNil{}}), rest)
961
962# every letter of a short cluster `-abc`, in order: a flag binds and the next
963# letter goes on; an option takes the rest of the word, after one `=`, or the
964# next word when nothing is left; an unknown letter, or a flag given `=`,
965# refuses the whole word
966def cluster(body: String, +orig: String, +st: St, +done: Bool) -> St:
967  match body:
968    case SNil{}:
969      st
970    case SCon{+cc, +rest}:
971      cluster(rest, orig, cluster.letter(done, cc, rest, orig, st), cluster.done(done, cc, rest, st))
972
973# whether a short option word is a request for help: `-h` alone, before any
974# positional of the current command is bound, when the command spells
975# neither `-h` nor `--help`
976def short_help(+body: String, +args: List<&2, Arg>, seen: Bool) -> Bool:
977  Bool.and(String.eq(body, "h"),
978    Bool.and(Bool.not(seen),
979      Bool.and(Maybe.is_none(&2, Arg, by_short(args, "h")), Maybe.is_none(&2, Arg, by_long(args, "help")))))
980
981# a request for help (`-h`, as `help`), or a cluster of short options
982def parse.take_short.go(
983  hit: Bool,
984  body: String,
985  +orig: String,
986  +args: List<&2, Arg>,
987  +up: List<&2, Level>,
988  +subs: List<&2, Sub>,
989  +path: List<&2, String>,
990  +binds: List<&2, Bind>,
991  +pos: List<&2, Arg>,
992  +raw: Bool,
993  +seen: Bool
994) -> St:
995  match hit:
996    case True{}:
997      St{Help{}, args, up, subs, path, binds, pos, raw, seen}
998    case False{}:
999      cluster(body, orig, St{Free{}, args, up, subs, path, binds, pos, raw, seen}, False{})
1000
1001# a short option body after `-`
1002def parse.take_short(
1003  +body: String,
1004  +orig: String,
1005  +args: List<&2, Arg>,
1006  +up: List<&2, Level>,
1007  +subs: List<&2, Sub>,
1008  +path: List<&2, String>,
1009  +binds: List<&2, Bind>,
1010  +pos: List<&2, Arg>,
1011  +raw: Bool,
1012  +seen: Bool
1013) -> St:
1014  parse.take_short.go(short_help(body, args, seen), body, orig, args, up, subs, path, binds, pos, raw, seen)
1015
1016# a rest positional stays; a plain one is consumed
1017def parse.take_pos.keep(keep: Bool, hh: Arg, tt: List<&2, Arg>) -> List<&2, Arg>:
1018  match keep:
1019    case True{}:
1020      hh <> tt
1021    case False{}:
1022      tt
1023
1024# the next remaining positional, or an unexpected word
1025def parse.take_pos(
1026  +tok: String,
1027  +args: List<&2, Arg>,
1028  +up: List<&2, Level>,
1029  subs: List<&2, Sub>,
1030  +path: List<&2, String>,
1031  +binds: List<&2, Bind>,
1032  pos: List<&2, Arg>,
1033  raw: Bool
1034) -> St:
1035  match pos:
1036    case Nil{}:
1037      parse.dead(Unexpected{path, tok}, args, up, subs, path, binds, pos, raw, True{})
1038    case Con{+h, t}:
1039      Arg{+name, _s, _l, _k, _h, _r, _d, +cs} = h
1040      parse.take_choice(allowed(cs, tok), name, tok, args, up, subs, path, binds,
1041        parse.take_pos.keep(rest.is(h), h, t), raw, True{})
1042
1043# this Sub's arguments become current, with no bindings of its own; the
1044# command it leaves keeps its arguments and bindings above it
1045def parse.enter(
1046  ss: Sub,
1047  +args: List<&2, Arg>,
1048  +up: List<&2, Level>,
1049  +path: List<&2, String>,
1050  binds: List<&2, Bind>
1051) -> St:
1052  Sub{+name, _a, +next, next_subs} = ss
1053  St{Free{}, next, Level{args, binds} <> up, next_subs,
1054    List.append(&2, String, path, [name]), [], pos_of(next), False{},
1055    False{}}
1056
1057# required and no default → Some{name}
1058def parse.req.go(req: Bool, bare: Bool, +nn: String) -> Maybe<&2, String>:
1059  Bool.pick(Maybe<&2, String>, Bool.and(req, bare), Some{nn}, None{})
1060
1061# a required Arg without a default, as a missing name
1062def parse.req(aa: Arg) -> Maybe<&2, String>:
1063  Arg{+n, _s, _l, _k, _h, +req, Fallback{_e, default}, _c} = aa
1064  parse.req.go(req, Maybe.is_none(&2, String, default), n)
1065
1066# this missing name, else the rest
1067def parse.first_req.at(
1068  here: Maybe<&2, String>,
1069  rest: Maybe<&2, String>
1070) -> Maybe<&2, String>:
1071  match here:
1072    case Some{n}:
1073      Some{n}
1074    case None{}:
1075      rest
1076
1077# a rest stays in the list, so it does not block a subcommand
1078def parse.first_req.skip(skip: Bool, aa: Arg) -> Maybe<&2, String>:
1079  match skip:
1080    case True{}:
1081      None{}
1082    case False{}:
1083      parse.req(aa)
1084
1085# the first leftover required positional
1086def parse.first_req(pos: List<&2, Arg>) -> Maybe<&2, String>:
1087  match pos:
1088    case Nil{}:
1089      None{}
1090    case Con{+h, t}:
1091      parse.first_req.at(parse.first_req.skip(rest.is(h), h), parse.first_req(t))
1092
1093# a leftover required positional blocks entering a subcommand
1094def parse.enter_or(
1095  miss: Maybe<&2, String>,
1096  ss: Sub,
1097  +args: List<&2, Arg>,
1098  +up: List<&2, Level>,
1099  +subs: List<&2, Sub>,
1100  +path: List<&2, String>,
1101  +binds: List<&2, Bind>,
1102  +pos: List<&2, Arg>,
1103  +raw: Bool,
1104  +seen: Bool
1105) -> St:
1106  match miss:
1107    case None{}:
1108      parse.enter(ss, args, up, path, binds)
1109    case Some{n}:
1110      parse.dead(Missing{path, n}, args, up, subs, path, binds, pos, raw, seen)
1111
1112# a found subcommand, or a positional
1113def parse.word.go(
1114  found: Maybe<&2, Sub>,
1115  +tok: String,
1116  +args: List<&2, Arg>,
1117  +up: List<&2, Level>,
1118  +subs: List<&2, Sub>,
1119  +path: List<&2, String>,
1120  +binds: List<&2, Bind>,
1121  +pos: List<&2, Arg>,
1122  +raw: Bool,
1123  +seen: Bool
1124) -> St:
1125  match found:
1126    case None{}:
1127      parse.take_pos(tok, args, up, subs, path, binds, pos, raw)
1128    case Some{s}:
1129      parse.enter_or(parse.first_req(pos), s, args, up, subs, path, binds, pos, raw,
1130        seen)
1131
1132# a word: a subcommand, or a positional
1133def parse.word(
1134  +tok: String,
1135  +args: List<&2, Arg>,
1136  +up: List<&2, Level>,
1137  +subs: List<&2, Sub>,
1138  +path: List<&2, String>,
1139  +binds: List<&2, Bind>,
1140  +pos: List<&2, Arg>,
1141  +raw: Bool,
1142  +seen: Bool
1143) -> St:
1144  parse.word.go(find_sub(subs, tok), tok, args, up, subs, path, binds, pos,
1145    raw, seen)
1146
1147# `-` as a word, or a short option
1148def parse.step.short.go(
1149  alone: Bool,
1150  +tok: String,
1151  +args: List<&2, Arg>,
1152  +up: List<&2, Level>,
1153  +subs: List<&2, Sub>,
1154  +path: List<&2, String>,
1155  +binds: List<&2, Bind>,
1156  +pos: List<&2, Arg>,
1157  +seen: Bool
1158) -> St:
1159  match alone:
1160    case True{}:
1161      parse.word(tok, args, up, subs, path, binds, pos, False{}, seen)
1162    case False{}:
1163      parse.take_short(String.drop(tok, 1n), tok, args, up, subs, path, binds, pos,
1164        False{}, seen)
1165
1166# `-` alone is a positional; otherwise a short option
1167def parse.step.short(
1168  dash: Bool,
1169  +tok: String,
1170  +args: List<&2, Arg>,
1171  +up: List<&2, Level>,
1172  +subs: List<&2, Sub>,
1173  +path: List<&2, String>,
1174  +binds: List<&2, Bind>,
1175  +pos: List<&2, Arg>,
1176  +seen: Bool
1177) -> St:
1178  match dash:
1179    case True{}:
1180      parse.step.short.go(String.is_empty(String.drop(tok, 1n)), tok, args, up, subs, path, binds,
1181        pos, seen)
1182    case False{}:
1183      parse.word(tok, args, up, subs, path, binds, pos, False{}, seen)
1184
1185# `--long` first, then `-s`, then a word
1186def parse.step.kind.go(
1187  long: Bool,
1188  dash: Bool,
1189  +tok: String,
1190  +args: List<&2, Arg>,
1191  +up: List<&2, Level>,
1192  +subs: List<&2, Sub>,
1193  +path: List<&2, String>,
1194  +binds: List<&2, Bind>,
1195  +pos: List<&2, Arg>,
1196  +seen: Bool
1197) -> St:
1198  match long:
1199    case True{}:
1200      parse.take_long(String.drop(tok, 2n), tok, args, up, subs, path, binds, pos,
1201        False{}, seen)
1202    case False{}:
1203      parse.step.short(dash, tok, args, up, subs, path, binds, pos, seen)
1204
1205# a long option, a short option, or a word
1206def parse.step.kind(
1207  +tok: String,
1208  +args: List<&2, Arg>,
1209  +up: List<&2, Level>,
1210  subs: List<&2, Sub>,
1211  +path: List<&2, String>,
1212  +binds: List<&2, Bind>,
1213  +pos: List<&2, Arg>,
1214  +seen: Bool
1215) -> St:
1216  parse.step.kind.go(String.starts_with(tok, "--"), String.starts_with(tok, "-"), tok,
1217    args, up, subs, path, binds, pos, seen)
1218
1219# `help` in command position collects the rest of argv as a path
1220def parse.step.help(
1221  hit: Bool,
1222  +tok: String,
1223  +args: List<&2, Arg>,
1224  +up: List<&2, Level>,
1225  +subs: List<&2, Sub>,
1226  +path: List<&2, String>,
1227  +binds: List<&2, Bind>,
1228  +pos: List<&2, Arg>,
1229  +seen: Bool
1230) -> St:
1231  match hit:
1232    case True{}:
1233      St{Help{}, args, up, subs, path, binds, pos, False{}, seen}
1234    case False{}:
1235      parse.step.kind(tok, args, up, subs, path, binds, pos, seen)
1236
1237# `--` ends option parsing
1238def parse.step.end(
1239  end: Bool,
1240  +tok: String,
1241  +args: List<&2, Arg>,
1242  +up: List<&2, Level>,
1243  +subs: List<&2, Sub>,
1244  +path: List<&2, String>,
1245  +binds: List<&2, Bind>,
1246  +pos: List<&2, Arg>,
1247  +seen: Bool
1248) -> St:
1249  match end:
1250    case True{}:
1251      St{Free{}, args, up, subs, path, binds, pos, True{}, seen}
1252    case False{}:
1253      parse.step.help(Bool.and(String.eq(tok, "help"), Bool.not(seen)), tok, args,
1254        up, subs, path, binds, pos, seen)
1255
1256# after `--`, every token is a positional
1257def parse.step.raw(
1258  raw: Bool,
1259  +tok: String,
1260  +args: List<&2, Arg>,
1261  +up: List<&2, Level>,
1262  +subs: List<&2, Sub>,
1263  +path: List<&2, String>,
1264  +binds: List<&2, Bind>,
1265  +pos: List<&2, Arg>,
1266  +seen: Bool
1267) -> St:
1268  match raw:
1269    case True{}:
1270      parse.take_pos(tok, args, up, subs, path, binds, pos, True{})
1271    case False{}:
1272      parse.step.end(String.eq(tok, "--"), tok, args, up, subs, path, binds, pos,
1273        seen)
1274
1275# a pending option value: a flag-shaped token is a missing value
1276def parse.step.need(
1277  flag: Bool,
1278  +name: String,
1279  +tok: String,
1280  +args: List<&2, Arg>,
1281  +up: List<&2, Level>,
1282  +subs: List<&2, Sub>,
1283  +path: List<&2, String>,
1284  +binds: List<&2, Bind>,
1285  +pos: List<&2, Arg>,
1286  +raw: Bool,
1287  +seen: Bool
1288) -> St:
1289  match flag:
1290    case True{}:
1291      parse.dead(NoValue{path, name}, args, up, subs, path, binds, pos, raw, seen)
1292    case False{}:
1293      parse.take_opt_val(name, tok, args, up, subs, path, binds, pos, raw, seen)
1294
1295# a word after `help`: the subcommand it names, whose own subcommands the
1296# next word is looked up in, or an unexpected word
1297def parse.step.help_path(
1298  found: Maybe<&2, Sub>,
1299  +tok: String,
1300  +args: List<&2, Arg>,
1301  +up: List<&2, Level>,
1302  +subs: List<&2, Sub>,
1303  +path: List<&2, String>,
1304  +binds: List<&2, Bind>,
1305  +pos: List<&2, Arg>,
1306  +raw: Bool,
1307  +seen: Bool
1308) -> St:
1309  match found:
1310    case None{}:
1311      parse.dead(Unexpected{path, tok}, args, up, subs, path, binds, pos, raw, seen)
1312    case Some{ss}:
1313      Sub{_n, _a, _g, next_subs} = ss
1314      St{Help{}, args, up, next_subs, List.append(&2, String, path, [tok]), binds,
1315        pos, raw, seen}
1316
1317# one token against the walker
1318def parse.step.mode(
1319  mode: Mode,
1320  +tok: String,
1321  +args: List<&2, Arg>,
1322  +up: List<&2, Level>,
1323  +subs: List<&2, Sub>,
1324  +path: List<&2, String>,
1325  +binds: List<&2, Bind>,
1326  +pos: List<&2, Arg>,
1327  +raw: Bool,
1328  +seen: Bool
1329) -> St:
1330  match mode:
1331    case Dead{e}:
1332      St{Dead{e}, args, up, subs, path, binds, pos, raw, seen}
1333    case Need{name}:
1334      parse.step.need(looks_flag(tok), name, tok, args, up, subs, path, binds, pos,
1335        raw, seen)
1336    case Help{}:
1337      parse.step.help_path(find_sub(subs, tok), tok, args, up, subs, path, binds, pos, raw,
1338        seen)
1339    case Free{}:
1340      parse.step.raw(raw, tok, args, up, subs, path, binds, pos, seen)
1341
1342# one token
1343def parse.step(+tok: String, st: St) -> St:
1344  St{mode, args, up, subs, path, binds, pending, raw, seen} = st
1345  parse.step.mode(mode, tok, args, up, subs, path, binds, pending, raw, seen)
1346
1347# every token, in order
1348def parse.walk(argv: List<&2, String>, st: St) -> St:
1349  match argv:
1350    case Nil{}:
1351      st
1352    case Con{+h, t}:
1353      parse.walk(t, parse.step(h, st))
1354
1355# a default value kept when the name is not already bound
1356def fill.one(
1357  skip: Bool,
1358  +name: String,
1359  +val: String,
1360  rest: List<&2, Bind>
1361) -> List<&2, Bind>:
1362  match skip:
1363    case True{}:
1364      rest
1365    case False{}:
1366      Bind{name, val} <> rest
1367
1368# a Some default is filled when unbound
1369def fill.arg.go(
1370  dd: Maybe<&2, String>,
1371  +name: String,
1372  +binds: List<&2, Bind>
1373) -> List<&2, Bind>:
1374  match dd:
1375    case None{}:
1376      binds
1377    case Some{v}:
1378      fill.one(bound(binds, name), name, v, binds)
1379
1380# this Arg's default, when it has one and is not bound
1381def fill.arg(aa: Arg, +binds: List<&2, Bind>) -> List<&2, Bind>:
1382  Arg{+n, _s, _l, _k, _h, _r, Fallback{_e, default}, _c} = aa
1383  fill.arg.go(default, n, binds)
1384
1385# defaults of every spec Arg
1386def fill.args(args: List<&2, Arg>, +binds: List<&2, Bind>) -> List<&2, Bind>:
1387  match args:
1388    case Nil{}:
1389      binds
1390    case Con{+h, t}:
1391      fill.arg(h, fill.args(t, binds))
1392
1393# a required name that is not bound
1394def miss.one(
1395  need: Bool,
1396  +name: String,
1397  rest: Maybe<&2, String>
1398) -> Maybe<&2, String>:
1399  match need:
1400    case True{}:
1401      Some{name}
1402    case False{}:
1403      rest
1404
1405# whether this Arg is required and unbound
1406def miss.arg(
1407  aa: Arg,
1408  +binds: List<&2, Bind>,
1409  rest: Maybe<&2, String>
1410) -> Maybe<&2, String>:
1411  Arg{+n, _s, _l, _k, _h, +req, _d, _c} = aa
1412  miss.one(Bool.and(req, Bool.not(bound(binds, n))), n, rest)
1413
1414# the first required name that is not bound
1415def miss.args(args: List<&2, Arg>, +binds: List<&2, Bind>) -> Maybe<&2, String>:
1416  match args:
1417    case Nil{}:
1418      None{}
1419    case Con{+h, t}:
1420      miss.arg(h, binds, miss.args(t, binds))
1421
1422# each command's defaults, filled in among its own bindings
1423def fill.levels(lvs: List<&2, Level>) -> List<&2, Level>:
1424  match lvs:
1425    case Nil{}:
1426      []
1427    case Con{hh, tt}:
1428      Level{+args, binds} = hh
1429      Level{args, fill.args(args, binds)} <> fill.levels(tt)
1430
1431# the first required argument a command left unbound, in list order
1432def miss.levels(lvs: List<&2, Level>) -> Maybe<&2, String>:
1433  match lvs:
1434    case Nil{}:
1435      None{}
1436    case Con{hh, tt}:
1437      Level{+args, +binds} = hh
1438      parse.first_req.at(miss.args(args, binds), miss.levels(tt))
1439
1440# the bindings a command made
1441def level.binds(lv: Level) -> List<&2, Bind>:
1442  Level{_a, binds} = lv
1443  binds
1444
1445# each command's Matched, root first, with the name selected under it
1446def matched.build(lvs: List<&2, Level>, names: List<&2, String>) -> Matched:
1447  match lvs:
1448    case Nil{}:
1449      Leaf{[]}
1450    case Con{hh, tt}:
1451      match names:
1452        case Nil{}:
1453          Leaf{List.reverse(&2, Bind, level.binds(hh))}
1454        case Con{nn, ns}:
1455          Node{List.reverse(&2, Bind, level.binds(hh)), nn, matched.build(tt, ns)}
1456
1457# a missing required name, or the matched result
1458def parse.finish.miss(
1459  mm: Maybe<&2, String>,
1460  path: List<&2, String>,
1461  +lvs: List<&2, Level>
1462) -> Result<&2, &2, ParseErr, Matched>:
1463  match mm:
1464    case Some{n}:
1465      Fail{Missing{path, n}}
1466    case None{}:
1467      Done{matched.build(lvs, path)}
1468
1469# every command's defaults, then its required arguments, root first
1470def parse.finish.ok(+path: List<&2, String>, +lvs: List<&2, Level>) -> Result<&2, &2, ParseErr, Matched>:
1471  parse.finish.miss(miss.levels(lvs), path, lvs)
1472
1473# a finished walker: help, a pending value, an error, or defaults + required
1474def parse.finish.mode(
1475  mode: Mode,
1476  +args: List<&2, Arg>,
1477  +up: List<&2, Level>,
1478  +path: List<&2, String>,
1479  +binds: List<&2, Bind>
1480) -> Result<&2, &2, ParseErr, Matched>:
1481  match mode:
1482    case Dead{e}:
1483      Fail{e}
1484    case Need{name}:
1485      Fail{NoValue{path, name}}
1486    case Help{}:
1487      Fail{NeedHelp{path}}
1488    case Free{}:
1489      parse.finish.ok(path, List.reverse(&2, Level, fill.levels(Level{args, binds} <> up)))
1490
1491# the walker, finished
1492def parse.finish(st: St) -> Result<&2, &2, ParseErr, Matched>:
1493  St{mode, args, up, _s, path, binds, _p, _r, _n} = st
1494  parse.finish.mode(mode, args, up, path, binds)
1495
1496# whether a word refused at `at` asks for the version: `--version`, or `-V`
1497# when the root does not spell `--version`, refused at the root of a spec
1498# with a version
1499def version.asks(+app: Cli, +at: List<&2, String>, +word: String) -> Bool:
1500  Cli{_n, _a, version, args, _s} = app
1501  Bool.and(Bool.or(String.eq(word, "--version"),
1502      Bool.and(String.eq(word, "-V"), Maybe.is_none(&2, Arg, by_long(args, "version")))),
1503    Bool.and(List.is_empty(&2, String, at), Maybe.is_some(&2, String, version)))
1504
1505# an error, or a request for the version when it is one
1506def version.err(+app: Cli, ee: ParseErr) -> ParseErr:
1507  match ee:
1508    case UnknownFlag{+at, +word}:
1509      Bool.pick(ParseErr, version.asks(app, at, word), NeedVersion{}, UnknownFlag{at, word})
1510    case other:
1511      other
1512
1513# a parse's answer, its failure read as a request for the version when it is
1514# one
1515def version.res(+app: Cli, rr: Result<&2, &2, ParseErr, Matched>) -> Result<&2, &2, ParseErr, Matched>:
1516  match rr:
1517    case Done{mm}:
1518      Done{mm}
1519    case Fail{ee}:
1520      Fail{version.err(app, ee)}
1521
1522# argv against a Cli
1523def parse(+app: Cli, argv: List<&2, String>) -> Result<&2, &2, ParseErr, Matched>:
1524  version.res(app, parse.finish(parse.walk(argv, parse.start(app))))
1525
1526# `name version`, when there is a version
1527def version_of.text(+name: String, version: Maybe<&2, String>) -> Maybe<&2, String>:
1528  match version:
1529    case None{}:
1530      None{}
1531    case Some{vv}:
1532      Some{name ++ " " ++ vv}
1533
1534# a spec's `name version`, when it has a version
1535def version_of.cli(app: Cli) -> Maybe<&2, String>:
1536  Cli{+name, _a, version, _g, _s} = app
1537  version_of.text(name, version)
1538
1539# `name version` for a request for the version, of a spec that has one
1540def version_of(+app: Cli, ee: ParseErr) -> Maybe<&2, String>:
1541  match ee:
1542    case NeedVersion{}:
1543      version_of.cli(app)
1544    case _other:
1545      None{}
1546
1547# this pair's value when its name matches, else the rest
1548def env.get.at(hit: Bool, +vv: String, rest: Maybe<&2, String>) -> Maybe<&2, String>:
1549  match hit:
1550    case True{}:
1551      Some{vv}
1552    case False{}:
1553      rest
1554
1555# the value of the first pair named `name`
1556def env.get(vars: List<&2, Var>, +name: String) -> Maybe<&2, String>:
1557  match vars:
1558    case Nil{}:
1559      None{}
1560    case Con{hh, tt}:
1561      (+nn, +vv) = hh
1562      env.get.at(String.eq(nn, name), vv, env.get(tt, name))
1563
1564# a value that is not empty
1565def env.full(mv: Maybe<&2, String>) -> Maybe<&2, String>:
1566  match mv:
1567    case None{}:
1568      None{}
1569    case Some{+vv}:
1570      Bool.pick(Maybe<&2, String>, String.is_empty(vv), None{}, Some{vv})
1571
1572# the env value of an env var: its first pair's value, when that is not empty
1573def env.of(ev: Maybe<&2, String>, vars: List<&2, Var>) -> Maybe<&2, String>:
1574  match ev:
1575    case None{}:
1576      None{}
1577    case Some{+var}:
1578      env.full(env.get(vars, var))
1579
1580# whether an env value turns a flag off, as clap's `SetTrue` reads it
1581def env.off(+vv: String) -> Bool:
1582  allowed.ok(["0", "false", "no", "off", "n", "f"], String.to_lower(vv))
1583
1584# the default an env value gives an argument of this kind: a flag is set
1585# unless the value turns it off; every other kind takes the value
1586def env.kind(kk: ArgKind, +vv: String) -> Maybe<&2, String>:
1587  match kk:
1588    case Flag{}:
1589      Bool.pick(Maybe<&2, String>, env.off(vv), None{}, Some{"true"})
1590    case Opt{}:
1591      Some{vv}
1592    case Many{}:
1593      Some{vv}
1594    case Pos{}:
1595      Some{vv}
1596    case Rest{}:
1597      Some{vv}
1598
1599# a fallback with its default replaced by what the env value gives, when
1600# there is one
1601def resolve.with(
1602  found: Maybe<&2, String>,
1603  kk: ArgKind,
1604  ev: Maybe<&2, String>,
1605  dd: Maybe<&2, String>
1606) -> Fallback:
1607  match found:
1608    case None{}:
1609      Fallback{ev, dd}
1610    case Some{+vv}:
1611      Fallback{ev, env.kind(kk, vv)}
1612
1613# an argument whose default is its fallback under `vars`
1614def resolve.arg(aa: Arg, vars: List<&2, Var>) -> Arg:
1615  Arg{+n, +s, +l, +kk, +h, +r, Fallback{+ev, dd}, +cs} = aa
1616  Arg{n, s, l, kk, h, r, resolve.with(env.of(ev, vars), kk, ev, dd), cs}
1617
1618# every argument's default is its fallback
1619def resolve.args(args: List<&2, Arg>, +vars: List<&2, Var>) -> List<&2, Arg>:
1620  match args:
1621    case Nil{}:
1622      []
1623    case Con{hh, tt}:
1624      resolve.arg(hh, vars) <> resolve.args(tt, vars)
1625
1626# every argument of every subcommand, its default its fallback
1627def resolve.subs(subs: List<&2, Sub>, +vars: List<&2, Var>) -> List<&2, Sub>:
1628  match subs:
1629    case Nil{}:
1630      []
1631    case Con{hh, tt}:
1632      Sub{+n, +a, args, kids} = hh
1633      Sub{n, a, resolve.args(args, vars), resolve.subs(kids, vars)} <> resolve.subs(tt, vars)
1634
1635# the spec whose every argument's default is its fallback under `vars`
1636def resolve(app: Cli, +vars: List<&2, Var>) -> Cli:
1637  Cli{+n, +a, +v, args, subs} = app
1638  Cli{n, a, v, resolve.args(args, vars), resolve.subs(subs, vars)}
1639
1640# whether this kind is a flag
1641def env.flag.is(kk: ArgKind) -> Bool:
1642  match kk:
1643    case Flag{}:
1644      True{}
1645    case Opt{}:
1646      False{}
1647    case Many{}:
1648      False{}
1649    case Pos{}:
1650      False{}
1651    case Rest{}:
1652      False{}
1653
1654# an argument bound to an env value outside its choices: never a flag, and
1655# only for a value its command's bindings hold
1656def env.bad.val(
1657  found: Maybe<&2, String>,
1658  kk: ArgKind,
1659  +name: String,
1660  +cs: List<&2, String>,
1661  +binds: List<&2, Bind>
1662) -> Maybe<&2, Var>:
1663  match found:
1664    case None{}:
1665      None{}
1666    case Some{+vv}:
1667      Bool.pick(Maybe<&2, Var>,
1668        Bool.and(Bool.not(env.flag.is(kk)), Bool.and(Bool.not(allowed(cs, vv)),
1669          List.contains(~String, ~String.eq, get_all.bind(binds, name), vv))),
1670        Some{(name, vv)}, None{})
1671
1672# this argument's name and env value, when its command's bindings hold that
1673# value and its choices do not
1674def env.bad.arg(aa: Arg, vars: List<&2, Var>, +binds: List<&2, Bind>) -> Maybe<&2, Var>:
1675  Arg{+n, _s, _l, kk, _h, _r, Fallback{ev, _d}, +cs} = aa
1676  env.bad.val(env.of(ev, vars), kk, n, cs, binds)
1677
1678# the first of two answers that is one
1679def env.first(here: Maybe<&2, Var>, rest: Maybe<&2, Var>) -> Maybe<&2, Var>:
1680  match here:
1681    case None{}:
1682      rest
1683    case Some{pp}:
1684      Some{pp}
1685
1686# the first argument of a command bound to an env value outside its choices
1687def env.bad.args(
1688  args: List<&2, Arg>,
1689  +vars: List<&2, Var>,
1690  +binds: List<&2, Bind>
1691) -> Maybe<&2, Var>:
1692  match args:
1693    case Nil{}:
1694      None{}
1695    case Con{hh, tt}:
1696      env.first(env.bad.arg(hh, vars, binds), env.bad.args(tt, vars, binds))
1697
1698# the arguments of a found subcommand, or none
1699def env.sub.args(found: Maybe<&2, Sub>) -> List<&2, Arg>:
1700  match found:
1701    case None{}:
1702      []
1703    case Some{ss}:
1704      Sub{_n, _a, args, _k} = ss
1705      args
1706
1707# the subcommands of a found subcommand, or none
1708def env.sub.kids(found: Maybe<&2, Sub>) -> List<&2, Sub>:
1709  match found:
1710    case None{}:
1711      []
1712    case Some{ss}:
1713      Sub{_n, _a, _g, kids} = ss
1714      kids
1715
1716# the first argument bound to an env value outside its choices, the command
1717# first, then down the selected path
1718def env.bad.go(
1719  mm: Matched,
1720  +args: List<&2, Arg>,
1721  +subs: List<&2, Sub>,
1722  +vars: List<&2, Var>
1723) -> Maybe<&2, Var>:
1724  match mm:
1725    case Leaf{+bs}:
1726      env.bad.args(args, vars, bs)
1727    case Node{+bs, +name, next}:
1728      env.first(env.bad.args(args, vars, bs),
1729        env.bad.go(next, env.sub.args(find_sub(subs, name)), env.sub.kids(find_sub(subs, name)), vars))
1730
1731# a success, or the first env value outside its choices that it bound
1732def env.check.done(bad: Maybe<&2, Var>, +mm: Matched) -> Result<&2, &2, ParseErr, Matched>:
1733  match bad:
1734    case None{}:
1735      Done{mm}
1736    case Some{pp}:
1737      (+name, +vv) = pp
1738      Fail{BadValue{path_of(mm), name, vv}}
1739
1740# a successful parse checked for env values outside their choices
1741def env.check.ok(app: Cli, +vars: List<&2, Var>, +mm: Matched) -> Result<&2, &2, ParseErr, Matched>:
1742  Cli{_n, _a, _v, +args, subs} = app
1743  env.check.done(env.bad.go(mm, args, subs, vars), mm)
1744
1745# a failed parse as it is; a successful one checked for env values outside
1746# their choices
1747def env.check(
1748  app: Cli,
1749  +vars: List<&2, Var>,
1750  got: Result<&2, &2, ParseErr, Matched>
1751) -> Result<&2, &2, ParseErr, Matched>:
1752  match got:
1753    case Fail{ee}:
1754      Fail{ee}
1755    case Done{+mm}:
1756      env.check.ok(app, vars, mm)
1757
1758# argv against a Cli, every argument falling back to its env value under
1759# `vars`, then to its default
1760def parse_env(
1761  +app: Cli,
1762  argv: List<&2, String>,
1763  +vars: List<&2, Var>
1764) -> Result<&2, &2, ParseErr, Matched>:
1765  env.check(app, vars, parse(resolve(app, vars), argv))
1766
1767# an env var in front of the names, when there is one
1768def env.names.put(ev: Maybe<&2, String>, rest: List<&2, String>) -> List<&2, String>:
1769  match ev:
1770    case None{}:
1771      rest
1772    case Some{var}:
1773      var <> rest
1774
1775# the env vars of a command's arguments, in order
1776def env.names.args(args: List<&2, Arg>) -> List<&2, String>:
1777  match args:
1778    case Nil{}:
1779      []
1780    case Con{hh, tt}:
1781      Arg{_n, _s, _l, _k, _h, _r, Fallback{ev, _d}, _c} = hh
1782      env.names.put(ev, env.names.args(tt))
1783
1784# the env vars of every subcommand's arguments, depth first
1785def env.names.forest(subs: List<&2, Sub>) -> List<&2, String>:
1786  match subs:
1787    case Nil{}:
1788      []
1789    case Con{hh, tt}:
1790      Sub{_n, _a, args, kids} = hh
1791      List.append(&2, String, env.names.args(args),
1792        List.append(&2, String, env.names.forest(kids), env.names.forest(tt)))
1793
1794# the env vars of a spec: the root's arguments', then every subcommand's
1795def env.names(app: Cli) -> List<&2, String>:
1796  Cli{_n, _a, _v, args, subs} = app
1797  List.append(&2, String, env.names.args(args), env.names.forest(subs))
1798
1799# the short/long label of an option, plus a metavar for Opt
1800def help.label.kind(kk: ArgKind, +name: String, +label: String) -> String:
1801  match kk:
1802    case Flag{}:
1803      label
1804    case Opt{}:
1805      label ++ " <" ++ String.to_upper(name) ++ ">"
1806    case Many{}:
1807      label ++ " <" ++ String.to_upper(name) ++ ">..."
1808    case Pos{}:
1809      label
1810    case Rest{}:
1811      label
1812
1813# `-s, --long` or one of them
1814def help.label.pair(+short: String, +long: String) -> String:
1815  Bool.pick(String, String.is_empty(short),
1816    Bool.pick(String, String.is_empty(long), "", "    --" ++ long),
1817    Bool.pick(String, String.is_empty(long), "  -" ++ short,
1818      "  -" ++ short ++ ", --" ++ long))
1819
1820# the usage label of an option
1821def help.label(aa: Arg) -> String:
1822  Arg{+name, short, long, kind, _h, _r, _d, _c} = aa
1823  help.label.kind(kind, name, help.label.pair(text.of(short, ""), text.of(long, "")))
1824
1825# extras after the help string: default and choices
1826def help.extra.go(+dd: String, +cs: List<&2, String>) -> String:
1827  Bool.pick(String, String.is_empty(dd),
1828    Bool.pick(String, List.is_empty(&2, String, cs), "",
1829      " [possible values: " ++ String.join(cs, ", ") ++ "]"),
1830    Bool.pick(String, List.is_empty(&2, String, cs),
1831      " [default: " ++ dd ++ "]",
1832      " [default: " ++ dd ++ "] [possible values: " ++ String.join(cs, ", ") ++
1833        "]"))
1834
1835# the env var after the help string, before the default
1836def help.env(ev: Maybe<&2, String>) -> String:
1837  match ev:
1838    case None{}:
1839      ""
1840    case Some{var}:
1841      " [env: " ++ var ++ "]"
1842
1843# extras after the help string: env var, default and choices
1844def help.extra(aa: Arg) -> String:
1845  Arg{_n, _s, _l, _k, _h, _r, Fallback{ev, default}, cs} = aa
1846  help.env(ev) ++ help.extra.go(text.of(default, ""), cs)
1847
1848# one option line, given the label width
1849def help.opt_line(+aa: Arg, ww: Nat) -> String:
1850  Arg{_n, _s, _l, _k, +h, _r, _d, _c} = aa
1851  help.pad(help.label(aa), ww) ++ "  " ++ h ++ help.extra(aa)
1852
1853# the max option-label width
1854def help.opt_width(args: List<&2, Arg>, nn: Nat) -> Nat:
1855  match args:
1856    case Nil{}:
1857      nn
1858    case Con{+h, t}:
1859      help.opt_width(t, help.max(nn, String.length(help.label(h))))
1860
1861# a non-positional option line
1862def help.opt_lines.at(skip: Bool, hh: Arg, rest: String, ww: Nat) -> String:
1863  match skip:
1864    case True{}:
1865      rest
1866    case False{}:
1867      help.opt_line(hh, ww) ++ "\n" ++ rest
1868
1869# option lines, skipping positionals
1870def help.opt_lines(args: List<&2, Arg>, +ww: Nat) -> String:
1871  match args:
1872    case Nil{}:
1873      ""
1874    case Con{+h, t}:
1875      help.opt_lines.at(pos.is(h), h, help.opt_lines(t, ww), ww)
1876
1877# wrap option lines in a heading
1878def help.opts.go(+body: String) -> String:
1879  Bool.pick(String, String.is_empty(body), "", "Options:\n" ++ body ++ "\n")
1880
1881# the Options block, or empty when there are none
1882def help.opts(+args: List<&2, Arg>) -> String:
1883  help.opts.go(help.opt_lines(args, help.opt_width(args, 0n)))
1884
1885# a command's name
1886def help.sub_name(ss: Sub) -> String:
1887  Sub{n, _a, _g, _c} = ss
1888  n
1889
1890# a command's about
1891def help.sub_about(ss: Sub) -> String:
1892  Sub{_n, a, _g, _c} = ss
1893  a
1894
1895# max command-name width, including `help`
1896def help.cmd_width(subs: List<&2, Sub>, nn: Nat) -> Nat:
1897  match subs:
1898    case Nil{}:
1899      help.max(nn, String.length("help"))
1900    case Con{+h, t}:
1901      help.cmd_width(t, help.max(nn, String.length(help.sub_name(h))))
1902
1903# one command line
1904def help.cmd_line(+name: String, +about: String, ww: Nat) -> String:
1905  "  " ++ help.pad(name, ww) ++ "  " ++ about ++ "\n"
1906
1907# command lines, then `help`
1908def help.cmd_lines(subs: List<&2, Sub>, +ww: Nat) -> String:
1909  match subs:
1910    case Nil{}:
1911      help.cmd_line("help",
1912        "Print this message or the help of the given subcommand(s)", ww)
1913    case Con{+h, t}:
1914      help.cmd_line(help.sub_name(h), help.sub_about(h), ww) ++ help.cmd_lines(t, ww)
1915
1916# the Commands block
1917def help.cmds(+subs: List<&2, Sub>) -> String:
1918  "Commands:\n" ++ help.cmd_lines(subs, help.cmd_width(subs, 0n)) ++ "\n"
1919
1920# a rest mark: `...`, or empty
1921def help.pos.dots(many: Bool) -> String:
1922  Bool.pick(String, many, "...", "")
1923
1924# a positional in a usage line: `<NAME>` or `[NAME]`
1925def help.pos.wrap(req: Bool, +nn: String) -> String:
1926  Bool.pick(String, req, " <" ++ nn ++ ">", " [" ++ nn ++ "]")
1927
1928# a positional in a usage line: `<NAME>` or `[NAME]`, plus `...` when rest
1929def help.pos.one(aa: Arg) -> String:
1930  Arg{+n, _s, _l, kind, _h, +req, _d, _c} = aa
1931  help.pos.wrap(req, String.to_upper(n)) ++ help.pos.dots(rest.is.kind(kind))
1932
1933# this positional's hint, else the rest
1934def help.pos.at(keep: Bool, hh: Arg, rest: String) -> String:
1935  match keep:
1936    case True{}:
1937      help.pos.one(hh) ++ rest
1938    case False{}:
1939      rest
1940
1941# every positional in a usage line
1942def help.pos(args: List<&2, Arg>) -> String:
1943  match args:
1944    case Nil{}:
1945      ""
1946    case Con{+h, t}:
1947      help.pos.at(pos.is(h), h, help.pos(t))
1948
1949# a positional's label in the Arguments block: its usage mark without the
1950# space before it
1951def help.pos.label(aa: Arg) -> String:
1952  String.drop(help.pos.one(aa), 1n)
1953
1954# one Arguments line, given the label width
1955def help.arg_line(+aa: Arg, ww: Nat) -> String:
1956  Arg{_n, _s, _l, _k, +h, _r, _d, _c} = aa
1957  "  " ++ help.pad(help.pos.label(aa), ww) ++ "  " ++ h ++ help.extra(aa)
1958
1959# the max positional-label width
1960def help.arg_width(args: List<&2, Arg>, nn: Nat) -> Nat:
1961  match args:
1962    case Nil{}:
1963      nn
1964    case Con{+h, t}:
1965      help.arg_width(t, help.max(nn, String.length(help.pos.label(h))))
1966
1967# a positional's Arguments line
1968def help.arg_lines.at(keep: Bool, hh: Arg, rest: String, ww: Nat) -> String:
1969  match keep:
1970    case True{}:
1971      help.arg_line(hh, ww) ++ "\n" ++ rest
1972    case False{}:
1973      rest
1974
1975# Arguments lines, skipping flags and options
1976def help.arg_lines(args: List<&2, Arg>, +ww: Nat) -> String:
1977  match args:
1978    case Nil{}:
1979      ""
1980    case Con{+h, t}:
1981      help.arg_lines.at(pos.is(h), h, help.arg_lines(t, ww), ww)
1982
1983# wrap Arguments lines in a heading
1984def help.args.go(+body: String) -> String:
1985  Bool.pick(String, String.is_empty(body), "", "Arguments:\n" ++ body ++ "\n")
1986
1987# the Arguments block, or empty when there are no positionals
1988def help.args(+args: List<&2, Arg>) -> String:
1989  help.args.go(help.arg_lines(args, help.arg_width(pos_of(args), 0n)))
1990
1991# the bracketed options word when the spec has a flag or option
1992def help.opts_hint.go(has: Bool) -> String:
1993  Bool.pick(String, has, " [" ++ String.to_upper("options") ++ "]", "")
1994
1995# True when this Arg is a flag or option, else the rest
1996def help.has_opt.at(is_pos: Bool, rest: Bool) -> Bool:
1997  match is_pos:
1998    case True{}:
1999      rest
2000    case False{}:
2001      True{}
2002
2003# whether any Arg is not a positional
2004def help.has_opt(args: List<&2, Arg>) -> Bool:
2005  match args:
2006    case Nil{}:
2007      False{}
2008    case Con{+h, t}:
2009      help.has_opt.at(pos.is(h), help.has_opt(t))
2010
2011# the options hint when needed
2012def help.opts_hint(args: List<&2, Arg>) -> String:
2013  help.opts_hint.go(help.has_opt(args))
2014
2015# `[COMMAND]` when there are subcommands
2016def help.cmd_hint(+subs: List<&2, Sub>) -> String:
2017  Bool.pick(String, List.is_empty(&2, Sub, subs), "", " [COMMAND]")
2018
2019# `Usage: name ...`
2020def help.usage(
2021  +name: String,
2022  +args: List<&2, Arg>,
2023  +subs: List<&2, Sub>
2024) -> String:
2025  "Usage: " ++ name ++ help.opts_hint(args) ++ help.pos(args) ++ help.cmd_hint(subs)
2026
2027# `name` or `name version`
2028def title.go(+name: String, vv: Maybe<&2, String>) -> String:
2029  match vv:
2030    case None{}:
2031      name
2032    case Some{ver}:
2033      name ++ " " ++ ver
2034
2035# a built-in spelling a page lists, unless the command spells it itself
2036def help.spell(taken: Maybe<&2, Arg>, +sp: String) -> Maybe<&2, String>:
2037  match taken:
2038    case None{}:
2039      Some{sp}
2040    case Some{_a}:
2041      None{}
2042
2043# the row for `--help`, and `-h` when the command does not spell it; none
2044# when the command spells long `help`
2045def help.help_row(long: Maybe<&2, Arg>, short: Maybe<&2, Arg>) -> List<&2, Arg>:
2046  match long:
2047    case None{}:
2048      [flag("help", help.spell(short, "h"), Some{"help"}, "Print help")]
2049    case Some{_a}:
2050      []
2051
2052# the row for `--version`, and `-V` when the command does not spell it, on a
2053# page with a version; none when the command spells long `version`
2054def help.version_row(version: Maybe<&2, String>, long: Maybe<&2, Arg>, short: Maybe<&2, Arg>) -> List<&2, Arg>:
2055  match version:
2056    case None{}:
2057      []
2058    case Some{_v}:
2059      match long:
2060        case None{}:
2061          [flag("version", help.spell(short, "V"), Some{"version"}, "Print version")]
2062        case Some{_a}:
2063          []
2064
2065# the built-in flags a page lists after its command's own: help, then the
2066# version on the root page
2067def help.builtins(+args: List<&2, Arg>, version: Maybe<&2, String>) -> List<&2, Arg>:
2068  List.append(&2, Arg, help.help_row(by_long(args, "help"), by_short(args, "h")),
2069    help.version_row(version, by_long(args, "version"), by_short(args, "V")))
2070
2071# a command's arguments, then the built-in flags its page lists
2072def help.with(+args: List<&2, Arg>, version: Maybe<&2, String>) -> List<&2, Arg>:
2073  List.append(&2, Arg, args, help.builtins(args, version))
2074
2075# one help page
2076def help.page(
2077  +title: String,
2078  +about: String,
2079  +usage: String,
2080  +args: List<&2, Arg>,
2081  +subs: List<&2, Sub>
2082) -> String:
2083  title ++ "\n" ++ about ++ "\n\n" ++ usage ++ "\n\n" ++ help.cmds(subs) ++
2084    help.args(args) ++ help.opts(args)
2085
2086# a found child becomes the page; an unknown name stays
2087def help.step.go(
2088  found: Maybe<&2, Sub>,
2089  +bin: String,
2090  +about: String,
2091  version: Maybe<&2, String>,
2092  args: List<&2, Arg>,
2093  subs: List<&2, Sub>,
2094  +next: String,
2095  +usage: String
2096) -> How:
2097  match found:
2098    case None{}:
2099      How{bin, about, version, args, subs, usage}
2100    case Some{s}:
2101      Sub{+name, +about2, args2, subs2} = s
2102      How{name, about2, None{}, args2, subs2, usage ++ " " ++ next}
2103
2104# one path segment against the current page
2105def help.step(how: How, +name: String) -> How:
2106  How{+bin, +about, version, args, +subs, +usage} = how
2107  help.step.go(find_sub(subs, name), bin, about, version, args, subs, name,
2108    usage)
2109
2110# the page at the end of a shrinking path
2111def help.go(path: List<&2, String>, how: How) -> String:
2112  match path:
2113    case Nil{}:
2114      How{+bin, +about, +version, +args, +subs, +usage} = how
2115      +all = help.with(args, version)
2116      help.page(title.go(bin, version), about, help.usage(usage, all, subs), all, subs)
2117    case Con{+h, t}:
2118      help.go(t, help.step(how, h))
2119
2120# usage for `path` under `app`; an unknown segment shows the last found page
2121def help(+app: Cli, path: List<&2, String>) -> String:
2122  Cli{+name, +about, version, args, subs} = app
2123  help.go(path, How{name, about, version, args, subs, name})
2124
2125# the usage line of the page at the end of a shrinking path
2126def usage.go(path: List<&2, String>, how: How) -> String:
2127  match path:
2128    case Nil{}:
2129      How{_b, _a, version, +args, +subs, +usage} = how
2130      help.usage(usage, help.with(args, version), subs)
2131    case Con{+hh, tt}:
2132      usage.go(tt, help.step(how, hh))
2133
2134# the usage line of the command at `path`, as `help` shows it
2135def usage.at(+app: Cli, path: List<&2, String>) -> String:
2136  Cli{+name, +about, version, args, subs} = app
2137  usage.go(path, How{name, about, version, args, subs, name})
2138
2139# where to look for more: `help`, and the path when there is one
2140def err.hint(+path: List<&2, String>) -> String:
2141  "For more information, try 'help" ++
2142    Bool.pick(String, List.is_empty(&2, String, path), "", " " ++ String.join(path, " ")) ++ "'.\n"
2143
2144# a short error, the usage line of the command where it happened, and the hint
2145def err.wrap(+app: Cli, +at: List<&2, String>, +msg: String) -> String:
2146  msg ++ "\n\n" ++ usage.at(app, at) ++ "\n\n" ++ err.hint(at)
2147
2148# a flag or an option spelled as an error names it: `--long`, else `-s`,
2149# followed by its value mark, else its name when it has no spelling
2150def err.spelled(+short: String, +long: String, +name: String, +mark: String) -> String:
2151  Bool.pick(String, String.is_empty(long),
2152    Bool.pick(String, String.is_empty(short), name, "-" ++ short ++ mark),
2153    "--" ++ long ++ mark)
2154
2155# an argument of this kind as an error names it
2156def err.form.kind(kk: ArgKind, +aa: Arg, +name: String, +sh: String, +lo: String) -> String:
2157  match kk:
2158    case Flag{}:
2159      err.spelled(sh, lo, name, "")
2160    case Opt{}:
2161      err.spelled(sh, lo, name, " <" ++ String.to_upper(name) ++ ">")
2162    case Many{}:
2163      err.spelled(sh, lo, name, " <" ++ String.to_upper(name) ++ ">...")
2164    case Pos{}:
2165      help.pos.label(aa)
2166    case Rest{}:
2167      help.pos.label(aa)
2168
2169# an argument as an error names it, as clap's: a flag by its spelling, an
2170# option by its spelling and value mark, a positional by its usage mark
2171def err.form(+aa: Arg) -> String:
2172  Arg{+name, short, long, kind, _h, _r, _d, _c} = aa
2173  err.form.kind(kind, aa, name, text.of(short, ""), text.of(long, ""))
2174
2175# the argument found here, else the one found above
2176def err.find.here(found: Maybe<&2, Arg>, best: Maybe<&2, Arg>) -> Maybe<&2, Arg>:
2177  match found:
2178    case None{}:
2179      best
2180    case Some{aa}:
2181      Some{aa}
2182
2183# the arguments of a page's command
2184def help.how_args(how: How) -> List<&2, Arg>:
2185  How{_b, _a, _v, args, _s, _u} = how
2186  args
2187
2188# the argument named `name` on the deepest page a path walks through that
2189# has one, else `best`
2190def err.find.go(path: List<&2, String>, +how: How, +name: String, best: Maybe<&2, Arg>) -> Maybe<&2, Arg>:
2191  match path:
2192    case Nil{}:
2193      err.find.here(by_name(help.how_args(how), name), best)
2194    case Con{+hh, tt}:
2195      err.find.go(tt, help.step(how, hh), name, err.find.here(by_name(help.how_args(how), name), best))
2196
2197# the argument named `name` of the deepest command on `at` that has one
2198def err.find(+app: Cli, at: List<&2, String>, +name: String) -> Maybe<&2, Arg>:
2199  Cli{+bin, +about, version, args, subs} = app
2200  err.find.go(at, How{bin, about, version, args, subs, bin}, name, None{})
2201
2202# a found argument's display form, else the name
2203def err.named(found: Maybe<&2, Arg>, +name: String) -> String:
2204  match found:
2205    case None{}:
2206      name
2207    case Some{aa}:
2208      err.form(aa)
2209
2210# the argument an error names, as it names it
2211def err.name(+app: Cli, at: List<&2, String>, +name: String) -> String:
2212  err.named(err.find(app, at, name), name)
2213
2214# clap's line of the values a found argument allows, or nothing
2215def err.values(found: Maybe<&2, Arg>) -> String:
2216  match found:
2217    case None{}:
2218      ""
2219    case Some{aa}:
2220      Arg{_n, _s, _l, _k, _h, _r, _d, +cs} = aa
2221      Bool.pick(String, List.is_empty(&2, String, cs), "",
2222        "\n  [possible values: " ++ String.join(cs, ", ") ++ "]")
2223
2224# the head of a row, or 0 past its end
2225def osa.head(xs: List<&2, Nat>) -> Nat:
2226  match xs:
2227    case Nil{}:
2228      0n
2229    case Con{hh, _t}:
2230      hh
2231
2232# a row after its head
2233def osa.tail(xs: List<&2, Nat>) -> List<&2, Nat>:
2234  match xs:
2235    case Nil{}:
2236      []
2237    case Con{_h, tt}:
2238      tt
2239
2240# the last cell of a row, `dd` for an empty one
2241def osa.last(xs: List<&2, Nat>, dd: Nat) -> Nat:
2242  match xs:
2243    case Nil{}:
2244      dd
2245    case Con{hh, tt}:
2246      osa.last(tt, hh)
2247
2248# the first row: `ii`, then one more for each char
2249def osa.first(bs: List<&2, Char>, +ii: Nat) -> List<&2, Nat>:
2250  match bs:
2251    case Nil{}:
2252      [ii]
2253    case Con{_c, tt}:
2254      ii <> osa.first(tt, 1n+ii)
2255
2256# whether the char before `cb` is `ca`, once the char before `ca` is `xa`
2257def osa.swap.b(+xa: Char, pb: Maybe<&2, Char>, +ca: Char, +cb: Char) -> Bool:
2258  match pb:
2259    case None{}:
2260      False{}
2261    case Some{xb}:
2262      Bool.and(Char.is_eq(ca, xb), Char.is_eq(xa, cb))
2263
2264# whether the two chars before these, swapped, are these two
2265def osa.swap(pa: Maybe<&2, Char>, pb: Maybe<&2, Char>, +ca: Char, +cb: Char) -> Bool:
2266  match pa:
2267    case None{}:
2268      False{}
2269    case Some{xa}:
2270      osa.swap.b(xa, pb, ca, cb)
2271
2272# the cheaper of a cell and a swap from two rows up and two cells left
2273def osa.cell.swap(swap: Bool, +best: Nat, +far: Nat) -> Nat:
2274  Bool.pick(Nat, swap, Nat.min(best, 1n+far), best)
2275
2276# one cell: the cheapest of a deletion, an insertion, a substitution and a
2277# swap of two adjacent chars
2278def osa.cell(
2279  swap: Bool,
2280  +up: Nat,
2281  +left: Nat,
2282  +diag: Nat,
2283  +cost: Nat,
2284  +far: Nat
2285) -> Nat:
2286  osa.cell.swap(swap, Nat.min(Nat.min(1n+up, 1n+left), Nat.add(diag, cost)), far)
2287
2288# the rest of a row for the char `ca`, whose char before is `pa`: `ps` is the
2289# row above from the cell above-left on, `qs` the row two up from two cells
2290# left on, `pb` the char of `bs` before its head
2291def osa.row(
2292  bs: List<&2, Char>,
2293  +ca: Char,
2294  +pa: Maybe<&2, Char>,
2295  pb: Maybe<&2, Char>,
2296  left: Nat,
2297  +ps: List<&2, Nat>,
2298  +qs: List<&2, Nat>
2299) -> List<&2, Nat>:
2300  match bs:
2301    case Nil{}:
2302      []
2303    case Con{+cb, bt}:
2304      +rr = osa.cell(osa.swap(pa, pb, ca, cb), osa.head(osa.tail(ps)), left, osa.head(ps),
2305        Bool.pick(Nat, Char.is_eq(ca, cb), 0n, 1n), osa.head(qs))
2306      rr <> osa.row(bt, ca, pa, Some{cb}, rr, osa.tail(ps), osa.tail(qs))
2307
2308# the rows for the chars of `as`, the last row `pp` and the one before `qq`,
2309# down to the distance in the last row's last cell
2310def osa.rows(
2311  as: List<&2, Char>,
2312  +bs: List<&2, Char>,
2313  pa: Maybe<&2, Char>,
2314  +ii: Nat,
2315  +pp: List<&2, Nat>,
2316  qq: List<&2, Nat>
2317) -> Nat:
2318  match as:
2319    case Nil{}:
2320      osa.last(pp, 0n)
2321    case Con{+ca, at}:
2322      osa.rows(at, bs, Some{ca}, 1n+ii, (1n+ii) <> osa.row(bs, ca, pa, None{}, 1n+ii, pp, 0n <> qq), pp)
2323
2324# the optimal string alignment distance from `aa` to `bb`: the fewest
2325# insertions, deletions, substitutions and swaps of two adjacent chars, no
2326# char edited twice
2327def osa(aa: String, bb: String) -> Nat:
2328  +bs = String.to_list(bb)
2329  osa.rows(String.to_list(aa), bs, None{}, 0n, osa.first(bs, 0n), osa.first(bs, 0n))
2330
2331# whether a candidate is close to the typed spelling
2332def sug.close.go(+dd: Nat, +room: Nat) -> Bool:
2333  Bool.and(Nat.is_lt(0n, dd), Nat.is_le(Nat.mul(3n, dd), room))
2334
2335# whether `cc` is close to `typed`: some edits away, and at most a third of
2336# the longer as many
2337def sug.close(+typed: String, +cc: String) -> Bool:
2338  sug.close.go(osa(typed, cc), Nat.max(String.length(typed), String.length(cc)))
2339
2340# a close candidate against the closest one after it: the earlier on a tie
2341def sug.keep.rest(+typed: String, +cc: String, rest: Maybe<&2, String>) -> Maybe<&2, String>:
2342  match rest:
2343    case None{}:
2344      Some{cc}
2345    case Some{+ww}:
2346      Bool.pick(Maybe<&2, String>, Nat.is_le(osa(typed, cc), osa(typed, ww)), Some{cc}, Some{ww})
2347
2348# a candidate, when it is close, against the closest one after it
2349def sug.keep(close: Bool, +typed: String, +cc: String, rest: Maybe<&2, String>) -> Maybe<&2, String>:
2350  match close:
2351    case False{}:
2352      rest
2353    case True{}:
2354      sug.keep.rest(typed, cc, rest)
2355
2356# the closest close candidate, the first among equals
2357def sug.best(cands: List<&2, String>, +typed: String) -> Maybe<&2, String>:
2358  match cands:
2359    case Nil{}:
2360      None{}
2361    case Con{+cc, tt}:
2362      sug.keep(sug.close(typed, cc), typed, cc, sug.best(tt, typed))
2363
2364# a long spelling in front of the rest, when there is one
2365def sug.cands.put(long: Maybe<&2, String>, rest: List<&2, String>) -> List<&2, String>:
2366  match long:
2367    case None{}:
2368      rest
2369    case Some{ll}:
2370      ll <> rest
2371
2372# the long spellings of a command's arguments, in order
2373def sug.cands(args: List<&2, Arg>) -> List<&2, String>:
2374  match args:
2375    case Nil{}:
2376      []
2377    case Con{hh, tt}:
2378      Arg{_n, _s, long, _k, _h, _r, _d, _c} = hh
2379      sug.cands.put(long, sug.cands(tt))
2380
2381# the arguments of the page at the end of a shrinking path
2382def sug.args.go(path: List<&2, String>, how: How) -> List<&2, Arg>:
2383  match path:
2384    case Nil{}:
2385      How{_b, _a, _v, args, _s, _u} = how
2386      args
2387    case Con{+hh, tt}:
2388      sug.args.go(tt, help.step(how, hh))
2389
2390# the arguments of the command at `path`, reached as `help` reaches it
2391def sug.args(+app: Cli, path: List<&2, String>) -> List<&2, Arg>:
2392  Cli{+name, +about, version, args, subs} = app
2393  sug.args.go(path, How{name, about, version, args, subs, name})
2394
2395# the spelling a long option word was typed with: its chars up to `=`
2396def sug.typed(cut: String & Maybe<&2, String>) -> String:
2397  (nn, _v) = cut
2398  nn
2399
2400# a candidate spelled as a long option word
2401def sug.found(mm: Maybe<&2, String>) -> Maybe<&2, String>:
2402  match mm:
2403    case None{}:
2404      None{}
2405    case Some{cc}:
2406      Some{"--" ++ cc}
2407
2408# the suggestion for a word, when it is a long option word
2409def sug.word.go(long: Bool, +app: Cli, +at: List<&2, String>, +word: String) -> Maybe<&2, String>:
2410  match long:
2411    case False{}:
2412      None{}
2413    case True{}:
2414      sug.found(sug.best(sug.cands(sug.args(app, at)), sug.typed(cut_eq(String.drop(word, 2n)))))
2415
2416# the long spelling a word refused at `at` was likely meant to be
2417def sug.word(+app: Cli, +at: List<&2, String>, +word: String) -> Maybe<&2, String>:
2418  sug.word.go(String.starts_with(word, "--"), app, at, word)
2419
2420# the long spelling an unknown long option was likely meant to be, as clap's
2421# "a similar argument exists"; None for every other error
2422def suggestion(+app: Cli, ee: ParseErr) -> Maybe<&2, String>:
2423  match ee:
2424    case UnknownFlag{+at, +word}:
2425      sug.word(app, at, word)
2426    case Missing{_at, _name}:
2427      None{}
2428    case NoValue{_at, _name}:
2429      None{}
2430    case BadValue{_at, _name, _value}:
2431      None{}
2432    case NeedHelp{_path}:
2433      None{}
2434    case Unexpected{_at, _arg}:
2435      None{}
2436    case Repeated{_at, _name}:
2437      None{}
2438    case NeedVersion{}:
2439      None{}
2440
2441# clap's tip line for a suggestion, or nothing
2442def sug.tip(mm: Maybe<&2, String>) -> String:
2443  match mm:
2444    case None{}:
2445      ""
2446    case Some{ss}:
2447      "\n\n  tip: a similar argument exists: '" ++ ss ++ "'"
2448
2449# error text; NeedHelp and NeedVersion are empty (the caller prints `help`,
2450# or `version_of`)
2451def err_text(+app: Cli, ee: ParseErr) -> String:
2452  match ee:
2453    case UnknownFlag{+at, +word}:
2454      err.wrap(app, at, "error: unexpected argument '" ++ word ++ "' found" ++ sug.tip(sug.word(app, at, word)))
2455    case Missing{+at, +name}:
2456      err.wrap(app, at, "error: the following required argument was not provided:\n  " ++
2457        err.name(app, at, name))
2458    case NoValue{+at, +name}:
2459      err.wrap(app, at, "error: a value is required for '" ++ err.name(app, at, name) ++ "' but none was supplied")
2460    case BadValue{+at, +name, value}:
2461      err.wrap(app, at, "error: invalid value '" ++ value ++ "' for '" ++ err.name(app, at, name) ++ "'" ++
2462        err.values(err.find(app, at, name)))
2463    case NeedHelp{_path}:
2464      ""
2465    case Unexpected{+at, arg}:
2466      err.wrap(app, at, "error: unexpected argument '" ++ arg ++ "' found")
2467    case Repeated{+at, +name}:
2468      err.wrap(app, at, "error: the argument '" ++ err.name(app, at, name) ++ "' cannot be used multiple times")
2469    case NeedVersion{}:
2470      ""