1	# lock/plan: `ez lock` as a pure planner. It reads a World (lock/world.bend)
2	# and returns either the questions it still needs answered (`step`) or a Plan:
3	# the effects to run and how the command ends (`plan`). The interpreter
4	# (lock/run.bend) loops on `step`, answering each question by IO, until
5	# nothing is left to ask, then executes the plan.
6	#
7	# Under `--upgrade` the upgrade's questions come first (lock/up.bend): what
8	# the remote says each selected pin moves to. Once they are answered, the
9	# lock is planned exactly as a plain lock is, over the ledger the upgrade
10	# leaves rather than ez.toml as it was, and the upgrade's writes go around it
11	# in one plan: trees laid, ez.toml written once, `.gitignore`, the rewritten
12	# sources, the committed trees that moved removed, and the lock last.
13	#
14	# `wants` only scans the answers it has for imports; `plan` checks every
15	# package once, so a lock pays for each file's SHA-256 once however deep the
16	# import graph is. A package that fails a check may make `wants` ask for more
17	# than the lock needs, which costs a fetch and changes nothing, since `plan`
18	# refuses it.
19	#
20	# A named import, `import <name>@<version>/...`, is a hub package too
21	# (EZ-HUB-3). One the project's own sources import must be a dependency
22	# ez.toml records by that name, and resolves to the hash ez.toml records
23	# beside it; one a package imports resolves the same way when ez.toml names
24	# it, then by the lock being rewritten, and only then by asking the hub, once
25	# (EZ-HUB-2). The package it resolves to is walked and checked like any hub
26	# package, and the lock records every name it resolved under `[names]`.
27	#
28	# What a lock decides depends on a World only through `W.inputs`: the ledger
29	# it is made from, the upgrade's refusal if any, the committed sources, and
30	# the verdict on every answer. How a tree arrived only decides whether it is
31	# laid under BEND_LIB for the build that follows, which is a cache and not
32	# something the lock records.
33	import Base
34	import ./world.bend as W
35	import ./up.bend as Up
36	import ./lock.bend as L
37	import ../ledger/manifest.bend as M
38	import ../pkg/pkg.bend as K
39	import ../pkg/path.bend as Path
40	import ../share/pin.bend as Pin
41	
42	# ---------------------------------------------------------------------------
43	# the walk
44	
45	# a verdict looked up, or none when nothing has been asked about the hash yet
46	type Look is Data:
47	  Found{verdict: W.Verdict}
48	  Absent{}
49	
50	# this verdict when it is the hash asked for, otherwise the rest's
51	def look.at(hit: Bool, verdict: W.Verdict, rest: Look) -> Look:
52	  match hit:
53	    case True{}:
54	      Found{verdict}
55	    case False{}:
56	      rest
57	
58	# the first verdict recorded for a hash
59	def look(js: List<&2, W.Judged>, +hash: String) -> Look:
60	  match js:
61	    case []:
62	      Absent{}
63	    case W.Judged{+h, v} <> t:
64	      look.at(String.eq(h, hash), v, look(t, hash))
65	
66	# a walk in progress: the hashes still queued, the packages resolved, the
67	# hashes still to be asked about, and the first refusal, "" while there is
68	# none. The walk is one step, which does not recurse, iterated; so a fact
69	# about the walk is a fact about one step, carried by induction on the fuel.
70	type Walk is Data:
71	  Walk{queue: List<&2, String>, packs: List<&2, L.Pack>, asks: List<&2, String>, bad: String}
72	
73	# the first refusal wins
74	def first(+bad: String, why: String) -> String:
75	  Bool.pick(String, String.is_empty(bad), why, bad)
76	
77	# one package, by its verdict. Its imports are queued by hash, and by the
78	# hash the table of names gives each name it imports.
79	def step.verdict(
80	  verdict: W.Verdict,
81	  +ns: List<&2, L.Name>,
82	  +src: L.Src,
83	  +hash: String,
84	  rest: List<&2, String>,
85	  packs: List<&2, L.Pack>,
86	  asks: List<&2, String>,
87	  bad: String
88	) -> Walk:
89	  match verdict:
90	    case W.No{why}:
91	      Walk{rest, packs, asks, first(bad, why)}
92	    case W.Ok{fs, ss}:
93	      Walk{List.append(&2, String, rest, L.kids.in(ns, ss)), L.Pack{hash, src, fs} <> packs,
94	        asks, bad}
95	    case W.Named{_names}:
96	      Walk{rest, packs, asks, first(bad, "ez: " ++ hash ++ " is imported as a package, and it is not one")}
97	
98	# one package, asked about when nothing has answered for it yet
99	def step.look(
100	  found: Look,
101	  +ns: List<&2, L.Name>,
102	  +src: L.Src,
103	  +hash: String,
104	  rest: List<&2, String>,
105	  packs: List<&2, L.Pack>,
106	  asks: List<&2, String>,
107	  bad: String
108	) -> Walk:
109	  match found:
110	    case Absent{}:
111	      Walk{rest, packs, hash <> asks, bad}
112	    case Found{v}:
113	      step.verdict(v, ns, src, hash, rest, packs, asks, bad)
114	
115	# a hash already resolved, or already asked about, is passed over
116	def step.pick(
117	  seen: Bool,
118	  +orgs: List<&2, L.Origin>,
119	  +ns: List<&2, L.Name>,
120	  +js: List<&2, W.Judged>,
121	  +hash: String,
122	  rest: List<&2, String>,
123	  packs: List<&2, L.Pack>,
124	  asks: List<&2, String>,
125	  bad: String
126	) -> Walk:
127	  match seen:
128	    case True{}:
129	      Walk{rest, packs, asks, bad}
130	    case False{}:
131	      step.look(look(js, hash), ns, L.origin(orgs, hash), hash, rest, packs, asks, bad)
132	
133	# the next hash of the queue, or the walk as it is when the queue is empty
134	def step.pop(
135	  +orgs: List<&2, L.Origin>,
136	  +ns: List<&2, L.Name>,
137	  +js: List<&2, W.Judged>,
138	  queue: List<&2, String>,
139	  +packs: List<&2, L.Pack>,
140	  +asks: List<&2, String>,
141	  bad: String
142	) -> Walk:
143	  match queue:
144	    case []:
145	      Walk{[], packs, asks, bad}
146	    case +h <> t:
147	      step.pick(Bool.or(L.has(packs, h), L.seen.holds(asks, h)), orgs, ns, js, h, t,
148	        packs, asks, bad)
149	
150	# one step of the walk
151	def walk.step(+orgs: List<&2, L.Origin>, +ns: List<&2, L.Name>, +js: List<&2, W.Judged>, wk: Walk) -> Walk:
152	  Walk{queue, packs, asks, bad} = wk
153	  step.pop(orgs, ns, js, queue, packs, asks, bad)
154	
155	# whether a walk has nothing left in its queue
156	def walk.done(+wk: Walk) -> Bool:
157	  Walk{queue, _packs, _asks, _bad} = wk
158	  List.is_empty(&2, String, queue)
159	
160	# a walk that ran out of fuel with its queue not empty, refused
161	def walk.spent(wk: Walk) -> Walk:
162	  Walk{queue, packs, asks, bad} = wk
163	  Walk{queue, packs, asks, first(bad, "ez: the import graph is too deep to lock")}
164	
165	# the walk as it is when it is done, or one step further when it is not. The
166	# rest of the walk arrives as a function, since a def may not call itself from
167	# another def.
168	def walk.more(done: Bool, wk: Walk, go: Walk -> Walk) -> Walk:
169	  match done:
170	    case True{}:
171	      wk
172	    case False{}:
173	      go(wk)
174	
175	# the fuel ran out: refused, unless the walk had just finished
176	def walk.out(done: Bool, wk: Walk) -> Walk:
177	  match done:
178	    case True{}:
179	      wk
180	    case False{}:
181	      walk.spent(wk)
182	
183	# every package the queue reaches, each one once. A walk that runs out of fuel
184	# with the queue not empty is a refusal, never a lock of what it had so far.
185	def walk(fuel: Nat, +orgs: List<&2, L.Origin>, +ns: List<&2, L.Name>, +js: List<&2, W.Judged>, +wk: Walk) -> Walk:
186	  match fuel:
187	    case 0n:
188	      walk.out(walk.done(wk), wk)
189	    case 1n+f:
190	      walk.more(walk.done(wk), wk, now => walk(f, orgs, ns, js, walk.step(orgs, ns, js, now)))
191	
192	# the packages a walk has resolved
193	def walk.packs(wk: Walk) -> List<&2, L.Pack>:
194	  Walk{_queue, packs, _asks, _bad} = wk
195	  packs
196	
197	# every hub package one committed source imports. The committed trees under
198	# `.ez/` are packages, not the project's own sources.
199	def roots.one(+src: W.Source) -> List<&2, String>:
200	  W.Source{at, text} = src
201	  Bool.pick(List<&2, String>, String.starts_with(at, ".ez/"), [],
202	    L.specs(K.scan.mods(K.scan(text))))
203	
204	# every hub package the committed sources import. Every committed `.bend`
205	# file is a root, so no local import has to be followed, and a file that is
206	# not committed is never read.
207	def roots(fs: List<&2, W.Source>) -> List<&2, String>:
208	  match fs:
209	    case []:
210	      []
211	    case +h <> t:
212	      List.append(&2, String, roots.one(h), roots(t))
213	
214	# every name one committed source imports, outside `.ez/`
215	def roots.named.one(+src: W.Source) -> List<&2, String>:
216	  W.Source{at, text} = src
217	  Bool.pick(List<&2, String>, String.starts_with(at, ".ez/"), [],
218	    L.named(K.scan.mods(K.scan(text))))
219	
220	# every name the committed sources import. Each must be one ez.toml records
221	# a dependency by.
222	def roots.named(fs: List<&2, W.Source>) -> List<&2, String>:
223	  match fs:
224	    case []:
225	      []
226	    case +h <> t:
227	      List.append(&2, String, roots.named.one(h), roots.named(t))
228	
229	# the table of names a lock resolves names by: those ez.toml records, each
230	# with the hash beside it, first, then those the answers resolve, the lock
231	# being rewritten's before the hub's
232	def table(+led: M.Read, js: List<&2, W.Judged>) -> List<&2, L.Name>:
233	  List.append(&2, L.Name, L.ledger.names(led), W.names.of(js))
234	
235	# how many imports one verdict queues: a package's, or none
236	def fuel.verdict(verdict: W.Verdict, ns: List<&2, L.Name>) -> Nat:
237	  match verdict:
238	    case W.Ok{_fs, ss}:
239	      List.length(&2, String, L.kids.in(ns, ss))
240	    case W.No{_why}:
241	      0n
242	    case W.Named{_names}:
243	      0n
244	
245	# how many imports every verdict queues between them
246	def fuel.judged(js: List<&2, W.Judged>, +ns: List<&2, L.Name>) -> Nat:
247	  match js:
248	    case []:
249	      0n
250	    case W.Judged{_h, v} <> t:
251	      Nat.add(fuel.verdict(v, ns), fuel.judged(t, ns))
252	
253	# how many steps the walk may take: one for each hash the queue starts with,
254	# one for each import a verdict can queue, since a hash is resolved at most
255	# once, and one more to spare. That is a step for every hash the walk can
256	# queue, and it is a function of the walk's inputs rather than a fixed
257	# number, as the add walk's is: a proof about inputs it does not know leaves it unevaluated,
258	# where bend 2.0.33 and 2.0.34 compare a fixed fuel's walk one stack frame a
259	# step and overflow the checker past about 10000.
260	def walk.fuel(queue: List<&2, String>, ns: List<&2, L.Name>, js: List<&2, W.Judged>) -> Nat:
261	  Nat.add(1n, Nat.add(List.length(&2, String, queue), fuel.judged(js, ns)))
262	
263	# the walk from every committed source: every package they import by hash,
264	# and every one they import by a name the table resolves. A listing git
265	# could not give is a walk refused before its first step.
266	def walk.of(+led: M.Read, listing: W.Listing, +ns: List<&2, L.Name>, +js: List<&2, W.Judged>) -> Walk:
267	  match listing:
268	    case W.Unlisted{why}:
269	      Walk{[], [], [], why}
270	    case W.Listed{+fs}:
271	      walk(walk.fuel(List.append(&2, String, roots(fs), L.name.hashes(ns, roots.named(fs))), ns, js),
272	        L.ledger.read(led), ns, js,
273	        Walk{List.append(&2, String, roots(fs), L.name.hashes(ns, roots.named(fs))), [], [], ""})
274	
275	# the committed sources a listing holds, none when git could not list them
276	def listing.files(listing: W.Listing) -> List<&2, W.Source>:
277	  match listing:
278	    case W.Unlisted{_why}:
279	      []
280	    case W.Listed{fs}:
281	      fs
282	
283	# the texts of a package the walk resolved, as its verdict holds them
284	def pack.srcs(found: Look) -> List<&2, String>:
285	  match found:
286	    case Absent{}:
287	      []
288	    case Found{v}:
289	      match v:
290	        case W.Ok{_fs, ss}:
291	          ss
292	        case _:
293	          []
294	
295	# every name the packages a walk resolved import
296	def packs.named(+js: List<&2, W.Judged>, ps: List<&2, L.Pack>) -> List<&2, String>:
297	  match ps:
298	    case []:
299	      []
300	    case +h <> t:
301	      List.append(&2, String, L.kids.named(pack.srcs(look(js, L.pack.hash(h)))),
302	        packs.named(js, t))
303	
304	# every name a lock needs resolved: those the committed sources import, then
305	# those the packages it reaches import
306	def needed(listing: W.Listing, +js: List<&2, W.Judged>, ps: List<&2, L.Pack>) -> List<&2, String>:
307	  List.append(&2, String, roots.named(listing.files(listing)), packs.named(js, ps))
308	
309	# why a plain lock cannot copy the ledger's tool pins, or "" when it can. A
310	# ledger that does not parse is refused here too.
311	def need.why(ledger: M.Read) -> String:
312	  match ledger:
313	    case M.Bad{why}:
314	      "ez: " ++ M.show(M.Bad{why})
315	    case M.Good{m}:
316	      M.Manifest{_n, _e, _b, _h, _pa, _pv, _ds, ts} = m
317	      Pin.gaps(ts)
318	
319	# ---------------------------------------------------------------------------
320	# what the lock may hold
321	
322	# a char the lock's TOML cannot carry inside a quoted key or value: eztoml
323	# neither writes nor reads escapes
324	def char.bad(+ch: Char) -> Bool:
325	  Bool.or(Char.is_eq(ch, '"'), Bool.or(Char.is_eq(ch, '\\'), Char.is_eq(ch, '\n')))
326	
327	# whether a key or value can be written as it is
328	def clean(text: String) -> Bool:
329	  match text:
330	    case SNil{}:
331	      True{}
332	    case SCon{+h, t}:
333	      +rest = clean(t)
334	      Bool.and(Bool.not(char.bad(h)), rest)
335	
336	# whether every string in a list can be written as it is
337	def clean.all(ss: List<&2, String>) -> Bool:
338	  match ss:
339	    case []:
340	      True{}
341	    case h <> t:
342	      +rest = clean.all(t)
343	      Bool.and(clean(h), rest)
344	
345	# every value a package's source writes
346	def src.values(source: L.Src) -> List<&2, String>:
347	  match source:
348	    case L.Hub{}:
349	      []
350	    case L.Git{url, rev, entry, root, nar, tag}:
351	      [url, rev, entry, root, nar, tag]
352	    case L.Member{path, entry}:
353	      [path, entry]
354	
355	# every path and sum a package's files write
356	def file.values(fs: List<&2, K.Item>) -> List<&2, String>:
357	  match fs:
358	    case []:
359	      []
360	    case K.Item{at, sum} <> t:
361	      at <> (sum <> file.values(t))
362	
363	# every hash, key and value a package writes
364	def pack.values(pack: L.Pack) -> List<&2, String>:
365	  L.Pack{hash, src, fs} = pack
366	  hash <> List.append(&2, String, src.values(src), file.values(fs))
367	
368	# whether a file path holds no `=`. A path is written as a quoted key, and
369	# `bootstrap.sh`, which reads the lock without ez, cuts a pair line at its
370	# first `=`, so a path holding one would read back there as another path with
371	# another sum. eztoml 0.4 reads a quoted key whole; the restriction lifts when
372	# bootstrap.sh does too.
373	def path.eqless(text: String) -> Bool:
374	  match text:
375	    case SNil{}:
376	      True{}
377	    case SCon{+h, t}:
378	      +rest = path.eqless(t)
379	      Bool.and(Bool.not(Char.is_eq(h, '=')), rest)
380	
381	# whether no file path of a package holds `=`
382	def paths.ok(fs: List<&2, K.Item>) -> Bool:
383	  match fs:
384	    case []:
385	      True{}
386	    case K.Item{at, _sum} <> t:
387	      +rest = paths.ok(t)
388	      Bool.and(path.eqless(at), rest)
389	
390	# whether every package can be written, and no hash is written twice
391	def packs.ok(ps: List<&2, L.Pack>) -> Bool:
392	  match ps:
393	    case []:
394	      True{}
395	    case +h <> +t:
396	      +rest = packs.ok(t)
397	      Bool.and(Bool.and(paths.ok(L.pack.files(h)),
398	        Bool.and(clean.all(pack.values(h)), Bool.not(L.has(t, L.pack.hash(h))))),
399	        rest)
400	
401	# every name, key and value a tool pin writes
402	def tool.values(pin: M.Tool) -> List<&2, String>:
403	  M.Tool{n, e, b, s} = pin
404	  match s:
405	    case M.Hub{_named}:
406	      [n, e, b]
407	    case M.Git{url, rev, tag, root, nar, _vend}:
408	      [n, e, b, url, rev, tag, root, nar]
409	    case M.Member{_path, _named}:
410	      [n, e, b]
411	
412	# whether every tool pin can be written
413	def tools.ok(ts: List<&2, M.Tool>) -> Bool:
414	  match ts:
415	    case []:
416	      True{}
417	    case h <> t:
418	      +rest = tools.ok(t)
419	      Bool.and(clean.all(tool.values(h)), rest)
420	
421	# whether a lock can be written so that it reads back: every hash is written
422	# once, no hash, key or value holds `"`, `\` or a newline, and no file path
423	# holds `=` (eztoml#24, above). The planner
424	# refuses a lock that is not, so every lock ez writes is one of these.
425	def lockable(ps: List<&2, L.Pack>, ts: List<&2, M.Tool>, hub: String) -> Bool:
426	  Bool.and(clean(hub), Bool.and(packs.ok(ps), tools.ok(ts)))
427	
428	# the first path among a package's files that holds `=`, or "" when none
429	# does. A path that holds one is not empty, so "" is never such a path.
430	def path.eq.pick(ok: Bool, at: String, rest: String) -> String:
431	  match ok:
432	    case True{}:
433	      rest
434	    case False{}:
435	      at
436	
437	def path.eq.first(fs: List<&2, K.Item>) -> String:
438	  match fs:
439	    case []:
440	      ""
441	    case K.Item{+at, _sum} <> t:
442	      path.eq.pick(path.eqless(at), at, path.eq.first(t))
443	
444	# why a package with such a path cannot be locked, naming it and the path
445	def path.eq.why(+hash: String, +at: String) -> String:
446	  "ez: ez.lock.toml cannot be written: package " ++ hash ++ " has a file " ++
447	    at ++ " whose path holds `=`, which the lock's TOML reader would cut the" ++
448	    " key at (https://github.com/Emerging-Patterns/eztoml/issues/24)"
449	
450	# the reason for the first package with such a path, or the rest's
451	def packs.eq.pick(none: Bool, +hash: String, +at: String, rest: String) -> String:
452	  match none:
453	    case True{}:
454	      rest
455	    case False{}:
456	      path.eq.why(hash, at)
457	
458	# why the first package with a path holding `=` cannot be locked, or "" when
459	# no package has one
460	def packs.eq(ps: List<&2, L.Pack>) -> String:
461	  match ps:
462	    case []:
463	      ""
464	    case L.Pack{+hash, _src, fs} <> t:
465	      +at = path.eq.first(fs)
466	      packs.eq.pick(String.is_empty(at), hash, at, packs.eq(t))
467	
468	# the reason a lock that is not `lockable` gives: the package and path when a
469	# path holds `=`, which is the one case a clean-looking lock hides
470	def lockable.pick(none: Bool, why: String) -> String:
471	  match none:
472	    case True{}:
473	      "ez: ez.lock.toml cannot be written: a hash repeats, or a hash, path or value holds a quote, a backslash or a newline"
474	    case False{}:
475	      why
476	
477	def lockable.why(ps: List<&2, L.Pack>) -> String:
478	  +why = packs.eq(ps)
479	  lockable.pick(String.is_empty(why), why)
480	
481	# whether every name the lock records can be written so that it reads back:
482	# a name is written as a quoted key and its hash as a value, the way a
483	# package's file is, so it is held to what a file is held to
484	def names.ok(ns: List<&2, L.Name>) -> Bool:
485	  +fs = L.name.files(ns)
486	  Bool.and(paths.ok(fs), clean.all(file.values(fs)))
487	
488	# whether a lock with names can be written so that it reads back
489	def lockable.named(ns: List<&2, L.Name>, ps: List<&2, L.Pack>, ts: List<&2, M.Tool>, hub: String) -> Bool:
490	  Bool.and(names.ok(ns), lockable(ps, ts, hub))
491	
492	# the reason a lock with names that is not lockable gives
493	def lockable.why.pick(ok: Bool, ps: List<&2, L.Pack>) -> String:
494	  match ok:
495	    case True{}:
496	      lockable.why(ps)
497	    case False{}:
498	      "ez: ez.lock.toml cannot be written: a name, or the hash ez.toml records for it, holds `=`, a quote, a backslash or a newline"
499	
500	def lockable.why.named(ns: List<&2, L.Name>, ps: List<&2, L.Pack>) -> String:
501	  lockable.why.pick(names.ok(ns), ps)
502	
503	# ---------------------------------------------------------------------------
504	# the names a lock needs
505	
506	# a name, when it is the first the search wants, or the rest's
507	def names.missing.pick(gone: Bool, +nv: String, rest: Unit -> String) -> String:
508	  match gone:
509	    case True{}:
510	      nv
511	    case False{}:
512	      rest(Unit{})
513	
514	# the first name of a list the hub rules out, or "" when it rules them all in
515	def names.ruled(nvs: List<&2, String>) -> String:
516	  match nvs:
517	    case []:
518	      ""
519	    case +h <> t:
520	      names.missing.pick(Bool.not(K.name.ok(h)), h, _u => names.ruled(t))
521	
522	# the first name of a list the table does not resolve, or "" when it
523	# resolves them all
524	def names.missing(+ns: List<&2, L.Name>, nvs: List<&2, String>) -> String:
525	  match nvs:
526	    case []:
527	      ""
528	    case +h <> t:
529	      names.missing.pick(String.is_empty(L.name.find(ns, h)), h, _u => names.missing(ns, t))
530	
531	# why a name nothing resolved stops the lock: what its answer said, or that
532	# it was never asked
533	def names.open.why(found: Look, +nv: String) -> String:
534	  match found:
535	    case Found{v}:
536	      match v:
537	        case W.No{why}:
538	          why
539	        case _:
540	          "ez: " ++ nv ++ " was never resolved, so there is nothing to lock it from"
541	    case Absent{}:
542	      "ez: " ++ nv ++ " was never resolved, so there is nothing to lock it from"
543	
544	# why a name the project imports and ez.toml does not record stops the lock
545	def names.unledgered.why(+nv: String) -> String:
546	  "ez: " ++ nv ++ " is imported, and ez.toml records no dependency by that name; " ++
547	    "a named package is recorded as `hub = \"" ++ nv ++ "\"` beside the hash it names"
548	
549	# a reason, or when there is none the next one, looked at only then
550	def why.then.at(none: Bool, why: String, rest: Unit -> String) -> String:
551	  match none:
552	    case True{}:
553	      rest(Unit{})
554	    case False{}:
555	      why
556	
557	def why.then(+why: String, rest: Unit -> String) -> String:
558	  why.then.at(String.is_empty(why), why, rest)
559	
560	# no reason when no name is at fault, and the fault's otherwise
561	def why.missing.at(none: Bool, reason: Unit -> String) -> String:
562	  match none:
563	    case True{}:
564	      ""
565	    case False{}:
566	      reason(Unit{})
567	
568	def why.missing(+nv: String, reason: Unit -> String) -> String:
569	  why.missing.at(String.is_empty(nv), reason)
570	
571	# why the names a lock needs stop it, or "" when they do not: a name the hub
572	# rules out, as bend refuses it; a name the project imports that ez.toml does
573	# not record, which is the lock's own rule, since only a dependency ez.toml
574	# records vouches for where a name came from; and a name nothing resolved
575	def names.why(
576	  +lns: List<&2, L.Name>,
577	  +ns: List<&2, L.Name>,
578	  +js: List<&2, W.Judged>,
579	  +roots: List<&2, String>,
580	  +need: List<&2, String>
581	) -> String:
582	  +bad = names.ruled(need)
583	  why.then(why.missing(bad, _u => K.unnamed.why(bad)), _v =>
584	    why.then(why.missing(names.missing(lns, roots), _w =>
585	        names.unledgered.why(names.missing(lns, roots))), _x =>
586	      why.missing(names.missing(ns, need), _y =>
587	        names.open.why(look(js, names.missing(ns, need)), names.missing(ns, need)))))
588	
589	# ---------------------------------------------------------------------------
590	# the lock's text, or why there is none
591	
592	# what a plain lock decides: the text of ez.lock.toml, or why it refuses
593	type Doc is Data:
594	  Doc{text: String}
595	  Stop{why: String}
596	
597	# a lock that can be written, written, with the names it resolved
598	def doc.lockable(
599	  ok: Bool,
600	  +ns: List<&2, L.Name>,
601	  +hub: String,
602	  packs: List<&2, L.Pack>,
603	  ts: List<&2, M.Tool>
604	) -> Doc:
605	  match ok:
606	    case True{}:
607	      Doc{L.render.names(ns, ts, hub, packs)}
608	    case False{}:
609	      Stop{lockable.why.named(ns, packs)}
610	
611	# a walk with nothing left to ask is the lock. One that still has a question
612	# is a World the interpreter did not finish, and is refused rather than
613	# guessed at.
614	def doc.asks(
615	  asks: List<&2, String>,
616	  +ns: List<&2, L.Name>,
617	  +hub: String,
618	  +packs: List<&2, L.Pack>,
619	  +ts: List<&2, M.Tool>
620	) -> Doc:
621	  match asks:
622	    case []:
623	      doc.lockable(lockable.named(ns, packs, ts, hub), ns, hub, packs, ts)
624	    case h <> _t:
625	      Stop{"ez: " ++ h ++ " was never read, so there is nothing to lock it from"}
626	
627	# the names settled: a name that stops the lock stops it, and otherwise the
628	# lock records each name it needed with the hash the table gives it
629	def doc.named(
630	  clean: Bool,
631	  why: String,
632	  asks: List<&2, String>,
633	  +ns: List<&2, L.Name>,
634	  +need: List<&2, String>,
635	  +hub: String,
636	  packs: List<&2, L.Pack>,
637	  ts: List<&2, M.Tool>
638	) -> Doc:
639	  match clean:
640	    case True{}:
641	      doc.asks(asks, L.name.pairs(ns, need), hub, packs, ts)
642	    case False{}:
643	      Stop{why}
644	
645	# a refusal wins over everything after it
646	def doc.bad(
647	  clean: Bool,
648	  +bad: String,
649	  asks: List<&2, String>,
650	  +led: M.Read,
651	  listing: W.Listing,
652	  +ns: List<&2, L.Name>,
653	  +js: List<&2, W.Judged>,
654	  +packs: List<&2, L.Pack>
655	) -> Doc:
656	  match clean:
657	    case True{}:
658	      +fs = listing.files(listing)
659	      +need = List.append(&2, String, roots.named(fs), packs.named(js, packs))
660	      +why = names.why(L.ledger.names(led), ns, js, roots.named(fs), need)
661	      doc.named(String.is_empty(why), why, asks, ns, need, M.hub_of(led), packs,
662	        M.tools_of(led))
663	    case False{}:
664	      Stop{bad}
665	
666	# the walk's result
667	def doc.walk(wk: Walk, +led: M.Read, listing: W.Listing, +ns: List<&2, L.Name>, +js: List<&2, W.Judged>) -> Doc:
668	  Walk{_queue, packs, asks, +bad} = wk
669	  doc.bad(String.is_empty(bad), bad, asks, led, listing, ns, js, packs)
670	
671	# a tool pin a plain lock would have to fill stops it before the walk counts
672	def doc.gap(
673	  clean: Bool,
674	  +gap: String,
675	  wk: Walk,
676	  +led: M.Read,
677	  listing: W.Listing,
678	  +ns: List<&2, L.Name>,
679	  +js: List<&2, W.Judged>
680	) -> Doc:
681	  match clean:
682	    case True{}:
683	      doc.walk(wk, led, listing, ns, js)
684	    case False{}:
685	      Stop{gap}
686	
687	# plain `ez lock` over a parsed ledger
688	def decide.led(+led: M.Read, +listing: W.Listing, +js: List<&2, W.Judged>) -> Doc:
689	  +gap = need.why(led)
690	  +ns = table(led, js)
691	  doc.gap(String.is_empty(gap), gap, walk.of(led, listing, ns, js), led, listing, ns, js)
692	
693	# an upgrade that refused, or still asks, stops the lock before anything else
694	def decide.stop(clean: Bool, +stop: String, +led: M.Read, listing: W.Listing, +js: List<&2, W.Judged>) -> Doc:
695	  match clean:
696	    case True{}:
697	      decide.led(led, listing, js)
698	    case False{}:
699	      Stop{stop}
700	
701	# `ez lock` over what the lock may depend on
702	def decide(ins: W.Inputs) -> Doc:
703	  W.Inputs{+ledger, +stop, listing, +js} = ins
704	  decide.stop(String.is_empty(stop), stop, ledger, listing, js)
705	
706	# ---------------------------------------------------------------------------
707	# the plan
708	
709	# where a package is laid: `.ez/lib`, which is committed for a vendored
710	# dependency, `$BEND_LIB`, which is a cache, or `<dir>/.ez/lib`, the committed
711	# trees of the workspace root at `dir`, where `ez add` and `ez remove` in a
712	# workspace lay the root lock's (ws/relock.bend)
713	type Place is Data:
714	  Committed{}
715	  Cache{}
716	  Under{dir: String}
717	
718	# one thing the interpreter does. A `Lay` writes each file under
719	# `<place>/<hash>`, in order; the manifest comes last, so a tree that has one
720	# is a tree that finished. A `Drop` removes `.ez/lib/<hash>`, a committed tree
721	# an upgrade moved off. A `Name` writes `$BEND_LIB/names/<nv>` holding the
722	# hash and a newline, the file bend reads a name's hash from before it would
723	# ask the hub (EZ-HUB-4). A `Say` is a line a person is told.
724	type Effect is Data:
725	  Write{path: String, text: String}
726	  Lay{place: Place, hash: String, files: List<&2, W.Source>}
727	  Drop{hash: String}
728	  Say{text: String}
729	  Name{nv: String, hash: String}
730	
731	# how the command ends: exit 0, or exit 1 with the reason
732	type Outcome is Data:
733	  Success{}
734	  Refused{why: String}
735	
736	# the effects, in order, and how the command ends after them
737	type Plan is Data:
738	  Plan{effects: List<&2, Effect>, outcome: Outcome}
739	
740	# the status a command exits with (EZ-OUT-1): 0 when it succeeds, 1 when it
741	# refuses. Every planner's plan ends with an Outcome, and the interpreter
742	# exits with this status of it (`Run.end`), so this is the one place the
743	# mapping lives.
744	def status(outcome: Outcome) -> U32:
745	  match outcome:
746	    case Success{}:
747	      0
748	    case Refused{_why}:
749	      1
750	
751	# the status of a command that refused, or did not
752	def status.of(refused: Bool) -> U32:
753	  Bool.pick(U32, refused, 1, 0)
754	
755	# what a command that ends is said to have ended on: nothing when it
756	# succeeded, and the reason when it refused
757	def why(outcome: Outcome) -> String:
758	  match outcome:
759	    case Success{}:
760	      ""
761	    case Refused{why}:
762	      why
763	
764	# the status a plan ends with
765	def code(pl: Plan) -> U32:
766	  Plan{_es, o} = pl
767	  status(o)
768	
769	# one of the upgrade's questions, as the upgrade looks its answer up (`ask`,
770	# with the source the ledger records) and as git is asked it (`git`, with
771	# that source anchored at the directory the lock runs in, `Up.anchor`). The
772	# interpreter answers `git` and records the answer under `ask`.
773	type Query is Data:
774	  Query{ask: Up.Ask, git: Up.Ask}
775	
776	# the questions still open, the lock's and the upgrade's, or the plan once
777	# there are none. The lock's are about packages, and, apart from them, about
778	# names: the lock being rewritten, and what the hub says a name names.
779	type Step is Data:
780	  Asking{asks: List<&2, W.Ask>, ups: List<&2, Query>, names: List<&2, W.Ask>}
781	  Run{plan: Plan}
782	
783	# what a plan leaves at one path: nothing written, or this text
784	type Wrote is Data:
785	  Kept{}
786	  Put{text: String}
787	
788	# the lock's path, which is fixed
789	def lockfile() -> String:
790	  "ez.lock.toml"
791	
792	# every hash a clone answered: those are the trees a lock lays under BEND_LIB
793	# for the build that follows
794	def cloned.how(how: W.How, +hash: String) -> List<&2, String>:
795	  match how:
796	    case W.Lib{}:
797	      []
798	    case W.Clone{_nar}:
799	      [hash]
800	    case W.Served{}:
801	      []
802	
803	def cloned.one(+hash: String, answer: W.Answer) -> List<&2, String>:
804	  match answer:
805	    case W.Miss{_why}:
806	      []
807	    case W.Got{how, _manifest, _ss}:
808	      cloned.how(how, hash)
809	    case W.Said{_text}:
810	      []
811	    case W.Locked{_text}:
812	      []
813	
814	# every hash a clone answered, in the order they were answered
815	def cloned(rs: List<&2, W.Reply>) -> List<&2, String>:
816	  match rs:
817	    case []:
818	      []
819	    case W.Reply{ask, answer} <> t:
820	      List.append(&2, String, cloned.one(W.ask.hash(ask), answer), cloned(t))
821	
822	# where a tree is laid: under `.ez/lib`, committed, when the ledger the lock
823	# is made from vendors its hash, and under BEND_LIB otherwise
824	def place.of(vend: Bool) -> Place:
825	  match vend:
826	    case True{}:
827	      Committed{}
828	    case False{}:
829	      Cache{}
830	
831	# a checked tree laid, ahead of what follows: its files with their texts,
832	# then the manifest of those texts, which is the manifest whose name the
833	# verdict checked (`W.body.laid`)
834	def lay.verdict(verdict: W.Verdict, place: Place, +hash: String, rest: List<&2, Effect>) -> List<&2, Effect>:
835	  match verdict:
836	    case W.No{_why}:
837	      rest
838	    case W.Ok{fs, ss}:
839	      +ls = W.laid(fs, ss)
840	      Lay{place, hash, List.append(&2, W.Source, ls,
841	        [W.Source{"manifest", W.manifest(ls)}])} <> rest
842	    case W.Named{_ns}:
843	      rest
844	
845	def lay.pick(hit: Bool, verdict: W.Verdict, place: Place, +hash: String, rest: List<&2, Effect>) -> List<&2, Effect>:
846	  match hit:
847	    case True{}:
848	      lay.verdict(verdict, place, hash, rest)
849	    case False{}:
850	      rest
851	
852	# every cloned tree that passed its checks, laid ahead of what follows. `vs`
853	# are the hashes committed under `.ez/lib`; a plain lock has none, and lays
854	# every tree in the cache.
855	def lays(
856	  +cs: List<&2, String>,
857	  +vs: List<&2, String>,
858	  js: List<&2, W.Judged>,
859	  rest: List<&2, Effect>
860	) -> List<&2, Effect>:
861	  match js:
862	    case []:
863	      rest
864	    case W.Judged{+h, v} <> t:
865	      lay.pick(L.seen.holds(cs, h), v, place.of(L.seen.holds(vs, h)), h,
866	        lays(cs, vs, t, rest))
867	
868	# a names file for every name a lock records, ahead of what follows, so bend
869	# reads each name's hash from BEND_LIB and never asks the hub for it
870	def names.lay(ns: List<&2, L.Name>, rest: List<&2, Effect>) -> List<&2, Effect>:
871	  match ns:
872	    case []:
873	      rest
874	    case L.Name{nv, hash} <> t:
875	      Name{nv, hash} <> names.lay(t, rest)
876	
877	# the lines a person is told, ahead of what follows
878	def says.of(ss: List<&2, String>, rest: List<&2, Effect>) -> List<&2, Effect>:
879	  match ss:
880	    case []:
881	      rest
882	    case h <> t:
883	      Say{h} <> says.of(t, rest)
884	
885	# the lines a list of effects says, in order
886	def said.in(es: List<&2, Effect>) -> List<&2, String>:
887	  match es:
888	    case []:
889	      []
890	    case e <> t:
891	      match e:
892	        case Say{text}:
893	          text <> said.in(t)
894	        case _:
895	          said.in(t)
896	
897	# the lines a plan says, in order, which is what a person is told
898	def said(pl: Plan) -> List<&2, String>:
899	  Plan{es, _outcome} = pl
900	  said.in(es)
901	
902	# the files the upgrade writes, in order, ahead of what follows
903	def edits.of(es: List<&2, Up.Edit>, rest: List<&2, Effect>) -> List<&2, Effect>:
904	  match es:
905	    case []:
906	      rest
907	    case Up.Edit{at, text} <> t:
908	      Write{at, text} <> edits.of(t, rest)
909	
910	# the committed trees the upgrade moved off, removed ahead of what follows
911	def drops.of(ds: List<&2, String>, rest: List<&2, Effect>) -> List<&2, Effect>:
912	  match ds:
913	    case []:
914	      rest
915	    case h <> t:
916	      Drop{h} <> drops.of(t, rest)
917	
918	# the plan for what was decided. A refusal has no effect at all, so a refused
919	# lock, plain or upgrade, writes nothing, lays nothing and removes nothing; its
920	# reason is how it ends. A lock that is made runs, in order: what a person is
921	# told, the trees laid, a names file for every name the lock records (read
922	# back from the lock's own text, so the files and the lock never disagree),
923	# the upgrade's files (ez.toml once, `.gitignore`, the rewritten sources), the
924	# committed trees removed, and the lock last. A plain lock has only the
925	# trees, the names and the lock.
926	def made(+nx: Up.Next, cs: List<&2, String>, js: List<&2, W.Judged>, doc: Doc) -> Plan:
927	  match doc:
928	    case Doc{+text}:
929	      Plan{says.of(Up.next.says(nx),
930	        lays(cs, Up.next.vends(nx), js, names.lay(L.names.read(text),
931	          edits.of(Up.next.edits(nx),
932	            edits.of(Up.edit.sources(Up.next.found(nx), Up.next.swaps(nx)),
933	              drops.of(Up.next.drops(nx), [Write{lockfile(), text}])))))), Success{}}
934	    case Stop{why}:
935	      Plan{[], Refused{why}}
936	
937	# `ez lock` once the upgrade decided: every package checked once, and the plan
938	def plan.of(+nx: Up.Next, listing: W.Listing, +replies: List<&2, W.Reply>) -> Plan:
939	  +js = W.judged.of(nx, replies)
940	  made(nx, cloned(W.replies.of(nx, replies)), js,
941	    decide(W.Inputs{Up.next.read(nx), Up.next.stop(nx), W.listing.of(nx, listing), js}))
942	
943	# `ez lock` over a World
944	def plan(world: W.World) -> Plan:
945	  W.World{args, +ledger, listing, replies, ups} = world
946	  plan.of(W.next(args, ledger, ups), listing, replies)
947	
948	# whether what was decided is a refusal
949	def refuses.doc(doc: Doc) -> Bool:
950	  match doc:
951	    case Doc{_text}:
952	      False{}
953	    case Stop{_why}:
954	      True{}
955	
956	# whether `ez lock` refuses on a World
957	def refuses(world: W.World) -> Bool:
958	  refuses.doc(decide(W.inputs(world)))
959	
960	# the packages `ez lock` resolves once the upgrade decided
961	def packs.of(+nx: Up.Next, listing: W.Listing, replies: List<&2, W.Reply>) -> List<&2, L.Pack>:
962	  +js = W.judged.of(nx, replies)
963	  walk.packs(walk.of(Up.next.read(nx), W.listing.of(nx, listing),
964	    table(Up.next.read(nx), js), js))
965	
966	# the packages `ez lock` resolves on a World, which are the packages its lock
967	# renders when it writes one
968	def packs(world: W.World) -> List<&2, L.Pack>:
969	  W.World{args, +ledger, listing, replies, ups} = world
970	  packs.of(W.next(args, ledger, ups), listing, replies)
971	
972	# the ledger model an upgrade renders into ez.toml; ez.toml as it was when
973	# the upgrade refuses, still asks, or moves nothing, and for a plain lock. The
974	# upgrade's decisions (EZ-RES-4 to 6 and 8) are stated over it, and hold of
975	# ez.toml's bytes, which read back as it (EZ-LED-4).
976	def ledger.next(world: W.World) -> M.Read:
977	  W.World{args, +ledger, _listing, _replies, ups} = world
978	  Up.next.model(W.next(args, ledger, ups))
979	
980	# ---------------------------------------------------------------------------
981	# what a plan writes
982	
983	# one effect's part in what a path is left holding, with what the effects
984	# after it leave already known. A later write wins.
985	def put.one(effect: Effect, +path: String, rest: Wrote) -> Wrote:
986	  match effect:
987	    case Write{at, text}:
988	      match rest:
989	        case Kept{}:
990	          Bool.pick(Wrote, String.eq(at, path), Put{text}, Kept{})
991	        case Put{later}:
992	          Put{later}
993	    case Lay{_place, _hash, _files}:
994	      rest
995	    case Drop{_hash}:
996	      rest
997	    case Say{_text}:
998	      rest
999	    case Name{_nv, _hash}:
1000	      rest
1001	
1002	# what a list of effects leaves at a path
1003	def put.in(es: List<&2, Effect>, +path: String) -> Wrote:
1004	  match es:
1005	    case []:
1006	      Kept{}
1007	    case e <> t:
1008	      put.one(e, path, put.in(t, path))
1009	
1010	# what a plan leaves at a path
1011	def put.plan(pl: Plan, +path: String) -> Wrote:
1012	  Plan{es, _outcome} = pl
1013	  put.in(es, path)
1014	
1015	# the bytes `ez lock` writes to a path on a World, or Kept when it writes
1016	# none
1017	def put(world: W.World, +path: String) -> Wrote:
1018	  put.plan(plan(world), path)
1019	
1020	# whether an effect writes, lays or removes anything
1021	def writes.one(effect: Effect) -> Bool:
1022	  match effect:
1023	    case Write{_at, _text}:
1024	      True{}
1025	    case Lay{_place, _hash, _files}:
1026	      True{}
1027	    case Drop{_hash}:
1028	      True{}
1029	    case Say{_text}:
1030	      False{}
1031	    case Name{_nv, _hash}:
1032	      True{}
1033	
1034	# whether a plan writes, lays or removes anything
1035	def writes.in(es: List<&2, Effect>) -> Bool:
1036	  match es:
1037	    case []:
1038	      False{}
1039	    case e <> t:
1040	      +rest = writes.in(t)
1041	      Bool.or(writes.one(e), rest)
1042	
1043	# whether a plan writes, lays or removes anything at all
1044	def writes(pl: Plan) -> Bool:
1045	  Plan{es, _outcome} = pl
1046	  writes.in(es)
1047	
1048	# ---------------------------------------------------------------------------
1049	# the trees a plan lays, named (EZ-HASH-3). Law vocabulary for `ez lock`,
1050	# `ez add` and `ez fetch`, which lay trees through the same effect.
1051	
1052	# every file of a tree but the last, which a `Lay` writes as the manifest
1053	def front(fs: List<&2, W.Source>) -> List<&2, W.Source>:
1054	  match fs:
1055	    case []:
1056	      []
1057	    case h <> t:
1058	      match t:
1059	        case []:
1060	          []
1061	        case h2 <> t2:
1062	          h <> front(h2 <> t2)
1063	
1064	# a file's text
1065	def text.of(src: W.Source) -> String:
1066	  W.Source{_at, text} = src
1067	  text
1068	
1069	# the last file's text, "" for no file
1070	def last(fs: List<&2, W.Source>) -> String:
1071	  match fs:
1072	    case []:
1073	      ""
1074	    case h <> t:
1075	      match t:
1076	        case []:
1077	          text.of(h)
1078	        case h2 <> t2:
1079	          last(h2 <> t2)
1080	
1081	# whether a laid tree is named by the manifest of the texts it lays: its
1082	# last file is the manifest of the others, each weighed by its own text,
1083	# and its hash is the `0x` name of that manifest
1084	def lay.named(+hash: String, +fs: List<&2, W.Source>) -> Bool:
1085	  +sums = K.files_of(W.weighs(front(fs)))
1086	  Bool.and(String.eq(hash, K.hash_of(sums)), String.eq(last(fs), K.manifest_of(sums)))
1087	
1088	# whether an effect that lays a tree lays a named one
1089	def lays.one(effect: Effect) -> Bool:
1090	  match effect:
1091	    case Lay{_place, hash, fs}:
1092	      lay.named(hash, fs)
1093	    case _:
1094	      True{}
1095	
1096	# whether every tree a list of effects lays is named by its manifest
1097	def lays.named(es: List<&2, Effect>) -> Bool:
1098	  match es:
1099	    case []:
1100	      True{}
1101	    case h <> t:
1102	      +rest = lays.named(t)
1103	      Bool.and(lays.one(h), rest)
1104	
1105	# the effects of a plan
1106	def effects(pl: Plan) -> List<&2, Effect>:
1107	  Plan{es, _outcome} = pl
1108	  es
1109	
1110	# ---------------------------------------------------------------------------
1111	# what is still to ask
1112	
1113	# an answer as far as `wants` needs it: the texts it may import from, taken
1114	# as they are and not checked, or the miss
1115	def scan.one(+hash: String, +hub: String, answer: W.Answer) -> W.Verdict:
1116	  match answer:
1117	    case W.Miss{why}:
1118	      W.No{why}
1119	    case W.Got{_how, _manifest, ss}:
1120	      W.Ok{[], ss}
1121	    case W.Said{text}:
1122	      W.said(hash, hub, text)
1123	    case W.Locked{text}:
1124	      W.locked(text)
1125	
1126	# the hub a question names, "" for the lock's
1127	def ask.hub(ask: W.Ask) -> String:
1128	  match ask:
1129	    case W.Pkg{_hash, _src, hub}:
1130	      hub
1131	    case W.Name{_nv, hub}:
1132	      hub
1133	    case W.Lock{}:
1134	      ""
1135	
1136	# every reply, scanned
1137	def scan(rs: List<&2, W.Reply>) -> List<&2, W.Judged>:
1138	  match rs:
1139	    case []:
1140	      []
1141	    case W.Reply{+ask, answer} <> t:
1142	      W.Judged{W.ask.hash(ask), scan.one(W.ask.hash(ask), ask.hub(ask), answer)} <> scan(t)
1143	
1144	# a package's source as git is to read it: a path anchored at the directory
1145	# the lock runs in (`Path.anchor`), and a URL or an absolute path as it is. A
1146	# hub package names no source. The lock records the source as the ledger
1147	# gives it; only the question carries this.
1148	def anchor.src(+here: String, src: L.Src) -> L.Src:
1149	  match src:
1150	    case L.Hub{}:
1151	      L.Hub{}
1152	    case L.Git{url, rev, entry, root, nar, tag}:
1153	      L.Git{Path.anchor(here, url), rev, entry, root, nar, tag}
1154	    case L.Member{path, entry}:
1155	      L.Member{path, entry}
1156	
1157	# each hash still to ask about, as the question for it, with its source
1158	# anchored
1159	def asks.of(hs: List<&2, String>, +here: String, +orgs: List<&2, L.Origin>, +hub: String) -> List<&2, W.Ask>:
1160	  match hs:
1161	    case []:
1162	      []
1163	    case +h <> t:
1164	      W.Pkg{h, anchor.src(here, L.origin(orgs, h)), hub} <> asks.of(t, here, orgs, hub)
1165	
1166	# nothing more is asked once the lock is known to refuse
1167	def wants.bad(
1168	  clean: Bool,
1169	  hs: List<&2, String>,
1170	  +here: String,
1171	  +orgs: List<&2, L.Origin>,
1172	  +hub: String
1173	) -> List<&2, W.Ask>:
1174	  match clean:
1175	    case True{}:
1176	      asks.of(List.reverse(&2, String, hs), here, orgs, hub)
1177	    case False{}:
1178	      []
1179	
1180	def wants.walk(wk: Walk, +here: String, +orgs: List<&2, L.Origin>, +hub: String) -> List<&2, W.Ask>:
1181	  Walk{_queue, _packs, hs, +bad} = wk
1182	  wants.bad(String.is_empty(bad), hs, here, orgs, hub)
1183	
1184	def wants.gap(clean: Bool, wk: Walk, +here: String, +orgs: List<&2, L.Origin>, +hub: String) -> List<&2, W.Ask>:
1185	  match clean:
1186	    case True{}:
1187	      wants.walk(wk, here, orgs, hub)
1188	    case False{}:
1189	      []
1190	
1191	def wants.led(+here: String, +led: M.Read, listing: W.Listing, +js: List<&2, W.Judged>) -> List<&2, W.Ask>:
1192	  wants.gap(String.is_empty(need.why(led)), walk.of(led, listing, table(led, js), js), here,
1193	    L.ledger.read(led), M.hub_of(led))
1194	
1195	# nothing is asked about packages while the upgrade refuses or still asks
1196	def wants.stop(clean: Bool, +here: String, +led: M.Read, listing: W.Listing, js: List<&2, W.Judged>) -> List<&2, W.Ask>:
1197	  match clean:
1198	    case True{}:
1199	      wants.led(here, led, listing, js)
1200	    case False{}:
1201	      []
1202	
1203	# the package questions still open once the upgrade decided
1204	def wants.of(+here: String, +nx: Up.Next, listing: W.Listing, replies: List<&2, W.Reply>) -> List<&2, W.Ask>:
1205	  wants.stop(String.is_empty(Up.next.stop(nx)), here, Up.next.read(nx),
1206	    W.listing.of(nx, listing), scan(W.replies.of(nx, replies)))
1207	
1208	# the package questions a World still leaves open: every package the walk
1209	# reaches that nothing has answered for yet. None once the lock is known to
1210	# refuse, and none while the upgrade still asks.
1211	def wants(world: W.World) -> List<&2, W.Ask>:
1212	  W.World{+args, +ledger, listing, replies, ups} = world
1213	  wants.of(W.here.of(args), W.next(args, ledger, ups), listing, replies)
1214	
1215	# the upgrade's questions a World still leaves open; none for a plain lock
1216	def wants.up(world: W.World) -> List<&2, Up.Ask>:
1217	  W.World{args, +ledger, _listing, _replies, ups} = world
1218	  Up.next.asks(W.next(args, ledger, ups))
1219	
1220	# whether the upgrade has every answer it needs
1221	def answered(world: W.World) -> Bool:
1222	  List.is_empty(&2, Up.Ask, wants.up(world))
1223	
1224	# each of the upgrade's questions, with the question git is asked for it
1225	def queries(+here: String, as: List<&2, Up.Ask>) -> List<&2, Query>:
1226	  match as:
1227	    case []:
1228	      []
1229	    case +h <> t:
1230	      Query{h, Up.anchor(here, h)} <> queries(here, t)
1231	
1232	# ---------------------------------------------------------------------------
1233	# the names still to resolve
1234	
1235	# a name kept among the ones to ask about when it is not one already kept
1236	def names.once.put(dup: Bool, +nv: String, rest: List<&2, String>) -> List<&2, String>:
1237	  match dup:
1238	    case True{}:
1239	      rest
1240	    case False{}:
1241	      nv <> rest
1242	
1243	# every name of a list once, each where it first stands
1244	def names.once(nvs: List<&2, String>, +seen: List<&2, String>) -> List<&2, String>:
1245	  match nvs:
1246	    case []:
1247	      []
1248	    case +h <> t:
1249	      names.once.put(L.seen.holds(seen, h), h, names.once(t, h <> seen))
1250	
1251	# whether nothing has answered for a key
1252	def is.absent(found: Look) -> Bool:
1253	  match found:
1254	    case Absent{}:
1255	      True{}
1256	    case Found{_v}:
1257	      False{}
1258	
1259	# whether a name is still to be resolved: the hub rules it in, the table does
1260	# not resolve it, the project does not import it (that one ez.toml must
1261	# record, and the lock refuses it), and nothing has answered for it yet
1262	def name.open(+ns: List<&2, L.Name>, +js: List<&2, W.Judged>, +roots: List<&2, String>, +nv: String) -> Bool:
1263	  Bool.and(K.name.ok(nv), Bool.and(String.is_empty(L.name.find(ns, nv)),
1264	    Bool.and(Bool.not(L.seen.holds(roots, nv)), is.absent(look(js, nv)))))
1265	
1266	def names.open.put(open: Bool, +nv: String, rest: List<&2, String>) -> List<&2, String>:
1267	  match open:
1268	    case True{}:
1269	      nv <> rest
1270	    case False{}:
1271	      rest
1272	
1273	# every name of a list still to be resolved
1274	def names.open(
1275	  +ns: List<&2, L.Name>,
1276	  +js: List<&2, W.Judged>,
1277	  +roots: List<&2, String>,
1278	  nvs: List<&2, String>
1279	) -> List<&2, String>:
1280	  match nvs:
1281	    case []:
1282	      []
1283	    case +h <> t:
1284	      names.open.put(name.open(ns, js, roots, h), h, names.open(ns, js, roots, t))
1285	
1286	# each name as the question the hub is asked about it
1287	def names.asked(+hub: String, nvs: List<&2, String>) -> List<&2, W.Ask>:
1288	  match nvs:
1289	    case []:
1290	      []
1291	    case h <> t:
1292	      W.Name{h, hub} <> names.asked(hub, t)
1293	
1294	# the questions for the names still open: none when there are none; the lock
1295	# being rewritten first, since a name it records is not put to the hub
1296	# (EZ-HUB-2); and then each name the lock does not record, once
1297	def names.ask.lock(read: Bool, +hub: String, nvs: List<&2, String>) -> List<&2, W.Ask>:
1298	  match read:
1299	    case True{}:
1300	      names.asked(hub, names.once(nvs, []))
1301	    case False{}:
1302	      [W.Lock{}]
1303	
1304	def names.ask(+hub: String, +js: List<&2, W.Judged>, nvs: List<&2, String>) -> List<&2, W.Ask>:
1305	  match nvs:
1306	    case []:
1307	      []
1308	    case h <> t:
1309	      names.ask.lock(Bool.not(is.absent(look(js, W.lockfile()))), hub, h <> t)
1310	
1311	def names.wants.bad(
1312	  clean: Bool,
1313	  +led: M.Read,
1314	  listing: W.Listing,
1315	  +ns: List<&2, L.Name>,
1316	  +js: List<&2, W.Judged>,
1317	  packs: List<&2, L.Pack>
1318	) -> List<&2, W.Ask>:
1319	  match clean:
1320	    case True{}:
1321	      names.ask(M.hub_of(led), js,
1322	        names.open(ns, js, roots.named(listing.files(listing)), packs.named(js, packs)))
1323	    case False{}:
1324	      []
1325	
1326	# the name questions of a walk, which ask nothing once the lock is known to
1327	# refuse
1328	def names.wants.walk(
1329	  wk: Walk,
1330	  +led: M.Read,
1331	  +listing: W.Listing,
1332	  +ns: List<&2, L.Name>,
1333	  +js: List<&2, W.Judged>
1334	) -> List<&2, W.Ask>:
1335	  Walk{_queue, packs, _asks, +bad} = wk
1336	  names.wants.bad(String.is_empty(bad), led, listing, ns, js, packs)
1337	
1338	def names.wants.gap(clean: Bool, +led: M.Read, +listing: W.Listing, +js: List<&2, W.Judged>) -> List<&2, W.Ask>:
1339	  match clean:
1340	    case True{}:
1341	      +ns = table(led, js)
1342	      names.wants.walk(walk.of(led, listing, ns, js), led, listing, ns, js)
1343	    case False{}:
1344	      []
1345	
1346	def names.wants.stop(clean: Bool, +led: M.Read, listing: W.Listing, +js: List<&2, W.Judged>) -> List<&2, W.Ask>:
1347	  match clean:
1348	    case True{}:
1349	      names.wants.gap(String.is_empty(need.why(led)), led, listing, js)
1350	    case False{}:
1351	      []
1352	
1353	# the name questions still open once the upgrade decided, over the answers
1354	# scanned as `wants` scans them
1355	def names.wants.of(+nx: Up.Next, listing: W.Listing, replies: List<&2, W.Reply>) -> List<&2, W.Ask>:
1356	  names.wants.stop(String.is_empty(Up.next.stop(nx)), Up.next.read(nx),
1357	    W.listing.of(nx, listing), scan(W.replies.of(nx, replies)))
1358	
1359	# the name questions a World still leaves open: for every name a package the
1360	# walk reaches imports, that ez.toml does not record and nothing has
1361	# answered for yet, the lock being rewritten, and once it is read, the hub
1362	def wants.names(world: W.World) -> List<&2, W.Ask>:
1363	  W.World{+args, +ledger, listing, replies, ups} = world
1364	  names.wants.of(W.next(args, ledger, ups), listing, replies)
1365	
1366	# the package questions still open, or the name questions, or the plan once
1367	# there are none
1368	def step.names(names: List<&2, W.Ask>, +nx: Up.Next, listing: W.Listing, replies: List<&2, W.Reply>) -> Step:
1369	  match names:
1370	    case []:
1371	      Run{plan.of(nx, listing, replies)}
1372	    case h <> t:
1373	      Asking{[], [], h <> t}
1374	
1375	def step.pkgs(
1376	  asks: List<&2, W.Ask>,
1377	  names: List<&2, W.Ask>,
1378	  +nx: Up.Next,
1379	  listing: W.Listing,
1380	  replies: List<&2, W.Reply>
1381	) -> Step:
1382	  match asks:
1383	    case []:
1384	      step.names(names, nx, listing, replies)
1385	    case h <> t:
1386	      Asking{h <> t, [], names}
1387	
1388	# the upgrade's questions first, since the packages the lock reads depend on
1389	# where the pins move
1390	def step.ups(
1391	  ups: List<&2, Up.Ask>,
1392	  +here: String,
1393	  +nx: Up.Next,
1394	  +listing: W.Listing,
1395	  +replies: List<&2, W.Reply>
1396	) -> Step:
1397	  match ups:
1398	    case []:
1399	      step.pkgs(wants.of(here, nx, listing, replies), names.wants.of(nx, listing, replies), nx,
1400	        listing, replies)
1401	    case h <> t:
1402	      Asking{[], queries(here, h <> t), []}
1403	
1404	# what the interpreter does next on a World. The upgrade is decided once per
1405	# round, and every answer of the round is read from that one decision.
1406	def step(world: W.World) -> Step:
1407	  W.World{+args, +ledger, +listing, +replies, ups} = world
1408	  +nx = W.next(args, ledger, ups)
1409	  step.ups(Up.next.asks(nx), W.here.of(args), nx, listing, replies)