Conversation
(A, B) types (own per-element domains, trailing @clk default), (a, b) expressions (comma makes the tuple), x.0 via field_access accepting a number, and pattern binders for let and for — the two-identifier `for i, x in` form is replaced by `for (i, x) in` (planning/tuples.md). No new GLR conflicts; corpus extended and green (25/25). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Tuple types lower to ValueKind::Tuple(Vec<Type>) — elements are full types with their own domains. (a, b) lowers to ExprKind::TupleLit; x.0 reuses ExprKind::Field with a numeric name. let/for binders are patterns: a tuple pattern binds a synthetic local plus one projection let per element, recursively — no pattern IR (planning/tuples.md). `for (i, x) in v.enumerate()` keeps the genvar-reuse special shape; a bare binder over .enumerate() is now the ForEnumerateForm diagnostic (fail-expected updated); working examples moved to the new binder form. mirin-fmt learns the tuple nodes and the pattern fields. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Tuples unify element-wise (arity mismatch is its own diagnostic) and SUBSUME element-wise — each element of a tuple at a coercion site is itself at a coercion site, so a const element fits a clocked slot without weakening Vec/struct invariance. Projection p.N indexes the element list, stamping the receiver's domain over Unspecified slots like struct fields; out-of-range is TupleIndexOutOfBounds. Vec(N,A).enumerate() -> Vec(N, (integer, A)) is a real builtin method. Fix exposed by enumerate: `integer` is elaboration-only, so an unannotated integer slot lowers @const from birth instead of being lifted to a pure signature's __Dom (Const-vs-Param mismatch on `-> Vec(3, (integer, uint(8)))`). Mixed-domain tuple test pins the fully-polymorphic case: two clocks in one tuple project back to their own domains, and crossing them is a DomainMismatch. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
flatten_leaves: a tuple flattens like a struct whose field names are element indices (x.0.valid → x__0__valid); port elements fold direction through their own flattening. expr_leaves: TupleLit prefixes element leaves with their index. Projection/registering/destructuring all ride the existing Field suffix-strip machinery — a registered tuple var gets per-leaf always_ff, a tuple result flattens to result__0/result__1, and vec-of-tuples is struct-of-arrays (ps__0[0:2] + ps__1[0:2]). bind_pattern skips the synthetic copy when destructuring an existing local. Drive completeness descends tuples: `r.0 = …` without `r.1` diagnoses "field 1 of r is never driven". Known pre-existing limit (NOT a tuple regression): a RETURNED port's consumer-side fields emit as outputs (so do a returned tuple's port elements) — out-params are the directional path today. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Working examples: tuples (construct/project/destructure), tuple_register (per-leaf always_ff), vec_of_tuples (struct-of-arrays + enumerate + tuple binder), tuple_multi_domain (two clocks in one tuple) — all in CLEAN + VERILATOR_CLEAN. Fail-expected: arity mismatch, .2 out of bounds, undriven element, cross-domain projection add. RTL behavioural tests drive the registered tuple and the vec-of-tuples sum under verilator. type_has_domain now accepts a tuple return type whose elements all carry domains (explicit-mode annotation rule). Docs: for_loops/when_ram/syntax synced to pattern binders and real-method enumerate. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Pin down the integer-domain rule Jon flagged: an UNANNOTATED integer defaults to @const (so enumerate's genvar-shaped index stays const and is not lifted into a pure signature's clock domain), while integer @clk remains a legitimate non-const integer for testbenches. The behaviour already worked after the tuples slice; this refines the rationale comment and adds a regression test pinning both `Vec(3, (integer @const, uint(8) @clk))` (enumerate) and `integer @clk` round-trip. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A function returning a port emitted EVERY result leaf as an output, ignoring the per-leaf drive flag that flatten_leaves already computes via direction folding. So a returned port's consumer-side `in` field (e.g. a Stream's ready) became a module output instead of an input, and drive_result drove it forward (`result__ready = …`) — wrong direction, and the backpressure place was left undriven. Two-line shape of the fix: result-port emission now picks Input/Output from leaf.drives (identical to the param path), and drive_result drives `out` leaves forward but `in` leaves in reverse (`<place> = result__x`), the same split as a record `field => target` binding. Bug was purely in emission + drive; flatten_leaves was already correct. Adds dataflow_stage.mrn — a pipeline register that RETURNS its downstream Stream (registered valid/data, combinational ready backpressure) — in CLEAN + VERILATOR_CLEAN, a cocotb behavioural test, and a backend unit test asserting result__ready is an input. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…te's type Jon's review: defaulting unannotated `integer` to @const was an inconsistent special rule. Reverted — `integer`'s domain follows annotation/data-flow like any type (so a testbench `integer @clk` is legal), and the const-ness of enumerate's index lives in enumerate's own (proper) type: {dom D} (Vec(N,A) @d) -> Vec(N, (integer @const, A @d)) @d. Consequence, now consistent: a PURE function lifts every domain slot onto one __Dom, so it cannot directly RETURN a mixed-domain aggregate (enumerate's @const index vs the lifted-clocked written index; aggregate elements are invariant). The common usages are unaffected — a `for`-loop consumes the index as a genvar, a `let` binding takes enumerate's honest type (lets are not lifted). Pinned by fail-expected/enumerate-pure-return (the ratchet will flag it for promotion when dependency-aware lifting lands — the principled general fix, documented in planning/tuples.md). Tests reworked to real usage (let + projection; integer @clk round-trip). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A domain stored on an aggregate type (Vec/tuple), separate from its element domains and reconciled only lazily on reads, launders clock domains: an @b on a Vec/tuple stamps the element on read but never unifies with incoming @A data on write, so @A exits as @b. Documents the bug, the evidence, and the fix from domain_checking_redux.md — @ is a constraint on a TYPE (integer @d is fine, integer is a type; N @const is a category error, N is a value), aggregates carry no domain of their own (Vec(N, T), Tuple(T, U)), and @d on an aggregate propagates into element leaf slots and unifies. Worklist fixtures (no checker yet, so todo-incorrect-pass / todo, not fail-expected): cdc-launder-vec, cdc-launder-tuple, vec-domain-drift (wrongly accepted → reject after Stage 1/3); mixed-domain-vec-return (wrongly rejected → accept after Stage 2). No compiler code yet — design + worklist only. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…check Stage 1+2 of planning/aggregate_domains.md. Stage 1 (soundness): an explicit @d on a Vec/tuple type is the constraint "every clock slot is D" — stamp_domain propagates it into the element's unspecified domain slots AT LOWERING, exactly as the pure-function lift does for __Dom. The element carries @d from birth, so writing @A data into an @b-stamped aggregate now meets a concrete element domain and conflicts instead of laundering the crossing (unify_domain(@A, Unspecified) was lenient). Closes the Vec and tuple CDC-laundry holes. Stage 2 (completeness): type_has_domain derives "annotated" structurally — a Vec is annotated iff its element is; a tuple iff every element is — so an element-annotated Vec with no redundant outer @d is accepted. Fixtures flipped: cdc-launder-vec/tuple -> fail-expected (now DomainMismatch); new working/vec_elem_domain (element-annotated Vec, no outer @, emits clean, in CLEAN+VERILATOR_CLEAN). vec-domain-drift stays in todo-incorrect-pass — the stamp fills only unspecified slots, so a conflicting EXPLICIT element domain isn't caught until Stage 3 makes the aggregate domain unrepresentable. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Stage 3 of planning/aggregate_domains.md. Move Vec and Tuple out of the domain-carrying Type::Value wrapper into top-level Type::Vec/Type::Tuple variants with NO domain field — a domain now lives only on leaves (and on structs, whose domain stamps their fields). An aggregate's domain is derived: a Vec's is its element's; a tuple's is the per-element set (none singular). Drift between a stored aggregate domain and its elements is now UNREPRESENTABLE rather than kept-consistent-by-hand. Mechanical across the Type matches: super_fold/match_header (types), unify/subsume/merge/freshen/with_domain/field/index/VecLit/TupleLit/ enumerate/replace/range/for (infer), lower_type (sig), completeness (check), flatten_leaves/sv_type/subst_type (backend). Behavior-preserving: 152 workspace + 12 RTL tests green. Fixed a latent gap on the way — the backend subst_type never substituted into tuple element types (no Tuple arm). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The leaf-domain model's last rule: an aggregate @d may only FILL unspecified element slots, never override one. An aggregate @d that meets an element's own explicit clock domain != D — drift (Vec(2, uint(8) @b) @A) or an inert mixed-tuple annotation ((uint(8) @A, uint(8) @b) @c) — is now a ConflictingDomain error rather than a silent no-op. Checked syntactically over signature types, with @const compatible with any clock. Fixtures: vec-domain-drift + new tuple-domain-inert -> fail-expected; the aggregate-domains worklist in todo-incorrect-pass is now fully flipped and empty. 152 workspace + 12 RTL green. Known gap: body-ascription conflicts (a "let v: Vec(.. @b) @A") aren't scanned — only signature types. Noted in planning/aggregate_domains.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.