bolt

Search uses release 1.27.0.0 · 1,644 definitions

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 invalid
expected a fresh constructor name (duplicate declaration: Ready)

at src/lsp/frame.bend:295
10 files do not load
1.11.0.0 invalid
expected a fresh constructor name (duplicate declaration: Ready)

at src/lsp/frame.bend:295
10 files do not load

Definitions (1,644)

src/role.bend

type Marka file (normalized) and its role
def edgesthe import graph of the files
def pathsthe paths of the files
def rootsthe roots of the laws: every LAWS.bend and PROOF.bend
def lawfulthe roots of the law files: every LAWS.bend
def reachwhat the walk from some files reaches, through every file of the run
def codethe roots of the code: every package's main.bend, and every file the laws do not reach
def role.ofa file's role: its role by name, or else its role on the laws' side
def marks.ofthe marks of the files the laws reach and the code does not, in the run's order: a law file when a LAWS.bend reaches it
def marks.factsthe role of every file on the laws' side of a graph given as facts
def marksthe role of every file on the laws' side.
def of.norma normalized path's role among the marks: neither when it is not marked
def ofa file's role among the marks: a LAWS.bend or PROOF.bend by its name, any other file as marked, and neither when it is not marked

src/rules.bend

def on.paththe file a Src was read from
def on.atfindings put at a path: a per-file rule reports on its own file, so this keeps what each rule gave and makes it hold by construction
def on.rules.roleevery per-file rule on a file, told its role (src/role.bend): the rules a law or proof file changes (doc, hole, param, fromrev, prefix, empty, closed) read the role, never the path, and the cost rules check nothing in a law or proof file
def on.roleevery rule's findings on a file read once, told its role, each at that file
def haswhether a directory is among the directories
def ups.go
def upsa directory and each of its parents but ``, nearest first: `a/b/` is `a/b/` then `a/`
def owner.gothe first of the directories that is a root, or `` (the package `.`)
def ownerthe package of a file in a directory: the nearest root at or above it
def membersthe files of one package, in order
def covers`coverage` on each package but `.`
def projectevery project rule's findings on the files and the package roots but `.` (each a directory as Digest.dir names one): each file is read down to its digest once (rules/digest.bend); `coverage` runs on each package's files, `.` first
def groupthe group a rule is in; an unknown slug grades with correctness
def gradedthe findings at the levels a config gives their rules; the ones set off are dropped

src/rules/calls.bend

type Defa def: its name, its own tokens (the signature) and the statements under it
def defs.pusha def with a name joins the others; one without (half-written) does not
def defsthe defs of a parsed source, in order
def leaf.kinda leaf's kind, none for anything else: kind tests read this, never a text
def kind.ofa kind test on a kind, when there is one
def kind.leafa leaf of this kind?
def kind.colona `:`
def kind.uppera capitalized name
def kind.arrow`->`
def kind.opera plain operator (`-`, `~`, `+`)
def leaf.texta leaf's text, "" for anything else
def args.gothe arguments of a group, split at its top-level commas (each a chain)
def argsthe arguments of a group
def argthe nth argument, or nothing
def callsis there a call of the name, `name(..)`, anywhere under the node?
def params.of.gothe kids of a signature's first `(` group: the parameters; hit: a group before sig was one, so the search stops there
def params.ofthe kids of a signature's first `(` group: the parameters
def paramsa def's parameters, each its chain up to a comma (`+xs: List<&2, U32>`)
def param_namea parameter's name: its first lowercase name before the colon ("" for a type parameter like `-A: Type`)
def names.go
def namesthe names of a def's parameters
def has_colondoes a chain hold a top-level colon?
def is_live.signdoes the chain open with a `-` or `~` operator?
def is_livea live parameter: typed, and neither erased (`-A: Type`) nor a template (`~f: A -> B`); a bare quantity name (`a` in `List.get(a, ..)`) is not one
def type_head.gothe head of a parameter's type: the first capitalized name after the colon, "" for none; hit: a name before pp was it, so the search stops there
def type_headthe head of a parameter's type: the first capitalized name after the colon (`List` in `+xs: +List<A>`), "" for none
def walked.go
def walkedthe type head of the first live parameter: the one a self-call must shrink
def seqdoes the def walk a list or a string (its first live parameter's type)?
def returns_proof.ora `{` group after the arrow, or a proof further on
def returns_proofdoes the signature return a proof, `-> {a == b : T}`?
def has_arrowdoes a chain hold a top-level `->`?
def typeddoes the signature write a type: a `:` among its parameters, or a `->`?
def proofis the def a proof?
def exempta law file, a proof file, or a def that is a proof: none of it runs, so its cost does not matter

src/rules/correctness/arms.bend

type Armwhat an arm matches: from k up (text is its pattern), exactly k, or other
type Widethe widest n+p arm so far: its k and its pattern
def bindera lone binder, inside `Succ{..}` or after `kn+`: a name or `_`
def lit.shape`kn+p:` (p a name or `_`) or `kn:`
def lit.ofa Nat literal token's arm, once its value is read
def arma case pattern's arm
def widenthe widest n+p arm after this one
def verdict.ona finding when the arm is inside the widest one above
def verdictthe arm against the widest one above, if any
def armsa match's arms in order, against the widest n+p arm above each
def single`match x:`: one scrutinee
def walkevery statement, at any depth; a single-scrutinee match's arms are read
def checkthe rule

src/rules/correctness/escape.bend

type Syma literal's char as the rule reads it: a backslash, a `0`, another digit, or anything else.
def syma char as a Sym
def symsa literal's chars as Syms
def octalthe Sym's char when it is an octal digit
def run.ifkeep the octal digit, and those after it
def runthe octal digits (at most two) right after the `\0`, in order
def valuethe digits' octal value
def hexda hex digit
def hexa value under 256 in hex, without leading zeros
def findingthe finding for `\0` at a column, the digits after it in ds
def afterafter a `\0` at a column: a finding when a digit follows
def scana literal's Syms from a column; an escape is its backslash and one char
def check.go
def checkthe rule

src/rules/correctness/hole.bend

def check.todoTrue when the first token past spaces, newlines and comments is `TODO`
def check.widththe width of the hole a `?` at line, col starts: through the next token past spaces, newlines and comments when it sits on the same line, else 1
def check.go
def check.on
def check.rolethe rule, told the file's role (src/role.bend): a law file is skipped
def checkthe rule

src/rules/correctness/pick.bend

def bothdo both branches (the third and fourth arguments) call the def?
def oncedoes either branch call the def?
def muteis argument nth of a group quiet: the group's own quiet, or, in a branch (the third or fourth argument) of a reported pick, hushed
def nextthe argument a token leaves the walk in: one further past a top-level comma
def walkevery `Bool.pick(..)` in a chain, at any depth, that recurses in both branches or in one.