bolt

Releases (13)

• 1.27.0.0 indexed
• 1.26.0.0 unindexed
• 1.25.0.0 unindexed
• 1.24.0.0 unindexed
• 1.23.0.0 unindexed
• 1.22.0.0 unindexed
• 1.21.0.0 unindexed
• 1.20.0.0 unindexed
• 1.19.0.0 unindexed
• 1.18.0.0 unindexed
• 1.17.0.0 unindexed
• 1.12.0.0 unindexed
• 1.11.0.0 unindexed

Definitions (1,644)

src/rules/table.bend

• def builta list literal, a sized array, or a constant-size constructor
• def call_namethe chain is exactly this call's name, with no arguments that matter: `name()`
• def lone_namethe chain is exactly one lowercase name
• def keyone use of a name, told apart from its other uses by where it stands
• def lone_keythe chain is exactly one lowercase name: that use's key
• def ownsthe list argument is a fixed table: inline, a use of a let that holds one, or `name()` / `name` for a table def of the file
• def bind_badone plain name before `=`, when the pattern is not a destructure
• def bind_atone plain name before `=`, when there is one
• def bind_namethe one plain name a statement binds, or empty
• def bind_rhsthe right-hand side: the chain after a statement's top-level `=`
• def dropthe names in scope without this one
• def rebindafter a let of `nm`: it holds a table only when this binding is one
• def use_ata name use joins the keys when the let in scope for it holds a table
• def letsthe keys of every name use under the node whose binding in scope is a table: a let reaches the statements after it and their bodies, not an enclosing block or a sibling arm, and a later let of the name replaces it
• def mod_onea def whose body is one fixed table
• def modulesdefs of this file whose body is one fixed table
• def scopefixed tables visible in this def: the file's table defs by name, and each use of a let whose binding in scope is a table, by its key
• def citethe finding for a get or a set
• def hita get or a set of a fixed table at a computed index

src/rules/tokens.bend

• def sigthe tokens without space, newlines and comments
• def code.cuta text cut to its first char
• def code.toka string literal cut to its opening quote; any other token as it is
• def code.toksthe tokens, each string literal cut to its opening quote
• def codea text with each string literal cut to its opening quote: what of it is code, as the lexer reads it
• def is_lita number, a char or a string literal?
• def nat_okdigits, then one final `n`: a Nat literal's chars
• def digits_okdigits alone, one or more: a U32 literal's chars
• def stemthe text without its last char (a Nat literal's digits)
• def nat_valuea Nat literal's value (`12n` is 12); none for anything else or past U32
• def widtha text's width in chars
• def keywordis the first node the keyword?
• def patterna case statement's pattern (its tokens after `case`, the colon and an inline body included)

src/src.bend

• type Srcthe path, the text, and the three readings of it every rule shares
• def ofread a file's text once

src/status.bend

• def stopexit 1 when the run found errors, else fall through (exit 0)

src/stop.bend

• def saya text on its stream
• def leave.at
• def leaveexit with a code: 0 falls through, any other ends the run with it

src/syntax/bind.bend

• type BindKindwhat 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 BindKLocal is a name a let, a do-bind or a lambda binds; KPat one bound by a pattern (a case, or a destructuring let).
• type Targetwhat 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 Usea name that is not a binder, with what it refers to
• type Scopethe names in scope at a statement's line
• type Boundeverything the binder knows about a source, each list in source order
• type Posa line and a column
• def declared.is_namea name that can be declared: plain, capitalized or dotted
• def declared.namea leaf's name, when its kind is one: the kind is tested, the text only kept
• def declared.gothe item a statement declares: the first name after its keyword
• def declared.is_keya keyword?
• def declared.keya keyword leaf?
• def declaredthe item a statement declares: the first name after its keyword
• def push_name.againis the name at the head of the list?
• def push_namea 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 ctorsa type's constructors: the first name of each line under it
• def itemsthe defs, laws, types and constructors of a source
• def last_textthe text of a chain's last leaf
• def aliasesthe import aliases of a source: the last token of each `import ..
• def find.gothe innermost binder of a name in an environment; hit: the binder before env was the name, so the search stops there
• def findthe innermost binder of a name in an environment
• def head_of.go
• def head_ofa dotted name's part before the first dot
• def rest_ofa dotted name's part after the first dot
• def hasis the name among these?
• def sametwo names alike, char by char, stopping at the first that differs: String.eq, without the pairs String.cmp builds on every step
• def has_itemis the name among the file's items?
• type Namesthe names an environment holds, and the file's items and aliases
• def resolve.local
• def resolvewhat a name at a point refers to, given what is in scope
• type Outwhat the walk has gathered so far, each list reversed
• type Modewhat 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.
• type Wthe walk's result: the environment after, and the output
• def spaceda declaration as written: `+x: List<&2, U32>`, `~f: U32 -> U32`.
• def render_closea group's close bracket, "" when it never closed
• def render_allthe text of a whole chain
• def renderthe text of a chain up to its first comma
• def usea use of a name, resolved against the environment
• def markthe names in scope at a statement's line, recorded
• def tele_kindwhat the names of a telescope bind as, by its bracket: `(` parameters, `<` type parameters, `{` fields
• def env_ofa result's environment
• def out_ofa result's output
• def plan.lamdoes the chain start with a leaf of this kind?
• def plan.groupdoes the chain start with a group?
• def plan.nameddoes the chain start with a name (lower or upper case)?
• def plan.typeddoes the chain start with a name and a `:`?
• def plan.peekthe chain's first token; a blank one when it does not start with a leaf
• def plan.tailthe chain after its first node
• def plan.skipthe mode the rest is read in after a head that means nothing in this mode
• def plan.lmodethe mode the rest is read in after a leaf of kind k
• def plan.recdoes a leaf of kind k record a binder?
• def plan.pushdoes the binder a leaf records go into the environment too?
• def plan.usedoes a leaf of kind k use a name?
• def plan.keepis a leaf of kind k the `=` or `<-` of a let, whose right side sees the names outside the let?
• def plan.outerthe environment outside a let's left side
• def plan.aheada binder at the next token, with the note its kind shows
• def plan.ahead_namethe name of the next token, "" when there is none
• def plan.binderthe binder a leaf records: its own name, or for `op name`, `@x:` and `&x:` the name after it.
• def plan.pusheda binder onto the environment, when there is one
• def plan.recordeda binder onto the output, when there is one
• def plan.useda use onto the output, when there is one
• def plan.enterthe 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