Skip to content

Unification laws test#49

Merged
ClarkeRemy merged 2 commits intomainfrom
unification_test_laws
Apr 19, 2026
Merged

Unification laws test#49
ClarkeRemy merged 2 commits intomainfrom
unification_test_laws

Conversation

@ClarkeRemy
Copy link
Copy Markdown
Collaborator

@ClarkeRemy ClarkeRemy commented Apr 16, 2026

This branch adds a large test for unification, putting Prolog and MORK head to head to check MORK unification correctness.

With a check for cycles added, they agree on the results.

The test is done by running main in experiments/unification_test_laws.

A little bit of the complexity comes from the fact that, to have the test finish in a reasonable amount of time, they run fully in parallel; the Rust and Prolog code. On my machine it takes about 10 minutes per language to finish unifying. I've done my best to avoid over-optimizing however, as this isn't meant to be a benchmark.

This uses SWI Prolog, so one needs to install SWI Prolog to run the test.

…k head to head to check mork unification correctness.

With a check for cycles added, they agree on the results.
@Adam-Vandervorst
Copy link
Copy Markdown
Collaborator

Looks good except the unifiable change; ExprZipper should be seen as deprecated: the unifiable test should instead inline the unify method but use the coroutine version of apply with an Io::sink.

@ClarkeRemy
Copy link
Copy Markdown
Collaborator Author

I made the change in the unification test, I get the same results. Which is good.

I push the change, but I do feel that doing this inlining reveals that this pattern of inlining is done in a lot of parts of the code.
How many code paths will need to be changed to check if there were cycles that weren't before? I see 11 other calls for apply_e.

I think this pull request can stop here, and we can address the occurs check on the cycles btreemaps at those 11 call sites in another pull request.

@ClarkeRemy ClarkeRemy merged commit 4cef6f7 into main Apr 19, 2026
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.

2 participants