git » blacktide.git » commit 1e1e3a3

diff --git a/README.md b/README.md
index 4db2cb0..b72fcbf 100644
--- a/README.md
+++ b/README.md
@@ -4,9 +4,10 @@
 
 # Blacktide
 
-A Clojure-to-Clojure compiler library. Its `loophole` macro provides mutable
-lexical locals and explicit jumps for algorithmic code. It compiles to ordinary
-Clojure, without mutable cells or a runtime interpreter for local state.
+Blacktide is a Clojure-to-Clojure compiler library. Its `loophole` macro adds
+mutable lexical locals and explicit jumps within a bounded region of code.
+It compiles that region to ordinary Clojure, without mutable cells or an
+interpreter for local state.
 
 ```clojure
 (require '[com.tailrecursion.blacktide :refer [loophole setq psetq label goto]])
@@ -23,53 +24,67 @@ Clojure, without mutable cells or a runtime interpreter for local state.
   [(setq x (+ x 10)) y]) ; => [12 1]
 ```
 
-`setq` assigns pairs sequentially and returns the last value. `psetq` evaluates
-all right-hand sides before assigning and returns nil. Both work in expressions.
-Labels belong to the outer statement sequence; jumps can leave nested statement
-bodies. Every jump requires an explicit label.
+Both assignment forms work in expressions:
 
-The region supports `let`, destructuring, `if`, `case`, `loop`/`recur`, calls,
-collections and Java interop. Ordinary macros such as `when`, `cond`, `dotimes`
-and `doseq` work through expansion. Define functions and protect resources
-outside the region. Functions, `letfn`, `try`, native `set!` and nested `loophole`
-forms are rejected inside it, including through macroexpansion.
+| Form | Assignment order | Result |
+| --- | --- | --- |
+| `setq` | Evaluate and assign each pair in order. | Last value, or nil for no pairs. |
+| `psetq` | Evaluate all right-hand sides, then assign all targets, each in pair order. | nil |
 
-Read the [language reference](doc/language.md) for the exact boundary and
-[algorithm examples](examples/blacktide/algorithms.clj) for partitioning and parsing.
-This is a control-flow tool; it makes no general speedup guarantee.
+Labels belong to the region's outer statement sequence. Jumps can leave nested
+statement bodies, but every jump needs an explicit label.
+
+The region supports a defined subset of Clojure:
+
+- **Forms:** `let`, destructuring, `if`, `case`, `loop`/`recur`, calls,
+  collections and Java interop.
+- **Macros:** ordinary macros such as `when`, `cond`, `dotimes` and `doseq`,
+  provided their entire expansion uses supported forms.
+- **Exclusions:** function forms, `letfn`, `try`, native `set!` and nested
+  `loophole`. Define functions and manage resources outside the region.
+
+See the [language reference](doc/language.md) for the supported forms and their
+semantics. The [algorithm examples](examples/blacktide/algorithms.clj) show
+partitioning and parsing. Blacktide makes no general speedup guarantee.
 
 ## Use
 
-Requires Clojure 1.12.6 and JDK 17 or later. From a neighboring checkout:
+Requires Clojure 1.12.6 and JDK 17 or later. To use a neighboring checkout,
+add this dependency to your project's `deps.edn`:
 
 ```clojure
 {:deps {com.tailrecursion/blacktide {:local/root "../blacktide"}}}
 ```
 
 Run `clojure -X:deps prep` in the client project to compile the bundled JVM
-keyword-cache helper. Library JARs include it. Ordinary use depends only on
-Clojure; Typed Clojure checks compiler passes during development.
+keyword-cache helper. Library JARs already include the helper.
+
+Clojure is the only runtime dependency. Typed Clojure checks compiler passes
+during development.
 
 ## Develop
 
