src/syntax/bind.bend checks

raw source on the hub · import 0x013e0f9a479bbebad5ed196725eede95/src/syntax/bind.bend as Bind

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).

4 imports

import Base
import ./lex.bend as Lex
import ../lazy/lazy.bend as Lazy
import ./tree.bend as Tree

Types

type BindKind source · line 26 · raw

Data

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:

KItem
```
BindKind
```
KCtor
```
BindKind
```
KParam
```
BindKind
```
KTypeParam
```
BindKind
```
KField
```
BindKind
```
KLocal
```
BindKind
```
KPat
```
BindKind
```
KFor
```
BindKind
```
KTypeVar
```
BindKind
```

type Bind source · line 40 · raw

Data

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 it

Bind

@name:String -> @line:U32 -> @col:U32 -> @kind:BindKind -> @note:String -> Bind

type Target source · line 45 · raw

Data

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)

TLocal
```
@line:U32 -> @col:U32 -> Target
```
TItem
```
@name:String -> Target
```
TQual
```
@alias:String -> @name:String -> Target
```
TFree
```
Target
```

type Use source · line 52 · raw

Data

a name that is not a binder, with what it refers to

Use

@name:String -> @line:U32 -> @col:U32 -> @target:Target -> Use

type Scope source · line 56 · raw

Data

the names in scope at a statement's line

Scope

@line:U32 -> @env:List<&2, Bind> -> Scope

type Bound source · line 60 · raw

Data

everything the binder knows about a source, each list in source order

Bound

@binds:List<&2, Bind> -> @uses:List<&2, Use> -> @scopes:List<&2, Scope> -> Bound

type Pos source · line 64 · raw

Data

a line and a column

Pos
```
@line:U32 -> @col:U32 -> Pos
```

type Names source · line 241 · raw

Data

the names an environment holds, and the file's items and aliases

Names

@items:List<&2, String> -> @aliases:List<&2, String> -> Names

type Out source · line 264 · raw

Data

what the walk has gathered so far, each list reversed

Out

@binds:List<&2, Bind> -> @uses:List<&2, Use> -> @scopes:List<&2, Scope> -> Out

type Mode source · line 271 · raw

Data

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 more

MBlock
```
Mode
```
MCtors
```
Mode
```
MCtor
```
Mode
```
MHead
```
Mode
```
MName
```
Mode
```
MSig
```
Mode
```
MTele
```
@kind:BindKind -> Mode
```
MTeleType
```
@kind:BindKind -> Mode
```

MLhs

@outer:List<&2, Bind> -> @kind:BindKind -> Mode

MLhsType
```
@outer:List<&2, Bind> -> Mode
```
MTerm
```
Mode
```
MSkip
```
@next:Mode -> Mode
```
MStop
```
Mode
```

type W source · line 287 · raw

Data

the walk's result: the environment after, and the output

W
```
@env:List<&2, Bind> -> @out:Out -> W
```

type Site source · line 889 · raw

Data

where a name is: a binder, or a use of one

SBind
```
@bind:Bind -> Site
```
SUse
```
@use:Use -> Site
```

Definitions

def declared.is_name source · line 71 · raw

@kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> Bool

a name that can be declared: plain, capitalized or dotted

def declared.name source · line 83 · raw

@nn:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Maybe<&2, String>

a leaf's name, when its kind is one: the kind is tested, the text only kept

def declared.go source · line 91 · raw

@kids:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Maybe<&2, String>

the item a statement declares: the first name after its keyword

def declared.is_key source · line 99 · raw

@kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> Bool

a keyword?

def declared.key source · line 107 · raw

@nn:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bool

a keyword leaf? its kind is read, never its text

def declared source · line 115 · raw

@kids:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Maybe<&2, String>

the item a statement declares: the first name after its keyword

def push_name.again source · line 123 · raw

@acc:List<&2, String> -> @+name:String -> Bool

is the name at the head of the list?

def push_name source · line 133 · raw

