linter/lint.bend

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