linter/lint.bend
bend-lint-api@0.1.0.0 · 1,061 lines · 0 definitions
1# What a rule sees. A rule file imports this file, and defines `rule()`.
2#
3# Design
4# - The rules run in an ordinary Bend program that seam.ts writes from bend-lint.json, builds once and keeps. The C
5# lane is the target; the JS lane must work too.
6# - Bend's checker is TS for now: seam.ts makes each check's program of what Bend's parser and checker give, and answers
7# the questions rules ask about its types, over local TCP (see Seam in cli.bend). When the checker is Bend, glue in
8# Bend makes the same program, and the questions become calls.
9# - A file is a tree of syntax nodes. A rule walks it, and reads what a node is from the node and the nodes above it.
10# - Rules are pure, so they run in parallel. The runner answers every rule's questions of a round in one batch.
11# - A check is read once and shared by every rule. Facts and declarations are collected only if a rule needs them.
12# - A rule requests a fix as typed operations, and the linter plans them. Until Bend's checker is Bend, no fix is
13# proven to keep the program: `--fix-dangerously` makes them all, and `--fix` makes none.
14import Base
15import bend-lint-api@0.1.0.0/shared/lists.bend as Lists
16import bend-lint-api@0.1.0.0/shared/names.bend as Names
17import bend-lint-api@0.1.0.0/shared/strings.bend as Strings
18import bend-lint-api@0.1.0.0/shared/tables.bend as Tables
19
20# Program
21# =======
22type Quantity is Data:
23 Erased{}
24 Once{}
25 Many{}
26 Template{}
27
28# Where something is: its file, and offsets in code points.
29type Span is Data:
30 Span{path: String, beg: U32, end: U32}
31
32# What a syntax node is, as Bend's parser reads it: a declaration, a part of one, a term, or a pattern; with what only
33# nodes of its kind have: the global name it declares or uses (`target`, as the check names it; an import's is the path
34# of the file it loads), the binder it declares or a variable uses (numbered per top-level declaration), and its
35# quantity as written (a `~` parameter's is Template). An import's written path is an ImportPath under it; `import
36# Base` writes none. A Definition is `unsafe` if Bend's checker trusts its body (`@unsafe def f`, or `def f?`).
37type Syntax is Data:
38 Import{target: String}
39 ImportPath{}
40 Definition{target: String, unsafe: Bool}
41 Datatype{target: String}
42 Constructor{target: String}
43 Law{target: String}
44 Parameter{binder: U32, quantity: Quantity}
45 Field{binder: U32, quantity: Quantity}
46 Returns{}
47 Body{}
48 Variable{binder: U32}
49 Reference{target: String}
50 Substitution{}
51 Let{}
52 Binding{binder: U32, quantity: Quantity}
53 Sort{}
54 QuantityType{}
55 QuantityLiteral{quantity: Quantity}
56 QuantityMinimum{}
57 Forall{binder: U32, quantity: Quantity}
58 Lambda{binder: U32, quantity: Maybe<&2, Quantity>}
59 Application{}
60 TypeApplication{target: String}
61 Construction{target: String}
62 Literal{target: String}
63 Elimination{target: String}
64 Absurd{}
65 Equality{}
66 Reflexivity{}
67 Rewrite{}
68 Hole{}
69 Annotation{}
70 Match{}
71 Case{}
72 Destructure{quantity: Quantity}
73 PatternVariable{binder: U32, quantity: Quantity}
74 PatternConstructor{target: String}
75
76# A type the checker holds: a handle, good in the check it came from. Rules ask about it (show, same, normal). Two types
77# are the same only over the binders their scopes share: `A` of one def is not `A` of another.
78type TypeRef is Data:
79 TypeRef{check: U32, handle: U32}
80
81# What a fact says of its node: the type its term has, or the type its binder declares (a parameter, field, pattern
82# variable, lambda, forall or let binding).
83type Role is Data:
84 OfTerm{}
85 OfBinder{}
86
87# What the checker found for a node of the source: what the fact says of it, the quantity (how often the term is
88# demanded, or the binder's), for a binder of a parameter, lambda, let or case, how often its body uses it (the most of
89# its checked copies; none for a parameter a match takes apart), and the type. A fact is never wrong, but a node can
90# have none: a term the checker rewrote into another (a scrutinee used again, a call a template took) is not typed as
91# itself. A node has one fact per distinct type: pattern compilation can check one term in several branches, under
92# different refinements.
93type Fact is Data:
94 Fact{role: Role, quantity: Quantity, used: Maybe<&2, Quantity>, checked: TypeRef}
95
96# A syntax node: what it is, its name as written, where the file writes it (none for what the parser adds), the nodes
97# under it, in order, and the checker's facts on it, if a rule needs them. An application's nodes are its function,
98# then its arguments; a block's, its binders, then their values, then the rest of the block.
99type Node is Data:
100 Node{
101 syntax: Syntax,
102 name: String,
103 span: Maybe<&2, Span>,
104 kids: List<&2, Node>,
105 facts: List<&2, Fact>
106 }
107
108# A file the check parsed: its path, its namespace in the check ("" for the checked file), its text, and its nodes: its
109# imports, then its declarations, each constructor under its type.
110type Source is Data:
111 Source{path: String, namespace: String, text: String, nodes: List<&2, Node>}
112
113type Program is Data:
114 Program{sources: List<&2, Source>}
115
116# A name a node declares, and the nodes that use it, in order.
117type Declaration is Data:
118 Declaration{node: Node, references: List<&2, Node>}
119
120# The global name a node of this kind declares or uses, if any (an import's is the file it loads).
121def Syntax.target(syntax: Syntax) -> Maybe<&2, String>:
122 match syntax:
123 case Import{t}:
124 Some{t}
125 case Definition{t, u}:
126 Some{t}
127 case Datatype{t}:
128 Some{t}
129 case Constructor{t}:
130 Some{t}
131 case Law{t}:
132 Some{t}
133 case Reference{t}:
134 Some{t}
135 case TypeApplication{t}:
136 Some{t}
137 case Construction{t}:
138 Some{t}
139 case Literal{t}:
140 Some{t}
141 case Elimination{t}:
142 Some{t}
143 case PatternConstructor{t}:
144 Some{t}
145 case _:
146 None{}
147
148# The global name a node of this kind uses, if it uses one.
149def Syntax.used(syntax: Syntax) -> Maybe<&2, String>:
150 match syntax:
151 case Reference{t}:
152 Some{t}
153 case Construction{t}:
154 Some{t}
155 case TypeApplication{t}:
156 Some{t}
157 case PatternConstructor{t}:
158 Some{t}
159 case Elimination{t}:
160 Some{t}
161 case Literal{t}:
162 Some{t}
163 case _:
164 None{}
165
166# The binder a node of this kind declares, or, for a variable, uses.
167def Syntax.binder(syntax: Syntax) -> Maybe<&2, U32>:
168 match syntax:
169 case Parameter{b, q}:
170 Some{b}
171 case Field{b, q}:
172 Some{b}
173 case Variable{b}:
174 Some{b}
175 case Binding{b, q}:
176 Some{b}
177 case Forall{b, q}:
178 Some{b}
179 case Lambda{b, q}:
180 Some{b}
181 case PatternVariable{b, q}:
182 Some{b}
183 case _:
184 None{}
185
186# Whether a node of this kind declares a global name (Some{True{}}), a binder of its top-level declaration
187# (Some{False{}}), or nothing (an import declares an alias, which Declarations below handles).
188def Syntax.declares(syntax: Syntax) -> Maybe<&2, Bool>:
189 match syntax:
190 case Definition{t, u}:
191 Some{True{}}
192 case Datatype{t}:
193 Some{True{}}
194 case Constructor{t}:
195 Some{True{}}
196 case Law{t}:
197 Some{True{}}
198 case Parameter{b, q}:
199 Some{False{}}
200 case Field{b, q}:
201 Some{False{}}
202 case Binding{b, q}:
203 Some{False{}}
204 case Lambda{b, q}:
205 Some{False{}}
206 case Forall{b, q}:
207 Some{False{}}
208 case PatternVariable{b, q}:
209 Some{False{}}
210 case _:
211 None{}
212
213def Node.syntax(node: Node) -> Syntax:
214 match node:
215 case Node{syntax, name, span, kids, facts}:
216 syntax
217
218# "" for a node of a kind that names nothing.
219def Node.target(node: Node) -> String:
220 match node:
221 case Node{syntax, name, span, kids, facts}:
222 Maybe.default(&2, String, Syntax.target(syntax), "")
223
224def Node.kids(node: Node) -> List<&2, Node>:
225 match node:
226 case Node{syntax, name, span, kids, facts}:
227 kids
228
229# "" for no node, as are the next two.
230def Node.name(node: Maybe<&2, Node>) -> String:
231 match node:
232 case Some{Node{syntax, name, span, kids, facts}}:
233 name
234 case None{}:
235 ""
236
237def Node.span(node: Maybe<&2, Node>) -> Maybe<&2, Span>:
238 match node:
239 case Some{Node{syntax, name, span, kids, facts}}:
240 span
241 case None{}:
242 None{}
243
244def Span.text(source: String, span: Maybe<&2, Span>) -> String:
245 match span:
246 case Some{Span{path, beg, end}}:
247 Strings.slice(source, beg, end)
248 case None{}:
249 ""
250
251# The namespace of a global name: what comes before its first ":", or "" for Base and the checked file's own names.
252def Name.namespace(name: String) -> String:
253 Strings.before(name, ':')
254
255# Whether a parameter is written bare (`def f(x)`, filling a law): its quantity is the law's, which its node does not
256# give.
257def Node.is_bare(node: Node) -> Bool:
258 match node:
259 case Node{Parameter{b, q}, n, s, Con{Node{QuantityType{}, kn, ks, kk, kf}, rest}, f}:
260 True{}
261 case _:
262 False{}
263
264def Node.scrutinees.go(nodes: List<&2, Node>, out: List<&2, Node>) -> List<&2, Node>:
265 match nodes:
266 case Con{Node{Case{}, n, s, k, f}, rest}:
267 List.reverse(&2, Node, out)
268 case Con{node, rest}:
269 Node.scrutinees.go(rest, node <> out)
270 case Nil{}:
271 List.reverse(&2, Node, out)
272
273# The scrutinees of a match, in order: its nodes before its first case.
274def Node.scrutinees(node: Node) -> List<&2, Node>:
275 Node.scrutinees.go(Node.kids(node), [])
276
277# The binders of the pattern variables in `nodes`, patterns, and under them, onto `out`.
278def Node.bound(nodes: List<&2, Node>, out: List<&2, U32>) -> List<&2, U32>:
279 match nodes:
280 case Nil{}:
281 out
282 case Con{Node{PatternVariable{b, q}, n, s, k, f}, rest}:
283 Node.bound(rest, b <> out)
284 case Con{Node{PatternConstructor{t}, n, s, kids, f}, rest}:
285 Node.bound(rest, Node.bound(kids, out))
286 case Con{node, rest}:
287 Node.bound(rest, out)
288
289# Walking
290# =======
291
292# A node above another: the node, and the place among its nodes (from 0) of the one on the way down.
293type Above is Data:
294 Above{node: Node, at: U32}
295
296def Above.of(parent: Maybe<&2, Node>, at: U32, up: List<&2, Above>) -> List<&2, Above>:
297 match parent:
298 case Some{p}:
299 Above{p, at} <> up
300 case None{}:
301 up
302
303def visit.go(
304 ~C: Data,
305 ~A: Data,
306 ~f: @+c: C -> @+path: List<&2, Above> -> @+node: Node -> List<&2, A>,
307 nodes: List<&2, Node>,
308 +c: C,
309 +up: List<&2, Above>,
310 +parent: Maybe<&2, Node>,
311 +at: U32,
312 out: List<&2, A>
313) -> List<&2, A>:
314 match nodes:
315 case Nil{}:
316 out
317 case Con{Node{syntax, name, span, +kids, facts}, rest}:
318 +node = {Node{syntax, name, span, kids, facts}: Node}
319 +path = Above.of(parent, at, up)
320 visit.go(
321 ~C,
322 ~A,
323 ~f,
324 rest,
325 c,
326 up,
327 parent,
328 (at + 1: U32),
329 visit.go(~C, ~A, ~f, kids, c, path, Some{node}, 0, Lists.onto(&2, A, f(c, path, node), out))
330 )
331
332# `f(c, path, node)` for each node of `nodes` and under them, parents first, in order: `path` holds the nodes above the
333# node, innermost first.
334def visit(
335 ~C: Data,
336 ~A: Data,
337 ~f: @+c: C -> @+path: List<&2, Above> -> @+node: Node -> List<&2, A>,
338 c: C,
339 nodes: List<&2, Node>
340) -> List<&2, A>:
341 List.reverse(&2, A, visit.go(~C, ~A, ~f, nodes, c, [], None{}, 0, []))
342
343# `f(c, node, s)` for each node of `nodes` and under them, parents first, in order, from `s`.
344def fold(
345 ~C: Data,
346 ~S: Data,
347 ~f: @+c: C -> @+node: Node -> S -> S,
348 +c: C,
349 nodes: List<&2, Node>,
350 s: S
351) -> S:
352 match nodes:
353 case Nil{}:
354 s
355 case Con{Node{syntax, name, span, +kids, facts}, rest}:
356 fold(
357 ~C,
358 ~S,
359 ~f,
360 c,
361 rest,
362 fold(~C, ~S, ~f, c, kids, f(c, Node{syntax, name, span, kids, facts}, s))
363 )
364
365# The top-level declaration a node is in: the outermost node above it, or the node itself.
366def top(path: List<&2, Above>, node: Node) -> Node:
367 match path:
368 case Nil{}:
369 node
370 case Con{Above{n, at}, Nil{}}:
371 n
372 case Con{a, rest}:
373 top(rest, node)
374
375def calls(called: String, owner: Node) -> Bool:
376 match owner:
377 case Node{Definition{declared, u}, n, s, k, f}:
378 String.eq(called, declared)
379 case _:
380 False{}
381
382# Whether a node is an application of the definition it is in, below `path`: a step of a loop, as Bend repeats work by
383# recursion.
384def is_recursive(path: List<&2, Above>, +node: Node) -> Bool:
385 match node:
386 case Node{Application{}, n, s, Con{Node{Reference{called}, rn, rs, rk, rf}, args}, f}:
387 calls(called, top(path, node))
388 case _:
389 False{}
390
391# Whether an application's function is Pair: it builds a pair type (`A & B`), whose parts are types.
392def is_pair(kids: List<&2, Node>) -> Bool:
393 match kids:
394 case Con{Node{Reference{t}, n, s, k, f}, rest}:
395 String.eq(t, "Pair")
396 case _:
397 False{}
398
399def is_live.go(path: List<&2, Above>, ok: Bool) -> Bool:
400 match path ok:
401 case _ False{}:
402 False{}
403 case Nil{} True{}:
404 False{}
405 case Con{Above{Node{Body{}, n, s, k, f}, at}, rest} True{}:
406 True{}
407 case Con{Above{Node{Annotation{}, n, s, k, f}, at}, rest} True{}:
408 is_live.go(rest, U32.is_eq(at, 0))
409 case Con{Above{Node{Application{}, n, s, k, f}, at}, rest} True{}:
410 is_live.go(rest, Bool.not(is_pair(k)))
411 case Con{Above{Node{Equality{}, n, s, k, f}, at}, rest} True{}:
412 False{}
413 case Con{Above{Node{Forall{b, q}, n, s, k, f}, at}, rest} True{}:
414 False{}
415 case Con{Above{Node{TypeApplication{t}, n, s, k, f}, at}, rest} True{}:
416 False{}
417 case Con{a, rest} True{}:
418 is_live.go(rest, True{})
419
420# Whether a node below `path` is in live code: a definition's body, outside types: an annotation's type, an equality, a
421# function or pair type, a type's arguments. Types and equations are dead: the checker sees them, the program does not
422# run them.
423def is_live(path: List<&2, Above>) -> Bool:
424 is_live.go(path, True{})
425
426# The definitions of `nodes`, by the name the check gives them: read one with `Names.find`. Of two with one name, the
427# later is kept.
428def definitions(nodes: List<&2, Node>, out: Map<&2, Maybe<&2, Node>>) -> Map<&2, Maybe<&2, Node>>:
429 match nodes:
430 case Nil{}:
431 out
432 case Con{Node{Definition{+t, u}, n, s, k, f}, rest}:
433 definitions(
434 rest,
435 Map.set(&2, Maybe<&2, Node>, out, t, Some{Node{Definition{t, u}, n, s, k, f}})
436 )
437 case Con{node, rest}:
438 definitions(rest, out)
439
440def parameter.go(
441 nodes: List<&2, Node>,
442 found: Maybe<&2, Nat>,
443 +binder: U32,
444 +at: Nat
445) -> Maybe<&2, Nat>:
446 match nodes found:
447 case _ Some{n}:
448 Some{n}
449 case Nil{} None{}:
450 None{}
451 case Con{Node{Parameter{b, q}, n, s, k, f}, rest} None{}:
452 parameter.go(rest, Lists.when(Nat, U32.is_eq(b, binder), at), binder, 1n+at)
453 case Con{node, rest} None{}:
454 parameter.go(rest, None{}, binder, at)
455
456# Where the parameter that declares `binder` is among `nodes`, a definition's, counting from 0.
457def parameter(nodes: List<&2, Node>, binder: U32) -> Maybe<&2, Nat>:
458 parameter.go(nodes, None{}, binder, 0n)
459
460# Rules
461# =====
462type Severity is Data:
463 Error{}
464 Warning{}
465 Information{}
466 Hint{}
467
468def Severity.show(s: Severity) -> String:
469 match s:
470 case Error{}:
471 "error"
472 case Warning{}:
473 "warning"
474 case Information{}:
475 "information"
476 case Hint{}:
477 "hint"
478
479def Severity.names() -> List<&2, Names.Named<Severity>>:
480 Names.table(~Severity, ~Severity.show, [Error{}, Warning{}, Information{}, Hint{}])
481
482# An edit a fix asks for: replace a span's text; rename what the declaration written at `at` declares, with each of its
483# uses; or rename only its uses, to point them at a name the program declares already (to drop a duplicate import,
484# say). A rename changes an import's alias, the first part of each use (`U` of `U.two`), and any other name's last part.
485# The linter finds the uses, and drops the fix if the text does not write the name where one of them is. It drops a
486# Rename of a global name (a def, type, constructor or law), as files the check did not read can use it, and one whose
487# new name is taken where the declaration is.
488type Operation is Data:
489 Replace{span: Span, text: String}
490 Rename{at: Span, to: String}
491 RenameUses{at: Span, to: String}
492
493# A way to fix a finding: what it does, and its operations, in any of the program's own files (not Base, nor a hub
494# package).
495type Fix is Data:
496 Fix{title: String, operations: List<&2, Operation>}
497
498type Finding is Data:
499 Finding{severity: Severity, span: Span, message: String, fixes: List<&2, Fix>}
500
501type Found is Data:
502 Found{rule: String, finding: Finding}
503
504# A finding at `span`, if `hit` and `span` is known.
505def finding(
506 severity: Severity,
507 hit: Bool,
508 span: Maybe<&2, Span>,
509 text: String
510) -> List<&2, Finding>:
511 match hit span:
512 case True{} Some{s}:
513 [Finding{severity, s, text, []}]
514 case _ _:
515 []
516
517# Options
518# =======
519type Value is Data:
520 Num{n: U32}
521 Flag{on: Bool}
522 Text{text: String}
523
524# What an option accepts: a whole number in a range, a flag, text (one of `choices`, unless there are none), or what
525# one of `specs` accepts.
526type Spec is Data:
527 NumberOption{min: U32, max: U32}
528 FlagOption{}
529 TextOption{choices: List<&2, String>}
530 AnyOption{specs: List<&2, Spec>}
531
532# An option a rule declares: its name, its value when the config gives none, and what it accepts. The config gives
533# values as `"rule/id": {"name": value}`; a name the rule does not declare, or a value it does not accept, is an error.
534type Declared is Data:
535 Declared{name: String, default: Value, spec: Spec}
536
537# An option's value as a number, a flag or text; a value of another kind, or none, gives 0, False, "".
538def Value.number(value: Maybe<&2, Value>) -> U32:
539 match value:
540 case Some{Num{n}}:
541 n
542 case _:
543 0
544
545def Value.flag(value: Maybe<&2, Value>) -> Bool:
546 match value:
547 case Some{Flag{on}}:
548 on
549 case _:
550 False{}
551
552def Value.text(value: Maybe<&2, Value>) -> String:
553 match value:
554 case Some{Text{text}}:
555 text
556 case _:
557 ""
558
559# Declarations
560# ============
561
562# What uses a file's imports: the nodes written with an alias's prefix (`U.two`, a fill `def U.law(x):`), by alias; and
563# those that use Base: a global name with no namespace that the file does not declare (last first).
564type Imported is Data:
565 Imported{aliases: Map<&2, List<&2, Node>>, base: List<&2, Node>}
566
567# What the declarations of a top-level declaration are read with: the program's files (one of them is what an import
568# loads), the uses of global names in the files the declarations are read in, by name, the uses of the declaration's
569# binders, by binder (each last first), and what uses its file's imports.
570type Uses is Data:
571 Uses{
572 sources: List<&2, Source>,
573 globals: Map<&2, List<&2, Node>>,
574 binders: Tables.Table<List<&2, Node>>,
575 imported: Imported
576 }
577
578def Uses.global.add(
579 used: Maybe<&2, String>,
580 node: Node,
581 m: Map<&2, List<&2, Node>>
582) -> Map<&2, List<&2, Node>>:
583 match used:
584 case Some{t}:
585 Names.Group.add(Node, m, t, node)
586 case None{}:
587 m
588
589def Uses.global(+u: Unit, +node: Node, m: Map<&2, List<&2, Node>>) -> Map<&2, List<&2, Node>>:
590 Uses.global.add(Syntax.used(Node.syntax(node)), node, m)
591
592def Uses.binder.add(
593 +t: Tables.Table<List<&2, Node>>,
594 +b: U32,
595 node: Node
596) -> Tables.Table<List<&2, Node>>:
597 Tables.Table.set(
598 List<&2, Node>,
599 t,
600 b,
601 node <> Maybe.default(&2, List<&2, Node>, Tables.Table.get(List<&2, Node>, t, b), [])
602 )
603
604def Uses.binder(
605 +u: Unit,
606 +node: Node,
607 t: Tables.Table<List<&2, Node>>
608) -> Tables.Table<List<&2, Node>>:
609 match node:
610 case Node{Variable{b}, n, s, k, f}:
611 Uses.binder.add(t, b, node)
612 case _:
613 t
614
615def Imported.own.add(target: Maybe<&2, String>, out: Set()) -> Set():
616 match target:
617 case Some{t}:
618 Set.add(out, t)
619 case None{}:
620 out
621
622# The global names a file's own top-level declarations declare, as a set.
623def Imported.own(nodes: List<&2, Node>, out: Set()) -> Set():
624 match nodes:
625 case Nil{}:
626 out
627 case Con{Node{syntax, n, s, k, f}, rest}:
628 Imported.own(rest, Imported.own.add(Syntax.target(syntax), out))
629
630def Imported.is_base(own: Set(), used: Maybe<&2, String>) -> Bool:
631 match used:
632 case Some{+name}:
633 String.is_empty(Name.namespace(name)) && Bool.not(Pair.snd(Set(), Bool, Set.has(own, name)))
634 case None{}:
635 False{}
636
637def Imported.alias(
638 prefix: String,
639 node: Node,
640 aliases: Map<&2, List<&2, Node>>
641) -> Map<&2, List<&2, Node>>:
642 match prefix:
643 case SNil{}:
644 aliases
645 case SCon{h, t}:
646 Names.Group.add(Node, aliases, SCon{h, t}, node)
647
648def Imported.add(+own: Set(), +node: Node, uses: Imported) -> Imported:
649 match node uses:
650 case Node{syntax, name, s, k, f} Imported{aliases, base}:
651 Imported{
652 Imported.alias(Strings.before(name, '.'), node, aliases),
653 Lists.push(Node, Lists.when(Node, Imported.is_base(own, Syntax.used(syntax)), node), base)
654 }
655
656def Imported.of(+nodes: List<&2, Node>) -> Imported:
657 fold(
658 ~Set(),
659 ~Imported,
660 ~Imported.add,
661 Imported.own(nodes, Set.new()),
662 nodes,
663 Imported{Map.new(&2, List<&2, Node>), []}
664 )
665
666# The namespace of the file at `path`, as the check names it (`found`, once found): "" for Base, or a file the check
667# did not parse.
668def Declarations.namespace(
669 sources: List<&2, Source>,
670 +path: String,
671 found: Maybe<&2, String>
672) -> String:
673 match sources found:
674 case _ Some{namespace}:
675 namespace
676 case Nil{} None{}:
677 ""
678 case Con{Source{p, namespace, text, nodes}, rest} None{}:
679 Declarations.namespace(rest, path, Lists.when(String, String.eq(p, path), namespace))
680
681# The uses of an import, in order: of Base (`base`), or of its alias.
682def Declarations.imported(base: Bool, alias: String, imported: Imported) -> List<&2, Node>:
683 match base imported:
684 case True{} Imported{aliases, uses}:
685 List.reverse(&2, Node, uses)
686 case False{} Imported{aliases, uses}:
687 Names.Group.get(Node, aliases, alias)
688
689def Declarations.bound(
690 binder: Maybe<&2, U32>,
691 binders: Tables.Table<List<&2, Node>>
692) -> List<&2, Node>:
693 match binder:
694 case Some{b}:
695 List.reverse(
696 &2,
697 Node,
698 Maybe.default(&2, List<&2, Node>, Tables.Table.get(List<&2, Node>, binders, b), [])
699 )
700 case None{}:
701 []
702
703def Declarations.declared(
704 declares: Maybe<&2, Bool>,
705 +node: Node,
706 uses: Uses
707) -> List<&2, Declaration>:
708 match declares node uses:
709 case Some{True{}} _ Uses{sources, globals, binders, imported}:
710 [Declaration{node, Names.Group.get(Node, globals, Node.target(node))}]
711 case Some{False{}} Node{syntax, name, s, k, f} Uses{sources, globals, binders, imported}:
712 Bool.pick(
713 List<&2, Declaration>,
714 String.eq(name, "_"),
715 [],
716 [Declaration{node, Declarations.bound(Syntax.binder(syntax), binders)}]
717 )
718 case _ _ _:
719 []
720
721# A node's declaration, if it declares a name, with its uses, onto `out`.
722def Declarations.node(
723 +uses: Uses,
724 +node: Node,
725 out: List<&2, Declaration>
726) -> List<&2, Declaration>:
727 match uses node:
728 case Uses{sources, globals, binders, imported} Node{Import{t}, name, s, k, f}:
729 Declaration{
730 node,
731 Declarations.imported(
732 String.is_empty(Declarations.namespace(sources, t, None{})),
733 name,
734 imported
735 )
736 }
737 <> out
738 case _ _:
739 Lists.onto(
740 &2,
741 Declaration,
742 Declarations.declared(Syntax.declares(Node.syntax(node)), node, uses),
743 out
744 )
745
746def Declarations.tops(
747 nodes: List<&2, Node>,
748 +sources: List<&2, Source>,
749 +globals: Map<&2, List<&2, Node>>,
750 +imported: Imported,
751 out: List<&2, Declaration>
752) -> List<&2, Declaration>:
753 match nodes:
754 case Nil{}:
755 out
756 case Con{+top, rest}:
757 Declarations.tops(
758 rest,
759 sources,
760 globals,
761 imported,
762 fold(
763 ~Uses,
764 ~List<&2, Declaration>,
765 ~Declarations.node,
766 Uses{
767 sources,
768 globals,
769 fold(
770 ~Unit,
771 ~Tables.Table<List<&2, Node>>,
772 ~Uses.binder,
773 Unit{},
774 [top],
775 Tables.TLeaf{None{}}
776 ),
777 imported
778 },
779 [top],
780 out
781 )
782 )
783
784def Declarations.files(
785 files: List<&2, Source>,
786 +sources: List<&2, Source>,
787 +globals: Map<&2, List<&2, Node>>,
788 out: List<&2, Declaration>
789) -> List<&2, Declaration>:
790 match files:
791 case Nil{}:
792 out
793 case Con{Source{path, namespace, text, +nodes}, rest}:
794 Declarations.files(
795 rest,
796 sources,
797 globals,
798 Declarations.tops(nodes, sources, globals, Imported.of(nodes), out)
799 )
800
801def Declarations.globals(
802 files: List<&2, Source>,
803 m: Map<&2, List<&2, Node>>
804) -> Map<&2, List<&2, Node>>:
805 match files:
806 case Nil{}:
807 m
808 case Con{Source{path, namespace, text, nodes}, rest}:
809 Declarations.globals(
810 rest,
811 fold(~Unit, ~Map<&2, List<&2, Node>>, ~Uses.global, Unit{}, nodes, m)
812 )
813
814# The declarations of `files`, in order, with their uses in `files`; `sources` are the program's files.
815def Declarations.of(+files: List<&2, Source>, sources: List<&2, Source>) -> List<&2, Declaration>:
816 List.reverse(
817 &2,
818 Declaration,
819 Declarations.files(files, sources, Declarations.globals(files, Map.new(&2, List<&2, Node>)), [])
820 )
821
822def Declarations.when(
823 declare: Bool,
824 files: List<&2, Source>,
825 sources: List<&2, Source>
826) -> List<&2, Declaration>:
827 match declare:
828 case True{}:
829 Declarations.of(files, sources)
830 case False{}:
831 []
832
833def Source.is_own(source: Source) -> Bool:
834 match source:
835 case Source{path, namespace, text, nodes}:
836 Bool.not(String.starts_with(namespace, "0x"))
837
838# The program's own files: not hub packages.
839def Program.own(sources: List<&2, Source>) -> List<&2, Source>:
840 List.filter(~Source, ~Source.is_own, sources)
841
842# What a file rule sees: the program, from one of its files; that file's declarations, with their uses in it, if a rule
843# needs them; and the rule's options, each declared one with its value.
844type Here is Data:
845 Here{
846 program: Program,
847 source: Source,
848 declarations: List<&2, Declaration>,
849 options: List<&2, Names.Named<Value>>
850 }
851
852# What a program rule sees: the program (its files, hub packages aside); every declaration of its files, with their
853# uses in all of them, if a rule needs them; and the rule's options.
854type Whole is Data:
855 Whole{
856 program: Program,
857 declarations: List<&2, Declaration>,
858 options: List<&2, Names.Named<Value>>
859 }
860
861# The program from one of its files, built once for every file rule that runs on that file: its declarations, if a rule
862# needs them (`declare`). The runner gives each rule its options.
863def Here.of(program: Program, +source: Source, declare: Bool) -> Here:
864 match program:
865 case Program{+sources}:
866 Here{Program{sources}, source, Declarations.when(declare, [source], sources), []}
867
868# The whole program, built once for every program rule: the declarations of its own files, if a rule needs them
869# (`declare`).
870def Whole.of(program: Program, declare: Bool) -> Whole:
871 match program:
872 case Program{sources}:
873 +own = Program.own(sources)
874 Whole{Program{own}, Declarations.when(declare, own, own), []}
875
876def Here.path(here: Here) -> String:
877 match here:
878 case Here{program, Source{path, namespace, text, nodes}, declarations, options}:
879 path
880
881# "" for the checked file.
882def Here.namespace(here: Here) -> String:
883 match here:
884 case Here{program, Source{path, namespace, text, nodes}, declarations, options}:
885 namespace
886
887def Here.text(here: Here) -> String:
888 match here:
889 case Here{program, Source{path, namespace, text, nodes}, declarations, options}:
890 text
891
892# The file's nodes: its imports, then its declarations.
893def Here.nodes(here: Here) -> List<&2, Node>:
894 match here:
895 case Here{program, Source{path, namespace, text, nodes}, declarations, options}:
896 nodes
897
898# Every file of the check, hub packages too.
899def Here.sources(here: Here) -> List<&2, Source>:
900 match here:
901 case Here{Program{sources}, source, declarations, options}:
902 sources
903
904def Here.declarations(here: Here) -> List<&2, Declaration>:
905 match here:
906 case Here{program, source, declarations, options}:
907 declarations
908
909# The config's value, or the default.
910def Here.option(here: Here, name: String) -> Maybe<&2, Value>:
911 match here:
912 case Here{program, source, declarations, options}:
913 Names.lookup(Value, name, options)
914
915def Whole.declarations(whole: Whole) -> List<&2, Declaration>:
916 match whole:
917 case Whole{program, declarations, options}:
918 declarations
919
920def Whole.sources(whole: Whole) -> List<&2, Source>:
921 match whole:
922 case Whole{Program{sources}, declarations, options}:
923 sources
924
925def Whole.option(whole: Whole, name: String) -> Maybe<&2, Value>:
926 match whole:
927 case Whole{program, declarations, options}:
928 Names.lookup(Value, name, options)
929
930# Asking the checker
931# ==================
932
933# Show spells a type as its file does; Same compares as the checker does.
934type Question is Data:
935 Show{of: TypeRef}
936 Same{a: TypeRef, b: TypeRef}
937 Normal{of: TypeRef}
938
939type Answer is Data:
940 Shown{text: String}
941 Equal{same: Bool}
942 Normalized{handle: U32}
943
944# A run so far: finished, or waiting for the answers to its questions, in order.
945type Step<-R: Type> is Type:
946 Finished{value: R}
947 Pending{questions: List<&2, Question>, then: List<&2, Answer> -> Step<R>}
948
949# A computation that may ask the checker, in `do Lint.Ask<A>:` blocks. Continuation-passing, so binding needs no
950# recursion. A run may ask only cli.bend's `budget()` rounds, so ask for everything at once (show_all).
951def Ask(-A: Type) -> Type:
952 @-R: Type -> @k: (A -> Step<R>) -> Step<R>
953
954def Ask.pure(-A: Type, x: A) -> Ask(A):
955 R => k => k(x)
956
957def Ask.bind(-A: Type, -B: Type, m: Ask(A), f: A -> Ask(B)) -> Ask(B):
958 R => k => m(R, x => f(x, R, k))
959
960def ask.step(-R: Type, questions: List<&2, Question>, k: List<&2, Answer> -> Step<R>) -> Step<R>:
961 match questions:
962 case Nil{}:
963 k([])
964 case Con{q, rest}:
965 Pending{Con{q, rest}, k}
966
967# The answers to `questions`, in order, asked in one round; none asked, no round.
968def ask(questions: List<&2, Question>) -> Ask(List<&2, Answer>):
969 R => k => ask.step(R, questions, k)
970
971def done(findings: List<&2, Finding>) -> Ask(List<&2, Finding>):
972 Ask.pure(List<&2, Finding>, findings)
973
974def Answer.text(answers: List<&2, Answer>) -> String:
975 match answers:
976 case Con{Shown{text}, rest}:
977 text
978 case _:
979 ""
980
981def Answer.same(answers: List<&2, Answer>) -> Bool:
982 match answers:
983 case Con{Equal{same}, rest}:
984 same
985 case _:
986 False{}
987
988# `t` with the handle of its normal form, if the answers give one.
989def Answer.type(t: TypeRef, answers: List<&2, Answer>) -> TypeRef:
990 match t answers:
991 case TypeRef{check, handle} Con{Normalized{h}, rest}:
992 TypeRef{check, h}
993 case _ _:
994 t
995
996def show(t: TypeRef) -> Ask(String):
997 Ask.bind(
998 List<&2, Answer>,
999 String,
1000 ask([Show{t}]),
1001 answers => Ask.pure(String, Answer.text(answers))
1002 )
1003
1004def same(a: TypeRef, b: TypeRef) -> Ask(Bool):
1005 Ask.bind(
1006 List<&2, Answer>,
1007 Bool,
1008 ask([Same{a, b}]),
1009 answers => Ask.pure(Bool, Answer.same(answers))
1010 )
1011
1012def normal(+t: TypeRef) -> Ask(TypeRef):
1013 Ask.bind(
1014 List<&2, Answer>,
1015 TypeRef,
1016 ask([Normal{t}]),
1017 answers => Ask.pure(TypeRef, Answer.type(t, answers))
1018 )
1019
1020def Question.shows(types: List<&2, TypeRef>, out: List<&2, Question>) -> List<&2, Question>:
1021 match types:
1022 case Nil{}:
1023 List.reverse(&2, Question, out)
1024 case Con{t, rest}:
1025 Question.shows(rest, Show{t} <> out)
1026
1027def Answer.texts(answers: List<&2, Answer>, out: List<&2, String>) -> List<&2, String>:
1028 match answers:
1029 case Nil{}:
1030 List.reverse(&2, String, out)
1031 case Con{Shown{text}, rest}:
1032 Answer.texts(rest, text <> out)
1033 case Con{a, rest}:
1034 Answer.texts(rest, "" <> out)
1035
1036# How each type of `types` is shown, in order, asked in one round.
1037def show_all(types: List<&2, TypeRef>) -> Ask(List<&2, String>):
1038 Ask.bind(
1039 List<&2, Answer>,
1040 List<&2, String>,
1041 ask(Question.shows(types, [])),
1042 answers => Ask.pure(List<&2, String>, Answer.texts(answers, []))
1043 )
1044
1045# What a rule needs collected for it, as each costs time and memory: the checker's facts, and the declarations with
1046# their uses. A rule that does not ask for them gets none.
1047type Needs is Data:
1048 Needs{facts: Bool, declarations: Bool}
1049
1050# How a rule runs: once per linted file, reporting only in it; or once per check, on the whole program, reporting in any
1051# file (what it finds in a file that is not linted is dropped). When several entries check the named file, a program
1052# rule's finding stays if some check finds it, or, if `every`, if every check finds it; then, if an entry that reads the
1053# named file fails its check, the rule does not run.
1054type Run is Type:
1055 OnFile{run: @+here: Here -> Ask(List<&2, Finding>)}
1056 OnProgram{every: Bool, run: @+whole: Whole -> Ask(List<&2, Finding>)}
1057
1058# A rule: what it needs, the options it declares, and how it runs. Its id is its path in bend-lint-rules/, without
1059# .bend, as bend-lint.json names it.
1060type Rule is Type:
1061 Rule{needs: Needs, options: List<&2, Declared>, run: Run}