1	# src/rules/digest: one small reading of each file for the project rules.
2	# A project rule sees every file at once, and a `+` reuse of that list copies
3	# it: handed the parsed `Src` (src/src.bend), each extra use duplicated every
4	# file's text, tokens and tree, and the pair of project rules grew faster than
5	# the file count (100 files cost 362 s that way). So each file is read down
6	# once to what those rules ask of it -- its path, its top-level defs and types
7	# by name and line, what its laws name, what it imports, and its `@unsafe`
8	# and foreign defs -- and the phases run over these, which are strings and cheap to copy.
9	import Base
10	import ../src.bend as Src
11	import ../syntax/lex.bend as Lex
12	import ../syntax/tree.bend as Tree
13	import ../syntax/bind.bend as Bind
14	import ../syntax/outline.bend as Outline
15	import ../lazy/lazy.bend as Lazy
16	import ./imports.bend as Imports
17	import ./laws/closed.bend as Closed
18	import ../paths.bend as Paths
19	import ./correctness/foreign.bend as Foreign
20	
21	# what a file holds
22	# -----------------
23	
24	# a law names an item of a module: its path and its name
25	type Mention is Data:
26	  Mention{path: String, name: String}
27	
28	# a top-level def or type, by kind, name and the line it starts on, with a
29	# type's constructors by name (none for a def), and what the uses on its
30	# lines name (its calls, for a def): each as the binder resolved it, an item
31	# of the file or one behind an import alias
32	type Top is Data:
33	  Top{kind: Outline.ItemKind, name: String, line: U32, ctors: List<&2, String>, calls: List<&2, Mention>}
34	
35	# a def a proof may not reach (bend 2.0.32): an `@unsafe def`, where its
36	# `@` is, or a foreign def (its body only `import "./x.c"` / `import
37	# "./x.js"` lines), where its header starts; foreign says which
38	type Unsafe is Data:
39	  Unsafe{name: String, line: U32, col: U32, foreign: Bool}
40	
41	# a law of a LAWS.bend: its name, the line it starts on, whether it binds
42	# (a `for` or `exs` line), and the lines of its comment block, `# ` dropped
43	type Law is Data:
44	  Law{name: String, line: U32, binds: Bool, doc: List<&2, String>}
45	
46	# one file as the project rules see it: its path as given and normalized, its
47	# directory, whether it states laws (LAWS.bend) or proves them too
48	# (PROOF.bend), whether the coverage rule lets it off, its top-level items, what
49	# its own laws name, the files it imports, its `@unsafe` and foreign defs
50	type Digest is Data:
51	  Digest{path: String, norm: String, dir: String, is_laws: Bool, is_law_file: Bool, exempt: Bool,
52	    tops: List<&2, Top>, says: List<&2, Mention>, deps: List<&2, String>, unsafes: List<&2, Unsafe>,
53	    laws: List<&2, Law>}
54	
55	# what the laws name
56	# ------------------
57	
58	# an import alias and the path it names
59	type Alias is Data:
60	  Alias{name: String, path: String}
61	
62	# the aliases a file imports
63	def aliases(items: List<&2, Outline.Item>, +from: String) -> List<&2, Alias>:
64	  match items:
65	    case Nil{}:
66	      Nil{}
67	    case Con{Outline.Item{Outline.IImport{}, name, line, sig, doc, path}, rest}:
68	      Alias{name, Imports.resolve(from, path)} <> aliases(rest, from)
69	    case Con{other, rest}:
70	      aliases(rest, from)
71	
72	# the path an alias names, when it is one
73	def alias_path(as: List<&2, Alias>, +name: String) -> Maybe<&2, String>:
74	  match as:
75	    case Nil{}:
76	      None{}
77	    case Con{Alias{+n, p}, rest}:
78	      +more = alias_path(rest, name)
79	      Bool.pick(Maybe<&2, String>, String.eq(n, name), Some{p}, more)
80	
81	# the lines a quantified law's statement spans: from its header's first token
82	# to its body's last
83	type Span is Data:
84	  Span{from: U32, upto: U32}
85	
86	# the spans of every quantified law of a tree, in order. A closed law spans
87	# nothing (it covers one input, not the def)
88	def spans(root: Tree.Node) -> List<&2, Span>:
89	  match root:
90	    case Tree.NCons{Tree.Stmt{Tree.SLaw{}, kids, +body}, rest}:
91	      +more = spans(rest)
92	      Bool.pick(List<&2, Span>, Closed.binds(body),
93	        Span{Tree.line(kids), Tree.line.of(List.head(&2, Lex.Tok, Tree.leaves.go(body, [])))} <> more, more)
94	    case Tree.NCons{h, rest}:
95	      spans(rest)
96	    case other:
97	      Nil{}
98	
99	# is the line in one of the spans?
100	def within(ss: List<&2, Span>, +ln: U32) -> Bool:
101	  match ss:
102	    case Nil{}:
103	      False{}
104	    case Con{Span{+from, +upto}, rest}:
105	      Lazy.or_else(Bool.and(U32.is_le(from, ln), U32.is_le(ln, upto)), _u => within(rest, ln))
106	
107	# an item behind an alias, when an import names the alias, onto the others
108	def aliased(mm: Maybe<&2, String>, +name: String, more: List<&2, Mention>) -> List<&2, Mention>:
109	  match mm:
110	    case Some{p}:
111	      Mention{p, name} <> more
112	    case None{}:
113	      more
114	
115	# what the binder resolved a use to, as a mention onto the others: an item of
116	# the law's own file, or an item of the file an import alias names; nothing
117	# for a binder, a free name, or an alias no import names
118	def target(tt: Bind.Target, +as: List<&2, Alias>, +file: String, more: List<&2, Mention>) -> List<&2, Mention>:
119	  match tt:
120	    case Bind.TItem{n}:
121	      Mention{file, n} <> more
122	    case Bind.TQual{a, n}:
123	      aliased(alias_path(as, a), n, more)
124	    case other:
125	      more
126	
127	# the mentions of every use the binder records in the statement of a
128	# quantified law, in order. Its header's own name is a binder, not a use
129	def mentions(us: List<&2, Bind.Use>, +ss: List<&2, Span>, +as: List<&2, Alias>, +file: String) -> List<&2, Mention>:
130	  match us:
131	    case Nil{}:
132	      Nil{}
133	    case Con{Bind.Use{n, +l, c, tt}, rest}:
134	      +more = mentions(rest, ss, as, file)
135	      Lazy.stop(List<&2, Mention>, Bool.not(within(ss, l)), more, _u => target(tt, as, file, more))
136	
137	# the uses the binder recorded
138	def uses.of(bb: Bind.Bound) -> List<&2, Bind.Use>:
139	  match bb:
140	    case Bind.Bound{bs, us, scs}:
141	      us
142	
143	# what the file holds besides
144	# ---------------------------
145	
146	# the names of the constructors the items open with: a type's, since the
147	# outline lists them right after it
148	def ctors(items: List<&2, Outline.Item>) -> List<&2, String>:
149	  match items:
150	    case Con{Outline.Item{Outline.ICtor{}, name, line, sig, doc, path}, rest}:
151	      name <> ctors(rest)
152	    case other:
153	      Nil{}
154	
155	# the uses, in order, before the first one at or past the line
156	def before(us: List<&2, Bind.Use>, +at: U32) -> List<&2, Bind.Use>:
157	  match us:
158	    case Nil{}:
159	      Nil{}
160	    case Con{Bind.Use{nm, +l, c, tt}, rest}:
161	      Lazy.stop(List<&2, Bind.Use>, U32.is_le(at, l), [], _u => Bind.Use{nm, l, c, tt} <> before(rest, at))
162	
163	# the uses from the first one at or past the line on
164	def after(us: List<&2, Bind.Use>, +at: U32) -> List<&2, Bind.Use>:
165	  match us:
166	    case Nil{}:
167	      Nil{}
168	    case Con{Bind.Use{nm, +l, c, tt}, +rest}:
169	      Lazy.stop(List<&2, Bind.Use>, U32.is_le(at, l), Bind.Use{nm, l, c, tt} <> rest, _u => after(rest, at))
170	
171	# the uses before the line, when there is one; else all of them
172	def upto(us: List<&2, Bind.Use>, mm: Maybe<&2, U32>) -> List<&2, Bind.Use>:
173	  match mm:
174	    case None{}:
175	      us
176	    case Some{at}:
177	      before(us, at)
178	
179	# the uses from the line on, when there is one; else none
180	def past(us: List<&2, Bind.Use>, mm: Maybe<&2, U32>) -> List<&2, Bind.Use>:
181	  match mm:
182	    case None{}:
183	      Nil{}
184	    case Some{at}:
185	      after(us, at)
186	
187	# the line of the next item that ends an item's lines: any but a constructor,
188	# which the outline lists inside its type
189	def next_line(items: List<&2, Outline.Item>) -> Maybe<&2, U32>:
190	  match items:
191	    case Nil{}:
192	      None{}
193	    case Con{Outline.Item{Outline.ICtor{}, name, line, sig, doc, path}, rest}:
194	      next_line(rest)
195	    case Con{Outline.Item{kind, name, line, sig, doc, path}, rest}:
196	      Some{line}
197	
198	# what the uses name, in order: an item of the file, or one behind an alias
199	def called(us: List<&2, Bind.Use>, +as: List<&2, Alias>, +file: String) -> List<&2, Mention>:
200	  match us:
201	    case Nil{}:
202	      Nil{}
203	    case Con{Bind.Use{n, l, c, tt}, rest}:
204	      target(tt, as, file, called(rest, as, file))
205	
206	# the top-level defs and types, by name and line: what the coverage rule
207	# grades. The uses are read in order, once: each item but a constructor
208	# takes those before the next such item's line, and a def or a type keeps
209	# what they name (a def's calls)
210	def ranged(
211	  items: List<&2, Outline.Item>,
212	  +us: List<&2, Bind.Use>,
213	  +as: List<&2, Alias>,
214	  +file: String
215	) -> List<&2, Top>:
216	  match items:
217	    case Nil{}:
218	      Nil{}
219	    case Con{Outline.Item{Outline.ICtor{}, name, line, sig, doc, path}, rest}:
220	      ranged(rest, us, as, file)
221	    case Con{Outline.Item{Outline.IDef{}, name, line, sig, doc, path}, +rest}:
222	      +nx = next_line(rest)
223	      Top{Outline.IDef{}, name, line, [], called(upto(us, nx), as, file)} <> ranged(rest, past(us, nx), as, file)
224	    case Con{Outline.Item{Outline.IType{}, name, line, sig, doc, path}, +rest}:
225	      +nx = next_line(rest)
226	      Top{Outline.IType{}, name, line, ctors(rest), called(upto(us, nx), as, file)}
227	        <> ranged(rest, past(us, nx), as, file)
228	    case Con{Outline.Item{kind, name, line, sig, doc, path}, +rest}:
229	      ranged(rest, past(us, next_line(rest)), as, file)
230	
231	# a law file or a test, by its path alone: not under law. Nothing the file's
232	# text mentions exempts it; IO is not an exemption, since an IO equality is a
233	# law.
234	def is_exempt(+pp: String) -> Bool:
235	  Bool.or(Paths.is_law_file(pp), Paths.is_test(pp))
236	
237	# the significant tokens: no space, newline or comment
238	def significant(toks: List<&2, Lex.Tok>) -> List<&2, Lex.Tok>:
239	  match toks:
240	    case Nil{}:
241	      Nil{}
242	    case Con{Lex.Tok{+k, t, l, c}, rest}:
243	      +more = significant(rest)
244	      Bool.pick(List<&2, Lex.Tok>, Lex.significant(k), Lex.Tok{k, t, l, c} <> more, more)
245	
246	# the name after `unsafe def`, when the tokens run so
247	def unsafe_name(toks: List<&2, Lex.Tok>) -> Maybe<&2, String>:
248	  match toks:
249	    case Con{Lex.Tok{k1, +u, l1, c1}, Con{Lex.Tok{k2, +d, l2, c2}, Con{Lex.Tok{k3, n, l3, c3}, rest}}}:
250	      Bool.pick(Maybe<&2, String>, Bool.and(String.eq(u, "unsafe"), String.eq(d, "def")), Some{n}, None{})
251	    case other:
252	      None{}
253	
254	# an `@` that heads an unsafe def, onto the others
255	def push(mm: Maybe<&2, String>, +ll: U32, +cc: U32, more: List<&2, Unsafe>) -> List<&2, Unsafe>:
256	  match mm:
257	    case None{}:
258	      more
259	    case Some{n}:
260	      Unsafe{n, ll, cc, False{}} <> more
261	
262	# every `@ unsafe def name` run of tokens, on one line or two
263	def unsafe_defs(toks: List<&2, Lex.Tok>) -> List<&2, Unsafe>:
264	  match toks:
265	    case Nil{}:
266	      Nil{}
267	    case Con{Lex.Tok{k, +at, +l, +c}, +rest}:
268	      +more = unsafe_defs(rest)
269	      Bool.pick(List<&2, Unsafe>, String.eq(at, "@"), push(unsafe_name(rest), l, c, more), more)
270	
271	# a foreign def, when its body is one (Foreign.lanes), onto the others
272	def foreign.push(
273	  mm: Maybe<&2, Foreign.Lanes>,
274	  +name: String,
275	  +ll: U32,
276	  +cc: U32,
277	  more: List<&2, Unsafe>
278	) -> List<&2, Unsafe>:
279	  match mm:
280	    case None{}:
281	      more
282	    case Some{_lanes}:
283	      Unsafe{name, ll, cc, True{}} <> more
284	
285	# every top-level foreign def, where its header starts
286	def foreign_defs(root: Tree.Node) -> List<&2, Unsafe>:
287	  match root:
288	    case Tree.NCons{Tree.Stmt{Tree.SDef{}, +kids, body}, rest}:
289	      foreign.push(Foreign.lanes(body), Foreign.name.of(Bind.declared(kids)), Tree.line(kids), Tree.col(kids),
290	        foreign_defs(rest))
291	    case Tree.NCons{h, rest}:
292	      foreign_defs(rest)
293	    case other:
294	      Nil{}
295	
296	# the laws
297	# --------
298	
299	# the doc of the item on a line; the items are in line order, so the search
300	# stops at it
301	def doc_at(items: List<&2, Outline.Item>, +at: U32) -> String:
302	  match items:
303	    case Nil{}:
304	      ""
305	    case Con{Outline.Item{kk, nn, +ln, sig, +doc, pp}, rest}:
306	      Lazy.stop(String, U32.is_le(at, ln), Bool.pick(String, U32.is_eq(ln, at), doc, ""), _u => doc_at(rest, at))
307	
308	# every law of a tree, with whether it binds and its doc lines
309	def laws_of(root: Tree.Node, +items: List<&2, Outline.Item>) -> List<&2, Law>:
310	  match root:
311	    case Tree.NCons{Tree.Stmt{Tree.SLaw{}, +kids, body}, rest}:
312	      +at = Tree.line(kids)
313	      Law{Closed.name.of(Bind.declared(kids)), at, Closed.binds(body), String.lines(doc_at(items, at))}
314	        <> laws_of(rest, items)
315	    case Tree.NCons{h, rest}:
316	      laws_of(rest, items)
317	    case other:
318	      Nil{}
319	
320	# the laws of a LAWS.bend; no other file states any
321	def laws.in(is_laws: Bool, root: Tree.Node, items: List<&2, Outline.Item>) -> List<&2, Law>:
322	  match is_laws:
323	    case True{}:
324	      laws_of(root, items)
325	    case False{}:
326	      Nil{}
327	
328	# the digest
329	# ----------
330	
331	# what a file's laws name: only a LAWS.bend states laws that cover a def
332	def stated(is_laws: Bool, root: Tree.Node, bound: Bind.Bound, as: List<&2, Alias>, file: String) -> List<&2, Mention>:
333	  match is_laws:
334	    case True{}:
335	      mentions(uses.of(bound), spans(root), as, file)
336	    case False{}:
337	      Nil{}
338	
339	# one parsed file read down to its digest
340	def of(s2: Src.Src) -> Digest:
341	  Src.Src{+path, text, toks, +tree, +bound, +items} = s2
342	  +p = Imports.norm(path)
343	  +as = aliases(items, p)
344	  Digest{path, p, Imports.dir_of(path), Paths.is_laws(path), Paths.is_law_file(path), is_exempt(p),
345	    ranged(items, uses.of(bound), as, p), stated(Paths.is_laws(path), tree, bound, as, p), Imports.targets(items, p),
346	    List.append(&2, Unsafe, unsafe_defs(significant(toks)), foreign_defs(tree)),
347	    laws.in(Paths.is_laws(path), tree, items)}
348	
349	# every file the linter read, in one pass, in order
350	def all(ss: List<&2, Src.Src>) -> List<&2, Digest>:
351	  match ss:
352	    case Nil{}:
353	      Nil{}
354	    case Con{s, rest}:
355	      of(s) <> all(rest)
356	
357	# the import graph of the files, built once for every closure taken over it
358	def edges(ds: List<&2, Digest>) -> List<&2, Imports.Edge>:
359	  match ds:
360	    case Nil{}:
361	      Nil{}
362	    case Con{Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
363	      Imports.Edge{norm, deps} <> edges(rest)