-```sh
-clojure -T:build compile-java # after checkout or changes to src-java
-clojure -M:test              # semantic, generative, differential and AOT tests
-clojure -M:check             # language contracts and production pass bodies
-bin/check                   # all of the above; accepts CLI -S options
-clojure -T:build jar         # target/blacktide-0.1.0-SNAPSHOT.jar
-```
+| Command | Purpose |
+| --- | --- |
+| `clojure -T:build compile-java` | Compile the Java helper after checkout or changes to `src-java`. |
+| `clojure -M:test` | Run semantic, generative, differential and AOT tests. |
+| `clojure -M:check` | Check language contracts and production pass bodies. |
+| `bin/check` | Run all three steps above; accepts CLI `-S` options. |
+| `clojure -T:build jar` | Build `target/blacktide-0.1.0-SNAPSHOT.jar`. |
 
 Select a JDK with `JAVA_CMD=/path/to/jdk/bin/java bin/check`. Development targets
-JDK 25/27; 17/21 are compatibility targets. Generators use `test.check`, fixed
-seeds and independent models; failures report their seed and shrunk input.
-Shrinking preserves lexical scope and iteration bounds. Focused regressions
-remain ordinary `clojure.test` examples.
-Forgejo CI tests all four JDKs, checks pass types on 25/27, and builds the JAR.
-
-Pass test namespace names to `clojure -M:test` for a targeted run. At a test REPL,
-call a `defspec` function with a trial count and `:seed` to explore or reproduce
-another run, for example `(generated-nested-loops 1000 :seed 161803)`.
+JDK 25/27; 17/21 are compatibility targets. Forgejo CI tests all four JDKs,
+checks pass types on 25/27, and builds the JAR.
+
+Generated tests use `test.check`, fixed seeds and independent models.
+Failures report the seed and shrunk input. Shrinking preserves lexical scope
+and iteration bounds. Focused regressions use ordinary `clojure.test` examples.
+
+To narrow or reproduce a test run:
+
+- Pass test namespace names to `clojure -M:test` for a targeted run.
+- At a test REPL, call a `defspec` function with a trial count and `:seed`,
+  for example `(generated-nested-loops 1000 :seed 161803)`.
 
 See the [compiler architecture](doc/compiler.md) and [nanopass guide](doc/nanopass.md)
 for implementation contracts and extension guidance.
diff --git a/doc/compiler.md b/doc/compiler.md
index dea52a6..b15f1e6 100644
--- a/doc/compiler.md
+++ b/doc/compiler.md
@@ -1,50 +1,69 @@
 # Compiler architecture
 
-Blacktide transforms immutable Clojure data through languages defined with
-`com.tailrecursion.nanopass`. Typed Clojure checks production pass bodies; the
-checker is absent from ordinary library use. Namespace docstrings state pass
-contracts. Compiler namespaces and intermediate representations are internal.
+Blacktide represents each compiler stage as immutable Clojure data. Languages
+defined with `com.tailrecursion.nanopass` describe that data; passes transform it.
+Compiler namespaces and intermediate representations are internal.
 
-All grammars live in [`compiler/languages.clj`](../src/com/tailrecursion/blacktide/compiler/languages.clj).
-Transformations and their helpers live under [`compiler/passes/`](../src/com/tailrecursion/blacktide/compiler/passes/).
-The executable pipeline, including the backend choice, lives in
-[`compiler.clj`](../src/com/tailrecursion/blacktide/compiler.clj).
+Typed Clojure checks production pass bodies during development. Ordinary library
+use does not load the checker. Namespace docstrings state each pass's contract.
+
+## Pipeline
+
+- [`compiler/languages.clj`](../src/com/tailrecursion/blacktide/compiler/languages.clj): all grammars.
+- [`compiler/passes/`](../src/com/tailrecursion/blacktide/compiler/passes/): transformations and their helpers.
+- [`compiler.clj`](../src/com/tailrecursion/blacktide/compiler.clj): the executable pipeline and backend choice.
 
 | Stage | Responsibility |
 | --- | --- |
