karamel icon indicating copy to clipboard operation
karamel copied to clipboard

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

Open tahina-pro opened this issue 10 months ago • 1 comments

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!

tahina-pro avatar Feb 19 '25 04:02 tahina-pro

(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.

msprotz avatar Feb 21 '25 16:02 msprotz