Skip to content
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

Reset gensym for predictable names and better query caching #3515

Merged
merged 9 commits into from
Oct 3, 2024

Conversation

nikswamy
Copy link
Collaborator

@nikswamy nikswamy commented Oct 2, 2024

With Guido, we found that this change breaks query caching: 8efd8f6

The reason is that this causes the gensym for the desugaring/typing environment to change across invocations. So, if you write a definition in the IDE, then retract it, and feed it again with say one more line in it at the end, all the internal unique names of the definition are changed.

So, in this PR what I do instead is to reset the gensym before parsing each declaration, and reset it again before desugaring each decl, and reset it again before typechecking each decl. This results in stable unique indexes for Tm_names and results in better caching. It also produces names with smaller indexes, starting at 0.

There is one catch: although the gensym is mainly used to generate unique names when opening binders, it is also used to produce unique names for anonymous top-level definitions

E.g., When a user write

let _ = 0
let _ = 1

The gensym is used to turn this into

let _0 = 0
let _1 = 1

Resetting the gensym conflicts with this. So, when generating unique names for top-level definitions, my branch repeatedly takes names from the gensym until it finds the smallest next name that is not yet used in the top-level environment.

Fwiw, another possibility could have been to use two separate gensyms: one for top-level names that is only reset at module boundaries, and another for local names that is reset at each decl.

@nikswamy
Copy link
Collaborator Author

nikswamy commented Oct 3, 2024

This requires a refreshed snapshot in pulse and new hints in hacl, but otherwise check-world works.

@nikswamy nikswamy merged commit 9a46152 into master Oct 3, 2024
3 checks passed
@nikswamy nikswamy deleted the nik_gensym branch October 3, 2024 04:10
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.

1 participant