src/rules/laws/law.bend checks
raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/laws/law.bend as Law
rule coverage (project-wide; its module is law.bend, since law is a Bend
keyword and no bolt.bend could name it): in a project that states laws (a
LAWS.bend among the files the linter read), every def and type of every
file is reached from a quantified law in a LAWS.bend. A def is reached when
such a law names it (its binders or its statement use it, through an import
alias or in the law's own file), or when a reached def calls it: a use on
the def's lines, in its file or behind a relative import, across the files
of the run. A def no law reaches has no stated property, not even through
its callers: it is the coverage gap. A closed law, a law's own name, and a
law outside a LAWS.bend name nothing. A type is reached when such a law or
a reached def names it or one of its constructors (M.Sq{..} reaches a
type Shape with Sq{..}); a use of another def of its module does not
reach it, and a type reaches nothing. Out of scope: helper defs (dotted
names; a dotted type is graded, and a helper still carries the reach to
what it calls), tests, and the law files themselves -- decided by the name
and the file's path, never by what the file's text mentions. IO is no
exemption: a law can quantify over an IO value or state an IO equality, so
a def returning IO(..) is graded like any other, and so is every pure def
beside it. main is a def: a law that names it covers it. The rule reads
each file's digest (src/rules/digest.bend), never the parsed source: its
phases use the list three times, and a + reuse copies it. The reach is
one walk over one graph, the walk the unsafe rule takes over imports
(src/rules/imports.bend): its nodes are the defs, types and constructors
of the run by key (name, a space, path), and one more node, the empty key,
that leads to what the laws name.
6 imports
import Base import ../../lazy/lazy.bend as Lazy import ../../finding.bend as F import ../../syntax/outline.bend as Outline import ../digest.bend as Digest import ../imports.bend as Imports
Definitions
def named.put source · line 37 · raw
@laws:Bool -> @ms:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Mention> -> @more:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Mention> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Mention>
a file's uses onto the others', when the file is a LAWS.bend
def named source · line 46 · raw
@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Mention>
what 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 key source · line 58 · raw
@+pp:String -> @name:String -> String
an item's key: its name, a space, its file's path. A name has no space, so no two items share one, and no item has the empty key
def keys source · line 62 · raw
@ms:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Mention> -> List<&2, String>
the keys of what the mentions name
def ctor_nodes source · line 70 · raw
@cs:List<&2, String> -> @+pp:String -> @more:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge>
a type's constructors, each a node that leads nowhere, onto the others
def nodes source · line 79 · raw
@ts:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Top> -> @+pp:String -> @more:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge>
the items of a file as nodes onto the others: a def leads to what it calls, a type and its constructors to nothing
def graph.items source · line 91 · raw
@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge>
the items of every file as nodes
def graph source · line 100 · raw
@+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge>
the graph: the empty key first, leading to what the laws name, then the items
def any_item source · line 104 · raw
@ns:List<&2, String> -> @+cl:List<&2, String> -> @+pp:String -> Bool
a type's constructors: is one of them reached?
def law_dirs source · line 115 · raw
@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, String>
the directories that state laws
def gaps source · line 124 · raw
@ts:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Top> -> @+cl:List<&2, String> -> @+pp:String -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>
a def, or a type, that no law reaches
def check.go source · line 142 · raw
@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> @+cl:List<&2, String> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>
every file not exempt, against what the laws reach
def reached source · line 152 · raw
@+es:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge> -> List<&2, String>
what the laws reach: the walk from the empty key over the graph, built once
def check.first source · line 157 · raw
@+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> @dirs:List<&2, String> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>
a project states no laws: nothing of it is under law, and the graph is never built (a project with no LAWS.bend pays nothing)
def check source · line 165 · raw
@+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>
the rule, over every file the linter read