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

Splitting tuple types into separate modules for each #3204

Open
wants to merge 6 commits into
base: master
Choose a base branch
from

Conversation

mtzguido
Copy link
Member

@mtzguido mtzguido commented Feb 6, 2024

Discussed with @nikswamy today: always loading the definitions for all tuples (normal ones up to 14, dependent up to 5) is an unnecessary load on the typechecker and SMT solver.

This PR splits all tuples of arity >=3 into separate modules. The dependency analysis is modified to recognize tuple patterns and types and add the relevant dependencies (it is slightly conservative since it always treats * and & as referring to tuples even if they are overloaded, but over-approximating is not terrible here). I measured a very slight improvement in FStar.ModifiesGen (63s -> 60s). Not sure if other files will have more significant gains, but this anyway looks desirable to me.

It does mean that, in an interactive setting, if you try to use a tuple you have not yet used you will have to reload the module.

In a follow up, I think we should call the constructor for each tuple just Mk, since they are already in different modules. Also, I changed the tuple detection logic into just a table that we look up. This actually removes a few incorrect snippets, and is not too bad to maintain IMO.

@mtzguido
Copy link
Member Author

mtzguido commented Feb 7, 2024

@nikswamy FYI before merging we should fix Pulse and possibly other projects. If they mention, say, Mktuple3 directly now they need to use a qualified name. Pulse will break because of the snapshot too.

@mtzguido
Copy link
Member Author

mtzguido commented Feb 7, 2024

I have a patch for Steel+Pulse ready. HACL* is failing since I think Vale relies on the concrete location of tuples, I'm taking a look.

Maybe we wait until after the fork..?

Meanwhile I added an FStar.AllTuples module one can import to bring all tuple types in scope, for easy upgrading.

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