vest_lib/
macros.rs

1//! Utility macros.
2#[doc(hidden)]
3#[macro_export]
4macro_rules! __vest_build_tuple_ty {
5    ($ty:ty) => { $ty };
6    ($ty:ty, $($rest:ty),+) => { ($ty, $crate::__vest_build_tuple_ty!($($rest),+)) };
7}
8
9#[doc(hidden)]
10#[macro_export]
11macro_rules! __vest_build_tuple_pat {
12    ($id:ident) => { $id };
13    ($id:ident, $($rest:ident),+) => { ($id, $crate::__vest_build_tuple_pat!($($rest),+)) };
14}
15
16#[doc(hidden)]
17#[macro_export]
18macro_rules! __vest_build_tuple_expr {
19    ($i:expr, $id:ident) => { $i.$id };
20    ($i:expr, $id:ident, $($rest:ident),+) => { ($i.$id, $crate::__vest_build_tuple_expr!($i, $($rest),+)) };
21}
22
23#[doc(hidden)]
24#[macro_export]
25macro_rules! __vest_build_sum_ty {
26    ($ty:ty) => { $ty };
27    ($ty1:ty, $ty2:ty) => { $crate::combinators::Sum<$ty1, $ty2> };
28    ($ty:ty, $($rest:ty),+) => { $crate::combinators::Sum<$ty, $crate::__vest_build_sum_ty!($($rest),+)> };
29}
30
31#[doc(hidden)]
32#[macro_export]
33macro_rules! __vest_build_sum_map {
34    ($i:expr, $spec_name:ident, $variant:ident) => {
35        $spec_name::$variant($i)
36    };
37    ($i:expr, $spec_name:ident, $variant:ident, $($rest:ident),+) => {
38        match $i {
39            $crate::combinators::Sum::Inl(v) => $spec_name::$variant(v),
40            $crate::combinators::Sum::Inr(rest) => $crate::__vest_build_sum_map!(rest, $spec_name, $($rest),+),
41        }
42    };
43}
44
45#[doc(hidden)]
46#[macro_export]
47macro_rules! __vest_build_sum_map_rev {
48    ($i:expr, $spec_name:ident, $variant:ident) => {
49        match $i {
50            $spec_name::$variant(v) => v,
51            _ => ::vstd::prelude::arbitrary(),
52        }
53    };
54    ($i:expr, $spec_name:ident, $variant:ident, $($rest:ident),+) => {
55        match $i {
56            $spec_name::$variant(v) => $crate::combinators::Sum::Inl(v),
57            _ => $crate::combinators::Sum::Inr($crate::__vest_build_sum_map_rev!($i, $spec_name, $($rest),+)),
58        }
59    };
60}
61
62/// Defines paired executable/spec nominal value types and corresponding `DeepView` and `SpecMapper` impls.
63///
64/// The generated `DeepView` and `SpecMapper` implementations assume the exec and spec fields or
65/// variants are aligned by name and order.
66#[macro_export]
67macro_rules! with_deep_view {
68    (
69        $(#[$exec_attr:meta])*
70        pub struct $exec_name:ident <$lt:lifetime> {
71            $(pub $exec_field:ident: $exec_ty:ty,)*
72        }
73
74        $(#[$spec_attr:meta])*
75        pub struct $spec_name:ident {
76            $(pub $spec_field:ident: $spec_ty:ty,)*
77        }
78
79        type $inner_name:ident;
80    ) => {
81        verus! {
82            $(#[$exec_attr])*
83            pub struct $exec_name<$lt> {
84                $(pub $exec_field: $exec_ty,)*
85            }
86
87            $(#[$spec_attr])*
88            pub struct $spec_name {
89                $(pub $spec_field: $spec_ty,)*
90            }
91
92            type $inner_name = $crate::__vest_build_tuple_ty!($($spec_ty),*);
93
94            impl<$lt> ::vstd::prelude::DeepView for $exec_name<$lt> {
95                type V = $spec_name;
96
97                open spec fn deep_view(&self) -> Self::V {
98                    $spec_name {
99                        $($exec_field: self.$exec_field.deep_view(),)*
100                    }
101                }
102            }
103        }
104    };
105    (
106        $(#[$exec_attr:meta])*
107        pub enum $exec_name:ident <$lt:lifetime> {
108            $($exec_variant:ident($exec_ty:ty),)*
109        }
110
111        $(#[$spec_attr:meta])*
112        pub enum $spec_name:ident {
113            $($spec_variant:ident($spec_ty:ty),)*
114        }
115
116        type $inner_name:ident;
117    ) => {
118        verus! {
119            $(#[$exec_attr])*
120            pub enum $exec_name<$lt> {
121                $($exec_variant($exec_ty),)*
122            }
123
124            $(#[$spec_attr])*
125            pub enum $spec_name {
126                $($spec_variant($spec_ty),)*
127            }
128
129            type $inner_name = $crate::__vest_build_sum_ty!($($spec_ty),*);
130
131            impl<$lt> ::vstd::prelude::DeepView for $exec_name<$lt> {
132                type V = $spec_name;
133
134                open spec fn deep_view(&self) -> Self::V {
135                    match self {
136                        $($exec_name::$exec_variant(v) => $spec_name::$spec_variant(v.deep_view()),)*
137                    }
138                }
139            }
140        }
141    };
142}
143
144/// Defines paired executable/spec nominal value types and corresponding `DeepView` and `SpecMapper` impls.
145///
146/// The generated `DeepView` and `SpecMapper` implementations assume the exec and spec fields or
147/// variants are aligned by name and order.
148#[macro_export]
149macro_rules! with_deep_view_and_mapper {
150    (
151        $(#[$exec_attr:meta])*
152        pub struct $exec_name:ident <$lt:lifetime> {
153            $(pub $exec_field:ident: $exec_ty:ty,)*
154        }
155
156        $(#[$spec_attr:meta])*
157        pub struct $spec_name:ident {
158            $(pub $spec_field:ident: $spec_ty:ty,)*
159        }
160
161        type $inner_name:ident;
162        pub struct $mapper_name:ident;
163    ) => {
164        verus! {
165            $(#[$exec_attr])*
166            pub struct $exec_name<$lt> {
167                $(pub $exec_field: $exec_ty,)*
168            }
169
170            $(#[$spec_attr])*
171            pub struct $spec_name {
172                $(pub $spec_field: $spec_ty,)*
173            }
174
175            impl<$lt> ::vstd::prelude::DeepView for $exec_name<$lt> {
176                type V = $spec_name;
177
178                open spec fn deep_view(&self) -> Self::V {
179                    $spec_name {
180                        $($exec_field: self.$exec_field.deep_view(),)*
181                    }
182                }
183            }
184
185            type $inner_name = $crate::__vest_build_tuple_ty!($($spec_ty),*);
186            pub struct $mapper_name;
187
188            impl $crate::combinators::mapped::spec::SpecMapper for $mapper_name {
189                type In = $inner_name;
190                type Out = $spec_name;
191
192                open spec fn spec_map(&self, i: Self::In) -> Self::Out {
193                    let $crate::__vest_build_tuple_pat!($($spec_field),*) = i;
194                    $spec_name {
195                        $($spec_field,)*
196                    }
197                }
198
199                open spec fn spec_map_rev(&self, i: Self::Out) -> Self::In {
200                    $crate::__vest_build_tuple_expr!(i, $($spec_field),*)
201                }
202            }
203        }
204    };
205    (
206        $(#[$exec_attr:meta])*
207        pub enum $exec_name:ident <$lt:lifetime> {
208            $($exec_variant:ident($exec_ty:ty),)*
209        }
210
211        $(#[$spec_attr:meta])*
212        pub enum $spec_name:ident {
213            $($spec_variant:ident($spec_ty:ty),)*
214        }
215
216        type $inner_name:ident;
217        pub struct $mapper_name:ident;
218    ) => {
219        verus! {
220            $(#[$exec_attr])*
221            pub enum $exec_name<$lt> {
222                $($exec_variant($exec_ty),)*
223            }
224
225            $(#[$spec_attr])*
226            pub enum $spec_name {
227                $($spec_variant($spec_ty),)*
228            }
229
230            impl<$lt> ::vstd::prelude::DeepView for $exec_name<$lt> {
231                type V = $spec_name;
232
233                open spec fn deep_view(&self) -> Self::V {
234                    match self {
235                        $($exec_name::$exec_variant(v) => $spec_name::$spec_variant(v.deep_view()),)*
236                    }
237                }
238            }
239
240            type $inner_name = $crate::__vest_build_sum_ty!($($spec_ty),*);
241            pub struct $mapper_name;
242
243            impl $crate::combinators::mapped::spec::SpecMapper for $mapper_name {
244                type In = $inner_name;
245                type Out = $spec_name;
246
247                open spec fn spec_map(&self, i: Self::In) -> Self::Out {
248                    $crate::__vest_build_sum_map!(i, $spec_name, $($spec_variant),*)
249                }
250
251                open spec fn spec_map_rev(&self, i: Self::Out) -> Self::In {
252                    $crate::__vest_build_sum_map_rev!(i, $spec_name, $($spec_variant),*)
253                }
254            }
255        }
256    };
257}
258
259use vstd::prelude::*;
260
261pub use crate::with_deep_view;
262pub use crate::with_deep_view_and_mapper;
vest_lib/macros.rs

vest_lib/
macros.rs
