Skip to content

saw-core: Hash ExtCns values by name instead of VarIndex. #2436

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 21, 2025

Conversation

brianhuffman
Copy link
Contributor

This ensures that hashes of identical subterms will be stable across executions, and not depend on the particular VarIndexes that come from the hash-consing tables.

Fixes #2386.

This ensures that hashes of identical subterms will be stable across
executions, and not depend on the particular VarIndexes that come
from the hash-consing tables.

Fixes #2386.
Copy link
Contributor

@RyanGlScott RyanGlScott left a comment

Choose a reason for hiding this comment

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

I can see the appeal behind this, but on the other hand, I'm a bit uncomfortable about the Eq instance using ecVarIndex, but the Hashable instance using ecName. Surely the two ought to agree with each other?

@brianhuffman
Copy link
Contributor Author

Using the VarIndex for comparisons is kind of the whole point of having a VarIndex at all. I ought to add some documentation explaining the global uniqueness invariant, so it's clear why comparing just the VarIndex suffices for the Eq instance. The rationale for the Hashable instance not depending on the VarIndex also belongs in a comment in the code.

@brianhuffman brianhuffman merged commit 48417b6 into master Jun 21, 2025
37 checks passed
@brianhuffman brianhuffman deleted the bh/extcns-hashable branch June 21, 2025 00:28
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.

Inconsistent Hashable definitions between PrimName and ExtCns
2 participants