src/rules/laws/law.bend
bolt@1.26.0.0 · 169 lines · 0 definitions
1# rule coverage (project-wide; its module is law.bend, since `law` is a Bend
2# keyword and no bolt.bend could name it): in a project that states laws (a
3# LAWS.bend among the files the linter read), every def and type of every
4# file is reached from a quantified law in a LAWS.bend. A def is reached when
5# such a law names it (its binders or its statement use it, through an import
6# alias or in the law's own file), or when a reached def calls it: a use on
7# the def's lines, in its file or behind a relative import, across the files
8# of the run. A def no law reaches has no stated property, not even through
9# its callers: it is the coverage gap. A closed law, a law's own name, and a
10# law outside a LAWS.bend name nothing. A type is reached when such a law or
11# a reached def names it or one of its constructors (`M.Sq{..}` reaches a
12# `type Shape` with `Sq{..}`); a use of another def of its module does not
13# reach it, and a type reaches nothing. Out of scope: helper defs (dotted
14# names; a dotted type is graded, and a helper still carries the reach to
15# what it calls), defs that are proofs (Calls.proof: one that returns a
16# proof or is written with no type, so it fills a law; the digest drops
17# them, so they are not graded and carry no reach), tests, and the law files
18# themselves -- decided by the name, the signature and the file's path,
19# never by what the file's text mentions. IO is no
20# exemption: a law can quantify over an IO value or state an IO equality, so
21# a def returning `IO(..)` is graded like any other, and so is every pure def
22# beside it. `main` is a def: a law that names it covers it. The rule reads
23# each file's digest (src/rules/digest.bend), never the parsed source: its
24# phases use the list three times, and a `+` reuse copies it. The reach is
25# one walk over one graph, the walk the unsafe rule takes over imports
26# (src/rules/imports.bend): its nodes are the defs, types and constructors
27# of the run by key (name, a space, path), and one more node, the empty key,
28# that leads to what the laws name.
29import Base
30import bolt@1.26.0.0/src/lazy/lazy.bend as Lazy
31import bolt@1.26.0.0/src/finding.bend as F
32import bolt@1.26.0.0/src/syntax/outline.bend as Outline
33import bolt@1.26.0.0/src/rules/digest.bend as Digest
34import bolt@1.26.0.0/src/rules/imports.bend as Imports
35
36# what the laws name
37# ------------------
38
39# a file's uses onto the others', when the file is a LAWS.bend
40def named.put(laws: Bool, ms: List<&2, Digest.Mention>, more: List<&2, Digest.Mention>) -> List<&2, Digest.Mention>:
41 match laws:
42 case True{}:
43 List.append(&2, Digest.Mention, ms, more)
44 case False{}:
45 more
46
47# what the laws of every LAWS.bend name (Digest.of records uses for no
48# other file; a digest list handed in from elsewhere is read the same way)
49def named(ds: List<&2, Digest.Digest>) -> List<&2, Digest.Mention>:
50 match ds:
51 case Nil{}:
52 Nil{}
53 case Con{Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, laws}, rest}:
54 named.put(is_laws, says, named(rest))
55
56# the graph
57# ---------
58
59# an item's key: its name, a space, its file's path. A name has no space, so
60# no two items share one, and no item has the empty key
61def key(+pp: String, name: String) -> String:
62 name ++ " " ++ pp
63
64# the keys of what the mentions name
65def keys(ms: List<&2, Digest.Mention>) -> List<&2, String>:
66 match ms:
67 case Nil{}:
68 Nil{}
69 case Con{Digest.Mention{p, n}, rest}:
70 key(p, n) <> keys(rest)
71
72# a type's constructors, each a node that leads nowhere, onto the others
73def ctor_nodes(cs: List<&2, String>, +pp: String, more: List<&2, Imports.Edge>) -> List<&2, Imports.Edge>:
74 match cs:
75 case Nil{}:
76 more
77 case Con{c, rest}:
78 Imports.Edge{key(pp, c), []} <> ctor_nodes(rest, pp, more)
79
80# the items of a file as nodes onto the others: a def leads to what it
81# calls, a type and its constructors to nothing
82def nodes(ts: List<&2, Digest.Top>, +pp: String, more: List<&2, Imports.Edge>) -> List<&2, Imports.Edge>:
83 match ts:
84 case Nil{}:
85 more
86 case Con{Digest.Top{Outline.IDef{}, name, line, cs, calls}, rest}:
87 Imports.Edge{key(pp, name), keys(calls)} <> nodes(rest, pp, more)
88 case Con{Digest.Top{Outline.IType{}, name, line, cs, calls}, rest}:
89 Imports.Edge{key(pp, name), []} <> ctor_nodes(cs, pp, nodes(rest, pp, more))
90 case Con{other, rest}:
91 nodes(rest, pp, more)
92
93# the items of every file as nodes
94def graph.items(ds: List<&2, Digest.Digest>) -> List<&2, Imports.Edge>:
95 match ds:
96 case Nil{}:
97 Nil{}
98 case Con{Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, laws}, rest}:
99 nodes(tops, norm, graph.items(rest))
100
101# the graph: the empty key first, leading to what the laws name, then the
102# items
103def graph(+ds: List<&2, Digest.Digest>) -> List<&2, Imports.Edge>:
104 Imports.Edge{"", keys(named(ds))} <> graph.items(ds)
105
106# a type's constructors: is one of them reached?
107def any_item(ns: List<&2, String>, +cl: List<&2, String>, +pp: String) -> Bool:
108 match ns:
109 case Nil{}:
110 False{}
111 case Con{name, rest}:
112 Lazy.or_else(Imports.has(cl, key(pp, name)), _u => any_item(rest, cl, pp))
113
114# what is in scope
115# ----------------
116
117# the directories that state laws
118def law_dirs(ds: List<&2, Digest.Digest>) -> List<&2, String>:
119 match ds:
120 case Nil{}:
121 Nil{}
122 case Con{Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, laws}, rest}:
123 +more = law_dirs(rest)
124 Bool.pick(List<&2, String>, is_laws, dir <> more, more)
125
126# a def, or a type, that no law reaches
127def gaps(ts: List<&2, Digest.Top>, +cl: List<&2, String>, +pp: String, +path: String) -> List<&2, F.Finding>:
128 match ts:
129 case Nil{}:
130 Nil{}
131 case Con{Digest.Top{Outline.IDef{}, +name, +line, cs, calls}, rest}:
132 +more = gaps(rest, cl, pp, path)
133 Bool.pick(List<&2, F.Finding>,
134 Lazy.or_else(String.contains(name, "."), _u => Imports.has(cl, key(pp, name))), more,
135 F.Finding{path, line, 0, 0, "coverage", "No quantified law reaches def " ++ name ++ "."} <> more)
136 case Con{Digest.Top{Outline.IType{}, +name, +line, cs, calls}, rest}:
137 +more = gaps(rest, cl, pp, path)
138 Bool.pick(List<&2, F.Finding>, Lazy.or_else(Imports.has(cl, key(pp, name)), _u => any_item(cs, cl, pp)), more,
139 F.Finding{path, line, 0, 0, "coverage", "No quantified law reaches type " ++ name ++ " or any of its constructors."}
140 <> more)
141 case Con{other, rest}:
142 gaps(rest, cl, pp, path)
143
144# every file not exempt, against what the laws reach
145def check.go(ds: List<&2, Digest.Digest>, +cl: List<&2, String>) -> List<&2, F.Finding>:
146 match ds:
147 case Nil{}:
148 Nil{}
149 case Con{Digest.Digest{path, +norm, dir, is_laws, is_law_file, exempt, tops, says, deps, laws}, rest}:
150 +more = check.go(rest, cl)
151 Lazy.stop(List<&2, F.Finding>, exempt, more,
152 _u => List.append(&2, F.Finding, gaps(tops, cl, norm, path), more))
153
154# what the laws reach: the walk from the empty key over the graph, built once
155def reached(+es: List<&2, Imports.Edge>) -> List<&2, String>:
156 Imports.closure.go(es, Imports.paths(es), List.length(&2, Imports.Edge, es), "")
157
158# a project states no laws: nothing of it is under law, and the graph is
159# never built (a project with no LAWS.bend pays nothing)
160def check.first(+ds: List<&2, Digest.Digest>, dirs: List<&2, String>) -> List<&2, F.Finding>:
161 match dirs:
162 case Nil{}:
163 Nil{}
164 case Con{d, rest}:
165 check.go(ds, reached(graph(ds)))
166
167# the rule, over every file the linter read
168def check(+ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
169 check.first(ds, law_dirs(ds))