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.
14	import Base
15	import ../shared/lists.bend as Lists
16	import ../shared/names.bend as Names
17	import ../shared/strings.bend as Strings
18	import ../shared/tables.bend as Tables
19	
20	# Program
21	# =======
22	type Quantity is Data:
23	  Erased{}
24	  Once{}
25	  Many{}
26	  Template{}
27	
28	# Where something is: its file, and offsets in code points.
29	type 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?`).
37	type 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.
78	type 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).
83	type 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.
93	type 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.
99	type 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.
110	type Source is Data:
111	  Source{path: String, namespace: String, text: String, nodes: List<&2, Node>}
112	
113	type Program is Data:
114	  Program{sources: List<&2, Source>}
115	
116	# A name a node declares, and the nodes that use it, in order.
117	type 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).
121	def 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.
149	def 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.
167	def 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).
188	def 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	
213	def 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.
219	def 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	
224	def 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.
230	def 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	
237	def 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	
244	def 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.
252	def 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.
257	def 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	
264	def 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.
274	def 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`.
278	def 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.
293	type Above is Data:
294	  Above{node: Node, at: U32}
295	
296	def 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	
303	def 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.
334	def 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`.
344	def 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.
366	def 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	
375	def 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.
384	def 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.
392	def 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	
399	def 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.
423	def 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.
428	def 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	
440	def 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.
457	def parameter(nodes: List<&2, Node>, binder: U32) -> Maybe<&2, Nat>:
458	  parameter.go(nodes, None{}, binder, 0n)
459	
460	# Rules
461	# =====
462	type Severity is Data:
463	  Error{}
464	  Warning{}
465	  Information{}
466	  Hint{}
467	
468	def 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	
479	def 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.
488	type 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).
495	type Fix is Data:
496	  Fix{title: String, operations: List<&2, Operation>}
497	
498	type Finding is Data:
499	  Finding{severity: Severity, span: Span, message: String, fixes: List<&2, Fix>}
500	
501	type Found is Data:
502	  Found{rule: String, finding: Finding}
503	
504	# A finding at `span`, if `hit` and `span` is known.
505	def 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	# =======
519	type Value is Data:
520	  Num{n: U32}
521	  Flag{on: Bool}
522	  Chars{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.
526	type 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.
534	type 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, "".
538	def Value.number(value: Maybe<&2, Value>) -> U32:
539	  match value:
540	    case Some{Num{n}}:
541	      n
542	    case _:
543	      0
544	
545	def Value.flag(value: Maybe<&2, Value>) -> Bool:
546	  match value:
547	    case Some{Flag{on}}:
548	      on
549	    case _:
550	      False{}
551	
552	def Value.text(value: Maybe<&2, Value>) -> String:
553	  match value:
554	    case Some{Chars{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).
564	type 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.
570	type 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	
578	def 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	
589	def 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	
592	def 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	
604	def 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	
615	def 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.
623	def 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	
630	def 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	
637	def 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	
648	def 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	
656	def 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.
668	def 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.
682	def 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	
689	def 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	
703	def 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`.
722	def 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	
746	def 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	
784	def 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	
801	def 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.
815	def 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	
822	def 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	
833	def 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.
839	def 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.
844	type 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.
854	type 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.
863	def 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`).
870	def 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	
876	def 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.
882	def Here.namespace(here: Here) -> String:
883	  match here:
884	    case Here{program, Source{path, namespace, text, nodes}, declarations, options}:
885	      namespace
886	
887	def 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.
893	def 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.
899	def Here.sources(here: Here) -> List<&2, Source>:
900	  match here:
901	    case Here{Program{sources}, source, declarations, options}:
902	      sources
903	
904	def 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.
910	def 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	
915	def Whole.declarations(whole: Whole) -> List<&2, Declaration>:
916	  match whole:
917	    case Whole{program, declarations, options}:
918	      declarations
919	
920	def Whole.sources(whole: Whole) -> List<&2, Source>:
921	  match whole:
922	    case Whole{Program{sources}, declarations, options}:
923	      sources
924	
925	def 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.
934	type Question is Data:
935	  Show{of: TypeRef}
936	  Same{a: TypeRef, b: TypeRef}
937	  Normal{of: TypeRef}
938	
939	type 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.
945	type 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).
951	def Ask(-A: Type) -> Type:
952	  @-R: Type -> @k: (A -> Step<R>) -> Step<R>
953	
954	def Ask.pure(-A: Type, x: A) -> Ask(A):
955	  R => k => k(x)
956	
957	def 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	
960	def 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.
968	def ask(questions: List<&2, Question>) -> Ask(List<&2, Answer>):
969	  R => k => ask.step(R, questions, k)
970	
971	def done(findings: List<&2, Finding>) -> Ask(List<&2, Finding>):
972	  Ask.pure(List<&2, Finding>, findings)
973	
974	def Answer.text(answers: List<&2, Answer>) -> String:
975	  match answers:
976	    case Con{Shown{text}, rest}:
977	      text
978	    case _:
979	      ""
980	
981	def 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.
989	def 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	
996	def 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	
1004	def 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	
1012	def 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	
1020	def 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	
1027	def 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.
1037	def 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.
1047	type 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.
1054	type 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.
1060	type Rule is Type:
1061	  Rule{needs: Needs, options: List<&2, Declared>, run: Run}