@mm:Maybe<&2, String> -> @+acc:List<&2, String> -> List<&2, String>

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 list

def ctors source · line 141 · raw

@body:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @acc:List<&2, String> -> List<&2, String>

a type's constructors: the first name of each line under it

def items source · line 149 · raw

@root:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @acc:List<&2, String> -> List<&2, String>

the defs, laws, types and constructors of a source

def last_text source · line 163 · raw

@kids:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> String

the text of a chain's last leaf

def aliases source · line 173 · raw

@root:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @+acc:List<&2, String> -> List<&2, String>

the import aliases of a source: the last token of each import .. as X

def find source · line 187 · raw

@env:List<&2, Bind> -> @+name:String -> Maybe<&2, Bind>

the innermost binder of a name in an environment

def head_of.go source · line 195 · raw

@cs:List<&2, Char> -> List<&2, Char>

def head_of source · line 203 · raw

@cs:List<&2, Char> -> String

a dotted name's part before the first dot

def rest_of source · line 207 · raw

@cs:List<&2, Char> -> String

a dotted name's part after the first dot

def has source · line 215 · raw

@names:List<&2, String> -> @+name:String -> Bool

is the name among these?

def same source · line 220 · raw

@aa:String -> @bb:String -> Bool

two names alike, char by char, stopping at the first that differs: String.eq, without the pairs String.cmp builds on every step

def has_item source · line 233 · raw

@names:List<&2, String> -> @+name:String -> Bool

is the name among the file's items? has, stopping at the first hit, as every use no binder holds asks it of every item

def resolve.local source · line 244 · raw

@mm:Maybe<&2, Bind> -> @+name:String -> @ns:Names -> Target

def resolve source · line 257 · raw

@env:List<&2, Bind> -> @+name:String -> @ns:Names -> Target

what a name at a point refers to, given what is in scope

def spaced source · line 292 · raw

@+tt:String -> String

a declaration as written: +x: List<&2, U32>, ~f: U32 -> U32. A space follows : and ,, spaces surround ->, everything else is glued

def render_close source · line 297 · raw

@close:Maybe<&2, 0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.Tok> -> String

a group's close bracket, "" when it never closed

def render_all source · line 305 · raw

@nn:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> String

the text of a whole chain

def render source · line 315 · raw

@nn:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> String

the text of a chain up to its first comma

def use source · line 327 · raw

@+name:String -> @line:U32 -> @col:U32 -> @+env:List<&2, Bind> -> @ns:Names -> @out:Out -> W

a use of a name, resolved against the environment

def mark source · line 332 · raw

@line:U32 -> @+env:List<&2, Bind> -> @out:Out -> Out

the names in scope at a statement's line, recorded

def tele_kind source · line 338 · raw

@+oo:String -> BindKind

