src/rules/digest.bend checks

raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.bend as Digest

src/rules/digest: one small reading of each file for the project rules. A project rule sees every file at once, and a + reuse of that list copies it: handed the parsed Src (src/src.bend), each extra use duplicated every file's text, tokens and tree, and the pair of project rules grew faster than the file count (100 files cost 362 s that way). So each file is read down once to what those rules ask of it -- its path, its top-level defs and types by name and line, what its laws name, what it imports, and its @unsafe and foreign defs -- and the phases run over these, which are strings and cheap to copy.

11 imports

import Base
import ../src.bend as Src
import ../syntax/lex.bend as Lex
import ../syntax/tree.bend as Tree
import ../syntax/bind.bend as Bind
import ../syntax/outline.bend as Outline
import ../lazy/lazy.bend as Lazy
import ./imports.bend as Imports
import ./laws/closed.bend as Closed
import ../paths.bend as Paths
import ./correctness/foreign.bend as Foreign

Types

type Mention source · line 25 · raw

Data

a law names an item of a module: its path and its name

Mention
```
@path:String -> @name:String -> Mention
```

type Top source · line 32 · raw

Data

a 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

Top

@kind:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/outline.ItemKind -> @name:String -> @line:U32 -> @ctors:List<&2, String> -> @calls:List<&2, Mention> -> Top

type Unsafe source · line 38 · raw

Data

a def a proof may not reach (bend 2.0.32): an @unsafe def, where its @ is, or a foreign def (its body only import "./x.c" / import "./x.js" lines), where its header starts; foreign says which

Unsafe

@name:String -> @line:U32 -> @col:U32 -> @foreign:Bool -> Unsafe

type Law source · line 43 · raw

Data

a 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

Law

@name:String -> @line:U32 -> @binds:Bool -> @doc:List<&2, String> -> Law

type Digest source · line 50 · raw

Data

one 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, its @unsafe and foreign defs

Digest

@path:String -> @norm:String -> @dir:String -> @is_laws:Bool -> @is_law_file:Bool -> @exempt:Bool -> @tops:List<&2, Top> -> @says:List<&2, Mention> -> @deps:List<&2, String> -> @unsafes:List<&2, Unsafe> -> @laws:List<&2, Law> -> Digest

type Alias source · line 59 · raw

Data

an import alias and the path it names

Alias
```
@name:String -> @path:String -> Alias
```

type Span source · line 83 · raw

Data

the lines a quantified law's statement spans: from its header's first token to its body's last

Span
```
@from:U32 -> @upto:U32 -> Span
```

Definitions

def aliases source · line 63 · raw

@items:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/outline.Item> -> @+from:String -> List<&2, Alias>

the aliases a file imports

def alias_path source · line 73 · raw

@as:List<&2, Alias> -> @+name:String -> Maybe<&2, String>

the path an alias names, when it is one

def spans source · line 88 · raw

@root:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> List<&2, Span>

the spans of every quantified law of a tree, in order. A closed law spans nothing (it covers one input, not the def)

def within source · line 100 · raw

@ss:List<&2, Span> -> @+ln:U32 -> Bool

is the line in one of the spans?

def aliased source · line 108 · raw

@mm:Maybe<&2, String> -> @+name:String -> @more:List<&2, Mention> -> List<&2, Mention>

an item behind an alias, when an import names the alias, onto the others

def target source · line 118 · raw

@tt:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Target -> @+as:List<&2, Alias> -> @+file:String -> @more:List<&2, Mention> -> List<&2, Mention>

what 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 mentions source · line 129 · raw

@us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use> -> @+ss:List<&2, Span> -> @+as:List<&2, Alias> -> @+file:String -> List<&2, Mention>

the mentions of every use the binder records in the statement of a quantified law, in order. Its header's own name is a binder, not a use

def uses.of source · line 138 · raw

@bb:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Bound -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use>

the uses the binder recorded

def ctors source · line 148 · raw

@items:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/outline.Item> -> List<&2, String>

the names of the constructors the items open with: a type's, since the outline lists them right after it

def before source · line 156 · raw

@us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use> -> @+at:U32 -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use>

the uses, in order, before the first one at or past the line

def after source · line 164 · raw

@us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use> -> @+at:U32 -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use>

the uses from the first one at or past the line on

def upto source · line 172 · raw

@us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use> -> @mm:Maybe<&2, U32> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use>

the uses before the line, when there is one; else all of them

def past source · line 180 · raw

@us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use> -> @mm:Maybe<&2, U32> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use>

the uses from the line on, when there is one; else none

def next_line source · line 189 · raw

@items:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/outline.Item> -> Maybe<&2, U32>

the line of the next item that ends an item's lines: any but a constructor, which the outline lists inside its type

def called source · line 199 · raw

@us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use> -> @+as:List<&2, Alias> -> @+file:String -> List<&2, Mention>

what the uses name, in order: an item of the file, or one behind an alias

def ranged source · line 210 · raw

@items:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/outline.Item> -> @+us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Use> -> @+as:List<&2, Alias> -> @+file:String -> List<&2, Top>

the top-level defs and types, by name and line: what the coverage rule grades. The uses are read in order, once: each item but a constructor takes those before the next such item's line, and a def or a type keeps what they name (a def's calls)

def is_exempt source · line 234 · raw

@+pp:String -> Bool

a law file or a test, by its path alone: not under law. Nothing the file's text mentions exempts it; IO is not an exemption, since an IO equality is a law.

def significant source · line 238 · raw

@toks:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.Tok> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.Tok>

the significant tokens: no space, newline or comment

def unsafe_name source · line 247 · raw

@toks:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.Tok> -> Maybe<&2, String>

the name after unsafe def, when the tokens run so

def push source · line 255 · raw

@mm:Maybe<&2, String> -> @+ll:U32 -> @+cc:U32 -> @more:List<&2, Unsafe> -> List<&2, Unsafe>

an @ that heads an unsafe def, onto the others

def unsafe_defs source · line 263 · raw

@toks:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.Tok> -> List<&2, Unsafe>

every @ unsafe def name run of tokens, on one line or two

def foreign.push source · line 272 · raw

@mm:Maybe<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/correctness/foreign.Lanes> -> @+name:String -> @+ll:U32 -> @+cc:U32 -> @more:List<&2, Unsafe> -> List<&2, Unsafe>

a foreign def, when its body is one (Foreign.lanes), onto the others

def foreign_defs source · line 286 · raw

@root:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> List<&2, Unsafe>

every top-level foreign def, where its header starts

def doc_at source · line 301 · raw

@items:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/outline.Item> -> @+at:U32 -> String

the doc of the item on a line; the items are in line order, so the search stops at it

def laws_of source · line 309 · raw

@root:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+items:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/outline.Item> -> List<&2, Law>

every law of a tree, with whether it binds and its doc lines

def laws.in source · line 321 · raw

@is_laws:Bool -> @root:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @items:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/outline.Item> -> List<&2, Law>

the laws of a LAWS.bend; no other file states any

def stated source · line 332 · raw

@is_laws:Bool -> @root:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @bound:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Bound -> @as:List<&2, Alias> -> @file:String -> List<&2, Mention>

what a file's laws name: only a LAWS.bend states laws that cover a def

def of source · line 340 · raw

@s2:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/src.Src -> Digest

one parsed file read down to its digest

def all source · line 350 · raw

@ss:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/src.Src> -> List<&2, Digest>

every file the linter read, in one pass, in order

def edges source · line 358 · raw

@ds:List<&2, Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge>

the import graph of the files, built once for every closure taken over it