Seal unification semantics with differential tests against _unify - #114
Open
MesTTo wants to merge 1 commit into
Open
Seal unification semantics with differential tests against _unify#114MesTTo wants to merge 1 commit into
MesTTo wants to merge 1 commit into
Conversation
Eight targeted behavior tests (first-order MGU materialization, nested MGU from either side, repeated-variable constraints on both sides, indirect occurs cycles, variable-namespace separation, first-order-syntactic-only, symbol shape mismatch reporting) plus a ~900-pair differential against a clean walk/occurs oracle over finite terms, all through the existing engine entry point _unify. The crate had no integration tests for unification; these pin its contract without adding or duplicating any engine code.
MesTTo
changed the title
MesTTo
force-pushed
the
pr/mork-expr-unify-into
branch
from
July 4, 2026 12:45
5a03002 to
149c949
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.
Seals the unification engine's semantics with tests only — no engine code added. Eight behavior tests (first-order MGU materialization from either side, repeated-variable constraints on both sides, indirect occurs cycles, variable-namespace separation, first-order-syntactic-only, symbol shape mismatch) plus a ~900-pair differential against an independent walk/occurs-check oracle over finite terms, all through the existing
Expr::_unifyentry point. The crate previously had no integration tests for unification.Earlier revisions of this branch added
unify_into/apply_bindingswrappers; those duplicated the existing_unify/applybodies, so they are gone — the tests now target the engine's own entry point directly. If un-deprecating_unifyinto a public name is wanted, that is a separate four-line decision.