Skip to content

Migrate PEx expressions to the shared expression-visitor base#952

Merged
ankushdesai merged 1 commit into
claude/shared-expr-visitorfrom
claude/shared-expr-visitor-pex
May 25, 2026
Merged

Migrate PEx expressions to the shared expression-visitor base#952
ankushdesai merged 1 commit into
claude/shared-expr-visitorfrom
claude/shared-expr-visitor-pex

Conversation

@ankushdesai

Copy link
Copy Markdown
Member

Summary

Phase 2 of the shared expression-visitor refactor. Migrates PEx onto ExpressionGenerator<TContext> (introduced in #951).

PExCodeGenerator now extends ExpressionGenerator<CompilationContext>, and its WriteExpr switch is replaced by the 31 Write*Expr overrides, bodies moved verbatim. PEx's NondetExpr/FairNondetExpr previously shared one switch arm; they're now two overrides routed through a small private WriteRandomBool helper so the emitted code is unchanged.

With PChecker (#951) and PEx both on the base, adding a new IPExpr node forces both backends to handle it or fail to compile.

Stacked on #951 — review/merge that first. This PR's base is claude/shared-expr-visitor; GitHub will retarget it to master once #951 merges.

Verification (local, .NET 8)

  • CompilerCore builds clean (only the unrelated pre-existing TransformASTPass.cs:796 CS0162 warning).
  • PEx-generated Java for Tutorials 1–6 is byte-for-byte identical to master (diff -rq clean). EspressoMachine fails PEx codegen identically on both old and new — the pre-existing "receive in a loop body is not supported" limitation (TransformASTPass.cs:793), unrelated to this change.

Note on the old default arm

PEx's previous WriteExpr default emitted a /* Skipping expr ... */ comment; the shared base throws instead. Since all three imperative backends handle the identical 31-node set, that arm was dead for real input — confirmed by the byte-identical tutorial output.

Follow-ups

  • PR3: WriteStmt base + migrate PChecker/PEx statements.
  • PR4: adapt PObserve (signature differs — instance fields vs passed-in writer).

Generated by Claude Code

PExCodeGenerator now extends ExpressionGenerator<CompilationContext>;
its WriteExpr switch is replaced by the 31 Write*Expr overrides (bodies
moved verbatim). PEx's Nondet/FairNondet shared a switch arm, now routed
through a small WriteRandomBool helper to keep the emission identical.

With both PChecker and PEx on the base, adding a new IPExpr node forces
both to handle it at compile time.

Verified: CompilerCore builds clean; PEx-generated Java for tutorials
1-6 is byte-for-byte identical to master (EspressoMachine fails PEx
codegen identically on both, due to the pre-existing 'receive in loop'
limitation, unrelated to this change).
Copilot AI review requested due to automatic review settings May 24, 2026 23:53

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Phase 2 of the shared expression-visitor refactor: migrates PExCodeGenerator onto the ExpressionGenerator<CompilationContext> base introduced in #951, replacing the single WriteExpr switch with 31 per-node Write*Expr overrides whose bodies are moved verbatim.

Changes:

  • PExCodeGenerator now extends ExpressionGenerator<CompilationContext> instead of having its own WriteExpr switch.
  • The previously combined NondetExpr/FairNondetExpr switch arm is split into two overrides that delegate to a new private WriteRandomBool helper, preserving emitted output.
  • The old default arm that emitted /* Skipping expr ... */ is dropped in favor of the base class's throw (dead in practice).

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@ankushdesai ankushdesai merged commit 49195da into claude/shared-expr-visitor May 25, 2026
11 checks passed
@ankushdesai ankushdesai deleted the claude/shared-expr-visitor-pex branch May 25, 2026 01:03
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.

3 participants