src/rules/digest.bend checks

raw source on the hub · import 0x013e0f9a479bbebad5ed196725eede95/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 defs -- and the phases run over these, which are strings and cheap to copy.

10 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

Types

type Mention source · line 24 · 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 31 · 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:0x013e0f9a479bbebad5ed196725eede95/src/syntax/outline.ItemKind -> @name:String -> @line:U32 -> @ctors:List<&2, String> -> @calls:List<&2, Mention> -> Top

type Unsafe source · line 35 · raw

Data

an @unsafe def and where its @ is

Unsafe

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

type Law source · line 40 · 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 47 · 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, and its @unsafe 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 56 · raw

Data

an import alias and the path it names

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

type Span source · line 80 · 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 60 · raw

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

the aliases a file imports

def alias_path source · line 70 · raw

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

the path an alias names, when it is one

def spans source · line 85 · raw

@root:0x013e0f9a479bbebad5ed196725eede95/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 97 · raw

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

is the line in one of the spans?

def aliased source · line 105 · 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 115 · raw

@tt:0x013e0f9a479bbebad5ed196725eede95/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 126 · raw

@us:List<&2, 0x013e0f9a479bbebad5ed196725eede95/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 135 · raw

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

the uses the binder recorded

def ctors source · line 145 · raw

@items:List<&2, 0x013e0f9a479bbebad5ed196725eede95/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 153 · raw

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

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

def after source · line 161 · raw

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

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

def upto source · line 169 · raw

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

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

def past source · line 177 · raw

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

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

def next_line source · line 186 · raw

@items:List<&2, 0x013e0f9a479bbebad5ed196725eede95/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 196 · raw

@us:List<&2, 0x013e0f9a479bbebad5ed196725eede95/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 207 · raw

@items:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/syntax/outline.Item> -> @+us:List<&2, 0x013e0f9a479bbebad5ed196725eede95/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 231 · 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 235 · raw

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

the significant tokens: no space, newline or comment

def unsafe_name source · line 244 · raw

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

the name after unsafe def, when the tokens run so

def push source · line 252 · 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 260 · raw

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

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

def doc_at source · line 273 · raw

@items:List<&2, 0x013e0f9a479bbebad5ed196725eede95/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 281 · raw

@root:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @+items:List<&2, 0x013e0f9a479bbebad5ed196725eede95/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 293 · raw

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

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

def stated source · line 304 · raw

@is_laws:Bool -> @root:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @bound:0x013e0f9a479bbebad5ed196725eede95/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 312 · raw

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

one parsed file read down to its digest

def all source · line 321 · raw

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

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

def edges source · line 329 · raw

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

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