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. 29 import Base 30 import ../../lazy/lazy.bend as Lazy 31 import ../../finding.bend as F 32 import ../../syntax/outline.bend as Outline 33 import ../digest.bend as Digest 34 import ../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 40 def 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) 49 def 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, unsafes, 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 61 def key(+pp: String, name: String) -> String: 62 name ++ " " ++ pp 63 64 # the keys of what the mentions name 65 def 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 73 def 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 82 def 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 94 def 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, unsafes, 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 103 def 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? 107 def 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 118 def 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, unsafes, 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 127 def 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 145 def 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, unsafes, 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 155 def 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) 160 def 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 168 def check(+ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>: 169 check.first(ds, law_dirs(ds))