hax_lib/
proc_macros.rs

1//! This module re-exports macros from `hax-lib-macros` since a
2//! proc-macro crate cannot export anything but procedural macros.
3
4pub use hax_lib_macros::{
5    attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque,
6    opaque_type, refinement_type, requires, trait_fn_decoration, transparent,
7};
8
9pub use hax_lib_macros::{
10    process_init, process_read, process_write, protocol_messages, pv_constructor, pv_handwritten,
11};
12
13macro_rules! export_quoting_proc_macros {
14    ($backend:ident($expr_name:ident, $expr_unsafe_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident $(, {$($extra:tt)+})?)) => {
15        pub use hax_lib_macros::$expr_name as $backend;
16        #[doc(hidden)]
17        pub use hax_lib_macros::$expr_unsafe_name;
18
19        #[doc=concat!("Procedural macros for ", stringify!($backend))]
20        pub mod $backend {
21            pub use hax_lib_macros::$after_name as after;
22            pub use hax_lib_macros::$before_name as before;
23            pub use hax_lib_macros::$replace_name as replace;
24            $($($extra)*)?
25        }
26    };
27
28    ($backend:ident $payload:tt $($others:tt)+) => {
29        export_quoting_proc_macros!($backend$payload);
30        export_quoting_proc_macros!($($others)+);
31    }
32}
33
34export_quoting_proc_macros!(
35    fstar(fstar_expr, fstar_unsafe_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar, {
36        pub use hax_lib_macros::fstar_options as options;
37        pub use hax_lib_macros::fstar_verification_status as verification_status;
38    })
39
40    coq(coq_expr, coq_unsafe_expr, coq_before, coq_after, coq_replace, hax_backend_coq)
41
42    proverif(proverif_expr, proverif_unsafe_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif));
hax_lib/proc_macros.rs

hax_lib/
proc_macros.rs