-| Source | Expand macros in order, resolve unique lexical identities and source JVM facts, enforce the subset, solve loop representations without repeating expansion. |
-| Classification | Preserve analyzed loops without DSL effects and native keyword calls; materialize representations for loops requiring lowering. |
-| Normalization | Lower sequential/parallel assignments, case and collections; prepare conversions and save operands in evaluation order. |
-| Graph | Resolve outer labels, check destinations and definite initialization, compute liveness and allocate slots. |
-| Backend | Fold literal branches, recover structured control with shared joins, choose conservative primitive storage and compact safe intermediates. Fall back to the dispatcher when recovery is ineligible. |
-| Emission | Emit Clojure with original conversions, construction sites and an opaque Object result. |
+| Source | Expand macros in order. Assign unique lexical identities, record source JVM facts and enforce the supported subset. Determine loop representations without repeating expansion. |
+| Classification | Preserve analyzed loops without DSL effects and native keyword calls. Make representations explicit for loops that need lowering. |
+| Normalization | Lower sequential and parallel assignments, case and collections. Prepare conversions and save operands in evaluation order. |
+| Graph | Resolve outer labels and check destinations and definite initialization. Compute liveness and allocate slots. |
+| Backend | Fold literal branches and recover structured control with shared joins. Choose safe primitive storage and compact safe intermediates. Use the dispatcher when structured recovery is ineligible. |
+| Emission | Emit Clojure that preserves conversions and construction sites. Seal the result with an Object type boundary. |
+
+`compiler/compile-form` orchestrates source analysis and lowering:
+
+```text
+Bound → Classified → Sequential → Assigned → Cases → Collections
+      → Prepared → Ordered → Symbolic → CFG → Machine
+```
+
+The outer bindings enter as one lexical scope. `Native` contains analyzed
+subtrees without DSL operations. Both backends share graph validation:
 
-`compiler/compile-form` orchestrates:
+```text
+Dispatcher:  Machine → Code
+Structured:  Machine → Analysis → Planned → Joined → Stored → Compact → Code
+```
 
-`Bound → Classified → Sequential → Assigned → Cases → Collections → Prepared → Ordered → Symbolic → CFG → Machine → Code`.
+Language derivation describes how grammars relate. It does not set pass order:
+`Symbolic` extends `CFG`, which extends `Machine`, while lowering visits
+`Symbolic`, then `CFG`, then `Machine`.
 
-The outer bindings enter as one lexical scope; emission seals the result with an
-Object type boundary. `Native` contains analyzed subtrees without DSL operations.
-The structured backend uses `Machine → Analysis → Planned → Joined → Stored → Compact → Code`
-and shares graph validation with the dispatcher. Grammar derivation expresses
-structural relationships, not execution order: `Symbolic` extends `CFG`, which
-extends `Machine`, though lowering visits them in the opposite order.
+## Runtime boundaries
 
 Assignments, normalization and graph construction are pure. Locals become
 lexical bindings and loop parameters, never mutable cells. A generated
 `RT.box(Object)` is an identity operation that preserves an inference boundary;
 its appearance alone does not imply allocation.
 
-Java method values, functional-interface adapters and keyword sites must not be
-duplicated during control recovery. Keyword calls with effectful targets save
-the cache thunk before evaluating the target. `runtime.KeywordSite` implements
-that native cache protocol; an internal macro allocates each site during final
-Clojure analysis. The Java helper targets JDK 17 and is bundled in JARs.
-
-To extend the compiler, change the language and affected passes, then run
-`bin/check`. Prefer a compiler-local transformation over new nanopass machinery.
-Checking discovers compiler source namespaces and registers language and pass
-contracts from their metadata; new files need no separate registration list.
-Tests should establish source semantics or a necessary invariant. Generators
-use independent models or ordinary Clojure, deterministic seeds and shrinking;
-backend comparisons supplement those independent references.
+Control recovery must not duplicate Java method values, functional-interface
+adapters or keyword lookup sites. Keyword calls with effectful targets save
+the cache thunk before evaluating the target.
+
+The `runtime.KeywordSite` helper implements the native cache protocol. An internal
+macro allocates each site during final Clojure analysis. The helper targets
+JDK 17 and is bundled in JARs.
+
+## Extend the compiler
+
+1. Change the language and affected passes. Prefer a compiler-local transformation
+   over new nanopass machinery.
+2. Add coverage for the source semantics or invariant. For generated tests, use
+   fixed seeds, shrinking and an independent model or ordinary Clojure as the
+   reference. Backend comparisons supplement those independent checks.
+3. Run `bin/check` from the repository root.
+
+The check runner discovers compiler source namespaces. It registers language
+and pass contracts from their metadata, so new files need no registration list.
diff --git a/doc/language.md b/doc/language.md
index dfc6e12..f3662c9 100644
--- a/doc/language.md
+++ b/doc/language.md
@@ -1,9 +1,11 @@
 # Language reference
 
