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

Handle cyclic module dependencies #935

Merged
merged 11 commits into from
Oct 2, 2024
Merged

Conversation

maximebuyse
Copy link
Contributor

Closes #396

The idea is to put together objects that create a cyclic dependency at the module level. We bundle them in a newly created module (one for each cycle) and then use FStarLang/FStar#3369 to selectively include these objects in the module they actually belong to.
List of changes compared to the existing implementation (that was present in dependencies.ml but not used by any backend):

  • we solve name clashes in the bundles (by adding a hash to the names that clash)
  • we replace the let and type keywords by and for mutually recursive items
  • we replace the unfold let by include to make use of Add a new syntax to support partial opens and includes FStarLang/FStar#3369
  • we bundle not only mutually recursive items but also items that create a cyclic dependency without being recursive. This is done by computing the transitive closure of the item dependency graph. Looking for paths of three objects a1 -> b -> a2 such that a1, a2 belong to module A and b belongs to B (with B != A). Adding an edge between these items for each such path in a new graph. After finding all such paths, the bundles are exactly the connected components of this new graph.

Copy link
Collaborator

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

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

As we discussed, we should rename constructors in enumeration when their name are clashing, see https://hax-playground.cryspen.com/#fstar/0559a9e0ba/gist=02128b3051501d2c361787c887a82d26

@maximebuyse
Copy link
Contributor Author

As we discussed, we should rename constructors in enumeration when their name are clashing, see https://hax-playground.cryspen.com/#fstar/0559a9e0ba/gist=02128b3051501d2c361787c887a82d26

As discussed, it is easier (and maybe better as we keep the naming convention) to always rename the variants when we rename the enum. We also need to include the new variants in the module of origin with an alias (to make sure the original name is available).

I implemented that. Note that the import of variants also happens when there is no renaming (not sure if it is good or not).

Copy link
Collaborator

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

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

Thanks, that's great!
Let's merge it! 😃

@W95Psp W95Psp enabled auto-merge October 2, 2024 11:05
@W95Psp W95Psp added this pull request to the merge queue Oct 2, 2024
Merged via the queue into main with commit 9321a24 Oct 2, 2024
13 checks passed
@W95Psp W95Psp deleted the handle-cyclic-module-dependencies branch October 2, 2024 11:43
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.

Add utility function to deal with mutual dependency across different modules
2 participants