what the names of a telescope bind as, by its bracket: ( parameters, < type parameters, { fields

def env_of source · line 343 · raw

@ww:W -> List<&2, Bind>

a result's environment

def out_of source · line 348 · raw

@ww:W -> Out

a result's output

def plan.lam source · line 364 · raw

@rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bool

does the chain start with a leaf of this kind?

def plan.group source · line 372 · raw

@rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bool

does the chain start with a group?

def plan.named source · line 380 · raw

@rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bool

does the chain start with a name (lower or upper case)?

def plan.typed source · line 391 · raw

@rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @upper:Bool -> Bool

does the chain start with a name and a :? An upper-case name counts when upper says so

def plan.peek source · line 403 · raw

@rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> 0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.Tok

the chain's first token; a blank one when it does not start with a leaf

def plan.tail source · line 411 · raw

@rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> 0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node

the chain after its first node

def plan.skip source · line 419 · raw

@mode:Mode -> Mode

the mode the rest is read in after a head that means nothing in this mode

def plan.lmode source · line 449 · raw

@mode:Mode -> @kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> @+rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Mode

the mode the rest is read in after a leaf of kind k

def plan.rec source · line 483 · raw

@mode:Mode -> @kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> @+rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bool

does a leaf of kind k record a binder?

def plan.push source · line 516 · raw

@mode:Mode -> @kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> @rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bool

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 hold

def plan.use source · line 526 · raw

@mode:Mode -> @kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> @+rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bool

does a leaf of kind k use a name?

def plan.keep source · line 555 · raw

@mode:Mode -> @kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> Bool

is a leaf of kind k the = or <- of a let, whose right side sees the names outside the let?

def plan.outer source · line 569 · raw

@mode:Mode -> List<&2, Bind>

the environment outside a let's left side

def plan.ahead source · line 579 · raw

@tok:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.Tok -> @kind:BindKind -> @+note:String -> Bind

a binder at the next token, with the note its kind shows

def plan.ahead_name source · line 585 · raw

@tok:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.Tok -> String

the name of the next token, "" when there is none

def plan.binder source · line 592 · raw

@mode:Mode -> @kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> @+tt:String -> @ll:U32 -> @cc:U32 -> @+rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bind

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 declaration

def plan.pushed source · line 614 · raw

@push:Bool -> @+bb:Bind -> @env:List<&2, Bind> -> List<&2, Bind>

a binder onto the environment, when there is one

def plan.recorded source · line 622 · raw

@rec:Bool -> @+bb:Bind -> @out:Out -> Out

a binder onto the output, when there is one

def plan.used source · line 631 · raw

@usd:Bool -> @+name:String -> @line:U32 -> @col:U32 -> @env:List<&2, Bind> -> @ns:Names -> @out:Out -> Out

a use onto the output, when there is one

def plan.enter source · line 640 · raw

@keep:Bool -> @outer:List<&2, Bind> -> @push:Bool -> @+bb:Bind -> @env:List<&2, Bind> -> List<&2, Bind>

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 it

def plan.ginner source · line 654 · raw

@mode:Mode -> @+gt:String -> Mode

the mode a group's insides are read in; MStop when they mean nothing here

def plan.gnext source · line 670 · raw

@mode:Mode -> Mode

the mode the rest is read in after a group

def plan.gkeeps source · line 681 · raw

@mode:Mode -> Bool

do the names a group binds stay bound after it? A signature's parameters and a pattern's binders do

def plan.kmode source · line 691 · raw

@mode:Mode -> @sk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.StmtKind -> @+env:List<&2, Bind> -> Mode

the mode a statement's header is read in

def plan.bmode source · line 715 · raw

@mode:Mode -> @sk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.StmtKind -> Mode

the mode a statement's body is read in

def plan.mark_head source · line 727 · raw

@mode:Mode -> @sk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.StmtKind -> Bool

is the scope recorded before a statement's header?

def plan.mark_body source · line 743 · raw

@mode:Mode -> @sk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.StmtKind -> Bool

is the scope recorded between a statement's header and its body? A def's is

def plan.marked source · line 751 · raw

@yes:Bool -> @line:U32 -> @+env:List<&2, Bind> -> @out:Out -> Out

the scope recorded onto the output, when it is

def plan.scoped source · line 760 · raw

@mode:Mode -> @sk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.StmtKind -> Bool

does a statement close its scope for the statements after it? All but a let and a for in a block do

def plan.snext source · line 770 · raw

@mode:Mode -> Mode

the mode the statements after a statement are read in

def walk source · line 783 · raw

@nn:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @+mode:Mode -> @+env:List<&2, Bind> -> @+ns:Names -> @out:Out -> W

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 itself

def lstrip source · line 813 · raw

@cs:List<&2, Char> -> List<&2, Char>

leading spaces dropped

def stripped source · line 821 · raw

@+text:String -> String

a line's text without its indentation

def note_for source · line 826 · raw

@kind:BindKind -> @+note:String -> @text:(@_:Unit -> String) -> String

a declaration carries its own note; anything else shows the line that bound it, which text gives only when it is asked for

def annotate.ahead source · line 839 · raw

@+line:U32 -> @+at:U32 -> @cur:List<&2, String> -> List<&2, String>

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 line

def annotate.head source · line 843 · raw

@+cur:List<&2, String> -> String

the first line of these, or ""

def annotate.back source · line 847 · raw

@lines:List<&2, String> -> @+line:U32 -> String

a line read from the first, for a binder behind the last one

def annotate.go source · line 854 · raw

@binds:List<&2, Bind> -> @+lines:List<&2, String> -> @+at:U32 -> @+cur:List<&2, String> -> List<&2, Bind>

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 start

def annotate source · line 866 · raw

@binds:List<&2, Bind> -> @+lines:List<&2, String> -> List<&2, Bind>

every binder with its note filled

def finish source · line 873 · raw

@oo:Out -> @lines:List<&2, String> -> Bound

the gathered output, in source order and annotated

def of_tree source · line 878 · raw

@+root:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @lines:List<&2, String> -> Bound

the binding structure of a parsed source

def bound source · line 882 · raw

@+source:String -> Bound

the binding structure of a source

def covers source · line 894 · raw

@+l2:U32 -> @+c2:U32 -> @+name:String -> @+line:U32 -> @+col:U32 -> Bool

does the name at (l, c) cover the position (line, col)?

def bind_at source · line 899 · raw

@binds:List<&2, Bind> -> @+line:U32 -> @+col:U32 -> Maybe<&2, Site>

the binder whose name covers a position

def use_at source · line 908 · raw

@uses:List<&2, Use> -> @+line:U32 -> @+col:U32 -> Maybe<&2, Site>

the use whose name covers a position

def at.or source · line 916 · raw

@mm:Maybe<&2, Site> -> @uses:List<&2, Use> -> @line:U32 -> @col:U32 -> Maybe<&2, Site>

def at source · line 924 · raw

@bb:Bound -> @+line:U32 -> @+col:U32 -> Maybe<&2, Site>

the site at a position

def binder source · line 929 · raw

@binds:List<&2, Bind> -> @+line:U32 -> @+col:U32 -> Maybe<&2, Bind>

the binder at a position (a use's target, or the binder itself)

def visible.go source · line 940 · raw

@scopes:List<&2, Scope> -> @+qline:U32 -> @best:List<&2, Bind> -> List<&2, Bind>

the names in scope at a line: those of the statement on it, else of the nearest statement above

def noted source · line 949 · raw

@mm:Maybe<&2, Bind> -> @bb:Bind -> Bind

the scopes hold binders before their notes were filled: read each back

def refresh source · line 957 · raw

@env:List<&2, Bind> -> @+binds:List<&2, Bind> -> List<&2, Bind>

each binder of an environment, with the note its annotated twin carries

def visible source · line 966 · raw

@bb:Bound -> @qline:U32 -> List<&2, Bind>

the names in scope at a line: those of the statement on it, else of the nearest statement above

def sites.go source · line 971 · raw

@uses:List<&2, Use> -> @+line:U32 -> @+col:U32 -> List<&2, Pos>

every position a binder is named at: its own, then its uses'

def sites source · line 982 · raw

@bb:Bound -> @+line:U32 -> @+col:U32 -> List<&2, Pos>

every position a binder is named at: its own, then its uses'

def item_sites.binds source · line 988 · raw

@binds:List<&2, Bind> -> @+name:String -> List<&2, Pos>

every position an item of the file is named at: its declaration, then its uses

def item_sites.uses source · line 1001 · raw

@uses:List<&2, Use> -> @+name:String -> List<&2, Pos>

def item_sites source · line 1013 · raw

@bb:Bound -> @+name:String -> List<&2, Pos>

every position an item of the file is named at: its declaration, then its uses

def named_sites.go source · line 1019 · raw

@uses:List<&2, Use> -> @+name:String -> List<&2, Pos>

every position a name not of this file is used at (Base, or through an alias)

def named_sites source · line 1031 · raw

@bb:Bound -> @+name:String -> List<&2, Pos>

every position a name not of this file is used at (Base, or through an alias)