1	# src/syntax/bind: where every name in a source is bound, and what every other
2	# name refers to. One walk over the tree threads an environment (the binders
3	# in scope, innermost first) through Bend's binding forms:
4	#   - an item's name (`def f`, `type T`, `law l`, a constructor line);
5	#   - a telescope: a def's parameters, a type's parameters, a constructor's
6	#     fields, each type seeing the names before it;
7	#   - `case p:` patterns and `for x: T` / `exs x: T where P`, for the lines
8	#     under them;
9	#   - a let (`x = v`, `+x = v`, `x : T = v`, `x : T <- m`, `a b = f g`,
10	#     `(a, K{b}) = p`) for the lines after it in its block -- the right side
11	#     sees the outer names, so `st = step(st)` reads the old st;
12	#   - `x => e`, `@x: A -> B` and `&x: A -> B`, for the rest of their sequence.
13	# The walk branches on token and statement kinds, never on a computed test,
14	# so each step recurses on one subtree and the checker accepts it.
15	# A binder shadows an item of the same name; a dotted name is an item of the
16	# file (`text.of`) or, through an import alias, of another file (`Lex.Tok`);
17	# anything else is free (Base, or unknown).
18	import Base
19	import ./lex.bend as Lex
20	import ../lazy/lazy.bend as Lazy
21	import ./tree.bend as Tree
22	
23	# what a binder is: an item's or a constructor's name, a parameter, a type's
24	# parameter, a constructor's field, a let name, a pattern binder, a law's
25	# `for`, or a type-level `@x:` / `&x:`
26	type BindKind is Data:
27	  KItem{}
28	  KCtor{}
29	  KParam{}
30	  KTypeParam{}
31	  KField{}
32	  KLocal{}
33	  KPat{}
34	  KFor{}
35	  KTypeVar{}
36	
37	# KLocal is a name a let, a do-bind or a lambda binds; KPat one bound by a
38	# pattern (a case, or a destructuring let). note: what to show for it -- a
39	# declaration's own text (`+x: U32`), else the line that bound it
40	type Bind is Data:
41	  Bind{name: String, line: U32, col: U32, kind: BindKind, note: String}
42	
43	# what a use refers to: a binder of the file (by position), an item of the
44	# file, an item behind an import alias, or nothing known (Base, or unknown)
45	type Target is Data:
46	  TLocal{line: U32, col: U32}
47	  TItem{name: String}
48	  TQual{alias: String, name: String}
49	  TFree{}
50	
51	# a name that is not a binder, with what it refers to
52	type Use is Data:
53	  Use{name: String, line: U32, col: U32, target: Target}
54	
55	# the names in scope at a statement's line
56	type Scope is Data:
57	  Scope{line: U32, env: List<&2, Bind>}
58	
59	# everything the binder knows about a source, each list in source order
60	type Bound is Data:
61	  Bound{binds: List<&2, Bind>, uses: List<&2, Use>, scopes: List<&2, Scope>}
62	
63	# a line and a column
64	type Pos is Data:
65	  Pos{line: U32, col: U32}
66	
67	# names of the file
68	# -----------------
69	
70	# a name that can be declared: plain, capitalized or dotted
71	def declared.is_name(kk: Lex.TokKind) -> Bool:
72	  match kk:
73	    case Lex.TName{}:
74	      True{}
75	    case Lex.TUpper{}:
76	      True{}
77	    case Lex.TDotted{}:
78	      True{}
79	    case other:
80	      False{}
81	
82	# a leaf's name, when its kind is one: the kind is tested, the text only kept
83	def declared.name(nn: Tree.Node) -> Maybe<&2, String>:
84	  match nn:
85	    case Tree.Leaf{Lex.Tok{k, t, l, c}}:
86	      Bool.pick(Maybe<&2, String>, declared.is_name(k), Some{t}, None{})
87	    case other:
88	      None{}
89	
90	# the item a statement declares: the first name after its keyword
91	def declared.go(kids: Tree.Node) -> Maybe<&2, String>:
92	  match kids:
93	    case Tree.NCons{h, rest}:
94	      declared.name(h)
95	    case other:
96	      None{}
97	
98	# a keyword?
99	def declared.is_key(kk: Lex.TokKind) -> Bool:
100	  match kk:
101	    case Lex.TKey{}:
102	      True{}
103	    case other:
104	      False{}
105	
106	# a keyword leaf? its kind is read, never its text
107	def declared.key(nn: Tree.Node) -> Bool:
108	  match nn:
109	    case Tree.Leaf{Lex.Tok{k, t, l, c}}:
110	      declared.is_key(k)
111	    case other:
112	      False{}
113	
114	# the item a statement declares: the first name after its keyword
115	def declared(kids: Tree.Node) -> Maybe<&2, String>:
116	  match kids:
117	    case Tree.NCons{h, +rest}:
118	      Lazy.either(Maybe<&2, String>, declared.key(h), _u => declared.go(rest), _v => declared(rest))
119	    case other:
120	      None{}
121	
122	# is the name at the head of the list?
123	def push_name.again(acc: List<&2, String>, +name: String) -> Bool:
124	  match acc:
125	    case Nil{}:
126	      False{}
127	    case Con{hh, _rest}:
128	      String.eq(hh, name)
129	
130	# a name, when there is one, onto a list, unless it is the name just put
131	# there: a proof file's `law x` and its `def x` are one item, and every use
132	# no binder holds is looked for in this list
133	def push_name(mm: Maybe<&2, String>, +acc: List<&2, String>) -> List<&2, String>:
134	  match mm:
135	    case None{}:
136	      acc
137	    case Some{+name}:
138	      Lazy.stop(List<&2, String>, push_name.again(acc, name), acc, _u => name <> acc)
139	
140	# a type's constructors: the first name of each line under it
141	def ctors(body: Tree.Node, acc: List<&2, String>) -> List<&2, String>:
142	  match body:
143	    case Tree.NCons{Tree.Stmt{k, kids, b}, rest}:
144	      ctors(rest, push_name(declared.go(kids), acc))
145	    case other:
146	      acc
147	
148	# the defs, laws, types and constructors of a source
149	def items(root: Tree.Node, acc: List<&2, String>) -> List<&2, String>:
150	  match root:
151	    case Tree.NCons{Tree.Stmt{Tree.SDef{}, kids, body}, rest}:
152	      items(rest, push_name(declared(kids), acc))
153	    case Tree.NCons{Tree.Stmt{Tree.SLaw{}, kids, body}, rest}:
154	      items(rest, push_name(declared(kids), acc))
155	    case Tree.NCons{Tree.Stmt{Tree.SType{}, kids, body}, rest}:
156	      items(rest, ctors(body, push_name(declared(kids), acc)))
157	    case Tree.NCons{other, rest}:
158	      items(rest, acc)
159	    case other:
160	      acc
161	
162	# the text of a chain's last leaf
163	def last_text(kids: Tree.Node) -> String:
164	  match kids:
165	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, Tree.NNil{}}:
166	      t
167	    case Tree.NCons{h, rest}:
168	      last_text(rest)
169	    case other:
170	      ""
171	
172	# the import aliases of a source: the last token of each `import .. as X`
173	def aliases(root: Tree.Node, +acc: List<&2, String>) -> List<&2, String>:
174	  match root:
175	    case Tree.NCons{Tree.Stmt{Tree.SImport{}, kids, body}, rest}:
176	      +last = last_text(kids)
177	      aliases(rest, Bool.pick(List<&2, String>, Bool.or(String.eq(last, "Base"), String.eq(last, "import")), acc, last <> acc))
178	    case Tree.NCons{other, rest}:
179	      aliases(rest, acc)
180	    case other:
181	      acc
182	
183	# resolution
184	# ----------
185	
186	# the innermost binder of a name in an environment; hit: the binder before
187	# env was the name, so the search stops there
188	def find.go(env: List<&2, Bind>, +name: String, hit: Maybe<&2, Bind>) -> Maybe<&2, Bind>:
189	  match env:
190	    case Nil{}:
191	      hit
192	    case Con{Bind{+n, l, c, k, note}, t}:
193	      match hit:
194	        case Some{x}:
195	          Some{x}
196	        case None{}:
197	          find.go(t, name, Bool.pick(Maybe<&2, Bind>, String.eq(n, name), Some{Bind{n, l, c, k, note}}, None{}))
198	
199	# the innermost binder of a name in an environment
200	def find(env: List<&2, Bind>, +name: String) -> Maybe<&2, Bind>:
201	  find.go(env, name, None{})
202	
203	def head_of.go(cs: List<&2, Char>) -> List<&2, Char>:
204	  match cs:
205	    case Nil{}:
206	      Nil{}
207	    case Con{+c, t}:
208	      Lazy.stop(List<&2, Char>, Char.is_eq(c, '.'), Nil{}, _u => c <> head_of.go(t))
209	
210	# a dotted name's part before the first dot
211	def head_of(cs: List<&2, Char>) -> String:
212	  String.from_list(head_of.go(cs))
213	
214	# a dotted name's part after the first dot
215	def rest_of(cs: List<&2, Char>) -> String:
216	  match cs:
217	    case Nil{}:
218	      ""
219	    case Con{c, +t}:
220	      Lazy.stop(String, Char.is_eq(c, '.'), String.from_list(t), _u => rest_of(t))
221	
222	# is the name among these?
223	def has(names: List<&2, String>, +name: String) -> Bool:
224	  List.contains(~String, ~String.eq, names, name)
225	
226	# two names alike, char by char, stopping at the first that differs:
227	# String.eq, without the pairs String.cmp builds on every step
228	def same(aa: String, bb: String) -> Bool:
229	  match aa bb:
230	    case SNil{} SNil{}:
231	      True{}
232	    case SNil{} SCon{_h2, _t2}:
233	      False{}
234	    case SCon{_h1, _t1} SNil{}:
235	      False{}
236	    case SCon{h1, t1} SCon{h2, t2}:
237	      Lazy.and_then(Char.is_eq(h1, h2), _u => same(t1, t2))
238	
239	# is the name among the file's items? `has`, stopping at the first hit, as
240	# every use no binder holds asks it of every item
241	def has_item(names: List<&2, String>, +name: String) -> Bool:
242	  match names:
243	    case Nil{}:
244	      False{}
245	    case Con{hh, rest}:
246	      Lazy.or_else(same(hh, name), _u => has_item(rest, name))
247	
248	# the names an environment holds, and the file's items and aliases
249	type Names is Data:
250	  Names{items: List<&2, String>, aliases: List<&2, String>}
251	
252	def resolve.local(mm: Maybe<&2, Bind>, +name: String, ns: Names) -> Target:
253	  match mm:
254	    case Some{Bind{n, l, c, k, note}}:
255	      TLocal{l, c}
256	    case None{}:
257	      Names{its, als} = ns
258	      +cs = String.to_list(name)
259	      +head = head_of(cs)
260	      Bool.pick(Target, has_item(its, name), TItem{name},
261	        Lazy.stop(Target, Bool.not(Bool.and(String.contains(name, "."), has(als, head))), TFree{},
262	          _u => TQual{head, rest_of(cs)}))
263	
264	# what a name at a point refers to, given what is in scope
265	def resolve(env: List<&2, Bind>, +name: String, ns: Names) -> Target:
266	  resolve.local(find(env, name), name, ns)
267	
268	# the walk
269	# --------
270	
271	# what the walk has gathered so far, each list reversed
272	type Out is Data:
273	  Out{binds: List<&2, Bind>, uses: List<&2, Use>, scopes: List<&2, Scope>}
274	
275	# what the walk is reading; MLhs and MLhsType carry the environment the
276	# right side of the let will see, and MLhs the kind its names bind with.
277	# MSkip steps over one node (a name a form already bound), then reads on in
278	# next; MStop reads nothing more
279	type Mode is Data:
280	  MBlock{}
281	  MCtors{}
282	  MCtor{}
283	  MHead{}
284	  MName{}
285	  MSig{}
286	  MTele{kind: BindKind}
287	  MTeleType{kind: BindKind}
288	  MLhs{outer: List<&2, Bind>, kind: BindKind}
289	  MLhsType{outer: List<&2, Bind>}
290	  MTerm{}
291	  MSkip{next: Mode}
292	  MStop{}
293	
294	# the walk's result: the environment after, and the output
295	type W is Data:
296	  W{env: List<&2, Bind>, out: Out}
297	
298	# a declaration as written: `+x: List<&2, U32>`, `~f: U32 -> U32`. A space
299	# follows `:` and `,`, spaces surround `->`, everything else is glued
300	def spaced(+tt: String) -> String:
301	  Bool.pick(String, String.eq(tt, "->"), " -> ",
302	    Bool.pick(String, Bool.or(String.eq(tt, ":"), String.eq(tt, ",")), tt ++ " ", tt))
303	
304	# a group's close bracket, "" when it never closed
305	def render_close(close: Maybe<&2, Lex.Tok>) -> String:
306	  match close:
307	    case None{}:
308	      ""
309	    case Some{Lex.Tok{k, t, l, c}}:
310	      t
311	
312	# the text of a whole chain
313	def render_all(nn: Tree.Node) -> String:
314	  match nn:
315	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}:
316	      spaced(t) ++ render_all(rest)
317	    case Tree.NCons{Tree.Group{Lex.Tok{k, t, l, c}, kids, close}, rest}:
318	      t ++ render_all(kids) ++ render_close(close) ++ render_all(rest)
319	    case other:
320	      ""
321	
322	# the text of a chain up to its first comma
323	def render(nn: Tree.Node) -> String:
324	  match nn:
325	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TComma{}, t, l, c}}, rest}:
326	      ""
327	    case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}:
328	      spaced(t) ++ render(rest)
329	    case Tree.NCons{Tree.Group{Lex.Tok{k, t, l, c}, kids, close}, rest}:
330	      t ++ render_all(kids) ++ render_close(close) ++ render(rest)
331	    case other:
332	      ""
333	
334	# a use of a name, resolved against the environment
335	def use(+name: String, line: U32, col: U32, +env: List<&2, Bind>, ns: Names, out: Out) -> W:
336	  Out{binds, uses, scopes} = out
337	  W{env, Out{binds, Use{name, line, col, resolve(env, name, ns)} <> uses, scopes}}
338	
339	# the names in scope at a statement's line, recorded
340	def mark(line: U32, +env: List<&2, Bind>, out: Out) -> Out:
341	  Out{binds, uses, scopes} = out
342	  Out{binds, uses, Scope{line, env} <> scopes}
343	
344	# what the names of a telescope bind as, by its bracket: `(` parameters,
345	# `<` type parameters, `{` fields
346	def tele_kind(+oo: String) -> BindKind:
347	  Bool.pick(BindKind, String.eq(oo, "("), KParam{},
348	    Bool.pick(BindKind, String.eq(oo, "<"), KTypeParam{}, KField{}))
349	
350	# a result's environment
351	def env_of(ww: W) -> List<&2, Bind>:
352	  W{env, out} = ww
353	  env
354	
355	# a result's output
356	def out_of(ww: W) -> Out:
357	  W{env, out} = ww
358	  out
359	
360	# the plan of a step
361	# ------------------
362	# The walk takes a node apart only as far as its head (a leaf, a group, a
363	# statement, or anything else), and recurses on the head's parts and on the
364	# rest of the chain. What each step does -- the mode it reads the rest in,
365	# whether it binds or uses a name, which environment it passes on -- is
366	# decided by the plain defs below, from the mode, the head and a peek at the
367	# rest. The forms that need a peek (`K{..}`, `op name`, `x =>`, `@x:`, `&x:`)
368	# read the rest from where they are, and a name the form already bound is
369	# stepped over in MSkip.
370	
371	# does the chain start with a leaf of this kind?
372	def plan.lam(rest: Tree.Node) -> Bool:
373	  match rest:
374	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TLam{}, _t, _l, _c}}, _r}:
375	      True{}
376	    case _other:
377	      False{}
378	
379	# does the chain start with a group?
380	def plan.group(rest: Tree.Node) -> Bool:
381	  match rest:
382	    case Tree.NCons{Tree.Group{_o, _g, _cl}, _r}:
383	      True{}
384	    case _other:
385	      False{}
386	
387	# does the chain start with a name (lower or upper case)?
388	def plan.named(rest: Tree.Node) -> Bool:
389	  match rest:
390	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, _t, _l, _c}}, _r}:
391	      True{}
392	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TUpper{}, _t, _l, _c}}, _r}:
393	      True{}
394	    case _other:
395	      False{}
396	
397	# does the chain start with a name and a `:`? An upper-case name counts when
398	# upper says so
399	def plan.typed(rest: Tree.Node, upper: Bool) -> Bool:
400	  match rest:
401	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, _t, _l, _c}},
402	      Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, _ct, _cl, _cc}}, _r}}:
403	      True{}
404	    case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TUpper{}, _t, _l, _c}},
405	      Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, _ct, _cl, _cc}}, _r}}:
406	      upper
407	    case _other:
408	      False{}
409	
410	# the chain's first token; a blank one when it does not start with a leaf
411	def plan.peek(rest: Tree.Node) -> Lex.Tok:
412	  match rest:
413	    case Tree.NCons{Tree.Leaf{tok}, _r}:
414	      tok
415	    case _other:
416	      Lex.Tok{Lex.TSpace{}, "", 0, 0}
417	
418	# the chain after its first node
419	def plan.tail(rest: Tree.Node) -> Tree.Node:
420	  match rest:
421	    case Tree.NCons{_h, r}:
422	      r
423	    case _other:
424	      Tree.NNil{}
425	
426	# the mode the rest is read in after a head that means nothing in this mode
427	def plan.skip(mode: Mode) -> Mode:
428	  match mode:
429	    case MBlock{}:
430	      MStop{}
431	    case MCtors{}:
432	      MStop{}
433	    case MCtor{}:
434	      MSig{}
435	    case MHead{}:
436	      MHead{}
437	    case MName{}:
438	      MSig{}
439	    case MSig{}:
440	      MTerm{}
441	    case MTele{kind}:
442	      MTele{kind}
443	    case MTeleType{kind}:
444	      MTeleType{kind}
445	    case MLhs{outer, kind}:
446	      MLhs{outer, kind}
447	    case MLhsType{outer}:
448	      MLhsType{outer}
449	    case MTerm{}:
450	      MTerm{}
451	    case MSkip{next}:
452	      next
453	    case MStop{}:
454	      MStop{}
455	
456	# the mode the rest is read in after a leaf of kind k
457	def plan.lmode(mode: Mode, kk: Lex.TokKind, +rest: Tree.Node) -> Mode:
458	  match mode kk:
459	    case MHead{} Lex.TKey{}:
460	      MName{}
461	    case MTele{+kind} Lex.TOp{}:
462	      Bool.pick(Mode, plan.named(rest), MSkip{MTele{kind}}, MTele{kind})
463	    case MTele{kind} Lex.TColon{}:
464	      MTeleType{kind}
465	    case MTeleType{kind} Lex.TComma{}:
466	      MTele{kind}
467	    case MTeleType{+kind} Lex.TAll{}:
468	      Bool.pick(Mode, plan.typed(rest, False{}), MSkip{MTeleType{kind}}, MTeleType{kind})
469	    case MLhs{+outer, kind} Lex.TUpper{}:
470	      Bool.pick(Mode, plan.group(rest), MLhs{outer, KPat{}}, MLhs{outer, kind})
471	    case MLhs{+outer, kind} Lex.TDotted{}:
472	      Bool.pick(Mode, plan.group(rest), MLhs{outer, KPat{}}, MLhs{outer, kind})
473	    case MLhs{outer, _kind} Lex.TColon{}:
474	      MLhsType{outer}
475	    case MLhs{_outer, _kind} Lex.TEq{}:
476	      MTerm{}
477	    case MLhs{_outer, _kind} Lex.TBind{}:
478	      MTerm{}
479	    case MLhsType{_outer} Lex.TEq{}:
480	      MTerm{}
481	    case MLhsType{_outer} Lex.TBind{}:
482	      MTerm{}
483	    case MTerm{} Lex.TAll{}:
484	      Bool.pick(Mode, plan.typed(rest, True{}), MSkip{MTerm{}}, MTerm{})
485	    case MTerm{} Lex.TAmp{}:
486	      Bool.pick(Mode, plan.typed(rest, False{}), MSkip{MTerm{}}, MTerm{})
487	    case other _k:
488	      plan.skip(other)
489	
490	# does a leaf of kind k record a binder?
491	def plan.rec(mode: Mode, kk: Lex.TokKind, +rest: Tree.Node) -> Bool:
492	  match mode kk:
493	    case MCtor{} Lex.TUpper{}:
494	      True{}
495	    case MName{} Lex.TName{}:
496	      True{}
497	    case MName{} Lex.TUpper{}:
498	      True{}
499	    case MName{} Lex.TDotted{}:
500	      True{}
501	    case MTele{_kind} Lex.TOp{}:
502	      plan.named(rest)
503	    case MTele{_kind} Lex.TName{}:
504	      True{}
505	    case MTele{_kind} Lex.TUpper{}:
506	      True{}
507	    case MTeleType{_kind} Lex.TAll{}:
508	      plan.typed(rest, False{})
509	    case MLhs{_outer, _kind} Lex.TUpper{}:
510	      Bool.not(plan.group(rest))
511	    case MLhs{_outer, _kind} Lex.TName{}:
512	      True{}
513	    case MTerm{} Lex.TName{}:
514	      plan.lam(rest)
515	    case MTerm{} Lex.TAll{}:
516	      plan.typed(rest, True{})
517	    case MTerm{} Lex.TAmp{}:
518	      plan.typed(rest, False{})
519	    case _other _k:
520	      False{}
521	
522	# does the binder a leaf records go into the environment too? All do but an
523	# item's name and a constructor's, which the file's items hold
524	def plan.push(mode: Mode, kk: Lex.TokKind, rest: Tree.Node) -> Bool:
525	  match mode:
526	    case MCtor{}:
527	      False{}
528	    case MName{}:
529	      False{}
530	    case other:
531	      plan.rec(other, kk, rest)
532	
533	# does a leaf of kind k use a name?
534	def plan.use(mode: Mode, kk: Lex.TokKind, +rest: Tree.Node) -> Bool:
535	  match mode kk:
536	    case MTeleType{_kind} Lex.TName{}:
537	      True{}
538	    case MTeleType{_kind} Lex.TUpper{}:
539	      True{}
540	    case MTeleType{_kind} Lex.TDotted{}:
541	      True{}
542	    case MLhs{_outer, _kind} Lex.TUpper{}:
543	      plan.group(rest)
544	    case MLhs{_outer, _kind} Lex.TDotted{}:
545	      plan.group(rest)
546	    case MLhsType{_outer} Lex.TName{}:
547	      True{}
548	    case MLhsType{_outer} Lex.TUpper{}:
549	      True{}
550	    case MLhsType{_outer} Lex.TDotted{}:
551	      True{}
552	    case MTerm{} Lex.TName{}:
553	      Bool.not(plan.lam(rest))
554	    case MTerm{} Lex.TUpper{}:
555	      True{}
556	    case MTerm{} Lex.TDotted{}:
557	      True{}
558	    case _other _k:
559	      False{}
560	
561	# is a leaf of kind k the `=` or `<-` of a let, whose right side sees the
562	# names outside the let?
563	def plan.keep(mode: Mode, kk: Lex.TokKind) -> Bool:
564	  match mode kk:
565	    case MLhs{_outer, _kind} Lex.TEq{}:
566	      True{}
567	    case MLhs{_outer, _kind} Lex.TBind{}:
568	      True{}
569	    case MLhsType{_outer} Lex.TEq{}:
570	      True{}
571	    case MLhsType{_outer} Lex.TBind{}:
572	      True{}
573	    case _other _k:
574	      False{}
575	
576	# the environment outside a let's left side
577	def plan.outer(mode: Mode) -> List<&2, Bind>:
578	  match mode:
579	    case MLhs{outer, _kind}:
580	      outer
581	    case MLhsType{outer}:
582	      outer
583	    case _other:
584	      []
585	
586	# a binder at the next token, with the note its kind shows
587	def plan.ahead(tok: Lex.Tok, kind: BindKind, +note: String) -> Bind:
588	  match tok:
589	    case Lex.Tok{_k, t, l, c}:
590	      Bind{t, l, c, kind, note}
591	
592	# the name of the next token, "" when there is none
593	def plan.ahead_name(tok: Lex.Tok) -> String:
594	  match tok:
595	    case Lex.Tok{_k, t, _l, _c}:
596	      t
597	
598	# the binder a leaf records: its own name, or for `op name`, `@x:` and `&x:`
599	# the name after it. A telescope's binder notes its declaration
600	def plan.binder(mode: Mode, kk: Lex.TokKind, +tt: String, ll: U32, cc: U32, +rest: Tree.Node) -> Bind:
601	  match mode kk:
602	    case MCtor{} _k:
603	      Bind{tt, ll, cc, KCtor{}, ""}
604	    case MName{} _k:
605	      Bind{tt, ll, cc, KItem{}, ""}
606	    case MTele{kind} Lex.TOp{}:
607	      plan.ahead(plan.peek(rest), kind, tt ++ plan.ahead_name(plan.peek(rest)) ++ render(plan.tail(rest)))
608	    case MTele{kind} _k:
609	      Bind{tt, ll, cc, kind, "" ++ tt ++ render(rest)}
610	    case MTeleType{_kind} _k:
611	      plan.ahead(plan.peek(rest), KTypeVar{}, "")
612	    case MLhs{_outer, kind} _k:
613	      Bind{tt, ll, cc, kind, ""}
614	    case MTerm{} Lex.TName{}:
615	      Bind{tt, ll, cc, KLocal{}, ""}
616	    case MTerm{} _k:
617	      plan.ahead(plan.peek(rest), KTypeVar{}, "")
618	    case _other _k:
619	      Bind{tt, ll, cc, KLocal{}, ""}
620	
621	# a binder onto the environment, when there is one
622	def plan.pushed(push: Bool, +bb: Bind, env: List<&2, Bind>) -> List<&2, Bind>:
623	  match push:
624	    case True{}:
625	      bb <> env
626	    case False{}:
627	      env
628	
629	# a binder onto the output, when there is one
630	def plan.recorded(rec: Bool, +bb: Bind, out: Out) -> Out:
631	  match rec:
632	    case True{}:
633	      Out{binds, uses, scopes} = out
634	      Out{bb <> binds, uses, scopes}
635	    case False{}:
636	      out
637	
638	# a use onto the output, when there is one
639	def plan.used(usd: Bool, +name: String, line: U32, col: U32, env: List<&2, Bind>, ns: Names, out: Out) -> Out:
640	  match usd:
641	    case True{}:
642	      out_of(use(name, line, col, env, ns, out))
643	    case False{}:
644	      out
645	
646	# the environment the rest is read with after a leaf: the one outside a
647	# let's left side at its `=`, else this one with the leaf's binder on it
648	def plan.enter(
649	  keep: Bool,
650	  outer: List<&2, Bind>,
651	  push: Bool,
652	  +bb: Bind,
653	  env: List<&2, Bind>
654	) -> List<&2, Bind>:
655	  match keep:
656	    case True{}:
657	      outer
658	    case False{}:
659	      plan.pushed(push, bb, env)
660	
661	# the mode a group's insides are read in; MStop when they mean nothing here
662	def plan.ginner(mode: Mode, +gt: String) -> Mode:
663	  match mode:
664	    case MSig{}:
665	      MTele{tele_kind(gt)}
666	    case MTeleType{_kind}:
667	      MTerm{}
668	    case MLhs{outer, _kind}:
669	      MLhs{outer, KPat{}}
670	    case MLhsType{_outer}:
671	      MTerm{}
672	    case MTerm{}:
673	      MTerm{}
674	    case _other:
675	      MStop{}
676	
677	# the mode the rest is read in after a group
678	def plan.gnext(mode: Mode) -> Mode:
679	  match mode:
680	    case MSig{}:
681	      MTerm{}
682	    case MLhs{outer, _kind}:
683	      MLhs{outer, KPat{}}
684	    case other:
685	      plan.skip(other)
686	
687	# do the names a group binds stay bound after it? A signature's parameters
688	# and a pattern's binders do
689	def plan.gkeeps(mode: Mode) -> Bool:
690	  match mode:
691	    case MSig{}:
692	      True{}
693	    case MLhs{_outer, _kind}:
694	      True{}
695	    case _other:
696	      False{}
697	
698	# the mode a statement's header is read in
699	def plan.kmode(mode: Mode, sk: Tree.StmtKind, +env: List<&2, Bind>) -> Mode:
700	  match mode sk:
701	    case MBlock{} Tree.SDef{}:
702	      MHead{}
703	    case MBlock{} Tree.SLaw{}:
704	      MHead{}
705	    case MBlock{} Tree.SType{}:
706	      MHead{}
707	    case MBlock{} Tree.SImport{}:
708	      MStop{}
709	    case MBlock{} Tree.SCase{}:
710	      MLhs{env, KPat{}}
711	    case MBlock{} Tree.SFor{}:
712	      MLhs{env, KFor{}}
713	    case MBlock{} Tree.SLet{}:
714	      MLhs{env, KLocal{}}
715	    case MBlock{} Tree.STerm{}:
716	      MTerm{}
717	    case MCtors{} _sk:
718	      MCtor{}
719	    case _other _sk:
720	      MStop{}
721	
722	# the mode a statement's body is read in
723	def plan.bmode(mode: Mode, sk: Tree.StmtKind) -> Mode:
724	  match mode sk:
725	    case MBlock{} Tree.SType{}:
726	      MCtors{}
727	    case MBlock{} Tree.SImport{}:
728	      MStop{}
729	    case MBlock{} _sk:
730	      MBlock{}
731	    case _other _sk:
732	      MStop{}
733	
734	# is the scope recorded before a statement's header?
735	def plan.mark_head(mode: Mode, sk: Tree.StmtKind) -> Bool:
736	  match mode sk:
737	    case MBlock{} Tree.SCase{}:
738	      True{}
739	    case MBlock{} Tree.SFor{}:
740	      True{}
741	    case MBlock{} Tree.SLet{}:
742	      True{}
743	    case MBlock{} Tree.STerm{}:
744	      True{}
745	    case MCtors{} _sk:
746	      True{}
747	    case _other _sk:
748	      False{}
749	
750	# is the scope recorded between a statement's header and its body? A def's is
751	def plan.mark_body(mode: Mode, sk: Tree.StmtKind) -> Bool:
752	  match mode sk:
753	    case MBlock{} Tree.SDef{}:
754	      True{}
755	    case _other _sk:
756	      False{}
757	
758	# the scope recorded onto the output, when it is
759	def plan.marked(yes: Bool, line: U32, +env: List<&2, Bind>, out: Out) -> Out:
760	  match yes:
761	    case True{}:
762	      mark(line, env, out)
763	    case False{}:
764	      out
765	
766	# does a statement close its scope for the statements after it? All but a
767	# let and a `for` in a block do
768	def plan.scoped(mode: Mode, sk: Tree.StmtKind) -> Bool:
769	  match mode sk:
770	    case MBlock{} Tree.SFor{}:
771	      False{}
772	    case MBlock{} Tree.SLet{}:
773	      False{}
774	    case _other _sk:
775	      True{}
776	
777	# the mode the statements after a statement are read in
778	def plan.snext(mode: Mode) -> Mode:
779	  match mode:
780	    case MBlock{}:
781	      MBlock{}
782	    case MCtors{}:
783	      MCtors{}
784	    case other:
785	      plan.skip(other)
786	
787	# the walk: one node in one mode, against an environment. It takes the node
788	# apart as far as its head, and the plan above says what the head does in
789	# this mode. Every recursive call is on a subtree (kids, body, gkids or
790	# rest), never on n itself
791	def walk(nn: Tree.Node, +mode: Mode, +env: List<&2, Bind>, +ns: Names, out: Out) -> W:
792	  match nn:
793	    case Tree.NCons{hd, +rest}:
794	      match hd:
795	        case Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}:
796	          +keep = plan.keep(mode, k)
797	          +bb = plan.binder(mode, k, t, l, c, rest)
798	          +o1 = plan.recorded(plan.rec(mode, k, rest), bb, out)
799	          +o2 = plan.used(plan.use(mode, k, rest), t, l, c, env, ns, o1)
800	          +e2 = plan.enter(keep, plan.outer(mode), plan.push(mode, k, rest), bb, env)
801	          +r = walk(rest, plan.lmode(mode, k, rest), e2, ns, o2)
802	          W{Bool.pick(List<&2, Bind>, keep, env, env_of(r)), out_of(r)}
803	        case Tree.Group{Lex.Tok{_gk, gt, _gl, _gc}, gkids, _close}:
804	          +g = walk(gkids, plan.ginner(mode, gt), env, ns, out)
805	          walk(rest, plan.gnext(mode), Bool.pick(List<&2, Bind>, plan.gkeeps(mode), env_of(g), env), ns, out_of(g))
806	        case Tree.Stmt{+sk, +kids, body}:
807	          +h = walk(kids, plan.kmode(mode, sk, env), env, ns,
808	            plan.marked(plan.mark_head(mode, sk), Tree.line(kids), env, out))
809	          +b = walk(body, plan.bmode(mode, sk), env_of(h), ns,
810	            plan.marked(plan.mark_body(mode, sk), Tree.line(kids), env_of(h), out_of(h)))
811	          walk(rest, plan.snext(mode), Bool.pick(List<&2, Bind>, plan.scoped(mode, sk), env, env_of(h)), ns, out_of(b))
812	        case _other:
813	          walk(rest, plan.skip(mode), env, ns, out)
814	    case _other:
815	      W{env, out}
816	
817	# notes
818	# -----
819	
820	# leading spaces dropped
821	def lstrip(cs: List<&2, Char>) -> List<&2, Char>:
822	  match cs:
823	    case Con{' ', t}:
824	      lstrip(t)
825	    case other:
826	      other
827	
828	# a line's text without its indentation
829	def stripped(+text: String) -> String:
830	  String.from_list(lstrip(String.to_list(text)))
831	
832	# a declaration carries its own note; anything else shows the line that
833	# bound it, which `text` gives only when it is asked for
834	def note_for(kind: BindKind, +note: String, text: Unit -> String) -> String:
835	  match kind:
836	    case KParam{}:
837	      note
838	    case KField{}:
839	      note
840	    case KTypeParam{}:
841	      note
842	    case other:
843	      text(Unit{})
844	
845	# the lines from line `line` on, given the lines from line `at` on: a step
846	# forward from where the last binder was, not a walk from the first line
847	def annotate.ahead(+line: U32, +at: U32, cur: List<&2, String>) -> List<&2, String>:
848	  List.drop(&2, String, cur, U32.to_nat(U32.sub(line, at)))
849	
850	# the first line of these, or ""
851	def annotate.head(+cur: List<&2, String>) -> String:
852	  Maybe.default(&2, String, List.head(&2, String, cur), "")
853	
854	# a line read from the first, for a binder behind the last one
855	def annotate.back(lines: List<&2, String>, +line: U32) -> String:
856	  Maybe.default(&2, String, List.get(&2, String, lines, U32.to_nat(line)), "")
857	
858	# every binder with its note filled. Binders come in source order, so the
859	# lines are read once, front to back, from where the last binder was (`cur`
860	# holds the lines from line `at` on); a binder behind that point reads its
861	# line from the start
862	def annotate.go(binds: List<&2, Bind>, +lines: List<&2, String>, +at: U32, +cur: List<&2, String>) -> List<&2, Bind>:
863	  match binds:
864	    case Nil{}:
865	      Nil{}
866	    case Con{Bind{name, +line, col, +kind, note}, rest}:
867	      +ahead = U32.is_ge(line, at)
868	      +here = Lazy.either(List<&2, String>, ahead, _u => annotate.ahead(line, at, cur), _v => cur)
869	      +text = Lazy.either(String, ahead, _u => annotate.head(here), _v => annotate.back(lines, line))
870	      Bind{name, line, col, kind, note_for(kind, note, _w => stripped(text))}
871	        <> annotate.go(rest, lines, Bool.pick(U32, ahead, line, at), here)
872	
873	# every binder with its note filled
874	def annotate(binds: List<&2, Bind>, +lines: List<&2, String>) -> List<&2, Bind>:
875	  annotate.go(binds, lines, 0, lines)
876	
877	# putting it together
878	# -------------------
879	
880	# the gathered output, in source order and annotated
881	def finish(oo: Out, lines: List<&2, String>) -> Bound:
882	  Out{binds, uses, scopes} = oo
883	  Bound{annotate(List.reverse(&2, Bind, binds), lines), List.reverse(&2, Use, uses), List.reverse(&2, Scope, scopes)}
884	
885	# the binding structure of a parsed source
886	def of_tree(+root: Tree.Node, lines: List<&2, String>) -> Bound:
887	  finish(out_of(walk(root, MBlock{}, [], Names{items(root, []), aliases(root, [])}, Out{[], [], []})), lines)
888	
889	# the binding structure of a source
890	def bound(+source: String) -> Bound:
891	  of_tree(Tree.parse(source), String.lines(source))
892	
893	# queries
894	# -------
895	
896	# where a name is: a binder, or a use of one
897	type Site is Data:
898	  SBind{bind: Bind}
899	  SUse{use: Use}
900	
901	# does the name at (l, c) cover the position (line, col)?
902	def covers(+l2: U32, +c2: U32, +name: String, +line: U32, +col: U32) -> Bool:
903	  +end = (c2 + U32.from_nat(String.length(name)) : U32)
904	  Bool.and(U32.is_eq(l2, line), Bool.and(U32.is_le(c2, col), U32.is_lt(col, end)))
905	
906	# the binder whose name covers a position; hit: the one before binds did,
907	# so the search stops there
908	def bind_at.go(binds: List<&2, Bind>, +line: U32, +col: U32, hit: Maybe<&2, Site>) -> Maybe<&2, Site>:
909	  match binds:
910	    case Nil{}:
911	      hit
912	    case Con{Bind{+name, +l, +c, kind, note}, rest}:
913	      match hit:
914	        case Some{x}:
915	          Some{x}
916	        case None{}:
917	          bind_at.go(rest, line, col,
918	            Bool.pick(Maybe<&2, Site>, covers(l, c, name, line, col), Some{SBind{Bind{name, l, c, kind, note}}},
919	              None{}))
920	
921	# the binder whose name covers a position
922	def bind_at(binds: List<&2, Bind>, +line: U32, +col: U32) -> Maybe<&2, Site>:
923	  bind_at.go(binds, line, col, None{})
924	
925	# the use whose name covers a position; hit: the one before uses did, so the
926	# search stops there
927	def use_at.go(uses: List<&2, Use>, +line: U32, +col: U32, hit: Maybe<&2, Site>) -> Maybe<&2, Site>:
928	  match uses:
929	    case Nil{}:
930	      hit
931	    case Con{Use{+name, +l, +c, tg}, rest}:
932	      match hit:
933	        case Some{x}:
934	          Some{x}
935	        case None{}:
936	          use_at.go(rest, line, col,
937	            Bool.pick(Maybe<&2, Site>, covers(l, c, name, line, col), Some{SUse{Use{name, l, c, tg}}}, None{}))
938	
939	# the use whose name covers a position
940	def use_at(uses: List<&2, Use>, +line: U32, +col: U32) -> Maybe<&2, Site>:
941	  use_at.go(uses, line, col, None{})
942	
943	def at.or(mm: Maybe<&2, Site>, uses: List<&2, Use>, line: U32, col: U32) -> Maybe<&2, Site>:
944	  match mm:
945	    case Some{site}:
946	      Some{site}
947	    case None{}:
948	      use_at(uses, line, col)
949	
950	# the site at a position
951	def at(bb: Bound, +line: U32, +col: U32) -> Maybe<&2, Site>:
952	  Bound{binds, uses, scopes} = bb
953	  at.or(bind_at(binds, line, col), uses, line, col)
954	
955	# the binder at a position (a use's target, or the binder itself); hit: the
956	# one before binds was, so the search stops there
957	def binder.go(binds: List<&2, Bind>, +line: U32, +col: U32, hit: Maybe<&2, Bind>) -> Maybe<&2, Bind>:
958	  match binds:
959	    case Nil{}:
960	      hit
961	    case Con{Bind{name, +l, +c, kind, note}, rest}:
962	      match hit:
963	        case Some{x}:
964	          Some{x}
965	        case None{}:
966	          +here = Bool.and(U32.is_eq(l, line), U32.is_eq(c, col))
967	          binder.go(rest, line, col, Bool.pick(Maybe<&2, Bind>, here, Some{Bind{name, l, c, kind, note}}, None{}))
968	
969	# the binder at a position (a use's target, or the binder itself)
970	def binder(binds: List<&2, Bind>, +line: U32, +col: U32) -> Maybe<&2, Bind>:
971	  binder.go(binds, line, col, None{})
972	
973	# the names in scope at a line: those of the statement on it, else of the
974	# nearest statement above
975	def visible.go(scopes: List<&2, Scope>, +qline: U32, best: List<&2, Bind>) -> List<&2, Bind>:
976	  match scopes:
977	    case Nil{}:
978	      best
979	    case Con{Scope{+line, env}, rest}:
980	      +hit = U32.is_le(line, qline)
981	      visible.go(rest, qline, Bool.pick(List<&2, Bind>, hit, env, best))
982	
983	# the scopes hold binders before their notes were filled: read each back
984	def noted(mm: Maybe<&2, Bind>, bb: Bind) -> Bind:
985	  match mm:
986	    case None{}:
987	      bb
988	    case Some{full}:
989	      full
990	
991	# does (l1, c1) come before (l2, c2) in the source?
992	def before(+l1: U32, +c1: U32, +l2: U32, +c2: U32) -> Bool:
993	  Bool.or(U32.is_lt(l1, l2), Bool.and(U32.is_eq(l1, l2), U32.is_lt(c1, c2)))
994	
995	# does a cursor's head sit at or after a position (the seek stops there)?
996	def seek.stop(cur: List<&2, Bind>, +line: U32, +col: U32) -> Bool:
997	  match cur:
998	    case Nil{}:
999	      True{}
1000	    case Con{Bind{name, +l, +c, kind, note}, rest}:
1001	      Bool.not(before(l, c, line, col))
1002	
1003	# the binders from the first one not before a position on; the binders are in
1004	# source order, so none this drops sits at the position. stop is seek.stop of
1005	# binds, carried so the step stays a loop
1006	def seek(binds: List<&2, Bind>, +line: U32, +col: U32, +stop: Bool) -> List<&2, Bind>:
1007	  match binds:
1008	    case Nil{}:
1009	      Nil{}
1010	    case Con{h, +rest}:
1011	      match stop:
1012	        case True{}:
1013	          h <> rest
1014	        case False{}:
1015	          seek(rest, line, col, seek.stop(rest, line, col))
1016	
1017	# the binder at the head of a cursor, when it sits at the position
1018	def seek.head(cur: List<&2, Bind>, +line: U32, +col: U32) -> Maybe<&2, Bind>:
1019	  match cur:
1020	    case Nil{}:
1021	      None{}
1022	    case Con{Bind{name, +l, +c, kind, note}, rest}:
1023	      Bool.pick(Maybe<&2, Bind>, Bool.and(U32.is_eq(l, line), U32.is_eq(c, col)), Some{Bind{name, l, c, kind, note}},
1024	        None{})
1025	
1026	# each binder of an environment, outermost first, with the note its annotated
1027	# twin carries, pushed onto acc (so acc ends innermost first again). cur is a
1028	# cursor into binds that drops only binders before (tl, tc), the last one
1029	# read: an environment's binders were pushed in source order, so each lookup
1030	# picks up where the last stopped and binds is read once, not once per
1031	# binder. A binder before the last one read starts the cursor over
1032	def refresh.go(
1033	  env: List<&2, Bind>,
1034	  +binds: List<&2, Bind>,
1035	  +cur: List<&2, Bind>,
1036	  +tl: U32,
1037	  +tc: U32,
1038	  acc: List<&2, Bind>
1039	) -> List<&2, Bind>:
1040	  match env:
1041	    case Nil{}:
1042	      acc
1043	    case Con{Bind{name, +l, +c, kind, note}, rest}:
1044	      +start = Bool.pick(List<&2, Bind>, before(l, c, tl, tc), binds, cur)
1045	      +from = seek(start, l, c, seek.stop(start, l, c))
1046	      refresh.go(rest, binds, from, l, c, noted(seek.head(from, l, c), Bind{name, l, c, kind, note}) <> acc)
1047	
1048	# each binder of an environment, with the note its annotated twin carries
1049	def refresh(env: List<&2, Bind>, +binds: List<&2, Bind>) -> List<&2, Bind>:
1050	  refresh.go(List.reverse(&2, Bind, env), binds, binds, 0, 0, [])
1051	
1052	# the names in scope at a line: those of the statement on it, else of the
1053	# nearest statement above
1054	def visible(bb: Bound, qline: U32) -> List<&2, Bind>:
1055	  Bound{binds, uses, scopes} = bb
1056	  refresh(visible.go(scopes, qline, []), binds)
1057	
1058	# every position a binder is named at: its own, then its uses'
1059	def sites.go(uses: List<&2, Use>, +line: U32, +col: U32) -> List<&2, Pos>:
1060	  match uses:
1061	    case Nil{}:
1062	      Nil{}
1063	    case Con{Use{name, l, c, TLocal{+tl, +tc}}, rest}:
1064	      +more = sites.go(rest, line, col)
1065	      Bool.pick(List<&2, Pos>, Bool.and(U32.is_eq(tl, line), U32.is_eq(tc, col)), Pos{l, c} <> more, more)
1066	    case Con{other, rest}:
1067	      sites.go(rest, line, col)
1068	
1069	# every position a binder is named at: its own, then its uses'
1070	def sites(bb: Bound, +line: U32, +col: U32) -> List<&2, Pos>:
1071	  Bound{binds, uses, scopes} = bb
1072	  Pos{line, col} <> sites.go(uses, line, col)
1073	
1074	# every position an item of the file is named at: its declaration, then its
1075	# uses
1076	def item_sites.binds(binds: List<&2, Bind>, +name: String) -> List<&2, Pos>:
1077	  match binds:
1078	    case Nil{}:
1079	      Nil{}
1080	    case Con{Bind{+n, l, c, KItem{}, note}, rest}:
1081	      +more = item_sites.binds(rest, name)
1082	      Bool.pick(List<&2, Pos>, String.eq(n, name), Pos{l, c} <> more, more)
1083	    case Con{Bind{+n, l, c, KCtor{}, note}, rest}:
1084	      +more = item_sites.binds(rest, name)
1085	      Bool.pick(List<&2, Pos>, String.eq(n, name), Pos{l, c} <> more, more)
1086	    case Con{other, rest}:
1087	      item_sites.binds(rest, name)
1088	
1089	def item_sites.uses(uses: List<&2, Use>, +name: String) -> List<&2, Pos>:
1090	  match uses:
1091	    case Nil{}:
1092	      Nil{}
1093	    case Con{Use{n, l, c, TItem{+t}}, rest}:
1094	      +more = item_sites.uses(rest, name)
1095	      Bool.pick(List<&2, Pos>, String.eq(t, name), Pos{l, c} <> more, more)
1096	    case Con{other, rest}:
1097	      item_sites.uses(rest, name)
1098	
1099	# every position an item of the file is named at: its declaration, then its
1100	# uses
1101	def item_sites(bb: Bound, +name: String) -> List<&2, Pos>:
1102	  Bound{binds, uses, scopes} = bb
1103	  List.append(&2, Pos, item_sites.binds(binds, name), item_sites.uses(uses, name))
1104	
1105	# every position a name not of this file is used at (Base, or through an
1106	# alias)
1107	def named_sites.go(uses: List<&2, Use>, +name: String) -> List<&2, Pos>:
1108	  match uses:
1109	    case Nil{}:
1110	      Nil{}
1111	    case Con{Use{+n, l, c, TLocal{tl, tc}}, rest}:
1112	      named_sites.go(rest, name)
1113	    case Con{Use{+n, l, c, tg}, rest}:
1114	      +more = named_sites.go(rest, name)
1115	      Bool.pick(List<&2, Pos>, String.eq(n, name), Pos{l, c} <> more, more)
1116	
1117	# every position a name not of this file is used at (Base, or through an
1118	# alias)
1119	def named_sites(bb: Bound, +name: String) -> List<&2, Pos>:
1120	  Bound{binds, uses, scopes} = bb
1121	  named_sites.go(uses, name)