Skip to content

dslx: support semantic-sum types, values, and type information - #4777

Open
dank-openai wants to merge 1 commit into
google:mainfrom
xlsynth:dank/upstream/semantic-sum-values
Open

dslx: support semantic-sum types, values, and type information#4777
dank-openai wants to merge 1 commit into
google:mainfrom
xlsynth:dank/upstream/semantic-sum-values

Conversation

@dank-openai

@dank-openai dank-openai commented Aug 14, 2026

Copy link
Copy Markdown
Collaborator

Summary

  • Represent DSLX semantic sums as nominal, fully typed unit, tuple, and struct constructors in source declaration order.
  • Construct, validate, format, and round-trip interpreter values through one canonical sum encoding, including nested, enum, token, and proc payloads.
  • Serialize sum type information using only its source declaration and concrete payload types, while preserving existing non-sum formats.
  • Provide source-discriminant-aware zero values, constructor-aware type mismatch diagnostics, and explicit boundaries for unsupported formatting and IR lowering.

Why This Change

Parsed semantic-sum declarations need a concrete nominal type before DSLX support code can reason about constructor identity, payload shape, value layout, zero values, diagnostics, and serialized type information. Those consumers must agree on constructor order without independently reconstructing storage offsets or duplicating source-owned declaration metadata.

For example, consider a parsed declaration whose concrete types and source discriminants are available:

enum Message : u2 {
  Request(u8) = 1,
  Idle(u16) = 0,
}

MakeZeroValue selects Idle(u16:0) because Idle has source discriminant zero. Its interpreter representation is (u1:1, (u8:0, u16:0)): storage tag 1 identifies the second declared constructor, the u8 slot is an inactive canonical placeholder, and the u16 slot contains the active zero payload. The source discriminant and dense storage tag are distinct even when their numerical values happen to coincide elsewhere.

Type And Value Representation

SumType owns the nominal source definition and its declaration-ordered SumTypeVariant values. Shape-specific variant factories preserve the distinction between unit, tuple, and struct constructors, including empty payloads. Type equality, cloning, bit sizing, enum/token detection, visitor dispatch, and type-mismatch traversal use that same typed representation.

Phase1SumTypeEncoding derives the internal dense tag and flattened payload layout from the canonical type. Value construction, raw xls::Value restoration, sign conversion, active-payload validation, inactive placeholders, and formatting descriptors all consume that shared layout. Nested construction and restoration avoid repeated recursive validation. Invalid tags, malformed aggregates, mismatched payload types, incorrect enum identity or signedness, and noncanonical inactive payloads fail with explicit statuses.

MakeZeroValue selects the first constructor for implicit discriminants or the constructor whose explicit source discriminant is zero, then recursively zeroes its active payload. Sums without a valid zero constructor are rejected; zero-length arrays do not require an inhabitant of their element type. MakeAllOnesValue rejects semantic sums.

Direct interpreter formatting and type-mismatch diagnostics preserve constructor names, declaration order, nested payloads, struct field names, and the distinct spellings of unit, empty-tuple, and empty-struct constructors. Format macros reject sums, including sums nested inside aggregates, during type validation. IR type lowering likewise reports that semantic sums are unsupported rather than exposing an accidental representation contract.

Serialized Type Information

The source AST owns constructor names, declaration order, payload shape, struct field names, and visibility. Serialized type information stores only the source span and concrete member types that cannot be recovered from the declaration:

message SumTypeVariantProto {
  repeated TypeProto payload_members = 1;
}

message SumTypeProto {
  optional SpanProto sum_def_span = 1;
  repeated SumTypeVariantProto variants = 2;
}

TypeProto.sum_type uses field number 13. Although sum_def_span uses protobuf's optional syntax, it is required by the reader. Decoding resolves the source declaration and rejects missing spans, constructor-count mismatches, incorrect declaration-ordered payload counts, meta-type payloads, and concrete payload types that disagree with available type information.

No deployed serialized semantic-sum values impose an existing sum-wire compatibility contract. Existing non-sum TypeInfoProto encodings, optional legacy enum-member data, and published AST-node-kind values remain compatible.

Source-level constructor typechecking, pattern execution, full constructor evaluation, and IR lowering remain separate implementation work. Explicit source discriminants participate in zero selection when their evaluated values are available; they are not used as storage tags.

Validation

bazel test \
  //xls/dslx:interp_value_test \
  //xls/dslx:interp_value_utils_test \
  //xls/dslx:sum_type_encoding_test \
  //xls/dslx/type_system:type_zero_value_test \
  //xls/dslx/type_system:type_info_to_proto_test \
  //xls/dslx/type_system:deduce_utils_test \
  //xls/dslx/diagnostics:format_type_mismatch_test \
  --test_output=errors

Coverage includes deeply nested sums; active and inactive enum, token, proc, and uninhabited payloads; signed-enum restoration; canonical storage offsets; the production type-to-descriptor-to-value formatting path; nested mismatch diagnostics; explicit non-first zero-discriminant constructors; empty arrays; malformed raw values; source-backed binary protobuf round trips for unit, tuple, and struct constructors; malformed serialized metadata; and existing enum wire behavior.

@dank-openai
dank-openai force-pushed the dank/upstream/semantic-sum-values branch from 256e5e9 to 1a7dcc5 Compare August 14, 2026 15:25
@richmckeever
richmckeever self-requested a review August 14, 2026 15:27
Adds Phase 1 semantic sum value representation and encoding support, including diagnostics and tests for sum type mismatch formatting.
@dank-openai
dank-openai force-pushed the dank/upstream/semantic-sum-values branch from 1a7dcc5 to 5f64862 Compare August 17, 2026 18:21
@dank-openai
dank-openai marked this pull request as ready for review August 17, 2026 18:59
@dank-openai dank-openai changed the title dslx: represent and encode semantic sum values dslx: support semantic-sum types, values, and type information Aug 17, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant