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