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

Rust: support for std::option without monomorphization? (and possibly more) #541

Open
tahina-pro opened this issue Feb 19, 2025 · 1 comment

Comments

@tahina-pro
Copy link
Member

With -fkeep-tuples, Karamel extracts pairs to Rust pairs without monomorphizing their pair type.

Would it be possible to have a similar option for std::option, so that a user could instruct Karamel to extract F* option values to Rust std::option values without monomorphizing their option type?

Alternatively, more generally, could a user give a Karamel option to map an inductive type t to a Rust type u, assuming they have the same data constructors, and to instruct Karamel to not monomorphize such types? (For instance, the user could map FStar.Pervasives.Native.option to std::option, since their data constructors are called None and Some on both sides; but a mapping of FStar.Pervasives.either to either::Either would not work, since their data constructors are named differently in F* and in Rust, and it would be the responsibility of the user to first define a F* data type with the right constructor names; I would be fine with that.)

Thanks in advance!

@msprotz
Copy link
Contributor

msprotz commented Feb 21, 2025

(as discussed privately)

Disabling monomorphization for the Rust backend is a pretty big feature request, since monomorphization happens early on in the pipeline, and I do not know whether the phases that follow can deal with non-monomorphized types and definitions.

It would be nice to have, eventually, so I'm leaving this open.

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

2 participants