Skip to content

Commit ae537b5

Browse files
maximebuysemaximebuyse
authored
Merge pull request #1394 from cryspen/remove-paste-dependency
Replace `paste` by `with_builtin_macros`.
2 parents 76e2908 + c12ac20 commit ae537b5

File tree

5 files changed

+99
-108
lines changed

5 files changed

+99
-108
lines changed

‎Cargo.lock

Lines changed: 0 additions & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎hax-lib/macros/Cargo.toml

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ proc-macro = true
1515
[target.'cfg(hax)'.dependencies]
1616
proc-macro-error2 = { version = "2.0" }
1717
hax-lib-macros-types = { workspace = true }
18-
paste = { version = "1.0.15" }
1918
syn = { version = "2.0", features = ["full", "visit-mut", "visit"] }
2019

2120
[dependencies]

‎hax-lib/macros/src/implementation.rs

Lines changed: 97 additions & 99 deletions
Original file line numberDiff line numberDiff line change
@@ -782,110 +782,108 @@ macro_rules! make_quoting_item_proc_macro {
782782

783783
macro_rules! make_quoting_proc_macro {
784784
($backend:ident) => {
785-
paste::paste! {
786-
#[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")]
787-
///
788-
789-
/// While it is possible to directly write raw backend code,
790-
/// sometimes it can be inconvenient. For example, referencing
791-
/// Rust names can be a bit cumbersome: for example, the name
792-
/// `my_crate::my_module::CONSTANT` might be translated
793-
/// differently in a backend (e.g. in the F* backend, it will
794-
/// probably be `My_crate.My_module.v_CONSTANT`).
795-
///
796-
797-
/// To facilitate this, you can write Rust names directly,
798-
/// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3`
799-
/// will be replaced with `f My_crate.My_module.v_CONSTANT + 3`
800-
/// in the F* backend for instance.
801-
802-
/// If you want to refer to the Rust constructor
803-
/// `Enum::Variant`, you should write `$$Enum::Variant` (note
804-
/// the double dollar).
805-
806-
/// If the name refers to something polymorphic, you need to
807-
/// signal it by adding _any_ type informations,
808-
/// e.g. `${my_module::function<()>}`. The curly braces are
809-
/// needed for such more complex expressions.
810-
811-
/// You can also write Rust patterns with the `$?{SYNTAX}`
812-
/// syntax, where `SYNTAX` is a Rust pattern. The syntax
813-
/// `${EXPR}` also allows any Rust expressions
814-
/// `EXPR` to be embedded.
815-
816-
/// Types can be refered to with the syntax `$:{TYPE}`.
817-
#[proc_macro]
818-
pub fn [<$backend _expr>](payload: pm::TokenStream) -> pm::TokenStream {
819-
let ts: TokenStream = quote::expression(quote::InlineExprType::Unit, payload).into();
820-
quote!{{
821-
#[cfg([< hax_backend_ $backend >])]
822-
{
823-
#ts
824-
}
825-
}}.into()
826-
}
785+
#[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")]
786+
///
827787
828-
#[doc = concat!("The `Prop` version of `", stringify!($backend), "_expr`.")]
829-
#[proc_macro]
830-
pub fn [<$backend _prop_expr>](payload: pm::TokenStream) -> pm::TokenStream {
831-
let ts: TokenStream = quote::expression(quote::InlineExprType::Prop, payload).into();
832-
quote!{{
833-
#[cfg([< hax_backend_ $backend >])]
834-
{
835-
#ts
836-
}
837-
#[cfg(not([< hax_backend_ $backend >]))]
838-
{
839-
::hax_lib::Prop::from_bool(true)
840-
}
841-
}}.into()
842-
}
788+
/// While it is possible to directly write raw backend code,
789+
/// sometimes it can be inconvenient. For example, referencing
790+
/// Rust names can be a bit cumbersome: for example, the name
791+
/// `my_crate::my_module::CONSTANT` might be translated
792+
/// differently in a backend (e.g. in the F* backend, it will
793+
/// probably be `My_crate.My_module.v_CONSTANT`).
794+
///
843795
844-
#[doc = concat!("The unsafe (because polymorphic: even computationally relevant code can be inlined!) version of `", stringify!($backend), "_expr`.")]
845-
#[proc_macro]
846-
#[doc(hidden)]
847-
pub fn [<$backend _unsafe_expr>](payload: pm::TokenStream) -> pm::TokenStream {
848-
let ts: TokenStream = quote::expression(quote::InlineExprType::Anything, payload).into();
849-
quote!{{
850-
#[cfg([< hax_backend_ $backend >])]
851-
{
852-
#ts
853-
}
854-
}}.into()
855-
}
796+
/// To facilitate this, you can write Rust names directly,
797+
/// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3`
798+
/// will be replaced with `f My_crate.My_module.v_CONSTANT + 3`
799+
/// in the F* backend for instance.
800+
801+
/// If you want to refer to the Rust constructor
802+
/// `Enum::Variant`, you should write `$$Enum::Variant` (note
803+
/// the double dollar).
804+
805+
/// If the name refers to something polymorphic, you need to
806+
/// signal it by adding _any_ type informations,
807+
/// e.g. `${my_module::function<()>}`. The curly braces are
808+
/// needed for such more complex expressions.
809+
810+
/// You can also write Rust patterns with the `$?{SYNTAX}`
811+
/// syntax, where `SYNTAX` is a Rust pattern. The syntax
812+
/// `${EXPR}` also allows any Rust expressions
813+
/// `EXPR` to be embedded.
814+
815+
/// Types can be refered to with the syntax `$:{TYPE}`.
816+
#[proc_macro]
817+
pub fn ${concat($backend, _expr)}(payload: pm::TokenStream) -> pm::TokenStream {
818+
let ts: TokenStream = quote::expression(quote::InlineExprType::Unit, payload).into();
819+
quote!{{
820+
#[cfg(${concat(hax_backend_, $backend)})]
821+
{
822+
#ts
823+
}
824+
}}.into()
825+
}
856826

857-
make_quoting_item_proc_macro!($backend, [< $backend _before >], ItemQuotePosition::Before, [< hax_backend_ $backend >]);
858-
make_quoting_item_proc_macro!($backend, [< $backend _after >], ItemQuotePosition::After, [< hax_backend_ $backend >]);
827+
#[doc = concat!("The `Prop` version of `", stringify!($backend), "_expr`.")]
828+
#[proc_macro]
829+
pub fn ${concat($backend, _prop_expr)}(payload: pm::TokenStream) -> pm::TokenStream {
830+
let ts: TokenStream = quote::expression(quote::InlineExprType::Prop, payload).into();
831+
quote!{{
832+
#[cfg(${concat(hax_backend_, $backend)})]
833+
{
834+
#ts
835+
}
836+
#[cfg(not(${concat(hax_backend_, $backend)}))]
837+
{
838+
::hax_lib::Prop::from_bool(true)
839+
}
840+
}}.into()
841+
}
859842

860-
#[doc = concat!("Replaces a Rust item with some verbatim ", stringify!($backend)," code.")]
861-
#[proc_macro_error]
862-
#[proc_macro_attribute]
863-
pub fn [< $backend _replace >](payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
864-
let item: TokenStream = item.into();
865-
let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
866-
[< $backend _before >](payload, quote!{#attr #item}.into())
867-
}
843+
#[doc = concat!("The unsafe (because polymorphic: even computationally relevant code can be inlined!) version of `", stringify!($backend), "_expr`.")]
844+
#[proc_macro]
845+
#[doc(hidden)]
846+
pub fn ${concat($backend, _unsafe_expr)}(payload: pm::TokenStream) -> pm::TokenStream {
847+
let ts: TokenStream = quote::expression(quote::InlineExprType::Anything, payload).into();
848+
quote!{{
849+
#[cfg(${concat(hax_backend_, $backend)})]
850+
{
851+
#ts
852+
}
853+
}}.into()
854+
}
868855

869-
#[doc = concat!("Replaces the body of a Rust function with some verbatim ", stringify!($backend)," code.")]
870-
#[proc_macro_error]
871-
#[proc_macro_attribute]
872-
pub fn [< $backend _replace_body >](payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
873-
let payload: TokenStream = payload.into();
874-
let item: ItemFn = parse_macro_input!(item);
875-
let mut hax_item = item.clone();
876-
*hax_item.block.as_mut() = parse_quote!{
877-
{
878-
::hax_lib::$backend::unsafe_expr!(#payload)
879-
}
880-
};
881-
quote!{
882-
#[cfg([< hax_backend_ $backend >])]
883-
#hax_item
884-
885-
#[cfg(not([< hax_backend_ $backend >]))]
886-
#item
887-
}.into()
888-
}
856+
make_quoting_item_proc_macro!($backend, ${concat($backend, _before)}, ItemQuotePosition::Before, ${concat(hax_backend_, $backend)});
857+
make_quoting_item_proc_macro!($backend, ${concat($backend, _after)}, ItemQuotePosition::After, ${concat(hax_backend_, $backend)});
858+
859+
#[doc = concat!("Replaces a Rust item with some verbatim ", stringify!($backend)," code.")]
860+
#[proc_macro_error]
861+
#[proc_macro_attribute]
862+
pub fn ${concat($backend, _replace)}(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
863+
let item: TokenStream = item.into();
864+
let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
865+
${concat($backend, _before)}(payload, quote!{#attr #item}.into())
866+
}
867+
868+
#[doc = concat!("Replaces the body of a Rust function with some verbatim ", stringify!($backend)," code.")]
869+
#[proc_macro_error]
870+
#[proc_macro_attribute]
871+
pub fn ${concat($backend, _replace_body)}(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
872+
let payload: TokenStream = payload.into();
873+
let item: ItemFn = parse_macro_input!(item);
874+
let mut hax_item = item.clone();
875+
*hax_item.block.as_mut() = parse_quote!{
876+
{
877+
::hax_lib::$backend::unsafe_expr!(#payload)
878+
}
879+
};
880+
quote!{
881+
#[cfg(${concat(hax_backend_, $backend)})]
882+
#hax_item
883+
884+
#[cfg(not(${concat(hax_backend_, $backend)}))]
885+
#item
886+
}.into()
889887
}
890888
};
891889
($($backend:ident)*) => {

‎hax-lib/macros/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
// Proc-macros must "reside in the root of the crate": whence the use
22
// of `std::include!` instead of proper module declaration.
33

4+
#![feature(macro_metavar_expr_concat)]
5+
46
#[cfg(hax)]
57
std::include!("implementation.rs");
68

‎tests/Cargo.lock

Lines changed: 0 additions & 7 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)