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/sets.bend as Sets
18	import ../shared/strings.bend as Strings
19	import ../shared/tables.bend as Tables
20	
21	# Program
22	# =======
23	type Quantity is Data:
24	  Erased{}
25	  Once{}
26	  Many{}
27	  Template{}
28	
29	# Where something is: its file, and offsets in code points.
30	type 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?`).
38	type 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.
79	type 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).
84	type 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.
94	type 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.
100	type 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.
111	type Source is Data:
112	  Source{path: String, namespace: String, text: String, nodes: List<&2, Node>}
113	
114	type Program is Data:
115	  Program{sources: List<&2, Source>}
116	
117	# A name a node declares, and the nodes that use it, in order.
118	type 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).
122	def 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.
150	def 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.
168	def 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).
189	def 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	
214	def 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.
220	def 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	
225	def 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.
231	def 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	
238	def 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	
245	def 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.
253	def 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.
258	def 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	
265	def 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.
275	def 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`.
279	def 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.
294	type Above is Data:
295	  Above{node: Node, at: U32}
296	
297	def 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	
304	def 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.
335	def 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`.
345	def 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.
367	def 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	
376	def 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.
385	def 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.
393	def 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	
400	def 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.
424	def 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.
429	def 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	
441	def 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.
458	def parameter(nodes: List<&2, Node>, binder: U32) -> Maybe<&2, Nat>:
459	  parameter.go(nodes, None{}, binder, 0n)
460	
461	# Rules
462	# =====
463	type Severity is Data:
464	  Error{}
465	  Warning{}
466	  Information{}
467	  Hint{}
468	
469	def 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	
480	def 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.
489	type 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).
496	type Fix is Data:
497	  Fix{title: String, operations: List<&2, Operation>}
498	
499	type Finding is Data:
500	  Finding{severity: Severity, span: Span, message: String, fixes: List<&2, Fix>}
501	
502	type Found is Data:
503	  Found{rule: String, finding: Finding}
504	
505	# A finding at `span`, if `hit` and `span` is known.
506	def 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	# =======
520	type 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.
527	type 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.
535	type 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, "".
539	def Value.number(value: Maybe<&2, Value>) -> U32:
540	  match value:
541	    case Some{Num{n}}:
542	      n
543	    case _:
544	      0
545	
546	def Value.flag(value: Maybe<&2, Value>) -> Bool:
547	  match value:
548	    case Some{Flag{on}}:
549	      on
550	    case _:
551	      False{}
552	
553	def 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).
565	type 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.
571	type 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	
579	def 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	
590	def 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	
593	def 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	
605	def 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	
616	def 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.
624	def 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	
631	def 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	
638	def 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	
649	def 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	
657	def 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.
669	def 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.
683	def 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	
690	def 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	
704	def 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`.
723	def 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	
747	def 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	
785	def 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	
802	def 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.
816	def 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	
823	def 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	
834	def 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.
840	def 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).
847	type 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).
852	type 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).
862	def 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.
870	def 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`.
880	def 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`.
893	def 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.
917	def 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 "".
925	def 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	
934	def 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`.
942	def 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`.
972	def 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	
982	def 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.
990	def 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.
998	def 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	
1011	def 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.
1023	def 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.
1043	def 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.
1052	type 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.
1062	type 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.
1071	def 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`).
1078	def 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	
1084	def 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.
1090	def Here.namespace(here: Here) -> String:
1091	  match here:
1092	    case Here{program, Source{path, namespace, text, nodes}, declarations, options}:
1093	      namespace
1094	
1095	def 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.
1101	def 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.
1107	def Here.sources(here: Here) -> List<&2, Source>:
1108	  match here:
1109	    case Here{Program{sources}, source, declarations, options}:
1110	      sources
1111	
1112	def 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.
1118	def 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	
1123	def Whole.declarations(whole: Whole) -> List<&2, Declaration>:
1124	  match whole:
1125	    case Whole{program, declarations, options}:
1126	      declarations
1127	
1128	def Whole.sources(whole: Whole) -> List<&2, Source>:
1129	  match whole:
1130	    case Whole{Program{sources}, declarations, options}:
1131	      sources
1132	
1133	def 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.
1142	type Question is Data:
1143	  Show{of: TypeRef}
1144	  Same{a: TypeRef, b: TypeRef}
1145	  Normal{of: TypeRef}
1146	
1147	type 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.
1153	type 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).
1159	def Ask(-A: Type) -> Type:
1160	  @-R: Type -> @k: (A -> Step<R>) -> Step<R>
1161	
1162	def Ask.pure(-A: Type, x: A) -> Ask(A):
1163	  R => k => k(x)
1164	
1165	def 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	
1168	def 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.
1176	def ask(questions: List<&2, Question>) -> Ask(List<&2, Answer>):
1177	  R => k => ask.step(R, questions, k)
1178	
1179	def done(findings: List<&2, Finding>) -> Ask(List<&2, Finding>):
1180	  Ask.pure(List<&2, Finding>, findings)
1181	
1182	def Answer.text(answers: List<&2, Answer>) -> String:
1183	  match answers:
1184	    case Con{Shown{text}, rest}:
1185	      text
1186	    case _:
1187	      ""
1188	
1189	def 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.
1197	def 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	
1204	def 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	
1212	def 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	
1220	def 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	
1228	def 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	
1235	def 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.
1245	def 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.
1255	type 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.
1262	type 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.
1268	type Rule is Type:
1269	  Rule{needs: Needs, options: List<&2, Declared>, run: Run}