feat(laurel): add C-style compound assignment (+= -= *= /= %= ^=)#1383
Open
fabiomadge wants to merge 1 commit into
Open
feat(laurel): add C-style compound assignment (+= -= *= /= %= ^=)#1383fabiomadge wants to merge 1 commit into
fabiomadge wants to merge 1 commit into
Conversation
fabiomadge
force-pushed
the
feat/laurel-field-access-fixes
branch
from
2b9f28f to
175269c
Compare
fabiomadge
force-pushed
the
feat/laurel-compound-assign
branch
from
4ea74a9 to
235fc1f
Compare
fabiomadge
force-pushed
the
feat/laurel-field-access-fixes
branch
3 times, most recently
from
4eb1238 to
dea6bcc
Compare
fabiomadge
changed the base branch from
feat/laurel-field-access-fixes
to
reviewed-kbd-will-merge-to-main
fabiomadge
force-pushed
the
feat/laurel-compound-assign
branch
2 times, most recently
from
5826b2c to
83bb675
Compare
fabiomadge
force-pushed
the
feat/laurel-compound-assign
branch
4 times, most recently
from
a3d94ff to
9b93f9f
Compare
fabiomadge
changed the title
Compound assignment is the general case of which `++`/`--` is the degenerate `x op= 1` form. `x op= e` lowers to `x := x op e` and yields the new value, usable as a statement (`x += 2;`) or in expression position (`int y := (x += 2)`). * AST: new `StmtExpr.CompoundAssign (op : Operation) (target) (rhs)` ctor. The `op` is invariably one of Add/Sub/Mul/Div/Mod/StrConcat (enforced by the concrete-to-abstract translator); downstream sites treat any other as a bug. * Grammar: `+= -= *= /= %= ^=` at prec(10), rightassoc. Mixed `:=`/`op=` chaining is unsupported paren-free, matching `:=`'s existing behavior (plain `x := y := z` also does not parse); `a += b += c` groups right. * Lowering: `EliminateIncrDecr.lowerToAssign` is generalized to `lowerOpAssign` (arbitrary `Operation` + RHS), shared with the `++`/`--` path (rhs = 1). The `.PrimitiveOp` keeps `skipProof := false`, so `/=`/`%=` carry the same division-by-zero proof obligation as a hand-written `x := x / e`. Runs first in the pipeline, so no later pass observes `.CompoundAssign`. * Type checking is construct-keyed, by design: `++`/`--` reject `real` (the synthesized int `1` cannot type-check against a real under strict numeric typing), but `+= -= *= /=` accept `real` because the RHS is user-written; `%=` is int-only (`.Mod` has no real lowering); `^=` is string-only. The shared `compoundAssignAccepts` predicate drives both the resolution-time target check and the model-based RHS-type check (`compoundAssignRhsErrors`, run in the post-resolution validation phase). The RHS check is suppressed when the target type is already invalid, so one mistake yields one error. * All exhaustive `StmtExpr` matches updated (MapStmtExpr traverses the rhs even for Local/Declare targets, FilterPrelude, computeExprType, both grammar translators, the Core-translator defensive arm, the lift `contains*` helpers, resolution `collectStmtExpr` and the diamond-field walker). Tests: * T24_CompoundAssign: each operator on int; real for `+= -= *= /=`; string for `^=`; constrained-int (`nat`); expression position; nested side-effecting RHS; right-associative `a += b += c`. * T24b_CompoundAssignField: field target `c#n += e` and chained `o#inner#count += e`, both statement and expression position. * CompoundAssignTypeRejectionTest: per-operator target rejections; RHS-type mismatches; the intended `r += 1.0` accepts / `r++` rejects asymmetry; and a `/= 0` verification failure pinning `skipProof := false`. * CompoundAssignLiftTest: golden lowering for statement, expression, and nested-RHS forms.
fabiomadge
force-pushed
the
feat/laurel-compound-assign
branch
from
9b93f9f to
a735fbd
Compare
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.
Adds C-style compound assignment to the Laurel dialect (
+=-=*=/=%=, plus^=for string concatenation — Laurel's^, not bitwise XOR).x op= elowers tox := x op e, yields the new value, and is usable both as a statement and in expression position. It generalizes the++/--machinery from #1320 — compound assignment is the general case of which++/--is the degeneratex op= 1form.AST. A new
StmtExpr.CompoundAssign (op) (target) (rhs)constructor, distinct from.IncrDecr(which carries a mode and no RHS).Grammar. The six operators are added at prec 10 with
rightassoc, soa += b += cgroups right. Mixed:=/op=chaining is asymmetric:x := y += zdoes not parse (matching plainx := y := z), whilex += y := zdoes — use parentheses to be explicit.Lowering.
lowerToAssignis generalized to take an arbitrary operator and RHS, shared with the++/--path. The lowered.PrimitiveOpkeepsskipProof := false, so/=and%=carry the same division-by-zero obligation as a hand-writtenx := x / e. It runs first in the pipeline, so no later pass observes.CompoundAssign.Resolution / type checking. Resolution is handled by a new
Synth.compoundAssignrule in the bidirectionalSynth/Checkframework, modelled onSynth.incrDecr/Synth.assign: it resolves the target, checks the target's element type against the operator viacheckCompoundAssignTargetType, then checks the RHS against the target type withCheck.resolveStmtExpr(so a mismatched RHS is reported by the standardexpected 'T', got 'U'rule — no bespoke RHS pass needed).The target-type check is construct-keyed by design:
++/--rejectreal(their synthesized int1cannot type-check against a real under Laurel's strict numeric typing, which has no int→real coercion), but+= -= *= /=acceptrealbecause the RHS is user-written;%=is int-only (.Modhas no real lowering);^=is string-only.Tests.
T24_CompoundAssign— end-to-end verification: every operator on int;realfor+= -= *= /=;stringfor^=; constrained-int (nat); integer truncation (7 /= 2,7 %= 3); expression-position yielded value for+=and non-+=(-=,^=); right-associativea += b += c; and the same on composite-field and chained-field (o#inner#count) targets, including real/string//=on fields.CompoundAssignTypeRejectionTest— per-operator target rejections (^=on int,+=on string/bv/float64,%=on real); RHS-type mismatches (expected 'T', got 'U'); a real-based constrained type rejected by%=(constraint peels toreal); ther += 1.0-accepts /r++-rejects asymmetry; and/= 0/%= 0division-by-zero verification failures.CompoundAssignLiftTest— golden (#guard_msgs) lowering for statement, expression, and one-level nested-RHS forms.Full
lake buildandlake testpass.