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/rules/correctness/pick.bend

def picksevery reported pick in a chain walked at quiet, outside any pick's arguments
def check.go
def checkthe rule
def search.readsdoes a name leaf under the node spell xx?
def search.textthe node's tokens, each then a space (a group's open, not its close)
def search.cheapdoes a `Bool.pick(..)` under the node, at any depth, have the condition whose text is cond?
def search.emptyis the chain empty?
def search.loneis the chain the one name xx alone?
def search.citethe finding at the bound self-call; tail: the else branch is the bound name alone, so the call can carry the test instead
def search.judgethe statement that reads the bound name first: a finding when it is a `Bool.pick(..)` alone that reads the name only in its else branch, and the self-call (its arguments args) holds no pick on the same condition
def search.firstthe first statement of the chain that reads xx, the chain's end (NNil) when none does; hit: prev, the one before the chain, did
def search.callpast the bound name, `=` and the callee: a `(` group and nothing after it, and then the finding the first reader of the name gives
def search.calleepast the bound name and `=`: the leaf that names the call
def search.eqpast the bound name: the leaf that should be `=`
def search.bounda let's own tokens past any `+`: the leaf of the bound name
def search.leada let's own tokens, a leading `+` skipped
def search.stmta statement of the kind and own tokens, the chain after it rest: a let is read, anything else gives nothing
def search.walkevery search bound above its pick in a chain of statements and in the chains under them
def search.go
def searchthe rule's other half, run beside check: every search bound above its pick, def by def

src/rules/correctness/put.bend

def defines.namedis the first token `Map.put`?
def defines.keya keyword?
def calls.dotteda dotted name?
def definesdoes the file define Map.put: a `def` keyword right before a `Map.put`?
def calls.onea dotted name then an open bracket: a finding when they are `Map.put` and `(`, before what the rest reports
def callsevery `Map.put(` among the significant tokens
def check.on
def checkthe rule

src/rules/correctness/setting.bend

def foundeach setting as a finding at the bolt.bend's path and its def's line
def checkthe findings on a bolt.bend's text: one for each setting whose name is no rule or group, in file order

src/rules/correctness/twice.bend

def headthe literal a list pattern opens with: `x <> ..` or `Con{x, ..}`
def tailthe rest of a list pattern after its first element
def samea finding at the second literal when it repeats the first
def arma case statement's pattern, checked
def walkevery case statement under a recursive def, at any depth
def check.defa def's body, when it calls itself
def check.go
def checkthe rule

src/rules/digest.bend

type Mentiona law names an item of a module: its path and its name
type Topa top-level def or type, by kind, name and the line it starts on, with a type's constructors by name (none for a def), and what the uses on its lines name (its calls, for a def): each as the binder resolved it, an item of the file or one behind an import alias
type Lawa law of a LAWS.bend: its name, the line it starts on, whether it binds (a `for` or `exs` line), and the lines of its comment block, `# ` dropped
type Digestone file as the project rules see it: its path as given and normalized, its directory, whether it states laws (LAWS.bend) or proves them too (PROOF.bend), whether the coverage rule lets it off, its top-level items, what its own laws name, the files it imports, and its laws
type Aliasan import alias and the path it names
def aliasesthe aliases a file imports
def alias_path.gothe path an alias names, when it is one; hit: the alias before as was the name, so the search stops there
def alias_paththe path an alias names, when it is one: the first alias of the name
type Spanthe lines a quantified law's statement spans: from its header's first token to its body's last
def spansthe spans of every quantified law of a tree, in order.
def withinis the line in one of the spans?
def aliasedan item behind an alias, when an import names the alias, onto the others
def targetwhat the binder resolved a use to, as a mention onto the others: an item of the law's own file, or an item of the file an import alias names; nothing for a binder, a free name, or an alias no import names
def mentionsthe mentions of every use the binder records in the statement of a quantified law, in order.
def uses.ofthe uses the binder recorded
def ctorsthe names of the constructors the items open with: a type's, since the outline lists them right after it
def beforethe uses, in order, before the first one at or past the line
def afterthe uses from the first one at or past the line on
def uptothe uses before the line, when there is one; else all of them
def pastthe uses from the line on, when there is one; else none
def next_linethe line of the next item that ends an item's lines: any but a constructor, which the outline lists inside its type
def calledwhat the uses name, in order: an item of the file, or one behind an alias
def proofsthe names of the top-level defs that are proofs (Calls.proof: one that returns a proof, or one written with no type, which is how Bend fills the law named f).
def rangedthe top-level defs and types, by name and line, less the defs that are proofs (ps): what the coverage rule grades.
def is_exempta law file or a test, by its path alone: not under law.
def doc_atthe doc of the item on a line; the items are in line order, so the search stops at it
def from_line.stopdoes the first item sit on or after a line (from_line stops there)?
def from_linethe items from the first on or after a line; the items are in line order, and so are a tree's laws, so an item this drops lies above every later law too.
def laws_ofevery law of a tree, with whether it binds and its doc lines.
def laws.inthe laws of a LAWS.bend; no other file states any
def statedwhat a file's laws name: only a LAWS.bend states laws that cover a def
def ofone parsed file read down to its digest
def of.roleone parsed file read down to its digest, told its role (src/role.bend): a law file states the laws that cover defs, and a law or proof file is exempt
def of.markedone parsed file's digest, told its role among the marks (src/role.bend)
def all.roleevery file the linter read, each with its role among the marks, in one pass, in order
def edgesthe import graph of the files, built once for every closure taken over it

src/rules/imports.bend

def norm.puta segment onto the reversed path: `.` and empty are dropped, `..` pops
def norm.go
def norma path without `./`, `../` and doubled slashes, so two spellings compare
def initthe segments but the last
def dir_ofa path's directory, with its slash (`src/lsp/`; `` at the root)
def resolvea path imported from a file, normalized
type Edgea file (normalized) and the files it imports relatively (normalized)
def targetsthe relative imports among a file's items, resolved against it
def hasis the path among them?
def deps.specwhat the file at p imports (nothing when it was not read): the spec deps.first is proven against (src/rules/PROOF.bend imp.deps)
def fresh.specthe files of ds that were read and are not yet seen, each once: the spec fresh.fast is proven against (imp.fresh)
def pathsthe paths of the files
def walk.speca worklist walk; each read file enters todo once, and a start that was not read imports nothing, so fuel as many as the files never runs out (src/rules/LAWS.bend unsafe_shut).
def seek`has`, stopping at the first hit
def deps.first`deps.spec`, stopping at the first file of that path
def fresh.fast`fresh.spec`, asking the short lists first and each only while the answer is open: a target already found or seen is never looked for among every file
def walkthe walk: `walk.spec`, step for step, through the lookups above
def closure.gothe closure of the file at from, a path normalized already, over the graph

src/rules/laws/closed.bend

def bindsdoes a law's body bind anything (a `for` or `exs` line)?
def name.ofa law's name, `?` when it has none
def check.go
def checkthe rule
def check.rolethe rule, told the file's role (src/role.bend): only a law file is checked

src/rules/laws/law.bend

def named.puta file's uses onto the others', when the file is a LAWS.bend
def namedwhat the laws of every LAWS.bend name (Digest.of records uses for no other file; a digest list handed in from elsewhere is read the same way)
def keyan item's key: its name, a space, its file's path.