src/check.bend

shake@0.7.0.0 · 302 lines · 31 definitions

1# shake/check: the ways a Cli can contradict itself, internal (main.bend
2# exports `check`). `parse` does not call it: a program checks its spec once,
3# and every guarantee of SPEC.md's parse rows holds for a spec `check` passes.
4import Base
5import shake@0.7.0.0/src/cli.bend as C
6
7# one way a spec contradicts itself, at the command path where it does
8type SpecErr is Data:
9  RestNotLast{path: List<&2, String>, name: String}
10  SameName{path: List<&2, String>, name: String}
11  SameShort{path: List<&2, String>, short: String}
12  SameLong{path: List<&2, String>, long: String}
13  SameSub{path: List<&2, String>, name: String}
14  HelpSub{path: List<&2, String>}
15  DefaultNotChoice{path: List<&2, String>, name: String, value: String}
16  RequiredAfterOptional{path: List<&2, String>, name: String}
17
18# one report when the flag is set, else none
19def one(hit: Bool, err: SpecErr) -> List<&2, SpecErr>:
20  match hit:
21    case True{}:
22      [err]
23    case False{}:
24      []
25
26# two lists of reports, one after the other
27def both(xs: List<&2, SpecErr>, ys: List<&2, SpecErr>) -> List<&2, SpecErr>:
28  List.append(&2, SpecErr, xs, ys)
29
30# whether a spelling, when there is one, is among those already seen
31def spelled.seen(sp: Maybe<&2, String>, +seen: List<&2, String>) -> Bool:
32  match sp:
33    case None{}:
34      False{}
35    case Some{ss}:
36      List.contains(~String, ~String.eq, seen, ss)
37
38# the spellings seen, with this one when there is one
39def spelled.add(sp: Maybe<&2, String>, seen: List<&2, String>) -> List<&2, String>:
40  match sp:
41    case None{}:
42      seen
43    case Some{ss}:
44      ss <> seen
45
46# a default outside a nonempty choices list
47def args.default(
48  dflt: Maybe<&2, String>,
49  +cs: List<&2, String>,
50  +path: List<&2, String>,
51  +name: String
52) -> List<&2, SpecErr>:
53  match dflt:
54    case None{}:
55      []
56    case Some{+vv}:
57      one(Bool.and(Bool.not(List.is_empty(&2, String, cs)), Bool.not(C.allowed.ok(cs, vv))),
58        DefaultNotChoice{path, name, vv})
59
60# each argument's name and spellings against the earlier ones', and its
61# default against its choices
62def args.dups(
63  args: List<&2, C.Arg>,
64  +path: List<&2, String>,
65  +names: List<&2, String>,
66  +shorts: List<&2, String>,
67  +longs: List<&2, String>
68) -> List<&2, SpecErr>:
69  match args:
70    case Nil{}:
71      []
72    case Con{hh, tt}:
73      C.Arg{+name, +short, +long, _k, _h, _r, C.Fallback{_e, dflt}, +cs} = hh
74      both(one(List.contains(~String, ~String.eq, names, name), SameName{path, name}),
75        both(one(spelled.seen(short, shorts), SameShort{path, C.text.of(short, "")}),
76          both(one(spelled.seen(long, longs), SameLong{path, C.text.of(long, "")}),
77            both(args.default(dflt, cs, path, name),
78              args.dups(tt, path, name <> names, spelled.add(short, shorts),
79                spelled.add(long, longs))))))
80
81# the positionals in order: a rest before the last, and a required one after
82# an optional one
83def pos.order(
84  pos: List<&2, C.Arg>,
85  +path: List<&2, String>,
86  +opt_seen: Bool
87) -> List<&2, SpecErr>:
88  match pos:
89    case Nil{}:
90      []
91    case Con{hh, +tt}:
92      C.Arg{+name, _s, _l, kind, _h, +req, _d, _c} = hh
93      both(one(Bool.and(C.rest.is.kind(kind), Bool.not(List.is_empty(&2, C.Arg, tt))),
94          RestNotLast{path, name}),
95        both(one(Bool.and(req, opt_seen), RequiredAfterOptional{path, name}),
96          pos.order(tt, path, Bool.or(opt_seen, Bool.not(req)))))
97
98# each subcommand's name against the earlier ones', and against `help`
99def subs.dups(
100  subs: List<&2, C.Sub>,
101  +path: List<&2, String>,
102  +names: List<&2, String>
103) -> List<&2, SpecErr>:
104  match subs:
105    case Nil{}:
106      []
107    case Con{hh, tt}:
108      C.Sub{+name, _a, _g, _c} = hh
109      both(one(List.contains(~String, ~String.eq, names, name), SameSub{path, name}),
110        both(one(String.eq(name, "help"), HelpSub{path}),
111          subs.dups(tt, path, name <> names)))
112
113# one command's own reports
114def cmd(
115  +path: List<&2, String>,
116  +args: List<&2, C.Arg>,
117  subs: List<&2, C.Sub>
118) -> List<&2, SpecErr>:
119  both(args.dups(args, path, [], [], []),
120    both(pos.order(C.pos_of(args), path, False{}), subs.dups(subs, path, [])))
121
122# a name in front of a reversed path
123def pushed(name: String, back: List<&2, String>) -> List<&2, String>:
124  name <> back
125
126# every subcommand's reports, each under its own path, depth first. The path
127# is carried reversed, innermost name first, and read the right way round
128# once per command
129def forest(subs: List<&2, C.Sub>, +back: List<&2, String>) -> List<&2, SpecErr>:
130  match subs:
131    case Nil{}:
132      []
133    case Con{hh, tt}:
134      C.Sub{+name, _a, +args, +kids} = hh
135      +here = pushed(name, back)
136      both(cmd(List.reverse(&2, String, here), args, kids),
137        both(forest(kids, here), forest(tt, back)))
138
139# every way the spec contradicts itself: the root's reports, then each
140# subcommand's
141def check(app: C.Cli) -> List<&2, SpecErr>:
142  C.Cli{_n, _a, _v, +args, +subs} = app
143  both(cmd([], args, subs), forest(subs, []))
144
145# where a report is: the root, or a subcommand's path
146def at.pick(root: Bool, +path: List<&2, String>) -> String:
147  match root:
148    case True{}:
149      "spec: "
150    case False{}:
151      "spec, command '" ++ String.join(path, " ") ++ "': "
152
153# where a report is
154def at(+path: List<&2, String>) -> String:
155  at.pick(List.is_empty(&2, String, path), path)
156
157# a report as one line
158def text(err: SpecErr) -> String:
159  match err:
160    case RestNotLast{path, name}:
161      at(path) ++ "rest positional '" ++ name ++ "' is not the last positional"
162    case SameName{path, name}:
163      at(path) ++ "two arguments are named '" ++ name ++ "'"
164    case SameShort{path, short}:
165      at(path) ++ "two arguments are spelled '-" ++ short ++ "'"
166    case SameLong{path, long}:
167      at(path) ++ "two arguments are spelled '--" ++ long ++ "'"
168    case SameSub{path, name}:
169      at(path) ++ "two subcommands are named '" ++ name ++ "'"
170    case HelpSub{path}:
171      at(path) ++ "a subcommand is named 'help', which `parse` keeps for help"
172    case DefaultNotChoice{path, name, value}:
173      at(path) ++ "the default '" ++ value ++ "' of '" ++ name ++ "' is not one of its choices"
174    case RequiredAfterOptional{path, name}:
175      at(path) ++ "required positional '" ++ name ++ "' follows an optional one"
176
177# how a program reads an argument: whether a flag is on (`on`), or its values
178# (`get`, `get_all`)
179type Want is Data:
180  WantFlag{}
181  WantValue{}
182
183# one read a program makes: the command path, the argument's name, and how it
184# reads it
185type Read is Data:
186  Read{path: List<&2, String>, name: String, want: Want}
187
188# one read that does not fit the spec
189type ReadErr is Data:
190  NoCommand{path: List<&2, String>}
191  NoArg{path: List<&2, String>, name: String}
192  NotFlag{path: List<&2, String>, name: String}
193  IsFlag{path: List<&2, String>, name: String}
194
195# a read report when the flag is set, else none
196def reads.one(hit: Bool, err: ReadErr) -> List<&2, ReadErr>:
197  match hit:
198    case True{}:
199      [err]
200    case False{}:
201      []
202
203# the arguments of a found command
204def reads.args(here: Maybe<&2, C.Sub>) -> Maybe<&2, List<&2, C.Arg>>:
205  match here:
206    case None{}:
207      None{}
208    case Some{ss}:
209      C.Sub{_n, _a, args, _s} = ss
210      Some{args}
211
212# the subcommand named `name` of a found command
213def reads.down(here: Maybe<&2, C.Sub>, +name: String) -> Maybe<&2, C.Sub>:
214  match here:
215    case None{}:
216      None{}
217    case Some{ss}:
218      C.Sub{_n, _a, _g, subs} = ss
219      C.find_sub(subs, name)
220
221# the arguments of the command a path names below the command found, each
222# name a subcommand of the command before it, or None
223def reads.cmd(path: List<&2, String>, here: Maybe<&2, C.Sub>) -> Maybe<&2, List<&2, C.Arg>>:
224  match path:
225    case Nil{}:
226      reads.args(here)
227    case Con{+hh, tt}:
228      reads.cmd(tt, reads.down(here, hh))
229
230# whether an argument of this kind is a flag
231def reads.flag(kk: C.ArgKind) -> Bool:
232  match kk:
233    case C.Flag{}:
234      True{}
235    case C.Opt{}:
236      False{}
237    case C.Pos{}:
238      False{}
239    case C.Rest{}:
240      False{}
241    case C.Many{}:
242      False{}
243
244# a read of an argument that is, or is not, a flag
245def reads.want(want: Want, flag: Bool, +path: List<&2, String>, +name: String) -> List<&2, ReadErr>:
246  match want:
247    case WantFlag{}:
248      reads.one(Bool.not(flag), NotFlag{path, name})
249    case WantValue{}:
250      reads.one(flag, IsFlag{path, name})
251
252# a read of the argument found under its name, or of none
253def reads.arg(found: Maybe<&2, C.Arg>, want: Want, +path: List<&2, String>, +name: String) -> List<&2, ReadErr>:
254  match found:
255    case None{}:
256      [NoArg{path, name}]
257    case Some{aa}:
258      C.Arg{_n, _s, _l, kind, _h, _r, _d, _c} = aa
259      reads.want(want, reads.flag(kind), path, name)
260
261# a read of the command a path names, or of none
262def reads.at(
263  cmd: Maybe<&2, List<&2, C.Arg>>,
264  want: Want,
265  +path: List<&2, String>,
266  +name: String
267) -> List<&2, ReadErr>:
268  match cmd:
269    case None{}:
270      [NoCommand{path}]
271    case Some{args}:
272      reads.arg(C.by_name(args, name), want, path, name)
273
274# what is wrong with one read, or nothing
275def read(app: C.Cli, rr: Read) -> List<&2, ReadErr>:
276  C.Cli{+bin, +about, _v, args, subs} = app
277  Read{+path, +name, want} = rr
278  reads.at(reads.cmd(path, Some{C.Sub{bin, about, args, subs}}), want, path, name)
279
280# what is wrong with each read, in order
281def check_reads(+app: C.Cli, rs: List<&2, Read>) -> List<&2, ReadErr>:
282  match rs:
283    case Nil{}:
284      []
285    case Con{hh, tt}:
286      List.append(&2, ReadErr, read(app, hh), check_reads(app, tt))
287
288# where a read report is
289def read.at(+path: List<&2, String>) -> String:
290  Bool.pick(String, List.is_empty(&2, String, path), "read: ", "read, command '" ++ String.join(path, " ") ++ "': ")
291
292# a read report as one line
293def read_text(err: ReadErr) -> String:  # noqa: L001 a message: its words are not a guarantee
294  match err:
295    case NoCommand{+path}:
296      read.at(path) ++ "no command is named so"
297    case NoArg{+path, name}:
298      read.at(path) ++ "no argument is named '" ++ name ++ "'"
299    case NotFlag{+path, name}:
300      read.at(path) ++ "'" ++ name ++ "' is read as a flag, but it is not one"
301    case IsFlag{+path, name}:
302      read.at(path) ++ "'" ++ name ++ "' is read for a value, but it is a flag"