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