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