#hax #data #variations #mirroring #allowing #proc-macro #procedural

macro hax-adt-into

Provides the adt_into procedural macro, allowing for mirroring data types with small variations

4 releases

0.1.0 Jan 20, 2025
0.1.0-rc.1 Dec 17, 2024
0.1.0-pre.1 Oct 20, 2023
0.1.0-alpha.1 Oct 7, 2024

#2038 in Procedural macros

Download history 275/week @ 2024-10-07 33/week @ 2024-10-14 4/week @ 2024-10-21 2/week @ 2024-10-28 10/week @ 2024-11-04 13/week @ 2024-11-18 5/week @ 2024-11-25 5/week @ 2024-12-02 34/week @ 2024-12-09 148/week @ 2024-12-16 3/week @ 2025-01-06 1/week @ 2025-01-13 114/week @ 2025-01-20

118 downloads per month
Used in 8 crates (3 directly)

Apache-2.0

20KB
414 lines

hax adt into

This crate provides the adt_into procedural macro, allowing for mirroring data types with small variations.

This crate is used by the frontend of hax, where we need to mirror a big part of the data types defined by the Rust compiler. While the abstract syntax trees (ASTs) from the Rust compiler expose a lot of indirections (identifiers one should lookup, additional informations reachable only via interactive queries), hax exposes the same ASTs, removing indirections and inlining additional informations.

The adt_into derive macro can be used on structs and enums. adt_into then looks for another #[args(<GENERICS>, from: FROM_TYPE, state: STATE_TYPE as SOME_NAME)] attribute. Such an attribute means that the struct or enum mirrors the type FROM_TYPE, and that the transformation is carried along with a state of type STATE_TYPE that will be accessible via the name SOME_NAME.

An example is available in the tests folder.

Dependencies

~2MB
~47K SLoC