Remove constructors from merge functions#796
Open
saulshanabrook wants to merge 4 commits into
Open
Conversation
oflatt
requested changes
Jun 22, 2026
oflatt
left a comment
Member
There was a problem hiding this comment.
small comments from our discussion last time
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
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.
This removes constructor-producing encodings from merge functions so merge results are eager values selected from the existing inputs, which is needed for proof mode and for avoiding merge-driven e-node growth.
Stack
PR against Oliver's
oflatt-latest-egglogbranch.This now depends on:
egraphs-good/egglog, branchcodex/pr927-plus-pr930-eggcc-proof(9b5ce111), which merges container PR #927 with PR #930 and the proof-mode command-macro type-info fix.19ed866).The Cargo manifest points at the experimental PR branch, and
Cargo.lockpins that branch plus the combined egglog branch.What changed
TermAndCostis now aPair Term i64.ExtractedExprusespair-min-by-second-i64, which returns one of the existing pair values directly.Boundis nowMaybe (Either i64 bool).maybe-either-i64-bool-maxandmaybe-either-i64-bool-min.IntB,BoolB,Dead,bound-int, andbound-boolwere removed; eggcc now spells the generic container representation directly.IVTResis nowPair IVTPayload i64, with merges usingpair-min-by-second-i64.pair-firstandpair-secondinstead of matching on pair-shaped LHS terms.--run-mode egglogemits the generated egglog program for direct use with the experimental CLI.Validation
Passed locally:
Current composed-stack validation:
The full 2mm pass-1 export is checked into egglog-experimental PR #56 as
tests/fixtures/eggcc-2mm-pass1-merge-old.egg; it contains no:no-mergeand runs successfully in proof mode with the release CLI. The default experimental test suite keeps the full-export canary ignored because debug-profile proof execution was too slow for CI.Performance
Earlier local 2mm export runs for the constructor encoding vs eager encoding showed the eager encoding faster (about 13% on that run). I did not rerun the 5x benchmark after replacing eggcc-specific aliases with direct generic container forms.