feat(hax-lib/macros): add dummy int!

hacspec · Nov 12, 2024 · d37c423 · d37c423
1 parent 1b3ef89
commit d37c423
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 2 deletions.
diff --git a/hax-lib/macros/Cargo.toml b/hax-lib/macros/Cargo.toml
@@ -16,11 +16,11 @@ proc-macro = true
 proc-macro-error = { version = "1.0.4" }
 hax-lib-macros-types = { workspace = true }
 paste = { version = "1.0.15" }
-proc-macro2 = { workspace = true }
 syn = { version = "2.0", features = ["full", "visit-mut", "visit"] }
 
 [dependencies]
 syn = { version = "2.0", features = ["full", "visit-mut"] }
+proc-macro2 = { workspace = true }
 quote = { workspace = true }
 
 [dev-dependencies]

diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs
@@ -1,7 +1,7 @@
 mod hax_paths;
 
 use hax_paths::*;
-use proc_macro::TokenStream;
+use proc_macro::{TokenStream, TokenTree};
 use quote::quote;
 use syn::{visit_mut::VisitMut, *};
 
@@ -137,3 +137,17 @@ pub fn attributes(_attr: TokenStream, item: TokenStream) -> TokenStream {
 
     quote! { #item }.into()
 }
+
+#[proc_macro]
+pub fn int(payload: TokenStream) -> TokenStream {
+    let mut tokens = payload.into_iter().peekable();
+    let negative = matches!(tokens.peek(), Some(TokenTree::Punct(p)) if p.as_char() == '-');
+    if negative {
+        tokens.next();
+    }
+    let [lit @ TokenTree::Literal(_)] = &tokens.collect::<Vec<_>>()[..] else {
+        return quote! { ::std::compile_error!("Expected exactly one numeric literal") }.into();
+    };
+    let lit: proc_macro2::TokenStream = TokenStream::from(lit.clone()).into();
+    quote! {::hax_lib::int::Int(#lit)}.into()
+}