-The public namespace is `com.tailrecursion.blacktide`; its macros are `loophole`,
-`setq`, `psetq`, `label` and `goto`. Qualified calls and namespace aliases work.
-Lexical bindings can shadow macro names. DSL markers have no meaning outside
-`loophole` and report an error there.
+The public namespace is `com.tailrecursion.blacktide`. It provides `loophole`,
+`setq`, `psetq`, `label` and `goto`. A `loophole` form defines a region where
+assignment and jumps are allowed. The other four macros report an error outside
+that region.
+
+Qualified calls and namespace aliases work. Lexical bindings can shadow macro names.
 
 ## Bindings and assignment
 
@@ -21,24 +23,33 @@ bindings. The result is the last body value, or nil for an empty body.
   [(setq x 10) y]) ; => [10 1]
 ```
 
-`setq` writes each pair immediately and returns its last value (nil for no
-pairs). `psetq` evaluates every RHS before writing targets, in pair order, and
-returns nil. Repeated targets are written in order. Nested assignments take
-effect during RHS evaluation; an exception abandons pending parallel writes.
+| Form | Evaluation and assignment | Result |
+| --- | --- | --- |
+| `setq` | Evaluate a right-hand side and write its target before proceeding to the next pair. | Last value, or nil for no pairs. |
+| `psetq` | Evaluate all right-hand sides in pair order, then write all targets in pair order. | nil |
+
+These rules also apply to repeated targets.
+
+Nested assignments take effect while right-hand sides are evaluated. If one
+throws an exception, pending parallel writes are abandoned.
+
 Only bindings introduced by `loophole` are assignable. Shadowing with an ordinary
-`let` makes the inner binding immutable. Native `set!` is not admitted.
+`let` makes the inner binding immutable. Native `set!` is not allowed.
 
 ## Statements and jumps
 
-Labels are simple symbols in the **outer statement sequence**, including nested
-transparent `do` forms after macroexpansion. They cannot appear inside `let`,
-`loop`, conditional arms, operands or initializers. Names are unique within the
-region. Labels evaluate to nil.
+The placement rules distinguish labels from jumps:
+
+- **`label`:** a unique simple symbol in the **outer statement sequence**;
+  evaluates to nil. Nested `do` forms are transparent after macroexpansion.
+  Labels cannot appear inside `let`, `loop`, conditional arms, operands or
+  initializers.
+- **`goto`:** a statement that may occur in `if`/`case` arms and `let`/`loop`
+  bodies. It jumps to an explicit outer label in the same region. Execution
+  continues after that label.
 
-`goto` is a statement. It can occur in `if`/`case` arms and `let`/`loop` bodies
-and jump out to an outer label. It is forbidden anywhere within an operand or
-initializer, even a discarded expression nested in `do`. Every jump requires
-an explicit label in the same region; execution continues after that label.
+A jump cannot occur anywhere within an operand or initializer. This includes
+discarded expressions nested in `do`.
 
 ```clojure
 (loophole [x 0]
@@ -62,23 +73,40 @@ scope or bypass its initialization. These forms are errors:
 
 ## Clojure subset
 
-Supported forms are literals, quote/var, symbol reads, function calls, collection
-literals and their executable metadata, `do`, `if`, `throw`, `let`, `case`,
-`loop`/`recur`, Java calls, constructors, field reads and arrays. Ordinary `let`
-and `loop` support destructuring. Calls may use external function values;
-called code can use unrestricted Clojure.
+### Supported forms
+
+| Category | Supported forms |
+| --- | --- |
+| Values | Literals, `quote`, `var`, symbol reads and collection literals with executable metadata. |
+| Bindings | `let` and `loop`, including destructuring. |
+| Control | `do`, `if`, `throw`, `case` and `loop`/`recur`. |
+| Calls | Function calls, including external function values. |
+| Java interop | Method calls, constructors, field reads and arrays. |
+
+External functions called from the region can use unrestricted Clojure.
+
+### Macro expansion
+
+Macros expand in the caller namespace with lexical shadowing and visibility
+checks. The macro environment, `&env`, provides binding names, hints and inferred
+immutable types. It does not provide private `Compiler$LocalBinding` objects.
+
+Common supported macros include `when`, `when-not`, `cond`, `and`, `or`, `if-let`,
+`when-let`, threading, `dotimes`, `while` and `doseq`. A macro works only when
+its entire expansion uses supported forms. Quoted data is never analyzed as code.
+
+### Forms that belong outside the region
+
+The region rejects these forms, including forms produced by macroexpansion:
 
-Macros are expanded in the caller namespace with lexical shadowing and visibility
-checks. `&env` provides binding names, hints and inferred immutable types, not
-private `Compiler$LocalBinding` objects. Common admitted macros include `when`,
-`when-not`, `cond`, `and`, `or`, `if-let`, `when-let`, threading, `dotimes`, `while`
-and `doseq`. A macro is supported only when its entire expansion is admitted.
-Quoted data is never analyzed as code.
+- **Functions and deferred execution:** `fn`/`fn*`, `letfn`/`letfn*`, `delay`,
+  `lazy-seq` and `future`.
+- **Exceptions, resources and dynamic scope:** `try`/`catch`/`finally`, monitor
+  operations, `binding`, `locking`, `with-open` and `with-redefs`.
+- **Definitions:** namespace, Var and type definitions, and `reify`.
+- **Other excluded forms:** native `set!` and nested `loophole`.
 
-`fn`/`fn*`, `letfn`/`letfn*`, `try`/`catch`/`finally`, monitor operations, native
-`set!`, nested `loophole`, namespace/Var/type definitions and `reify` are rejected.
-This also excludes `delay`, `lazy-seq`, `future`, `binding`, `locking`, `with-open`
-and `with-redefs` **inside** the region. Put helpers and dynamic extent outside:
+Put helper functions, resource management and dynamic bindings outside:
 
 ```clojure
 (letfn [(step [n] (inc n))]
@@ -95,16 +123,25 @@ and `with-redefs` **inside** the region. Put helpers and dynamic extent outside:
   total) ; => 4
 ```
 
-Original `recur` keeps its local loop target, tail-position requirement and arity.
-Arguments evaluate before rebinding. Source primitive inference is preserved,
-including int→long and float→double initializer promotion and incompatible
-backedges that require boxing. Even unreachable recur contributes to inference.
-A recur cannot target a loop outside the region.
+### Loops and case dispatch
+
+Original `recur` preserves:
+
+- Its local loop target, tail-position requirement and arity.
+- Evaluation of all arguments before rebinding.
+
+`recur` cannot target a loop outside the region.
+
+Source primitive inference is preserved. This includes int→long and float→double
+initializer promotion. Incompatible backedges, where a recur returns to its loop,
+require boxing. Even an unreachable recur contributes to inference.
 
 `case` preserves Clojure's constant matching, grouping, hash collisions and
-missing-default exception. Dispatch executes once; only the selected arm runs.
-Each source arm is analyzed once in written order. Arms may assign or recur,
-and may jump when the case itself is a statement.
+missing-default exception:
+
+- The dispatch expression runs once; only the selected arm runs.
+- Each source arm is analyzed once in written order.
+- Arms may assign or recur, and may jump when the case itself is a statement.
 
 ```clojure
 (loophole [x 0]
@@ -117,19 +154,26 @@ and may jump when the case itself is a statement.
 
 ## JVM semantics and limits
 
+### Calls and compilation
+
 Source facts determine overloads and conversion order. Clojure 1.12 qualified
 method values, functional-interface adaptation and `:param-tags` are supported.
-Arithmetic respects `*unchecked-math*`; calls respect `:direct-linking` and direct
-protocol dispatch. Unreachable code still receives syntax and JVM compilation
-checks. Very large regions remain subject to JVM method-size limits.
-
-Mutable locals retain reference identity, including through assignment and
-immutable snapshots. Ordinary primitive locals retain Clojure's semantics:
-separate Object uses may box separately. Literal pooling is unspecified;
-independently embedded constants, macro-supplied quoted data, regex literals and
-inlined `^:const` values may share differently from ordinary Clojure. Bind a
-reference once when its identity matters. Runtime construction sites and cached
-lookup sites are not duplicated.
+Arithmetic respects `*unchecked-math*`. Calls respect `:direct-linking` and direct
+protocol dispatch.
+
+Unreachable code still receives syntax and JVM compilation checks. Very large
+regions remain subject to JVM method-size limits.
+
+### Identity and lookup sites
+
+Mutable locals retain reference identity through assignment and immutable
+snapshots. Ordinary primitive locals retain Clojure's semantics: separate Object
+uses may box separately.
+
+Literal pooling is unspecified. Embedded constants, macro-supplied quoted data,
+regex literals and inlined `^:const` values may share differently from ordinary
+Clojure. Bind a reference once when its identity matters. Runtime construction
+sites and cached lookup sites are not duplicated.
 
 ```clojure
 (let [token (Object.)]
@@ -142,8 +186,11 @@ Literal keyword calls retain Clojure's cached `IKeywordLookup` behavior, includi
 reentrant target evaluation. An assigned target uses a bundled cache helper;
 that cache never stores mutable region locals.
 
-Explicit reference conversions may use `Class.cast`, whose exception message
-differs from JVM `checkcast`. Invalid protocol fallback roots can also have
-different generated error text. Failing types and evaluation order are preserved.
+### Errors
+
+Explicit reference conversions may use `Class.cast`. Its exception message
+differs from JVM `checkcast`. Invalid protocol fallback roots can also produce
+different error text. Failing types and evaluation order are preserved.
+
 DSL errors carry `:kind`, `:form`, `:file`, available `:line`/`:column`, and relevant
 binding or label data. Clojure normally wraps them in `CompilerException`.
diff --git a/doc/nanopass.md b/doc/nanopass.md
index 1120b5b..b7ebd3f 100644
--- a/doc/nanopass.md
+++ b/doc/nanopass.md
@@ -1,7 +1,13 @@
 # Nanopass library
 
-Define languages from Typed Clojure syntax without loading the
-checker. Local nonterminals are rebound recursively when deriving a language:
+The nanopass library defines languages and passes over immutable Clojure data.
+A language describes the data's shape; a pass transforms data or computes a
+result. Definitions use Typed Clojure syntax without loading the checker.
+
+## Define a language
+
+A nonterminal is a named grammar type, such as `Expr`. When a language is derived,
+references to local nonterminals are rebound recursively to the derived language:
 
 ```clojure
 (require '[com.tailrecursion.nanopass :as np]
@@ -17,22 +23,29 @@ checker. Local nonterminals are rebound recursively when deriving a language:
                       :complete? true)]}})
 ```
 
-Descriptions are immutable values. `:replace` replaces or adds a complete
-nonterminal definition. Structural types support `U`, closed keyword-field
-`HMap`, fixed `HVec`, `Vec`, `Map`, `Set`, and `Option`. Other types are opaque
-terminals and cannot hide local nonterminal references. Quoted singleton data
-and `Val`/`Value` payloads stay untouched. Tagged productions have a required
-`:op` with a singleton keyword type. `clojure.core.typed` spelling is accepted too.
-Use explicit `HMap`/`HVec` constructors rather than their quoted collection
-shorthand. Declare complex polymorphic terminal types as external aliases.
+Language descriptions are immutable values. Derivation accepts three operations:
+
+| Option | Effect |
+| --- | --- |
+| `:remove` | Remove tagged productions from a nonterminal. |
+| `:add` | Add tagged productions to a nonterminal. |
+| `:replace` | Replace or add a complete nonterminal definition. |
+
+Structural types support `U`, closed keyword-field `HMap`, fixed `HVec`, `Vec`,
+`Map`, `Set`, and `Option`. Use explicit `HMap`/`HVec` constructors rather than
+quoted collection shorthand. The `clojure.core.typed` spelling is also accepted.
+
+Other types are opaque terminals. They cannot contain local nonterminal
+references. Quoted singleton data and `Val`/`Value` payloads stay untouched.
+Declare complex polymorphic terminal types as external aliases.
 
-An annotation-only namespace can require `typed.clojure` and call
-`(np/ann-languages Source Core)` to generate aliases `Source-Expr` and `Core-Expr`
-in the languages' defining namespace. Nothing registers types during ordinary
-language loading.
+Tagged productions require an `:op` field with a singleton keyword type.
+For example, `':negate` identifies the production removed above.
 
-Passes supply clauses for changed productions and inherit checked structural
-traversal for unchanged ones:
+## Define a pass
+
+Write clauses for productions that change. The library generates structural
+traversal for unchanged productions:
 
 ```clojure
 (np/defpass lower {:from [Source Expr] :to [Core Expr]}
@@ -42,29 +55,54 @@ traversal for unchanged ones:
            :right (lower (:value node))})
 ```
 
-Register `(np/ann-passes lower)` in the checking-only namespace, then check the
-implementation namespace with `typed.clojure/check-ns-clj`. Generated signatures
-are contracts, not a replacement for checking function bodies.
-
-`:processors {Binding lower-binding}` names other nonterminal processors. Group
-mutually recursive processors with `np/defpasses`; each entry uses `defpass`
-syntax without the macro name. See the [recursive traversal example](../test/com/tailrecursion/nanopass/passes.clj).
-Expansion produces one
-lexical `letfn` group and exports its functions with their individual signatures.
-The checker checks every body; the group is redefined as a unit.
-
-`:args [ContextType]` types leading
-arguments, which generated traversal forwards unchanged. Write explicit clauses
-when lexical context changes. With `:body true`, supply one ordinary expression
-and any result type in `:to`, including state/result tuples. Automatic clauses
-require matching fields and structural containers; removed productions and
-incompatible fields require explicit code. Missing cases are checked using a
-generated bottom-type guard. `macroexpand-1` exposes the complete generated code.
-Use qualified aliases such as `languages/Core-Expr` in `:args` and explicit
-result types; checking-only aliases need not exist as runtime Vars.
-
-Structural traversal preserves metadata and optional-field presence, including
-present nil values, and shares unchanged fields. Quoted payloads remain opaque. Map/set traversal is structural;
-use vectors and explicit clauses when order or scope has semantic significance.
-
-Run `bin/check` from the repository root to check pass bodies as well as generated contracts.
+Automatic clauses require matching fields and structural containers. Removed
+productions and incompatible fields need explicit code. A generated bottom-type
+guard lets the checker detect missing cases. Use `macroexpand-1` to inspect the
+generated code.
+
+## Pass options and recursive processors
+
+| Option | Meaning |
+| --- | --- |
+| `:from [Language Nonterminal]` | Input grammar and nonterminal. |
+| `:to [Language Nonterminal]` | Output grammar and nonterminal; may instead be an explicit result type. |
+| `:processors {Binding lower-binding}` | Functions that transform other nonterminals. |
+| `:args [ContextType]` | Types of leading arguments, forwarded unchanged by generated traversal. |
+| `:body true` | Supply one ordinary expression instead of tagged clauses. |
+
+Group mutually recursive processors with `np/defpasses`. Each entry uses
+`defpass` syntax without the macro name. See the
+[recursive traversal example](../test/com/tailrecursion/nanopass/passes.clj).
+
+Expansion produces one lexical `letfn` group. Its functions are exported with
+individual signatures. The checker checks every body, and the group is redefined
+as a unit.
+
+Write explicit clauses when lexical context changes. Passes may return results
+other than trees, including state/result tuples.
+
+Use qualified aliases such as `languages/Core-Expr` in `:args` and explicit result
+types. Aliases used only for checking need not exist as runtime Vars.
+
+## Traversal rules
+
+Structural traversal:
+
+- Preserves metadata and optional-field presence, including present nil values.
+- Shares unchanged fields and leaves quoted payloads opaque.
+- Treats maps and sets structurally. Use vectors and explicit clauses when
+  order or scope has semantic significance.
+
+## Check languages and pass bodies
+
+1. In an annotation-only namespace, require `typed.clojure` and call
+   `(np/ann-languages Source Core)`. This generates aliases `Source-Expr` and
+   `Core-Expr` in the languages' defining namespace.
+2. Register `(np/ann-passes lower)` in the same checking-only namespace.
+3. Check the implementation namespace with `typed.clojure/check-ns-clj`.
+
+Ordinary language loading does not register types. Generated signatures state
+the contracts; function bodies must also be checked. Blacktide's check runner
+discovers its compiler languages and passes and registers them automatically.
+
+Run `bin/check` from the repository root to check both bodies and contracts.