|
| 1 | +# Total derivation: the completeness spine |
| 2 | + |
| 3 | +Why `src/gen-tm.ts` emits *every* TextMate construct the grammar requires — not by |
| 4 | +testing a corpus, but because the generator's input is a **closed, finite algebra**, so |
| 5 | +"every obligation" is enumerable and each is discharged by a reachable emission. This is |
| 6 | +the dual of the soundness ledger (`KNOWN-GAPS.md`, which finds *wrong* paints); here we |
| 7 | +prove there are no *missing* ones. The proof is held exact by `test/tm-completeness.ts` |
| 8 | +and the ledger at the end. |
| 9 | + |
| 10 | +## The contract |
| 11 | + |
| 12 | +For every grammar `G` built from the public `src/api.ts` combinators and lowered through |
| 13 | +`defineGrammar()`: |
| 14 | + |
| 15 | +1. **Closure** — `G` is a value of the closed `RuleExpr` / `TokenPattern` algebra (plus a |
| 16 | + finite set of config records). Nothing the API can express falls outside it; nothing in |
| 17 | + it is unreachable from the API. |
| 18 | +2. **Coverage** — every highlighting obligation `G` induces (a token scope, a keyword, an |
| 19 | + operator, a region, an embed, a disambiguation, a config-driven construct) is emitted by |
| 20 | + `generateTmLanguage(G)`. |
| 21 | +3. **Reachability** — every emitted repository entry is reachable from the root patterns or |
| 22 | + from a declared export surface; conversely every export surface resolves. |
| 23 | + |
| 24 | +Three separations keep the claim honest: |
| 25 | + |
| 26 | +- **Parser** completeness (does `G` accept the language?) is a *different* axis, measured by |
| 27 | + the conformance run and `test/src-coverage.ts`. |
| 28 | +- **Highlighter** completeness (this document) is *coverage*: every obligation is |
| 29 | + recognised and scoped. Whether the scope is the *right* one at an ambiguous frontier is |
| 30 | + **soundness** — `test/scope-gap.ts` and `test/gap-ledger.ts`, a separate axis. |
| 31 | +- **TextMate-engine** expressiveness (can the regex model express the obligation at all?) |
| 32 | + is bounded by Oniguruma, not by Monogram; §"The frontier" settles where that bound |
| 33 | + actually lies. |
| 34 | + |
| 35 | +This is **not** the README corpus metrics (empirical agreement with external oracles). It |
| 36 | +is the formal derivation property: the map from the DSL grammar to the emitted grammar |
| 37 | +loses nothing representable. |
| 38 | + |
| 39 | +## Why a closed algebra makes this finite |
| 40 | + |
| 41 | +A TextMate grammar written by hand has no completeness theorem — there is no enumerable set |
| 42 | +of "everything it should match." Monogram's does, because `generateTmLanguage` consumes a |
| 43 | +value of a **closed union**: `RuleExpr` has 15 constructors and `TokenPattern` has 10 |
| 44 | +(`src/types.ts`), plus the finite config records (`TokenDecl`, `MarkupConfig`, |
| 45 | +`IndentConfig`, `NewlineConfig`, the Pratt tables, `scopeOverrides`, `canonicalRepoNames`, |
| 46 | +`aliasScopes`, `expressionRule`, `manifest`). An *obligation* is induced by a |
| 47 | +constructor-occurrence or a config-field-occurrence. So completeness reduces to: **for each |
| 48 | +obligation generator, the generator has a discharging, reachable emission** — three |
| 49 | +mechanically-checkable layers. |
| 50 | + |
| 51 | +## Layer A — closure: the universe is the algebra, and lowering is total |
| 52 | + |
| 53 | +**A1 — API lowering closure.** `toRuleExpr` (`src/api.ts`) is a total function with a finite |
| 54 | +case analysis ending in a `throw`: it never silently drops an element, and its image is |
| 55 | +exactly the `RuleExpr` union. Witnessed by instantiating *every* public combinator and |
| 56 | +marker into one grammar and confirming the lowered bodies use all 15 constructors and |
| 57 | +nothing outside them (`checkRuleExprClosure`). `formatExpr` in `src/cli.ts` is an |
| 58 | +independent exhaustive `switch` over the same 15 — a second guard that the union is closed. |
| 59 | + |
| 60 | +**A2 — TokenPattern compiler closure.** `tokenPatternToRegex`'s `emit` (`src/token-pattern.ts`) |
| 61 | +is a single `switch` over the 10 `TokenPattern` constructors with no `default` — TypeScript |
| 62 | +exhaustiveness makes a missing case a compile error. Witnessed by compiling every public |
| 63 | +token builder to a regex (`checkTokenPatternClosure`). |
| 64 | + |
| 65 | +**A3 — the literal-collection backbone is total.** Flat keyword / operator scoping is driven |
| 66 | +by the shared `collectLiterals` (`src/grammar-utils.ts`), looped over every rule body. It |
| 67 | +recurses into *all consuming* structural constructors (`seq`, `alt`, `quantifier`, `group`, |
| 68 | +`sep`) and omits only the ones that carry no consumed literal: `not` (a negative lookahead — |
| 69 | +the word is *absent* at the site) and `ref` (a cross-rule edge, collected when that rule's |
| 70 | +own body is walked). So no consumed literal is silently dropped, and the flat keyword |
| 71 | +obligation is discharged for *any* nesting. This is why a naïve end-to-end keyword probe is |
| 72 | +vacuous — `collectLiterals` already covers every nesting (`checkCollectLiteralsClosure`). |
| 73 | + |
| 74 | +The residual silent-drop risk therefore lives only in the **specialised region walkers** that |
| 75 | +do *not* use `collectLiterals` (they hoist keywords out of a derived `<…>` / region scope). |
| 76 | +Auditing the 48 RuleExpr walkers in `gen-tm.ts` found exactly one reachable gap: |
| 77 | +`getTypeParamElementKeywords` omitted `sep`, so a keyword inside a `sep`-list within a |
| 78 | +type-parameter element lost its keyword role inside `<…>`. No shipped grammar nests a keyword |
| 79 | +that way (TS type-param keywords are direct), so it was latent — but it is a *supported* |
| 80 | +combinator shape silently ignored, so it is **fixed** (one line: recurse into `sep.element`; |
| 81 | +`not` stays omitted on purpose — a forbidden word; `ref` stays unresolved so a constraint |
| 82 | +*type*'s own keywords like `keyof`/`typeof` are not mis-hoisted). The fix is byte-identical on |
| 83 | +all six shipped grammars (latent), and the `kwsep` probe in `regionKeywordProbe` is a biting |
| 84 | +regression guard (it fails without the fix). |
| 85 | + |
| 86 | +## Layer B — coverage: every obligation has a reachable discharge |
| 87 | + |
| 88 | +The obligation families, enumerated from `G`'s closed algebra **independently of gen-tm's own |
| 89 | +detectors** (a detector that missed a shape would otherwise also miss its obligation — |
| 90 | +co-blind): |
| 91 | + |
| 92 | +- **Tokens.** Every non-`skip` token bears a leaf-scope obligation, discharged by exactly one |
| 93 | + family: the flat token loop (a `#<name>` entry), the regex-literal family (`regex`-flagged), |
| 94 | + the indent/markup engine (a `never()` placeholder the region machinery replaces), the markup |
| 95 | + region machinery (a `markup` grammar emits no per-token keys), or a region that owns the |
| 96 | + token's delimiter (the JSX `/>` / `</` punctuation). `tokenCensus` classifies every token and |
| 97 | + asserts **zero orphans** — the emitter-completeness proof for tokens. |
| 98 | +- **Keyword literals & Pratt operators** are discharged through the flat backbone (A3) and the |
| 99 | + prec-table path; the `op`/`prefix`/`postfix` markers carry no literal (they route to |
| 100 | + `collectLiterals`' default), and an operator's scope comes from the prec-table value, not from |
| 101 | + a walked marker — so those three constructors being unwalked anywhere is *benign*, confirmed |
| 102 | + by adversarial review. |
| 103 | +- **Shapes** (JSX elements, generic/cast angle brackets, regex context, declarations, ternary, |
| 104 | + conditional types, arrow params, contextual operators/modifiers) and **config surfaces** |
| 105 | + (markup, indent, newline, `expressionRule`, `aliasScopes`, `canonicalRepoNames`, `manifest`, |
| 106 | + `inject`) each emit a family of repository entries; that the detectors fire on the *shape* |
| 107 | + rather than on TypeScript-specific names — the detector-completeness requirement — is held by |
| 108 | + `test/agnostic.ts` (synthetic grammars with deliberately non-TS names/delimiters). |
| 109 | + |
| 110 | +The empirical witness that all of the above actually paint is **leaf coverage**: over the |
| 111 | +deterministic grammar-derived corpus (`test/grammar-gen.ts`), every parsed leaf whose |
| 112 | +by-construction role (`buildRoleMap`) is a content/keyword role (keyword / string / number / |
| 113 | +comment) is confirmed to receive a non-root scope. The denominator is fixed (the obligation |
| 114 | +leaves); the metric is non-vacuous (deleting a discharging repository key drops it below 100%). |
| 115 | +Result: **2433/2433 across all six grammars.** |
| 116 | + |
| 117 | +## Reachability — root ∪ export surfaces |
| 118 | + |
| 119 | +Reachability is the transitive `#include` closure from the root `patterns`, **plus the declared |
| 120 | +export surfaces** an external embedder reaches by a `<scope>#<key>` include: the `#expression` |
| 121 | +sub-grammar (`expressionRule`), the `canonicalRepoNames` official keys, and `aliasScopes`. These |
| 122 | +are root-unreachable *by design* — they are the grammar's public repository API. A naïve |
| 123 | +root-only reachability flags ten keys as dead; the export-surface-aware closure flags **zero**. |
| 124 | +A `canonicalRepoNames` entry whose structural *source* is absent in a shared map (e.g. `type`/ |
| 125 | +`new-expr` in JavaScript, which has no type layer; `cast` in `.tsx`, where `<T>expr` is JSX, so |
| 126 | +only `as`-casts exist) induces no obligation and is correctly inert — distinct from a dangling |
| 127 | +reference with a *present* source, of which there are none. |
| 128 | + |
| 129 | +## The frontier — no proven impossibility |
| 130 | + |
| 131 | +Three sites looked like TextMate impossibilities; under adversarial attack (the project's |
| 132 | +discipline: a "can't" must survive a real attack before it is recorded), all three were |
| 133 | +**refuted** with constructions tested in the production engine: |
| 134 | + |
| 135 | +- **Cast/arrow "not after a value" across unbounded whitespace.** gen-tm emits a fixed-width |
| 136 | + negative-lookbehind ladder (`\s{k}`, k=0..16). The exact unbounded condition is a single |
| 137 | + variable-width lookbehind `(?<![\w$)\]]\s*)`, which **vscode-oniguruma compiles and runs |
| 138 | + correctly** (verified: suppresses `a <b`, fires at expr-start). An Onigmo-portable |
| 139 | + alternative also exists (a region that *owns* the post-value whitespace boundary instead of |
| 140 | + looking behind it). |
| 141 | +- **Arrow param list with nested parens** `(a = f(1)) => x`. The single-level `[^()]*` lookahead |
| 142 | + breaks at the inner `(`, but Oniguruma's recursive subroutine `(?<P>\((?:[^()]|\g<P>)*\))` |
| 143 | + matches balanced parens at arbitrary depth in a begin lookahead (verified to compile + match). |
| 144 | +- **Regex after a control-flow head** `if (a) /re/`. A variable-width positive lookbehind |
| 145 | + `(?<=\b(?:if|while|for|with)\s*\([^()]*\))` (or the recursive form for nested heads) |
| 146 | + **compiles and matches in vscode-oniguruma** (verified: matches `if (a) /`, not `a / b`). |
| 147 | + |
| 148 | +So none of these is a model impossibility. Each is (a) directly expressible in vscode-oniguruma |
| 149 | +— the engine VS Code actually runs — and (b) approximated by a fixed-width form *deliberately*, |
| 150 | +for **Onigmo portability** (RedCMD's YAML grammar runs under Onigmo, which rejects variable-width |
| 151 | +lookbehind; the same source must compile under both, see `test/redcmd-tm-diagnostics.ts`). And |
| 152 | +each is a **soundness-precision** matter, not a completeness gap: the `<` / `/` / arrow *is* |
| 153 | +recognised and scoped; what is refined at the frontier is *which* role at the ambiguous boundary. |
| 154 | +Improving that precision (var-width forms for the `vscode-oniguruma`-only grammars, `\g<>` for the |
| 155 | +arrow region) is a separate, soundness-gated change. **The completeness obligation is discharged.** |
| 156 | + |
| 157 | +## The proof ledger |
| 158 | + |
| 159 | +The fixed denominator is every measured obligation (token discharge + repository reachability + |
| 160 | +leaf painting), summed across the six grammars; the numerator is the discharged count. |
| 161 | +Auto-generated by `node test/tm-completeness.ts --write`; `--check` fails CI if it is stale. |
| 162 | + |
| 163 | +<!-- COMPLETENESS-LEDGER:START — auto-generated by `node test/tm-completeness.ts --write`; do not edit by hand. --> |
| 164 | + |
| 165 | +| Grammar | Tokens | Keyword literals | Operators | Repo keys (reachable) | Leaf obligations (painted) | |
| 166 | +|---|---:|---:|---:|---:|---:| |
| 167 | +| typescript | 11/11 | 73 | 53 | 158/158 | 199/199 | |
| 168 | +| javascript | 11/11 | 48 | 51 | 103/103 | 131/131 | |
| 169 | +| typescriptreact | 13/13 | 73 | 53 | 171/171 | 169/169 | |
| 170 | +| javascriptreact | 13/13 | 48 | 51 | 116/116 | 121/121 | |
| 171 | +| html | 7/7 | 0 | 0 | 28/28 | 175/175 | |
| 172 | +| yaml | 19/19 | 0 | 0 | 54/54 | 1638/1638 | |
| 173 | +| **total** | **74/74** | **242** | **208** | **630/630** | **2433/2433** | |
| 174 | + |
| 175 | +**Fixed-denominator completeness: 3137/3137 = 100.00%** (token discharge 74/74 · repository reachability 630/630 · leaf painting 2433/2433). Keyword literals (242) and Pratt operators (208) are discharged through the leaf-painting column. **0 open completeness gaps.** |
| 176 | + |
| 177 | +<!-- COMPLETENESS-LEDGER:END --> |
| 178 | + |
| 179 | +## The gates that hold this exact |
| 180 | + |
| 181 | +- `test/tm-completeness.ts` — Layer A closure (RuleExpr / TokenPattern / `collectLiterals`), the |
| 182 | + `sep`-recursion regression guard, reachability, the token census, and leaf coverage with a fixed |
| 183 | + denominator. `npm run completeness` prints it; `npm run completeness:check` gates the ledger. |
| 184 | +- `test/agnostic.ts` — detector shape-completeness: the detectors fire on structure, not on TS |
| 185 | + names, so "every shape that bears the obligation is detected" holds for any grammar. |
| 186 | +- `test/scope-gap.ts`, `test/gap-ledger.ts` — the **soundness** axis (is each painted scope |
| 187 | + correct?), the dual of this document, kept separate on purpose. |
0 commit comments