src/syntax/bind.bend source
src/syntax/bind.bend on the hub · documented module
# src/syntax/bind: where every name in a source is bound, and what every other# name refers to. One walk over the tree threads an environment (the binders# in scope, innermost first) through Bend's binding forms:# - an item's name (`def f`, `type T`, `law l`, a constructor line);# - a telescope: a def's parameters, a type's parameters, a constructor's# fields, each type seeing the names before it;# - `case p:` patterns and `for x: T` / `exs x: T where P`, for the lines# under them;# - a let (`x = v`, `+x = v`, `x : T = v`, `x : T <- m`, `a b = f g`,# `(a, K{b}) = p`) for the lines after it in its block -- the right side# sees the outer names, so `st = step(st)` reads the old st;# - `x => e`, `@x: A -> B` and `&x: A -> B`, for the rest of their sequence.# The walk branches on token and statement kinds, never on a computed test,# so each step recurses on one subtree and the checker accepts it.# A binder shadows an item of the same name; a dotted name is an item of the# file (`text.of`) or, through an import alias, of another file (`Lex.Tok`);# anything else is free (Base, or unknown).import Baseimport ./lex.bend as Leximport ../lazy/lazy.bend as Lazyimport ./tree.bend as Tree# what a binder is: an item's or a constructor's name, a parameter, a type's# parameter, a constructor's field, a let name, a pattern binder, a law's# `for`, or a type-level `@x:` / `&x:`type BindKind is Data: KItem{} KCtor{} KParam{} KTypeParam{} KField{} KLocal{} KPat{} KFor{} KTypeVar{}# KLocal is a name a let, a do-bind or a lambda binds; KPat one bound by a# pattern (a case, or a destructuring let). note: what to show for it -- a# declaration's own text (`+x: U32`), else the line that bound ittype Bind is Data: Bind{name: String, line: U32, col: U32, kind: BindKind, note: String}# what a use refers to: a binder of the file (by position), an item of the# file, an item behind an import alias, or nothing known (Base, or unknown)type Target is Data: TLocal{line: U32, col: U32} TItem{name: String} TQual{alias: String, name: String} TFree{}# a name that is not a binder, with what it refers totype Use is Data: Use{name: String, line: U32, col: U32, target: Target}# the names in scope at a statement's linetype Scope is Data: Scope{line: U32, env: List<&2, Bind>}# everything the binder knows about a source, each list in source ordertype Bound is Data: Bound{binds: List<&2, Bind>, uses: List<&2, Use>, scopes: List<&2, Scope>}# a line and a columntype Pos is Data: Pos{line: U32, col: U32}# names of the file# -----------------# a name that can be declared: plain, capitalized or dotteddef declared.is_name(kk: Lex.TokKind) -> Bool: match kk: case Lex.TName{}: True{} case Lex.TUpper{}: True{} case Lex.TDotted{}: True{} case other: False{}# a leaf's name, when its kind is one: the kind is tested, the text only keptdef declared.name(nn: Tree.Node) -> Maybe<&2, String>: match nn: case Tree.Leaf{Lex.Tok{k, t, l, c}}: Bool.pick(Maybe<&2, String>, declared.is_name(k), Some{t}, None{}) case other: None{}# the item a statement declares: the first name after its keyworddef declared.go(kids: Tree.Node) -> Maybe<&2, String>: match kids: case Tree.NCons{h, rest}: declared.name(h) case other: None{}# a keyword?def declared.is_key(kk: Lex.TokKind) -> Bool: match kk: case Lex.TKey{}: True{} case other: False{}# a keyword leaf? its kind is read, never its textdef declared.key(nn: Tree.Node) -> Bool: match nn: case Tree.Leaf{Lex.Tok{k, t, l, c}}: declared.is_key(k) case other: False{}# the item a statement declares: the first name after its keyworddef declared(kids: Tree.Node) -> Maybe<&2, String>: match kids: case Tree.NCons{h, +rest}: Lazy.either(Maybe<&2, String>, declared.key(h), _u => declared.go(rest), _v => declared(rest)) case other: None{}# is the name at the head of the list?def push_name.again(acc: List<&2, String>, +name: String) -> Bool: match acc: case Nil{}: False{} case Con{hh, _rest}: String.eq(hh, name)# a name, when there is one, onto a list, unless it is the name just put# there: a proof file's `law x` and its `def x` are one item, and every use# no binder holds is looked for in this listdef push_name(mm: Maybe<&2, String>, +acc: List<&2, String>) -> List<&2, String>: match mm: case None{}: acc case Some{+name}: Lazy.stop(List<&2, String>, push_name.again(acc, name), acc, _u => name <> acc)# a type's constructors: the first name of each line under itdef ctors(body: Tree.Node, acc: List<&2, String>) -> List<&2, String>: match body: case Tree.NCons{Tree.Stmt{k, kids, b}, rest}: ctors(rest, push_name(declared.go(kids), acc)) case other: acc# the defs, laws, types and constructors of a sourcedef items(root: Tree.Node, acc: List<&2, String>) -> List<&2, String>: match root: case Tree.NCons{Tree.Stmt{Tree.SDef{}, kids, body}, rest}: items(rest, push_name(declared(kids), acc)) case Tree.NCons{Tree.Stmt{Tree.SLaw{}, kids, body}, rest}: items(rest, push_name(declared(kids), acc)) case Tree.NCons{Tree.Stmt{Tree.SType{}, kids, body}, rest}: items(rest, ctors(body, push_name(declared(kids), acc))) case Tree.NCons{other, rest}: items(rest, acc) case other: acc# the text of a chain's last leafdef last_text(kids: Tree.Node) -> String: match kids: case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, Tree.NNil{}}: t case Tree.NCons{h, rest}: last_text(rest) case other: ""# the import aliases of a source: the last token of each `import .. as X`def aliases(root: Tree.Node, +acc: List<&2, String>) -> List<&2, String>: match root: case Tree.NCons{Tree.Stmt{Tree.SImport{}, kids, body}, rest}: +last = last_text(kids) aliases(rest, Bool.pick(List<&2, String>, Bool.or(String.eq(last, "Base"), String.eq(last, "import")), acc, last <> acc)) case Tree.NCons{other, rest}: aliases(rest, acc) case other: acc# resolution# ----------# the innermost binder of a name in an environmentdef find(env: List<&2, Bind>, +name: String) -> Maybe<&2, Bind>: match env: case Nil{}: None{} case Con{Bind{+n, l, c, k, note}, t}: +more = find(t, name) Bool.pick(Maybe<&2, Bind>, String.eq(n, name), Some{Bind{n, l, c, k, note}}, more)def head_of.go(cs: List<&2, Char>) -> List<&2, Char>: match cs: case Nil{}: Nil{} case Con{+c, t}: Lazy.stop(List<&2, Char>, Char.is_eq(c, '.'), Nil{}, _u => c <> head_of.go(t))# a dotted name's part before the first dotdef head_of(cs: List<&2, Char>) -> String: String.from_list(head_of.go(cs))# a dotted name's part after the first dotdef rest_of(cs: List<&2, Char>) -> String: match cs: case Nil{}: "" case Con{c, +t}: Lazy.stop(String, Char.is_eq(c, '.'), String.from_list(t), _u => rest_of(t))# is the name among these?def has(names: List<&2, String>, +name: String) -> Bool: List.contains(~String, ~String.eq, names, name)# two names alike, char by char, stopping at the first that differs:# String.eq, without the pairs String.cmp builds on every stepdef same(aa: String, bb: String) -> Bool: match aa bb: case SNil{} SNil{}: True{} case SNil{} SCon{_h2, _t2}: False{} case SCon{_h1, _t1} SNil{}: False{} case SCon{h1, t1} SCon{h2, t2}: Lazy.and_then(Char.is_eq(h1, h2), _u => same(t1, t2))# is the name among the file's items? `has`, stopping at the first hit, as# every use no binder holds asks it of every itemdef has_item(names: List<&2, String>, +name: String) -> Bool: match names: case Nil{}: False{} case Con{hh, rest}: Lazy.or_else(same(hh, name), _u => has_item(rest, name))# the names an environment holds, and the file's items and aliasestype Names is Data: Names{items: List<&2, String>, aliases: List<&2, String>}def resolve.local(mm: Maybe<&2, Bind>, +name: String, ns: Names) -> Target: match mm: case Some{Bind{n, l, c, k, note}}: TLocal{l, c} case None{}: Names{its, als} = ns +cs = String.to_list(name) +head = head_of(cs) Bool.pick(Target, has_item(its, name), TItem{name}, Lazy.stop(Target, Bool.not(Bool.and(String.contains(name, "."), has(als, head))), TFree{}, _u => TQual{head, rest_of(cs)}))# what a name at a point refers to, given what is in scopedef resolve(env: List<&2, Bind>, +name: String, ns: Names) -> Target: resolve.local(find(env, name), name, ns)# the walk# --------# what the walk has gathered so far, each list reversedtype Out is Data: Out{binds: List<&2, Bind>, uses: List<&2, Use>, scopes: List<&2, Scope>}# what the walk is reading; MLhs and MLhsType carry the environment the# right side of the let will see, and MLhs the kind its names bind with.# MSkip steps over one node (a name a form already bound), then reads on in# next; MStop reads nothing moretype Mode is Data: MBlock{} MCtors{} MCtor{} MHead{} MName{} MSig{} MTele{kind: BindKind} MTeleType{kind: BindKind} MLhs{outer: List<&2, Bind>, kind: BindKind} MLhsType{outer: List<&2, Bind>} MTerm{} MSkip{next: Mode} MStop{}# the walk's result: the environment after, and the outputtype W is Data: W{env: List<&2, Bind>, out: Out}# a declaration as written: `+x: List<&2, U32>`, `~f: U32 -> U32`. A space# follows `:` and `,`, spaces surround `->`, everything else is glueddef spaced(+tt: String) -> String: Bool.pick(String, String.eq(tt, "->"), " -> ", Bool.pick(String, Bool.or(String.eq(tt, ":"), String.eq(tt, ",")), tt ++ " ", tt))# a group's close bracket, "" when it never closeddef render_close(close: Maybe<&2, Lex.Tok>) -> String: match close: case None{}: "" case Some{Lex.Tok{k, t, l, c}}: t# the text of a whole chaindef render_all(nn: Tree.Node) -> String: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}: spaced(t) ++ render_all(rest) case Tree.NCons{Tree.Group{Lex.Tok{k, t, l, c}, kids, close}, rest}: t ++ render_all(kids) ++ render_close(close) ++ render_all(rest) case other: ""# the text of a chain up to its first commadef render(nn: Tree.Node) -> String: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TComma{}, t, l, c}}, rest}: "" case Tree.NCons{Tree.Leaf{Lex.Tok{k, t, l, c}}, rest}: spaced(t) ++ render(rest) case Tree.NCons{Tree.Group{Lex.Tok{k, t, l, c}, kids, close}, rest}: t ++ render_all(kids) ++ render_close(close) ++ render(rest) case other: ""# a use of a name, resolved against the environmentdef use(+name: String, line: U32, col: U32, +env: List<&2, Bind>, ns: Names, out: Out) -> W: Out{binds, uses, scopes} = out W{env, Out{binds, Use{name, line, col, resolve(env, name, ns)} <> uses, scopes}}# the names in scope at a statement's line, recordeddef mark(line: U32, +env: List<&2, Bind>, out: Out) -> Out: Out{binds, uses, scopes} = out Out{binds, uses, Scope{line, env} <> scopes}# what the names of a telescope bind as, by its bracket: `(` parameters,# `<` type parameters, `{` fieldsdef tele_kind(+oo: String) -> BindKind: Bool.pick(BindKind, String.eq(oo, "("), KParam{}, Bool.pick(BindKind, String.eq(oo, "<"), KTypeParam{}, KField{}))# a result's environmentdef env_of(ww: W) -> List<&2, Bind>: W{env, out} = ww env# a result's outputdef out_of(ww: W) -> Out: W{env, out} = ww out# the plan of a step# ------------------# The walk takes a node apart only as far as its head (a leaf, a group, a# statement, or anything else), and recurses on the head's parts and on the# rest of the chain. What each step does -- the mode it reads the rest in,# whether it binds or uses a name, which environment it passes on -- is# decided by the plain defs below, from the mode, the head and a peek at the# rest. The forms that need a peek (`K{..}`, `op name`, `x =>`, `@x:`, `&x:`)# read the rest from where they are, and a name the form already bound is# stepped over in MSkip.# does the chain start with a leaf of this kind?def plan.lam(rest: Tree.Node) -> Bool: match rest: case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TLam{}, _t, _l, _c}}, _r}: True{} case _other: False{}# does the chain start with a group?def plan.group(rest: Tree.Node) -> Bool: match rest: case Tree.NCons{Tree.Group{_o, _g, _cl}, _r}: True{} case _other: False{}# does the chain start with a name (lower or upper case)?def plan.named(rest: Tree.Node) -> Bool: match rest: case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, _t, _l, _c}}, _r}: True{} case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TUpper{}, _t, _l, _c}}, _r}: True{} case _other: False{}# does the chain start with a name and a `:`? An upper-case name counts when# upper says sodef plan.typed(rest: Tree.Node, upper: Bool) -> Bool: match rest: case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, _t, _l, _c}}, Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, _ct, _cl, _cc}}, _r}}: True{} case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TUpper{}, _t, _l, _c}}, Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, _ct, _cl, _cc}}, _r}}: upper case _other: False{}# the chain's first token; a blank one when it does not start with a leafdef plan.peek(rest: Tree.Node) -> Lex.Tok: match rest: case Tree.NCons{Tree.Leaf{tok}, _r}: tok case _other: Lex.Tok{Lex.TSpace{}, "", 0, 0}# the chain after its first nodedef plan.tail(rest: Tree.Node) -> Tree.Node: match rest: case Tree.NCons{_h, r}: r case _other: Tree.NNil{}# the mode the rest is read in after a head that means nothing in this modedef plan.skip(mode: Mode) -> Mode: match mode: case MBlock{}: MStop{} case MCtors{}: MStop{} case MCtor{}: MSig{} case MHead{}: MHead{} case MName{}: MSig{} case MSig{}: MTerm{} case MTele{kind}: MTele{kind} case MTeleType{kind}: MTeleType{kind} case MLhs{outer, kind}: MLhs{outer, kind} case MLhsType{outer}: MLhsType{outer} case MTerm{}: MTerm{} case MSkip{next}: next case MStop{}: MStop{}# the mode the rest is read in after a leaf of kind kdef plan.lmode(mode: Mode, kk: Lex.TokKind, +rest: Tree.Node) -> Mode: match mode kk: case MHead{} Lex.TKey{}: MName{} case MTele{+kind} Lex.TOp{}: Bool.pick(Mode, plan.named(rest), MSkip{MTele{kind}}, MTele{kind}) case MTele{kind} Lex.TColon{}: MTeleType{kind} case MTeleType{kind} Lex.TComma{}: MTele{kind} case MTeleType{+kind} Lex.TAll{}: Bool.pick(Mode, plan.typed(rest, False{}), MSkip{MTeleType{kind}}, MTeleType{kind}) case MLhs{+outer, kind} Lex.TUpper{}: Bool.pick(Mode, plan.group(rest), MLhs{outer, KPat{}}, MLhs{outer, kind}) case MLhs{+outer, kind} Lex.TDotted{}: Bool.pick(Mode, plan.group(rest), MLhs{outer, KPat{}}, MLhs{outer, kind}) case MLhs{outer, _kind} Lex.TColon{}: MLhsType{outer} case MLhs{_outer, _kind} Lex.TEq{}: MTerm{} case MLhs{_outer, _kind} Lex.TBind{}: MTerm{} case MLhsType{_outer} Lex.TEq{}: MTerm{} case MLhsType{_outer} Lex.TBind{}: MTerm{} case MTerm{} Lex.TAll{}: Bool.pick(Mode, plan.typed(rest, True{}), MSkip{MTerm{}}, MTerm{}) case MTerm{} Lex.TAmp{}: Bool.pick(Mode, plan.typed(rest, False{}), MSkip{MTerm{}}, MTerm{}) case other _k: plan.skip(other)# does a leaf of kind k record a binder?def plan.rec(mode: Mode, kk: Lex.TokKind, +rest: Tree.Node) -> Bool: match mode kk: case MCtor{} Lex.TUpper{}: True{} case MName{} Lex.TName{}: True{} case MName{} Lex.TUpper{}: True{} case MName{} Lex.TDotted{}: True{} case MTele{_kind} Lex.TOp{}: plan.named(rest) case MTele{_kind} Lex.TName{}: True{} case MTele{_kind} Lex.TUpper{}: True{} case MTeleType{_kind} Lex.TAll{}: plan.typed(rest, False{}) case MLhs{_outer, _kind} Lex.TUpper{}: Bool.not(plan.group(rest)) case MLhs{_outer, _kind} Lex.TName{}: True{} case MTerm{} Lex.TName{}: plan.lam(rest) case MTerm{} Lex.TAll{}: plan.typed(rest, True{}) case MTerm{} Lex.TAmp{}: plan.typed(rest, False{}) case _other _k: False{}# does the binder a leaf records go into the environment too? All do but an# item's name and a constructor's, which the file's items holddef plan.push(mode: Mode, kk: Lex.TokKind, rest: Tree.Node) -> Bool: match mode: case MCtor{}: False{} case MName{}: False{} case other: plan.rec(other, kk, rest)# does a leaf of kind k use a name?def plan.use(mode: Mode, kk: Lex.TokKind, +rest: Tree.Node) -> Bool: match mode kk: case MTeleType{_kind} Lex.TName{}: True{} case MTeleType{_kind} Lex.TUpper{}: True{} case MTeleType{_kind} Lex.TDotted{}: True{} case MLhs{_outer, _kind} Lex.TUpper{}: plan.group(rest) case MLhs{_outer, _kind} Lex.TDotted{}: plan.group(rest) case MLhsType{_outer} Lex.TName{}: True{} case MLhsType{_outer} Lex.TUpper{}: True{} case MLhsType{_outer} Lex.TDotted{}: True{} case MTerm{} Lex.TName{}: Bool.not(plan.lam(rest)) case MTerm{} Lex.TUpper{}: True{} case MTerm{} Lex.TDotted{}: True{} case _other _k: False{}# is a leaf of kind k the `=` or `<-` of a let, whose right side sees the# names outside the let?def plan.keep(mode: Mode, kk: Lex.TokKind) -> Bool: match mode kk: case MLhs{_outer, _kind} Lex.TEq{}: True{} case MLhs{_outer, _kind} Lex.TBind{}: True{} case MLhsType{_outer} Lex.TEq{}: True{} case MLhsType{_outer} Lex.TBind{}: True{} case _other _k: False{}# the environment outside a let's left sidedef plan.outer(mode: Mode) -> List<&2, Bind>: match mode: case MLhs{outer, _kind}: outer case MLhsType{outer}: outer case _other: []# a binder at the next token, with the note its kind showsdef plan.ahead(tok: Lex.Tok, kind: BindKind, +note: String) -> Bind: match tok: case Lex.Tok{_k, t, l, c}: Bind{t, l, c, kind, note}# the name of the next token, "" when there is nonedef plan.ahead_name(tok: Lex.Tok) -> String: match tok: case Lex.Tok{_k, t, _l, _c}: t# the binder a leaf records: its own name, or for `op name`, `@x:` and `&x:`# the name after it. A telescope's binder notes its declarationdef plan.binder(mode: Mode, kk: Lex.TokKind, +tt: String, ll: U32, cc: U32, +rest: Tree.Node) -> Bind: match mode kk: case MCtor{} _k: Bind{tt, ll, cc, KCtor{}, ""} case MName{} _k: Bind{tt, ll, cc, KItem{}, ""} case MTele{kind} Lex.TOp{}: plan.ahead(plan.peek(rest), kind, tt ++ plan.ahead_name(plan.peek(rest)) ++ render(plan.tail(rest))) case MTele{kind} _k: Bind{tt, ll, cc, kind, "" ++ tt ++ render(rest)} case MTeleType{_kind} _k: plan.ahead(plan.peek(rest), KTypeVar{}, "") case MLhs{_outer, kind} _k: Bind{tt, ll, cc, kind, ""} case MTerm{} Lex.TName{}: Bind{tt, ll, cc, KLocal{}, ""} case MTerm{} _k: plan.ahead(plan.peek(rest), KTypeVar{}, "") case _other _k: Bind{tt, ll, cc, KLocal{}, ""}# a binder onto the environment, when there is onedef plan.pushed(push: Bool, +bb: Bind, env: List<&2, Bind>) -> List<&2, Bind>: match push: case True{}: bb <> env case False{}: env# a binder onto the output, when there is onedef plan.recorded(rec: Bool, +bb: Bind, out: Out) -> Out: match rec: case True{}: Out{binds, uses, scopes} = out Out{bb <> binds, uses, scopes} case False{}: out# a use onto the output, when there is onedef plan.used(usd: Bool, +name: String, line: U32, col: U32, env: List<&2, Bind>, ns: Names, out: Out) -> Out: match usd: case True{}: out_of(use(name, line, col, env, ns, out)) case False{}: out# the environment the rest is read with after a leaf: the one outside a# let's left side at its `=`, else this one with the leaf's binder on itdef plan.enter( keep: Bool, outer: List<&2, Bind>, push: Bool, +bb: Bind, env: List<&2, Bind>) -> List<&2, Bind>: match keep: case True{}: outer case False{}: plan.pushed(push, bb, env)# the mode a group's insides are read in; MStop when they mean nothing heredef plan.ginner(mode: Mode, +gt: String) -> Mode: match mode: case MSig{}: MTele{tele_kind(gt)} case MTeleType{_kind}: MTerm{} case MLhs{outer, _kind}: MLhs{outer, KPat{}} case MLhsType{_outer}: MTerm{} case MTerm{}: MTerm{} case _other: MStop{}# the mode the rest is read in after a groupdef plan.gnext(mode: Mode) -> Mode: match mode: case MSig{}: MTerm{} case MLhs{outer, _kind}: MLhs{outer, KPat{}} case other: plan.skip(other)# do the names a group binds stay bound after it? A signature's parameters# and a pattern's binders dodef plan.gkeeps(mode: Mode) -> Bool: match mode: case MSig{}: True{} case MLhs{_outer, _kind}: True{} case _other: False{}# the mode a statement's header is read indef plan.kmode(mode: Mode, sk: Tree.StmtKind, +env: List<&2, Bind>) -> Mode: match mode sk: case MBlock{} Tree.SDef{}: MHead{} case MBlock{} Tree.SLaw{}: MHead{} case MBlock{} Tree.SType{}: MHead{} case MBlock{} Tree.SImport{}: MStop{} case MBlock{} Tree.SCase{}: MLhs{env, KPat{}} case MBlock{} Tree.SFor{}: MLhs{env, KFor{}} case MBlock{} Tree.SLet{}: MLhs{env, KLocal{}} case MBlock{} Tree.STerm{}: MTerm{} case MCtors{} _sk: MCtor{} case _other _sk: MStop{}# the mode a statement's body is read indef plan.bmode(mode: Mode, sk: Tree.StmtKind) -> Mode: match mode sk: case MBlock{} Tree.SType{}: MCtors{} case MBlock{} Tree.SImport{}: MStop{} case MBlock{} _sk: MBlock{} case _other _sk: MStop{}# is the scope recorded before a statement's header?def plan.mark_head(mode: Mode, sk: Tree.StmtKind) -> Bool: match mode sk: case MBlock{} Tree.SCase{}: True{} case MBlock{} Tree.SFor{}: True{} case MBlock{} Tree.SLet{}: True{} case MBlock{} Tree.STerm{}: True{} case MCtors{} _sk: True{} case _other _sk: False{}# is the scope recorded between a statement's header and its body? A def's isdef plan.mark_body(mode: Mode, sk: Tree.StmtKind) -> Bool: match mode sk: case MBlock{} Tree.SDef{}: True{} case _other _sk: False{}# the scope recorded onto the output, when it isdef plan.marked(yes: Bool, line: U32, +env: List<&2, Bind>, out: Out) -> Out: match yes: case True{}: mark(line, env, out) case False{}: out# does a statement close its scope for the statements after it? All but a# let and a `for` in a block dodef plan.scoped(mode: Mode, sk: Tree.StmtKind) -> Bool: match mode sk: case MBlock{} Tree.SFor{}: False{} case MBlock{} Tree.SLet{}: False{} case _other _sk: True{}# the mode the statements after a statement are read indef plan.snext(mode: Mode) -> Mode: match mode: case MBlock{}: MBlock{} case MCtors{}: MCtors{} case other: plan.skip(other)# the walk: one node in one mode, against an environment. It takes the node# apart as far as its head, and the plan above says what the head does in# this mode. Every recursive call is on a subtree (kids, body, gkids or# rest), never on n itselfdef walk(nn: Tree.Node, +mode: Mode, +env: List<&2, Bind>, +ns: Names, out: Out) -> W: match nn: case Tree.NCons{hd, +rest}: match hd: case Tree.Leaf{Lex.Tok{+k, +t, +l, +c}}: +keep = plan.keep(mode, k) +bb = plan.binder(mode, k, t, l, c, rest) +o1 = plan.recorded(plan.rec(mode, k, rest), bb, out) +o2 = plan.used(plan.use(mode, k, rest), t, l, c, env, ns, o1) +e2 = plan.enter(keep, plan.outer(mode), plan.push(mode, k, rest), bb, env) +r = walk(rest, plan.lmode(mode, k, rest), e2, ns, o2) W{Bool.pick(List<&2, Bind>, keep, env, env_of(r)), out_of(r)} case Tree.Group{Lex.Tok{_gk, gt, _gl, _gc}, gkids, _close}: +g = walk(gkids, plan.ginner(mode, gt), env, ns, out) walk(rest, plan.gnext(mode), Bool.pick(List<&2, Bind>, plan.gkeeps(mode), env_of(g), env), ns, out_of(g)) case Tree.Stmt{+sk, +kids, body}: +h = walk(kids, plan.kmode(mode, sk, env), env, ns, plan.marked(plan.mark_head(mode, sk), Tree.line(kids), env, out)) +b = walk(body, plan.bmode(mode, sk), env_of(h), ns, plan.marked(plan.mark_body(mode, sk), Tree.line(kids), env_of(h), out_of(h))) walk(rest, plan.snext(mode), Bool.pick(List<&2, Bind>, plan.scoped(mode, sk), env, env_of(h)), ns, out_of(b)) case _other: walk(rest, plan.skip(mode), env, ns, out) case _other: W{env, out}# notes# -----# leading spaces droppeddef lstrip(cs: List<&2, Char>) -> List<&2, Char>: match cs: case Con{' ', t}: lstrip(t) case other: other# a line's text without its indentationdef stripped(+text: String) -> String: String.from_list(lstrip(String.to_list(text)))# a declaration carries its own note; anything else shows the line that# bound it, which `text` gives only when it is asked fordef note_for(kind: BindKind, +note: String, text: Unit -> String) -> String: match kind: case KParam{}: note case KField{}: note case KTypeParam{}: note case other: text(Unit{})# the lines from line `line` on, given the lines from line `at` on: a step# forward from where the last binder was, not a walk from the first linedef annotate.ahead(+line: U32, +at: U32, cur: List<&2, String>) -> List<&2, String>: List.drop(&2, String, cur, U32.to_nat(U32.sub(line, at)))# the first line of these, or ""def annotate.head(+cur: List<&2, String>) -> String: Maybe.default(&2, String, List.head(&2, String, cur), "")# a line read from the first, for a binder behind the last onedef annotate.back(lines: List<&2, String>, +line: U32) -> String: Maybe.default(&2, String, List.get(&2, String, lines, U32.to_nat(line)), "")# every binder with its note filled. Binders come in source order, so the# lines are read once, front to back, from where the last binder was (`cur`# holds the lines from line `at` on); a binder behind that point reads its# line from the startdef annotate.go(binds: List<&2, Bind>, +lines: List<&2, String>, +at: U32, +cur: List<&2, String>) -> List<&2, Bind>: match binds: case Nil{}: Nil{} case Con{Bind{name, +line, col, +kind, note}, rest}: +ahead = U32.is_ge(line, at) +here = Lazy.either(List<&2, String>, ahead, _u => annotate.ahead(line, at, cur), _v => cur) +text = Lazy.either(String, ahead, _u => annotate.head(here), _v => annotate.back(lines, line)) Bind{name, line, col, kind, note_for(kind, note, _w => stripped(text))} <> annotate.go(rest, lines, Bool.pick(U32, ahead, line, at), here)# every binder with its note filleddef annotate(binds: List<&2, Bind>, +lines: List<&2, String>) -> List<&2, Bind>: annotate.go(binds, lines, 0, lines)# putting it together# -------------------# the gathered output, in source order and annotateddef finish(oo: Out, lines: List<&2, String>) -> Bound: Out{binds, uses, scopes} = oo Bound{annotate(List.reverse(&2, Bind, binds), lines), List.reverse(&2, Use, uses), List.reverse(&2, Scope, scopes)}# the binding structure of a parsed sourcedef of_tree(+root: Tree.Node, lines: List<&2, String>) -> Bound: finish(out_of(walk(root, MBlock{}, [], Names{items(root, []), aliases(root, [])}, Out{[], [], []})), lines)# the binding structure of a sourcedef bound(+source: String) -> Bound: of_tree(Tree.parse(source), String.lines(source))# queries# -------# where a name is: a binder, or a use of onetype Site is Data: SBind{bind: Bind} SUse{use: Use}# does the name at (l, c) cover the position (line, col)?def covers(+l2: U32, +c2: U32, +name: String, +line: U32, +col: U32) -> Bool: +end = (c2 + U32.from_nat(String.length(name)) : U32) Bool.and(U32.is_eq(l2, line), Bool.and(U32.is_le(c2, col), U32.is_lt(col, end)))# the binder whose name covers a positiondef bind_at(binds: List<&2, Bind>, +line: U32, +col: U32) -> Maybe<&2, Site>: match binds: case Nil{}: None{} case Con{Bind{+name, +l, +c, kind, note}, rest}: +more = bind_at(rest, line, col) Bool.pick(Maybe<&2, Site>, covers(l, c, name, line, col), Some{SBind{Bind{name, l, c, kind, note}}}, more)# the use whose name covers a positiondef use_at(uses: List<&2, Use>, +line: U32, +col: U32) -> Maybe<&2, Site>: match uses: case Nil{}: None{} case Con{Use{+name, +l, +c, tg}, rest}: +more = use_at(rest, line, col) Bool.pick(Maybe<&2, Site>, covers(l, c, name, line, col), Some{SUse{Use{name, l, c, tg}}}, more)def at.or(mm: Maybe<&2, Site>, uses: List<&2, Use>, line: U32, col: U32) -> Maybe<&2, Site>: match mm: case Some{site}: Some{site} case None{}: use_at(uses, line, col)# the site at a positiondef at(bb: Bound, +line: U32, +col: U32) -> Maybe<&2, Site>: Bound{binds, uses, scopes} = bb at.or(bind_at(binds, line, col), uses, line, col)# the binder at a position (a use's target, or the binder itself)def binder(binds: List<&2, Bind>, +line: U32, +col: U32) -> Maybe<&2, Bind>: match binds: case Nil{}: None{} case Con{Bind{name, +l, +c, kind, note}, rest}: +more = binder(rest, line, col) +here = Bool.and(U32.is_eq(l, line), U32.is_eq(c, col)) Bool.pick(Maybe<&2, Bind>, here, Some{Bind{name, l, c, kind, note}}, more)# the names in scope at a line: those of the statement on it, else of the# nearest statement abovedef visible.go(scopes: List<&2, Scope>, +qline: U32, best: List<&2, Bind>) -> List<&2, Bind>: match scopes: case Nil{}: best case Con{Scope{+line, env}, rest}: +hit = U32.is_le(line, qline) visible.go(rest, qline, Bool.pick(List<&2, Bind>, hit, env, best))# the scopes hold binders before their notes were filled: read each backdef noted(mm: Maybe<&2, Bind>, bb: Bind) -> Bind: match mm: case None{}: bb case Some{full}: full# each binder of an environment, with the note its annotated twin carriesdef refresh(env: List<&2, Bind>, +binds: List<&2, Bind>) -> List<&2, Bind>: match env: case Nil{}: Nil{} case Con{Bind{name, +l, +c, kind, note}, rest}: noted(binder(binds, l, c), Bind{name, l, c, kind, note}) <> refresh(rest, binds)# the names in scope at a line: those of the statement on it, else of the# nearest statement abovedef visible(bb: Bound, qline: U32) -> List<&2, Bind>: Bound{binds, uses, scopes} = bb refresh(visible.go(scopes, qline, []), binds)# every position a binder is named at: its own, then its uses'def sites.go(uses: List<&2, Use>, +line: U32, +col: U32) -> List<&2, Pos>: match uses: case Nil{}: Nil{} case Con{Use{name, l, c, TLocal{+tl, +tc}}, rest}: +more = sites.go(rest, line, col) Bool.pick(List<&2, Pos>, Bool.and(U32.is_eq(tl, line), U32.is_eq(tc, col)), Pos{l, c} <> more, more) case Con{other, rest}: sites.go(rest, line, col)# every position a binder is named at: its own, then its uses'def sites(bb: Bound, +line: U32, +col: U32) -> List<&2, Pos>: Bound{binds, uses, scopes} = bb Pos{line, col} <> sites.go(uses, line, col)# every position an item of the file is named at: its declaration, then its# usesdef item_sites.binds(binds: List<&2, Bind>, +name: String) -> List<&2, Pos>: match binds: case Nil{}: Nil{} case Con{Bind{+n, l, c, KItem{}, note}, rest}: +more = item_sites.binds(rest, name) Bool.pick(List<&2, Pos>, String.eq(n, name), Pos{l, c} <> more, more) case Con{Bind{+n, l, c, KCtor{}, note}, rest}: +more = item_sites.binds(rest, name) Bool.pick(List<&2, Pos>, String.eq(n, name), Pos{l, c} <> more, more) case Con{other, rest}: item_sites.binds(rest, name)def item_sites.uses(uses: List<&2, Use>, +name: String) -> List<&2, Pos>: match uses: case Nil{}: Nil{} case Con{Use{n, l, c, TItem{+t}}, rest}: +more = item_sites.uses(rest, name) Bool.pick(List<&2, Pos>, String.eq(t, name), Pos{l, c} <> more, more) case Con{other, rest}: item_sites.uses(rest, name)# every position an item of the file is named at: its declaration, then its# usesdef item_sites(bb: Bound, +name: String) -> List<&2, Pos>: Bound{binds, uses, scopes} = bb List.append(&2, Pos, item_sites.binds(binds, name), item_sites.uses(uses, name))# every position a name not of this file is used at (Base, or through an# alias)def named_sites.go(uses: List<&2, Use>, +name: String) -> List<&2, Pos>: match uses: case Nil{}: Nil{} case Con{Use{+n, l, c, TLocal{tl, tc}}, rest}: named_sites.go(rest, name) case Con{Use{+n, l, c, tg}, rest}: +more = named_sites.go(rest, name) Bool.pick(List<&2, Pos>, String.eq(n, name), Pos{l, c} <> more, more)# every position a name not of this file is used at (Base, or through an# alias)def named_sites(bb: Bound, +name: String) -> List<&2, Pos>: Bound{binds, uses, scopes} = bb named_sites.go(uses, name)