Conversation
Merge domain_checking.md + domain_checking_redux.md + aggregate_domains.md into a single focused planning/domain_checking.md: a short overview of what domain checking achieves, then the design as actually implemented — `@` as a constraint resolved by head (leaf slot / nominal stamp / aggregate propagation / opaque obligation), domains-live-on-leaves with aggregates carrying none, the Clock/Domain sorts, the @const-only lattice, pure-signature lifting, elision/defaults, the kinded-term representation, and a terse future-work list. Drops the rejected-design exploration (DomType / higher-kinded) and the staged-fix history. Deletes domain_checking_redux.md and aggregate_domains.md; repoints every reference (code comments, planning docs, example comments) to domain_checking.md. No code behavior change — comment/doc only. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… params Correct the Nominal bullet: a struct/port carries domains through its dom parameters. Elided (no dom param) = one whole-structure domain stamped onto every field; explicit dom params = fields drawn from them, so the type can span several domains (e.g. an AXI port with separate read/write clocks). The @d form fills every clock slot with D (Axi @clk collapses to one clock); supplying params separately keeps them distinct. Implemented for ports; structs are currently elided-only (dom params on a struct are a syntax gap). Cross-refs structs_and_ports.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add logical not / and / or, following the existing operator-trait desugar
(planning/traits.md T5):
- prelude.mrn: Not / And / Or traits + impls for bool (inline-SV !, &&, ||).
- grammar: ! joins unary_expression; || / && join binary_expression with new
logical_or / logical_and precedence levels (below comparison). Regenerated
parser.c with the pinned tree-sitter-cli 0.24.7 (ABI 14 — a newer CLI emits
ABI 15, which the linked 0.25 runtime mis-reads and breaks lexing).
- body.rs: ! -> not, || -> or, && -> and desugar to method calls.
- backend: SvBinOp::{And,Or}; prelude_neg generalised to prelude_unary so !x
emits inline (!x) like -x.
- const_eval: bool not / and / or folding.
- vscode: highlight the new operators (and ==, < for good measure).
- gitignore node_modules (the pinned CLI installs there).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Promote df_example from todo/ to working/ now that the bool operators it needs exist. DF::reg_fwd is a one-deep forward register: load-enable en = !reg_vld || out_rdy, backpressure self.ready = en, valid/data registered, ready passed back combinationally from the returned port's in-leaf. - df_example.mrn: the concrete uint(8) version. Cyclic vars carry explicit types (forward uses can't recover the type from a later equation). - df_example_poly.mrn: payload-polymorphic (port DF(A: Type), parametric impl). A returned generic port needs its type argument spelled out (-> DF(A) @clk), or the result leaves can't recover A's width. - both added to CLEAN + VERILATOR_CLEAN; tests/rtl/test_df_example.py drives the handshake under cocotb. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The unary_expression doc hardcoded text("-"), so the formatter silently
rewrote !x to -x once ! existed (changing the program's meaning). Read the
operator from the node, as the binary path already does. Regression test
covers ! and - round-tripping.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A side-effecting call in tail position (`inp.sink()` with no semicolon) in a unit-returning fn routed to drive_result, which bails when there's no return type — so the call, and the drives it carries (`self.ready = true`), silently vanished from the generated SV. Route the no-result case through the statement-call path (extracted as lower_call_stmt), covering both the tail and `return f();`. Regression test included. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
An inherent impl's subject is now a real type expression, not a bare
constructor: a generic owner must be written applied, with its params declared
in the binder — `impl {dom clk: Clock, A: Type} DF(A)` — exactly like a trait
impl's `for` self type (`impl {param n} Add for uint(n)`). Bare `impl DF` on a
generic owner is a diagnostic (GenericOwnerNotApplied); a non-generic owner
(`impl Sample`) is unchanged. This drops the old auto-binding of an owner's
params into each method.
- grammar: the impl `name` is a `return_type_expression`; the self type is the
`for` type (trait impl) or the subject itself (inherent). Corpus updated +
a new applied-owner case.
- sig.rs: owner = the self type's head; self type lowered uniformly via
`lower_type` (no auto-bind, no `owner_base_type`); the un-applied check.
- def_map: inherent impls now get a header def too, so its signature
diagnostics surface; both the CLI and the example harness print impl-header
(struct/port/impl) sig diagnostics, which were previously dropped.
- examples: migrate impl_parametric_owner + df_example_poly to `Owner(A)`;
fail-expected/impl-generic-owner-bare pins the new error; df_example drops
its now-redundant commented poly block (it lives in df_example_poly).
- docs: planning/syntax.md, planning/traits.md.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add a `return_expression` node so `return` parses as a primary/receiver — the function's result binding — usable as `return.valid` (a postfix field access) and as an assignment LHS (`return.valid = …`). The bare `return EXPR;` statement is unchanged; GLR resolves the shared `return` prefix at the next token (a declared conflict). Regenerated with the pinned 0.24.7 CLI (ABI 14); corpus case added. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`return` is now a referrable place — the function's result binding, a var-like signal node of the return type (the dual of `self`; rustc's MIR `_0`). The body can drive its out-leaves (`return.valid = x`) and read its in-leaves (`return.ready`, a returned port's backpressure), instead of (or alongside) building the whole result in a tail. See planning/return_variable.md. There is no new IR: - body.rs: with a return type, allocate a synthetic `return` local (Var, the return type) in the base scope. `return EXPR;` and the top-block tail desugar to a whole-result equation `return = EXPR`, so a body mixing a tail with `return.f = …` is one equation system. A unit fn keeps its side-effecting tail/return. - infer.rs: seed the result local with the same freshened return type the body is checked against (so a returned value's domain and the result port's domain are one variable); a whole-result drive joins like a return (merge_branch), a per-leaf drive coerces at the leaf (subsume). - check.rs: the result place is a Var — single-assignment + completeness apply (a field-driven struct/scalar result must cover every leaf; a partially field-driven port is exempt, the documented direction-folding gap). Also skip driver checks on inline-verilog bodies (trusted, like completeness). - backend/lower.rs: the result local emits as the `result` ports (base name `result`, not the SV-reserved `return`) and declares no nets of its own; `drive_result` remains for unit fns. - const_eval.rs: a const fn's return value is found at the whole-result equation as well as a bare tail/return. examples/working/return_place.mrn is df_example rewritten in the place style (verilator-clean, identical module); fail-expected/undriven-return-leaf pins the per-leaf completeness error. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add `struct_pattern` (`pair { a = x, b = y }`) and `struct_pattern_field` to
the pattern grammar, alongside `identifier` and `tuple_pattern`. The `name =
binding` form maps a field to a (possibly nested) sub-pattern — `=` matches the
record-literal field form (`:` is always "type"). Available wherever `_pattern`
is (let and for binders), and nests with tuple patterns. Regenerated with the
pinned 0.24.7 CLI; corpus case added.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`let pair { a = x, b = y } = e;` destructures a struct by projecting each field:
`let x = e.a; let y = e.b;` — the same CST→HIR desugaring as tuple patterns
(no pattern IR), reusing `bind_pattern`/`destructure_into` which now dispatch on
both `tuple_pattern` (project by index) and `struct_pattern` (project by field
name). Bindings nest, and a struct pattern composes with tuple patterns either
way. Destructuring an existing local projects straight off it; otherwise a
synthetic `__patN` carries the value.
Only structs and positive tuples are pattern-matchable: a pattern whose
constructor resolves to a port is rejected (PortNotPatternMatchable) — a port's
directional fields don't destructure positively.
- body.rs: dispatch + the port-constructor check (follows the ctor to its owner
type); collect_pattern_names / pattern_children learn struct patterns.
- mirin-fmt: format `struct_pattern`/`struct_pattern_field`, and add the kind to
the tuple-pattern child set (a nested struct pattern was being dropped).
- examples: working/struct_pattern.mrn (flat, nested, struct-in-tuple;
verilator-clean) + fail-expected/port-pattern-rejected.mrn; planning/tuples.md.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add `named_return` (`-> (output: DF @clk)`, `-> (sum: uint(8), carry: bool)`) and `named_result` (`name: T`) to the fn/trait-method return-type choice. A single element names the whole result; two or more name the parts of a tuple result. The `:` distinguishes it from a bare tuple_type return `(A, B)`. Regenerated with the pinned 0.24.7 CLI; corpus case added. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A fn can name its result(s) in the signature — `-> (output: DF @clk)` names the whole result, `-> (sum: T, carry: U)` names the parts of a tuple result. The names become the referrable result places (the `return` keyword doesn't exist then); the SV ports are unchanged — a single named result is the whole `result`, named tuple parts split into `result__0`/`result__1`/…. See planning/return_variable.md. One model via `Signature.result_places`: - sig.rs: `sig_of` always emits a `result_places` list — `[{return, ty, "result"}]` for a normal return, the named place(s) otherwise (a single name → the whole result; ≥2 → `result__i` parts + a `Type::Tuple` return type). Explicit-mode domain checks run per named-result type. - body.rs: a var-like local per result place; `LocalData.result_base` carries its SV base. The unnamed place is named `return`, so the keyword resolves only when unnamed. The whole-result drive (`return EXPR;`/tail/`name = E`) targets the single `sv_base == "result"` place (present for unnamed or single-named; absent for multi-part — drive the parts). - infer / const_eval / backend: key on `result_base` instead of the name `"return"`; a result local is seeded by the normal declared-type path. - mirin-fmt: format `named_return`/`named_result`. - examples: working/named_result.mrn (single named, tail-driven single, tuple parts; verilator-clean) + fail-expected/return-when-named.mrn (`return` is undefined under a named result). planning/return_variable.md, ir_pipeline.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Revises the naming decision: only the unnamed `return` is escaped (to `result`, since `return` is an SV reserved word). A named result/tuple part now surfaces in the generated SystemVerilog under its bound name — `-> (output: DF)` emits `output__valid`/`output__ready`, `-> (sum: uint(8), carry: bool)` emits `sum`/ `carry` — instead of `result`/`result__0`/`result__1`. - sig.rs: a named `ResultPlace.sv_base` is the bound name (was `result` / `result__i`). - backend: the module's own result ports and the connection to a callee's result ports both key on each `result_place.sv_base` (the callee's port names come from its signature), not a hardcoded `result`. - body.rs: the whole-result place is now the *sole* result place (a single named result's base is no longer `result`, so the old `sv_base == "result"` test no longer identifies it). - examples/working/named_result.mrn + planning/return_variable.md updated; a bound name colliding with an SV reserved word is caught by `reserved_words`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Goto-definition on a result place now jumps into the signature (result places have no body declaration span): a named result/tuple part lands on its name in `-> (name: T, …)`, and an unnamed `return` lands on the return type — the closest declaration of the result's shape. Rides the resolved HIR as before (the cursor's `ExprKind::Local` whose `result_base` is set), then reads the return-type node off the CST. See planning/return_variable.md. Also highlight a named result's declared name as `@variable.parameter` (it binds a result place, like a parameter). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Designs the first-pass operator set on the T5 operator-trait foundation: arithmetic (+ - * / %, unary -), bitwise (& | ^ ~), shift (<< >>), and comparison (== \!= < <= > >=). Per-type: uint/sint get all four; bits gets bitwise + shift + its existing Eq (no arithmetic, no ordering — a representation is not a number); integer gets arithmetic + comparison at const-eval time. Settled decisions: shift count is `integer` (widthless, so `x << 2` needs no annotation; dynamic shift by any uint is the additive `Unsigned`-marker follow-up); div/mod included as Div/Rem (signed for sint, const-eval via checked_div/checked_rem); full comparison method set for direct SV operators; bitwise traits kept distinct from the bool logicals. Staging O1–O4. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The four comparisons missing since T5 join `==`/`<`: grammar accepts them at the single non-associative comparison level; body lowering desugars `\!=`→ne, `<=`→le, `>`→gt, `>=`→ge; the prelude `Eq`/`Ord` traits gain `ne` and `le`/`gt`/`ge` with one-line inline-verilog impls for uint/sint/bits(ne)/ bool(ne)/integer; the backend emits each as its direct SV operator (`a >= b`, not `\!(a < b)`) — `prelude_op` now keys on the resolved method name since `Ord` backs four operators; const_eval folds all six on `integer`. Tests: corpus entry (full comparison set), body-desugar unit test over all six, working/comparison_ops.mrn (runtime, verilator-clean — signed compare for sint) and working/comparison_const.mrn (all four new ops fold in a width position), fail-expected/bits-no-ordering.mrn (bits has Eq but no Ord). 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.