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