refactor(hax-lib): generate redundant code with build.rs, polish ex…

…ports

hax-lib/build.rs

@@ -0,0 +1,50 @@
+use std::env;
+use std::fs;
+use std::path::Path;
+
+const FSTAR_EXTRA: &str = r"
+pub use hax_lib_macros::fstar_options as options;
+pub use hax_lib_macros::fstar_verification_status as verification_status;
+";
+
+fn main() {
+    let code = |backend: &str, extra: &str| {
+        format!(
+            r#"
+pub use hax_lib_macros::{backend}_expr as {backend};
+#[doc(hidden)]
+pub use hax_lib_macros::{backend}_unsafe_expr;
+#[doc(hidden)]
+pub use hax_lib_macros::{backend}_prop_expr;
+
+/// Procedular macros that have an effect only for the backend {backend}.
+pub mod {backend} {{
+    #[doc(hidden)]
+    pub use hax_lib_macros::{backend}_unsafe_expr as unsafe_expr;
+    pub use hax_lib_macros::{backend}_prop_expr as prop;
+    pub use hax_lib_macros::{backend}_after as after;
+    pub use hax_lib_macros::{backend}_before as before;
+    pub use hax_lib_macros::{backend}_replace as replace;
+    pub use hax_lib_macros::{backend}_replace_body as replace_body;
+
+    {extra}
+}}
+"#
+        )
+    };
+
+    let out_dir = env::var_os("OUT_DIR").unwrap();
+    let dest_path = Path::new(&out_dir).join("proc_macros_generated.rs");
+    fs::write(
+        &dest_path,
+        [
+            code("fstar", FSTAR_EXTRA),
+            code("proverif", ""),
+            code("coq", ""),
+        ]
+        .join("\n"),
+    )
+    .unwrap();
+
+    println!("cargo::rerun-if-changed=build.rs");
+}

hax-lib/macros/src/implementation.rs

@@ -875,14 +875,14 @@ macro_rules! make_quoting_proc_macro {
                 let mut hax_item = item.clone();
                 *hax_item.block.as_mut() = parse_quote!{
                     {
-                        ::hax_lib::[< $backend _unsafe_expr >](#payload)
+                        ::hax_lib::$backend::unsafe_expr!(#payload)
                     }
                 };
                 quote!{
-                    #[cfg(hax)]
+                    #[cfg([< hax_backend_ $backend >])]
                     #hax_item
 
-                    #[cfg(not(hax))]
+                    #[cfg(not([< hax_backend_ $backend >]))]
                     #item
                 }.into()
             }

hax-lib/macros/src/utils.rs

@@ -6,9 +6,9 @@ pub struct HaxQuantifiers;
 impl ToTokens for HaxQuantifiers {
     fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
         quote! {
-            use ::hax_lib::fstar_unsafe_expr as fstar;
-            use ::hax_lib::coq_unsafe_expr as coq;
-            use ::hax_lib::proverif_unsafe_expr as proverif;
+            use ::hax_lib::fstar::prop as fstar;
+            use ::hax_lib::coq::prop as coq;
+            use ::hax_lib::proverif::prop as proverif;
         }
         .to_tokens(tokens)
     }

hax-lib/src/proc_macros.rs

@@ -10,34 +10,4 @@ pub use hax_lib_macros::{
     process_init, process_read, process_write, protocol_messages, pv_constructor, pv_handwritten,
 };
 
-macro_rules! export_quoting_proc_macros {
-    ($backend:ident($expr_name:ident, $expr_unsafe_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $replace_body_name:ident, $cfg_name:ident $(, {$($extra:tt)+})?)) => {
-        pub use hax_lib_macros::$expr_name as $backend;
-        #[doc(hidden)]
-        pub use hax_lib_macros::$expr_unsafe_name;
-
-        #[doc=concat!("Procedural macros for ", stringify!($backend))]
-        pub mod $backend {
-            pub use hax_lib_macros::$after_name as after;
-            pub use hax_lib_macros::$before_name as before;
-            pub use hax_lib_macros::$replace_name as replace;
-            pub use hax_lib_macros::$replace_body_name as replace_body;
-            $($($extra)*)?
-        }
-    };
-
-    ($backend:ident $payload:tt $($others:tt)+) => {
-        export_quoting_proc_macros!($backend$payload);
-        export_quoting_proc_macros!($($others)+);
-    }
-}
-
-export_quoting_proc_macros!(
-    fstar(fstar_expr, fstar_unsafe_expr, fstar_before, fstar_after, fstar_replace, fstar_replace_body, hax_backend_fstar, {
-        pub use hax_lib_macros::fstar_options as options;
-        pub use hax_lib_macros::fstar_verification_status as verification_status;
-    })
-
-    coq(coq_expr, coq_unsafe_expr, coq_before, coq_after, coq_replace, coq_replace_body, hax_backend_coq)
-
-    proverif(proverif_expr, proverif_unsafe_expr, proverif_before, proverif_after, proverif_replace, proverif_replace_body, hax_backend_proverif));
+include!(concat!(env!("OUT_DIR"), "/proc_macros_generated.rs"));