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