Skip to content

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

@tahina-pro

Description

@tahina-pro

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!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions