You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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!
The text was updated successfully, but these errors were encountered:
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.
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 Ruststd::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 typeu
, assuming they have the same data constructors, and to instruct Karamel to not monomorphize such types? (For instance, the user could mapFStar.Pervasives.Native.option
tostd::option
, since their data constructors are calledNone
andSome
on both sides; but a mapping ofFStar.Pervasives.either
toeither::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!
The text was updated successfully, but these errors were encountered: