Consolidate structural_similarity into the intent_linearity registry as a row (one engine, two binders)

src/v2/lens/intent_linearity.dag

@@ -1,36 +1,70 @@
 module v2.lens.intent_linearity
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
 import v2.lens.simulated_relationship { chain_is_simulated }
+import v2.lens.structural_similarity { type_decls_anti_unify }
 import v2.std.node { Node, Symbol }
 import v2.std.algebra { FreeMonoid, length, any, for_all }
 import v2.std.logic { Bool }
 
 type CostAxis = ChangeTime | RunTime
 
+type Representation = TermChain | TypeForest
+
 type LinearityRule {
   name: Symbol
   axis: CostAxis
+  representation: Representation
   detect: fn(FreeMonoid<Node>) -> Bool
 }
 
 fn unroll_to_fold_rule() -> LinearityRule {
   LinearityRule {
     name: ^unroll_to_fold,
     axis: ChangeTime,
+    representation: TermChain,
     detect: fn(s) { chain_is_simulated(steps: s) }
   }
 }
 
+fn dup_type_to_generic_rule() -> LinearityRule {
+  LinearityRule {
+    name: ^dup_type_to_generic,
+    axis: ChangeTime,
+    representation: TypeForest,
+    detect: fn(s) { type_decls_anti_unify(decls: s) }
+  }
+}
+
 fn linearity_registry() -> FreeMonoid<LinearityRule> {
-  [ unroll_to_fold_rule() ]
+  [ unroll_to_fold_rule(), dup_type_to_generic_rule() ]
+}
+
+fn representation_eq(a: Representation, b: Representation) -> Bool {
+  match a {
+    TermChain => match b { TermChain => true  TypeForest => false }
+    TypeForest => match b { TermChain => false TypeForest => true }
+  }
 }
 
 fn rule_fires(rule: LinearityRule, steps: FreeMonoid<Node>) -> Bool {
   rule.detect(steps)
 }
 
+fn input_is_redundant_for(rep: Representation, input: FreeMonoid<Node>) -> Bool {
+  any(
+    xs: linearity_registry(),
+    predicate: fn(rule) {
+      representation_eq(a: rule.representation, b: rep) && rule_fires(rule: rule, steps: input)
+    }
+  )
+}
+
 fn chain_is_redundant(steps: FreeMonoid<Node>) -> Bool {
-  any(xs: linearity_registry(), predicate: fn(rule) { rule_fires(rule: rule, steps: steps) })
+  input_is_redundant_for(rep: TermChain, input: steps)
+}
+
+fn forest_is_redundant(decls: FreeMonoid<Node>) -> Bool {
+  input_is_redundant_for(rep: TypeForest, input: decls)
 }
 
 fn chain_residual(steps: FreeMonoid<Node>) -> Int {
@@ -51,8 +85,8 @@ fn body_is_linear(levels: FreeMonoid<FreeMonoid<Node>>) -> Bool {
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
   class: WallAfterGrounding {
-    grounding_authority: "the parse/resolve walk + chain projector decomposing a body into its per-level statement-chains (shared with v2.lens.simulated_relationship / v2.lens.structural_similarity)",
-    dissolve_on: "body_is_linear runs over live dsl/** bodies once the walk projects per-level chains; the registry grows by rows (complexity cost-recurrence rules join the change-time rows); until then this is a lens_unit over projected synthetic chains"
+    grounding_authority: "the parse/resolve walk + chain projector decomposing a body into its per-level statement-chains (shared with v2.lens.simulated_relationship / v2.lens.structural_similarity, all over the v2.std.anti_unification kernel)",
+    dissolve_on: "body_is_linear runs over live dsl bodies once the walk projects per-level chains; the registry grows by rows (complexity cost-recurrence rules join the change-time rows); Row 1 is the term-chain hand-unrolled fold, Row 2 the type-decl duplicate-to-generic, one anti-unification engine and two binders; until then this is a lens_unit over projected synthetic chains"
   },
-  rationale: "Intent-linearity is a wall up to the substrate's expressible abstraction (anti-unification computes the structural minimum) and a ratchet beyond it (global minimal description is Kolmogorov-uncomputable). The registry is the decidable wall-half; complexity.dag keeps the RatchetForever optimality residue. One engine, N rows (§2-horizontal)."
+  rationale: "Intent-linearity is a wall up to the substrate's expressible abstraction (anti-unification computes the structural minimum) and a ratchet beyond it (global minimal description is Kolmogorov-uncomputable). The registry is the decidable wall-half; complexity.dag keeps the RatchetForever optimality residue. One engine, N rows; the Representation field tags each row's binder so the term and type rows stay off each other's projection."
 }

src/v2/lens/structural_similarity.dag

@@ -1,53 +1,27 @@
 module v2.lens.structural_similarity
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
 
-import v2.std.collection { List, Map }
-import v2.std.nat { Nat, Zero }
-import v2.std.node { Symbol }
+import v2.std.node { Node }
+import v2.std.algebra { FreeMonoid, length }
+import v2.std.anti_unification { ChainGeneralization, anti_unify_chain, fillings_all_leaves }
+import v2.std.logic { Bool }
 
-type DeclId = Symbol
-
-type TypeIdent = Symbol
-
-type VariantShape {
-  field_arity: Nat
-  field_type_idents: List<TypeIdent>
-}
-
-type TypeShape {
-  variant_set: List<VariantShape>
-  total_variants: Nat
-}
-
-type FnShapeUnrealized {}
-
-type StructuralShape
-  = TypeDecl { shape: TypeShape }
-  | FnDecl { shape: FnShapeUnrealized }
-
-type StructuralSimilarityVerdict
-  = Unrealized
-  | Produced { index: Map<DeclId, StructuralShape> }
-
-type StructuralSimilarityFact {
-  verdict: StructuralSimilarityVerdict
-}
-
-data structural_similarity_empty_type_shape: TypeShape = {
-  variant_set: [],
-  total_variants: Zero
+fn forest_collapses_to_generic(g: ChainGeneralization) -> Bool {
+  fillings_all_leaves(per_element: g.per_element)
 }
 
-fn structural_similarity_fact() -> StructuralSimilarityFact {
-  StructuralSimilarityFact {
-    verdict: Unrealized
+fn type_decls_anti_unify(decls: FreeMonoid<Node>) -> Bool {
+  if length(xs: decls) < 2 {
+    false
+  } else {
+    forest_collapses_to_generic(g: anti_unify_chain(steps: decls))
   }
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
   class: WallAfterGrounding {
-    grounding_authority: "the parse/resolve walk producing per-decl TypeShape/VariantShape facts by construction",
-    dissolve_on: "per-decl structural-shape facts are produced by the substrate walk, not by a staged lens producer"
+    grounding_authority: "the parse/resolve walk that projects a module's type declarations into a FreeMonoid<Node> forest (anti-unified by the shared v2.std.anti_unification kernel, also used by v2.lens.simulated_relationship's statement-chain binder)",
+    dissolve_on: "type_decls_anti_unify runs over live dsl type-declaration forests once the parse/resolve walk produces per-module type-decl facts; until then this is a lens_unit predicate over synthetic type-decl forests, consumed as a row of the v2.lens.intent_linearity registry. This is the type-decl twin of v2.lens.simulated_relationship: the same anti_unify_chain engine, a different binder (the leaves that vary across a congruent family of type decls are a type-parameter hole, not a fold's list-element hole), so N near-identical type decls collapse to one generic (Int8..Int128 = one Compose axis). Unlike the term binder a pair suffices (threshold 2, not the fold's 3) and template_has_hole is NOT required, so byte-identical decls (the strongest section-3 nickname, a hole-free template) are also caught: the wall is fillings_all_leaves, i.e. all variance sits at leaf positions that become type parameters."
   },
-  rationale: "Per-decl structural shape is a decidable index; a scaffold producer-stage substrate (unblocking variant-parameter-clone and structural-similarity) until the parse/resolve walk lands."
+  rationale: "Structural anti-unification of type declarations is decidable (a wall): type decls whose only variance is at leaf positions collapse to one generic (the leaves becoming type parameters), and byte-identical decls are the strongest section-3 nickname. The undecidable residue (whether the leaf variance is semantically one type parameter or coincidental) stays a ratchet. One engine (v2.std.anti_unification), two binders (term chain / type forest)."
 }

src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag

@@ -1,6 +1,6 @@
 module v2.test.intent_linearity.lens_unit.discriminators
 
-import v2.lens.intent_linearity { chain_is_redundant, chain_residual, level_is_linear, body_is_linear }
+import v2.lens.intent_linearity { chain_is_redundant, forest_is_redundant, chain_residual, level_is_linear, body_is_linear }
 import v2.std.node {
   Node, Edge, EdgeLabel, Positional,
   NodeKind, TypeNode, Connective, Atom, Conj,
@@ -55,3 +55,14 @@ test fn all_minimal_body_is_linear() -> Bool {
 test fn single_minimal_level_is_linear() -> Bool {
   level_is_linear(level: linear_chain_b)
 }
+
+data dup_type_pair: List<Node> = [
+  conj2(a: atom(id: ^x86), b: atom(id: ^arm)),
+  conj2(a: atom(id: ^x86), b: atom(id: ^arm))
+]
+test fn dup_type_decls_redundant_through_registry() -> Bool {
+  forest_is_redundant(decls: dup_type_pair)
+}
+test fn dup_type_pair_not_flagged_by_term_binder() -> Bool {
+  !chain_is_redundant(steps: dup_type_pair)
+}

src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag

@@ -0,0 +1,65 @@
+module v2.test.structural_similarity.lens_unit.discriminators
+
+import v2.lens.structural_similarity { type_decls_anti_unify }
+import v2.std.node {
+  Node, Edge, Positional,
+  TypeNode, Atom, Conj, Disj,
+  Symbol, node_synthetic
+}
+import v2.std.collection { List }
+import v2.std.logic { Bool }
+
+fn atom(id: Symbol) -> Node {
+  node_synthetic(kind: TypeNode { connective: Atom { identity: id } }, children: [])
+}
+fn disj2(a: Node, b: Node) -> Node {
+  node_synthetic(kind: TypeNode { connective: Disj }, children: [
+    Edge { label: Positional, target: a }, Edge { label: Positional, target: b } ])
+}
+fn compose2(a: Node, b: Node) -> Node {
+  node_synthetic(kind: TypeNode { connective: Conj }, children: [
+    Edge { label: Positional, target: a }, Edge { label: Positional, target: b } ])
+}
+
+data nickname_pair: List<Node> = [
+  disj2(a: atom(id: ^x86), b: atom(id: ^arm)),
+  disj2(a: atom(id: ^x86), b: atom(id: ^arm))
+]
+
+data width_family: List<Node> = [
+  compose2(a: atom(id: ^int), b: atom(id: ^w8)),
+  compose2(a: atom(id: ^int), b: atom(id: ^w16)),
+  compose2(a: atom(id: ^int), b: atom(id: ^w32))
+]
+
+data distinct_decls: List<Node> = [
+  atom(id: ^unit),
+  disj2(a: atom(id: ^a), b: atom(id: ^b)),
+  compose2(a: atom(id: ^int), b: atom(id: ^w8))
+]
+
+data near_but_divergent: List<Node> = [
+  compose2(a: atom(id: ^int), b: atom(id: ^w8)),
+  compose2(a: atom(id: ^int), b: compose2(a: atom(id: ^ptr), b: atom(id: ^w16))),
+  compose2(a: atom(id: ^int), b: atom(id: ^w32))
+]
+
+data single_decl: List<Node> = [
+  disj2(a: atom(id: ^x), b: atom(id: ^y))
+]
+
+test fn nickname_pair_is_similar() -> Bool {
+  type_decls_anti_unify(decls: nickname_pair)
+}
+test fn width_family_is_similar() -> Bool {
+  type_decls_anti_unify(decls: width_family)
+}
+test fn distinct_decls_are_not_similar() -> Bool {
+  !type_decls_anti_unify(decls: distinct_decls)
+}
+test fn divergent_family_is_not_similar() -> Bool {
+  !type_decls_anti_unify(decls: near_but_divergent)
+}
+test fn single_decl_is_not_similar() -> Bool {
+  !type_decls_anti_unify(decls: single_decl)
+}