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.
4	import Base
5	import ./cli.bend as C
6	
7	# one way a spec contradicts itself, at the command path where it does
8	type 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
19	def 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
27	def 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
31	def 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
39	def 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
47	def 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
62	def 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
83	def 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`
99	def 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
114	def 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
123	def 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
129	def 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
141	def 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
146	def 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
154	def at(+path: List<&2, String>) -> String:
155	  at.pick(List.is_empty(&2, String, path), path)
156	
157	# a report as one line
158	def 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`)
179	type 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
185	type Read is Data:
186	  Read{path: List<&2, String>, name: String, want: Want}
187	
188	# one read that does not fit the spec
189	type 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
196	def 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
204	def 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
213	def 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
223	def 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
231	def 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
245	def 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
253	def 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
262	def 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
275	def 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
281	def 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
289	def 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
293	def 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"