diff --git a/docs/design-dissolution-lens.md b/docs/design-dissolution-lens.md index 152095427a6..4eb80bee4b0 100644 --- a/docs/design-dissolution-lens.md +++ b/docs/design-dissolution-lens.md @@ -1176,12 +1176,28 @@ import/alias of the resolver's authoritative shape. `connective_spec_fact` (6 arms → 2 skeletons, 5:1) — resolved via inline match-pattern with guard (`Atom { identity: id } if is_kernel_ambient(id) => ...; _ => default`), NOT via a named - `Bool` helper. **Fix-confidence: direct auto-apply.** Lens emits a - typed `Diff` rewriting the N-arm match to a 2-arm form: the - singleton arm's pattern + RHS preserved, the N-1 uniform arms - collapsed to `_ => `. - No naming decisions; the structural fix is unambiguous from the - histogram. + `Bool` helper. **Fix-confidence: split by RHS form** — skeleton + equivalence is a comparison-time notion, not executable syntax, so + the auto-fix has to materialize an actual replacement that compiles: + - **(a) Constructor identity does NOT appear in the uniform RHS** + (e.g. PR #3359 `connective_spec_fact`'s 5 uniform arms all + executing `classify_density(facts)` — the matched constructor + doesn't show up in the RHS at all). **Direct auto-apply:** the + catch-all is literally `_ => `; no constructor + reconstruction needed. + - **(b) Constructor identity DOES appear in the uniform RHS** (e.g. + RHSes like `Disposition { feature: }` — + this is more naturally a MultiOutlier shape, but Outlier + examples exist). **Templated auto-apply:** bind the matched + value in the catch-all (e.g. `c => `) + so the executable replacement is a real value-binding, NOT a + skeleton hole. The lens emits the Diff with the binding name + templated (default `c`/`x`/etc.; reviewer may override). + - The naive "substitute the constructor with a wildcard `_`" form + is a skeleton-equality device for COMPARING arms, not for + generating executable replacement code; cases that require it + should downgrade from direct-auto-apply to templated-auto-apply, + not emit syntactically invalid `_ => Foo { field: _ }` RHSes. - **MultiOutlier** — `K ≥ 2`, histogram contains both singleton(s) AND non-singleton group(s). `N ≥ 4`. Multiple base-cases + one or more uniform groups. Covers F14 (1:5:6 — one singleton + @@ -1205,11 +1221,13 @@ import/alias of the resolver's authoritative shape. sub-coproduct). Lens emits a typed `Diff` with templated holes for NEW type names (wrapping variant name, sub-coproduct name, sub-variant names). Default templates derive from existing constructor names — - e.g. F14's `Modeled` disposition + uniform group → wrapping variant - `ModeledFeature` with sub-coproduct `ModeledKind`. Reviewer may - override names before the candidate-state commit; same flow as any - typo-fix Diff. Auto-apply when reviewer accepts default templates; - one round of reviewer-edit when names need to differ. + e.g. F14's `DeclaredNormalized` uniform group (5 variants) → wrapping + variant `NormalizedFeature` with sub-coproduct `NormalizedKind`. + Singleton groups stay fieldless (no `{ kind: ... }` wrapper) per + the dissolution rule below — only non-singleton groups get wrapped. + Reviewer may override names before the candidate-state commit; same + flow as any typo-fix Diff. Auto-apply when reviewer accepts default + templates; one round of reviewer-edit when names need to differ. - **Categorical** — `K ≥ 2`, histogram contains ONLY non-singleton groups (every group size ≥ 2). `K ≤ ⌊N/2⌋`, `N ≥ 4`. Pure category projection with no singleton base case. Rarer than MultiOutlier in @@ -1306,24 +1324,41 @@ fn feature_disposition(f: FidelityFeature) -> FidelityDisposition { 12 arms, 3 distinct skeletons: `Modeled` (1), `DeclaredNormalized { feature: }` (5), `FailClosed { feature: }` (6). **MultiOutlier, 1:5:6** (one singleton + two uniform groups; per the classifier definition above, Categorical requires non-singleton-only groups — the `Modeled` arm is a singleton, so this is MultiOutlier). -**Clean shape:** push the categorization into `FidelityFeature`: +**Clean shape:** push the categorization into `FidelityFeature`. +**Singleton groups become fieldless top-level variants** (no `{ kind: _ }` +wrapping — a sub-coproduct of one element is empty overhead); **only +non-singleton groups get `{ kind: ... }` wrappers** carrying their +sub-coproduct: ```dag type FidelityFeature - = ModeledFeature { kind: ModeledKind } // StructuralCore - | NormalizedFeature { kind: NormalizedKind } // 5 normalized variants - | UnmodeledFeature { kind: UnmodeledKind } // 6 fail-closed variants + = ModeledFeature // singleton (StructuralCore) — fieldless + | NormalizedFeature { kind: NormalizedKind } // 5 normalized variants + | UnmodeledFeature { kind: UnmodeledKind } // 6 fail-closed variants + +type NormalizedKind + = SsaValueSpelling | BlockTextualOrder | LexicalTrivia + | TargetConfigToken | AdvisoryMetadata + +type UnmodeledKind + = UnmodeledInlineAsm | UnmodeledSemanticAttribute | UnmodeledType + | UnmodeledInstruction | UnmodeledConstExpr | MalformedStructure fn feature_disposition(f: FidelityFeature) -> FidelityDisposition { match f { - ModeledFeature { kind: _ } => Modeled - NormalizedFeature { kind: _ } => DeclaredNormalized { feature: f } - UnmodeledFeature { kind: _ } => FailClosed { feature: f } + ModeledFeature => Modeled + NormalizedFeature { kind: _ } => DeclaredNormalized { feature: f } + UnmodeledFeature { kind: _ } => FailClosed { feature: f } } } ``` 3 arms instead of 12. The N-to-3 projection lives in `FidelityFeature`'s type definition (its correct home — the category IS a property of the -feature), not as a hand-rolled function. +feature), not as a hand-rolled function. **General rule for the +MultiOutlier / Categorical dissolution** — applies to every shape with +mixed singletons + non-singleton groups: singleton-group variants are +fieldless; only non-singleton groups carry `{ kind: }` +wrappers. Wrapping a singleton is pure structural overhead with no +discrimination work to do. **Concrete match — F15 (PR #3452 `complexity_bound_from_class`):** 9 arms over `AsymptoticClass`, 3 distinct skeletons: `Constant` (1), @@ -1560,8 +1595,9 @@ uses. | Refinement-clause index (type → length / domain refinements) | `v4.compiler.04_infer` | L1.7 | | Import graph + target existence | `v4.compiler.02_parse` | L0.8, L1.8 | | Return-type → fail-closed-carrier? | `v4.compiler.03_resolve` | L0.14, L1.11 | +| Match-arm RHS skeleton + per-arm group membership + per-skeleton constructor-hole presence (normalized RHS after α-renaming + matched-arm constructor substitution; groups expose arm-ids so the auto-fix consumes them as facts, not by re-walking) | `v4.lens.match_arm_skeleton` (new derived stage — see §10.2) | L1.13 | -### 10.2 Three small derived stages cover what the pipeline doesn't already expose +### 10.2 Four small derived stages cover what the pipeline doesn't already expose These are themselves `.dag` stages — small folds with declared `consumes:` edges — and they're reusable across multiple lenses: @@ -1581,11 +1617,48 @@ module v4.lens.concept_home consumes: v4.compiler.03_resolve, v4.lens.canonical_observations_index produces: Map // each fn's primary-concept home file // reusable by: L1.8 + +module v4.lens.match_arm_skeleton +consumes: v4.compiler.02_parse, v4.compiler.03_resolve +produces: Map +// SkeletonReport = { +// arm_count: Nat, +// distinct_skeletons: Nat, +// histogram: [Nat], // sorted group-sizes, largest first +// classifier_shape: ClassifierShape, // PureTemplate | Outlier | MultiOutlier | Categorical | Mixed +// groups: [SkeletonGroup], // one entry per distinct skeleton — per-arm membership +// } +// SkeletonGroup = { +// skeleton: RhsSkeleton, // the normalized RHS expression tree +// arm_ids: [MatchArmId], // arms in this skeleton-equivalence class +// constructor_hole_present: Bool, // does the skeleton contain the constructor-hole at any +// // position? (distinguishes Outlier sub-cases a/b +// // without re-walking — drives Direct vs Templated +// // auto-apply per the L1.13 entry above) +// matched_constructors: [ConstructorId], // the constructors whose arms collapsed to this skeleton +// // (lens reads to derive templated names for the +// // MultiOutlier/Categorical wrapping-variant default) +// } +// Facts Flow Forward (Practice 3): the lens emits everything the L1.13 +// auto-fix and any future L1.13.b sub-signature need. No consumer +// re-walks the arms or re-derives skeleton equivalence — single +// authority (P2), one mechanism, multiple downstream projections. +// reusable by: L1.13, future L1.13.b (per-arm-name-parameterized-reference sub-signature), +// future match-as-typed-table lens +// Algorithm: tree-walk each arm's RHS, α-rename pattern-bound names, +// substitute every occurrence of the matched-arm constructor identity +// with a per-arm hole, structurally compare; group arms by skeleton +// (each group records arm_ids + matched_constructors + whether the +// skeleton contains the constructor-hole anywhere); sort group sizes +// (largest first) to form histogram; classify distribution-shape per +// L1.13's thresholds (PureTemplate / Outlier / MultiOutlier / +// Categorical / Mixed). ``` Each is a single deterministic fold. Once landed, multiple lenses share the result — landing `match_arm_shape` unblocks five lenses, -not one. +`match_arm_skeleton` unblocks L1.13 + the future L1.13.b and +match-as-typed-table sub-signatures. ### 10.3 A lens is a stage with declared dependencies @@ -1596,6 +1669,7 @@ consumes: v4.compiler.03_resolve v4.compiler.04_infer v4.lens.match_arm_shape + v4.lens.match_arm_skeleton v4.lens.closed_vocab_scan v4.lens.concept_home produces: