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"