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