src/rules/digest.bend
bolt@1.17.0.0 · 390 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.17.0.0/src/src.bend as Src
11import bolt@1.17.0.0/src/syntax/lex.bend as Lex
12import bolt@1.17.0.0/src/syntax/tree.bend as Tree
13import bolt@1.17.0.0/src/syntax/bind.bend as Bind
14import bolt@1.17.0.0/src/syntax/outline.bend as Outline
15import bolt@1.17.0.0/src/lazy/lazy.bend as Lazy
16import bolt@1.17.0.0/src/rules/imports.bend as Imports
17import bolt@1.17.0.0/src/rules/laws/closed.bend as Closed
18import bolt@1.17.0.0/src/paths.bend as Paths
19import bolt@1.17.0.0/src/rules/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
25type 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
32type 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
38type 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
43type 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
50type 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
59type Alias is Data:
60 Alias{name: String, path: String}
61
62# the aliases a file imports
63def 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
73def 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
83type 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)
88def 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?
100def 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
108def 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
118def 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
129def 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 +out = Bool.not(within(ss, l))
136 Lazy.stop(List<&2, Mention>, out, more, _u => target(tt, as, file, more))
137
138# the uses the binder recorded
139def uses.of(bb: Bind.Bound) -> List<&2, Bind.Use>:
140 match bb:
141 case Bind.Bound{bs, us, scs}:
142 us
143
144# what the file holds besides
145# ---------------------------
146
147# the names of the constructors the items open with: a type's, since the
148# outline lists them right after it
149def ctors(items: List<&2, Outline.Item>) -> List<&2, String>:
150 match items:
151 case Con{Outline.Item{Outline.ICtor{}, name, line, sig, doc, path}, rest}:
152 name <> ctors(rest)
153 case other:
154 Nil{}
155
156# the uses, in order, before the first one at or past the line
157def before(us: List<&2, Bind.Use>, +at: U32) -> List<&2, Bind.Use>:
158 match us:
159 case Nil{}:
160 Nil{}
161 case Con{Bind.Use{nm, +l, c, tt}, rest}:
162 Lazy.stop(List<&2, Bind.Use>, U32.is_le(at, l), [], _u => Bind.Use{nm, l, c, tt} <> before(rest, at))
163
164# the uses from the first one at or past the line on
165def after(us: List<&2, Bind.Use>, +at: U32) -> List<&2, Bind.Use>:
166 match us:
167 case Nil{}:
168 Nil{}
169 case Con{Bind.Use{nm, +l, c, tt}, +rest}:
170 Lazy.stop(List<&2, Bind.Use>, U32.is_le(at, l), Bind.Use{nm, l, c, tt} <> rest, _u => after(rest, at))
171
172# the uses before the line, when there is one; else all of them
173def upto(us: List<&2, Bind.Use>, mm: Maybe<&2, U32>) -> List<&2, Bind.Use>:
174 match mm:
175 case None{}:
176 us
177 case Some{at}:
178 before(us, at)
179
180# the uses from the line on, when there is one; else none
181def past(us: List<&2, Bind.Use>, mm: Maybe<&2, U32>) -> List<&2, Bind.Use>:
182 match mm:
183 case None{}:
184 Nil{}
185 case Some{at}:
186 after(us, at)
187
188# the line of the next item that ends an item's lines: any but a constructor,
189# which the outline lists inside its type
190def next_line(items: List<&2, Outline.Item>) -> Maybe<&2, U32>:
191 match items:
192 case Nil{}:
193 None{}
194 case Con{Outline.Item{Outline.ICtor{}, name, line, sig, doc, path}, rest}:
195 next_line(rest)
196 case Con{Outline.Item{kind, name, line, sig, doc, path}, rest}:
197 Some{line}
198
199# what the uses name, in order: an item of the file, or one behind an alias
200def called(us: List<&2, Bind.Use>, +as: List<&2, Alias>, +file: String) -> List<&2, Mention>:
201 match us:
202 case Nil{}:
203 Nil{}
204 case Con{Bind.Use{n, l, c, tt}, rest}:
205 target(tt, as, file, called(rest, as, file))
206
207# the top-level defs and types, by name and line: what the coverage rule
208# grades. The uses are read in order, once: each item but a constructor
209# takes those before the next such item's line, and a def or a type keeps
210# what they name (a def's calls)
211def ranged(
212 items: List<&2, Outline.Item>,
213 +us: List<&2, Bind.Use>,
214 +as: List<&2, Alias>,
215 +file: String
216) -> List<&2, Top>:
217 match items:
218 case Nil{}:
219 Nil{}
220 case Con{Outline.Item{Outline.ICtor{}, name, line, sig, doc, path}, rest}:
221 ranged(rest, us, as, file)
222 case Con{Outline.Item{Outline.IDef{}, name, line, sig, doc, path}, +rest}:
223 +nx = next_line(rest)
224 cs = called(upto(us, nx), as, file)
225 Top{Outline.IDef{}, name, line, [], cs} <> ranged(rest, past(us, nx), as, file)
226 case Con{Outline.Item{Outline.IType{}, name, line, sig, doc, path}, +rest}:
227 +nx = next_line(rest)
228 Top{Outline.IType{}, name, line, ctors(rest), called(upto(us, nx), as, file)}
229 <> ranged(rest, past(us, nx), as, file)
230 case Con{Outline.Item{kind, name, line, sig, doc, path}, +rest}:
231 ranged(rest, past(us, next_line(rest)), as, file)
232
233# a law file or a test, by its path alone: not under law. Nothing the file's
234# text mentions exempts it; IO is not an exemption, since an IO equality is a
235# law.
236def is_exempt(+pp: String) -> Bool:
237 Bool.or(Paths.is_law_file(pp), Paths.is_test(pp))
238
239# the significant tokens: no space, newline or comment
240def significant(toks: List<&2, Lex.Tok>) -> List<&2, Lex.Tok>:
241 match toks:
242 case Nil{}:
243 Nil{}
244 case Con{Lex.Tok{+k, t, l, c}, rest}:
245 +more = significant(rest)
246 Bool.pick(List<&2, Lex.Tok>, Lex.significant(k), Lex.Tok{k, t, l, c} <> more, more)
247
248# the name after `unsafe def`, when the tokens run so
249def unsafe_name(toks: List<&2, Lex.Tok>) -> Maybe<&2, String>:
250 match toks:
251 case Con{Lex.Tok{k1, +u, l1, c1}, Con{Lex.Tok{k2, +d, l2, c2}, Con{Lex.Tok{k3, n, l3, c3}, rest}}}:
252 Bool.pick(Maybe<&2, String>, Bool.and(String.eq(u, "unsafe"), String.eq(d, "def")), Some{n}, None{})
253 case other:
254 None{}
255
256# an `@` that heads an unsafe def, onto the others
257def push(mm: Maybe<&2, String>, +ll: U32, +cc: U32, more: List<&2, Unsafe>) -> List<&2, Unsafe>:
258 match mm:
259 case None{}:
260 more
261 case Some{n}:
262 Unsafe{n, ll, cc, False{}} <> more
263
264# every `@ unsafe def name` run of tokens, on one line or two
265def unsafe_defs(toks: List<&2, Lex.Tok>) -> List<&2, Unsafe>:
266 match toks:
267 case Nil{}:
268 Nil{}
269 case Con{Lex.Tok{k, +at, +l, +c}, +rest}:
270 +more = unsafe_defs(rest)
271 Bool.pick(List<&2, Unsafe>, String.eq(at, "@"), push(unsafe_name(rest), l, c, more), more)
272
273# a foreign def, when its body is one (Foreign.lanes), onto the others
274def foreign.push(
275 mm: Maybe<&2, Foreign.Lanes>,
276 +name: String,
277 +ll: U32,
278 +cc: U32,
279 more: List<&2, Unsafe>
280) -> List<&2, Unsafe>:
281 match mm:
282 case None{}:
283 more
284 case Some{_lanes}:
285 Unsafe{name, ll, cc, True{}} <> more
286
287# every top-level foreign def, where its header starts
288def foreign_defs(root: Tree.Node) -> List<&2, Unsafe>:
289 match root:
290 case Tree.NCons{Tree.Stmt{Tree.SDef{}, +kids, body}, rest}:
291 foreign.push(Foreign.lanes(body), Foreign.name.of(Bind.declared(kids)), Tree.line(kids), Tree.col(kids),
292 foreign_defs(rest))
293 case Tree.NCons{h, rest}:
294 foreign_defs(rest)
295 case other:
296 Nil{}
297
298# the laws
299# --------
300
301# the doc of the item on a line; the items are in line order, so the search
302# stops at it
303def doc_at(items: List<&2, Outline.Item>, +at: U32) -> String:
304 match items:
305 case Nil{}:
306 ""
307 case Con{Outline.Item{kk, nn, +ln, sig, +doc, pp}, rest}:
308 Lazy.stop(String, U32.is_le(at, ln), Bool.pick(String, U32.is_eq(ln, at), doc, ""), _u => doc_at(rest, at))
309
310# does the first item sit on or after a line (from_line stops there)?
311def from_line.stop(items: List<&2, Outline.Item>, +at: U32) -> Bool:
312 match items:
313 case Nil{}:
314 True{}
315 case Con{Outline.Item{kk, nn, +ln, sig, doc, pp}, rest}:
316 U32.is_le(at, ln)
317
318# the items from the first on or after a line; the items are in line order,
319# and so are a tree's laws, so an item this drops lies above every later law
320# too. stop is from_line.stop of items, carried so the step stays a loop
321def from_line(items: List<&2, Outline.Item>, +at: U32, +stop: Bool) -> List<&2, Outline.Item>:
322 match items:
323 case Nil{}:
324 Nil{}
325 case Con{h, +rest}:
326 match stop:
327 case True{}:
328 h <> rest
329 case False{}:
330 from_line(rest, at, from_line.stop(rest, at))
331
332# every law of a tree, with whether it binds and its doc lines. items is a
333# cursor: each law's search starts where the last one stopped, so the items
334# are read once over all the laws, not once per law
335def laws_of(root: Tree.Node, +items: List<&2, Outline.Item>) -> List<&2, Law>:
336 match root:
337 case Tree.NCons{Tree.Stmt{Tree.SLaw{}, +kids, body}, rest}:
338 +at = Tree.line(kids)
339 +left = from_line(items, at, from_line.stop(items, at))
340 dd = doc_at(left, at)
341 Law{Closed.name.of(Bind.declared(kids)), at, Closed.binds(body), String.lines(dd)} <> laws_of(rest, left)
342 case Tree.NCons{h, rest}:
343 laws_of(rest, items)
344 case other:
345 Nil{}
346
347# the laws of a LAWS.bend; no other file states any
348def laws.in(is_laws: Bool, root: Tree.Node, items: List<&2, Outline.Item>) -> List<&2, Law>:
349 match is_laws:
350 case True{}:
351 laws_of(root, items)
352 case False{}:
353 Nil{}
354
355# the digest
356# ----------
357
358# what a file's laws name: only a LAWS.bend states laws that cover a def
359def stated(is_laws: Bool, root: Tree.Node, bound: Bind.Bound, as: List<&2, Alias>, file: String) -> List<&2, Mention>:
360 match is_laws:
361 case True{}:
362 mentions(uses.of(bound), spans(root), as, file)
363 case False{}:
364 Nil{}
365
366# one parsed file read down to its digest
367def of(s2: Src.Src) -> Digest:
368 Src.Src{+path, text, toks, +tree, +bound, +items} = s2
369 +p = Imports.norm(path)
370 +as = aliases(items, p)
371 Digest{path, p, Imports.dir_of(path), Paths.is_laws(path), Paths.is_law_file(path), is_exempt(p),
372 ranged(items, uses.of(bound), as, p), stated(Paths.is_laws(path), tree, bound, as, p), Imports.targets(items, p),
373 List.append(&2, Unsafe, unsafe_defs(significant(toks)), foreign_defs(tree)),
374 laws.in(Paths.is_laws(path), tree, items)}
375
376# every file the linter read, in one pass, in order
377def all(ss: List<&2, Src.Src>) -> List<&2, Digest>:
378 match ss:
379 case Nil{}:
380 Nil{}
381 case Con{s, rest}:
382 of(s) <> all(rest)
383
384# the import graph of the files, built once for every closure taken over it
385def edges(ds: List<&2, Digest>) -> List<&2, Imports.Edge>:
386 match ds:
387 case Nil{}:
388 Nil{}
389 case Con{Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
390 Imports.Edge{norm, deps} <> edges(rest)