syntax/bind.bend checks

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

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 183 · 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 206 · 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 211 · 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

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
```

type W source · line 225 · raw

Data

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

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

type Site source · line 553 · raw

Data

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

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

Definitions

def declared.go source · line 71 · raw

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

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

def declared source · line 83 · raw

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

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

def push_name source · line 93 · raw

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

a name, when there is one, onto a list

def ctors source · line 101 · raw

@body:0x729eecea86ea5a2cdba3a2856a313bca/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 109 · raw

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

the defs, laws, types and constructors of a source

def last_text source · line 123 · raw

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

the text of a chain's last leaf

def aliases source · line 133 · raw

@root:0x729eecea86ea5a2cdba3a2856a313bca/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 147 · 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 155 · raw

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

def head_of source · line 165 · raw

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

a dotted name's part before the first dot

def rest_of source · line 169 · raw

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

a dotted name's part after the first dot

def has source · line 179 · raw

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

is the name among these?

def resolve.local source · line 186 · raw

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

def resolve source · line 199 · raw

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

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

def bind source · line 229 · raw

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

a new binder, into the environment and the output

def spaced source · line 236 · raw

@+t: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 241 · raw

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

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

def render_all source · line 249 · raw

@n:0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node -> String

the text of a whole chain

def render source · line 259 · raw

@n:0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node -> String

the text of a chain up to its first comma

def bind_decl source · line 272 · raw

@+name:String -> @+line:U32 -> @+col:U32 -> @kind:BindKind -> @+quantity:String -> @rest:0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node -> @env:List<&2, Bind> -> @out:Out -> W

a telescope binder, with its declaration as the note: the quantity before it, its name, and the rest up to the comma

def use source · line 279 · 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 284 · 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 290 · raw

@+o:String -> BindKind

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

def env_of source · line 295 · raw

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

a result's environment

def out_of source · line 300 · raw

@w:W -> Out

a result's output

def walk source · line 306 · raw

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

the walk: one node in one mode, against an environment. Every recursive call is on a subtree (kids, body, gkids or rest), never on n itself

def lstrip source · line 501 · raw

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

leading spaces dropped

def line_text source · line 509 · raw

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

the n-th line of a source, without its indentation

def note_for source · line 514 · raw

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

a declaration carries its own note; anything else shows the line that bound it

def annotate source · line 526 · raw

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

every binder with its note filled

def finish source · line 537 · raw

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

the gathered output, in source order and annotated

def of_tree source · line 542 · raw

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

the binding structure of a parsed source

def bound source · line 546 · raw

@+source:String -> Bound

the binding structure of a source

def covers source · line 558 · raw

@+l:U32 -> @+c:U32 -> @+name:String -> @+line:U32 -> @+col:U32 -> Bool

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

def bind_at source · line 563 · raw

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

the binder whose name covers a position

def use_at source · line 572 · raw

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

the use whose name covers a position

def at.or source · line 580 · raw

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

def at source · line 588 · raw

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

the site at a position

def binder source · line 593 · 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 604 · 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 613 · raw

@m:Maybe<&2, Bind> -> @b:Bind -> Bind

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

def refresh source · line 621 · 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 630 · raw

@b: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 635 · 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 646 · raw

@b: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 652 · 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 665 · raw

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

def item_sites source · line 677 · raw

@b: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 683 · 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 695 · raw

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

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

def kind_at source · line 700 · raw

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

the kind of the binder at a position, for what a use looks like

def kind_of_item source · line 709 · raw

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

the kind of an item or constructor of the file, by name