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

engine: ast: rework the item Use #1034

Open
W95Psp opened this issue Oct 24, 2024 · 0 comments
Open

engine: ast: rework the item Use #1034

W95Psp opened this issue Oct 24, 2024 · 0 comments

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented Oct 24, 2024

Currently, we export in the AST an item Use.
In Rust, [pub[(visibility)]] use some::path is twofold:

  1. it allows to bring something in scope, possibly under a new name, e.g. use some::path as name or use some::path::*
  2. it allows a module to re-export names

Importantly, rustc resolves names very early: when we observe the THIR, such renamings are all gone. Thus, when a module module has a pub use some::path::to::foo as bar, we will never see any reference to module::bar: instead we will see some::path::to::foo.

In consequence, the (2) is not something we are concerned by: we never want to re-export names that were re-exported in Rust by a use item.

However, in the backends, we may be interested in (1): it may be useful to have --as hints-- that the Rust developer wanted to open a scope or to rename an item. We can use this information locally to improve the quality of the code we generate.
Note that this is purely cosmetic: we can always use the full paths, which is what we do in the current F* printer, but that may change.

Next steps

We discussed with @cmester0 and @maximebuyse about this (while discussing #1030).

In (1), use items are not items properly speaking, just module-wise hints. More precisely, we don't want to give such use hints any name.
Thus, I think we should introduce a notion of module in the engine (maybe as shallow items), and carry a list of use hints there.
This way the backends can pick up this information. We anyway need a place to store comments and attributes on modules, so this design looks good to me.

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

No branches or pull requests

1 participant