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