src/syntax/bind.bend

bolt@1.27.0.0 · 1,121 lines · 110 definitions

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).
18import Base
19import bolt@1.27.0.0/src/syntax/lex.bend as Lex
20import bolt@1.27.0.0/src/lazy/lazy.bend as Lazy
21import bolt@1.27.0.0/src/syntax/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:`
26type 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
40type 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)
45type 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
52type Use is Data:
53  Use{name: String, line: U32, col: U32, target: Target}
54
55# the names in scope at a statement's line
56type 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
60type Bound is Data:
61  Bound{binds: List<&2, Bind>, uses: List<&2, Use>, scopes: List<&2, Scope>}
62
63# a line and a column
64type 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
71def 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
83def 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
91def 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?
99def 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
107def 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
115def 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?
123def 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
133def 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
141def 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
149def 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
163def 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`
173def 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
188def 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
200def find(env: List<&2, Bind>, +name: String) -> Maybe<&2, Bind>:
201  find.go(env, name, None{})
202
203def 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
211def 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
215def 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?
223def 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
228def 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
241def 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
249type Names is Data:
250  Names{items: List<&2, String>, aliases: List<&2, String>}
251
252def 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
265def 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
272type 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
279type 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
295type 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
300def 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
305def 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
313def 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
323def 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
335def 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
340def 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
346def 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
351def env_of(ww: W) -> List<&2, Bind>:
352  W{env, out} = ww
353  env
354
355# a result's output
356def 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?
372def 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?
380def 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)?
388def 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
399def 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
411def 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
419def 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
427def 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
457def 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?
491def 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
524def 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?
534def 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?
563def 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
577def 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
587def 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
593def 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
600def 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
622def 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
630def 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
639def 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
648def 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
662def 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
678def 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
689def 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
699def 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
723def 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?
735def 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
751def 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
759def 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
768def 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
778def 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
791def 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
821def 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
829def 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
834def 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
847def 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 ""
851def 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
855def 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
862def 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
874def 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
881def 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
886def 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
890def 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
897type Site is Data:
898  SBind{bind: Bind}
899  SUse{use: Use}
900
901# does the name at (l, c) cover the position (line, col)?
902def 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
908def 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
922def 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
927def 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
940def use_at(uses: List<&2, Use>, +line: U32, +col: U32) -> Maybe<&2, Site>:
941  use_at.go(uses, line, col, None{})
942
943def 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
951def 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
957def 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)
970def 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
975def 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
984def 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?
992def 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)?
996def 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
1006def 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
1018def 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
1032def 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
1049def 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
1054def 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'
1059def 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'
1070def 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
1076def 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
1089def 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
1101def 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)
1107def 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)
1119def named_sites(bb: Bound, +name: String) -> List<&2, Pos>:
1120  Bound{binds, uses, scopes} = bb
1121  named_sites.go(uses, name)