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