Small example of using a proc-macro that we need to expand

for subsequent code to type check
verus-lang · Dec 13, 2024 · 7ee68d9 · 7ee68d9
1 parent 3e43467
commit 7ee68d9
Show file tree

Hide file tree

Showing 4 changed files with 48 additions and 6 deletions.
diff --git a/crates/va-test/examples/storage-macros/Cargo.toml b/crates/va-test/examples/storage-macros/Cargo.toml
@@ -0,0 +1,14 @@
+[package]
+name = "storage-macros"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+proc-macro = true
+
+[dependencies]
+quote = "1"
+proc-macro2 = "1.0"
+syn = "2.0"
+
+[workspace]
diff --git a/crates/va-test/examples/storage-macros/src/lib.rs b/crates/va-test/examples/storage-macros/src/lib.rs
@@ -0,0 +1,17 @@
+use proc_macro::TokenStream;
+use quote::{quote,format_ident};
+use syn::{parse_macro_input, DeriveInput};
+
+#[proc_macro_derive(Hello)]
+pub fn hello_derive(input: TokenStream) -> TokenStream {
+    let input = parse_macro_input!(input as DeriveInput);
+    let name = input.ident;
+    let fn_name = format_ident!("say_hello_{}", name);
+
+    quote!{
+        //#[verifier::external_body]
+        fn #fn_name() {
+            println!("#name says hi");
+        }
+    }.into()
+}
diff --git a/crates/va-test/examples/storage/Cargo.toml b/crates/va-test/examples/storage/Cargo.toml
@@ -3,6 +3,8 @@ name = "verified-storage"
 version = "0.1.0"
 edition = "2021"
 
+[dependencies]
+storage-macros = { path = "../storage-macros" }
+
 [workspace]
 
-[dependencies]
diff --git a/crates/va-test/examples/storage/src/main.rs b/crates/va-test/examples/storage/src/main.rs
@@ -1,9 +1,18 @@
+#![allow(non_snake_case)]
+#![allow(dead_code)]
 //use vstd::prelude::*;
+use storage_macros::Hello;
 
-verus! {
-    pub broadcast group all_the_axioms {
-        axiom_jay_lorch
-    }
+
+//verus! {
+
+#[derive(Hello)]
+struct TestKey {
+    val: u64,
 }
 
-fn main() { }
+//}
+
+fn main() { 
+    say_hello_TestKey();
+}