src/check.bend
shake@0.4.0.0 · 175 lines · 0 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.4.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, 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"