prusto_rs/types/
seq.rs

1use std::cmp::Ord;
2use std::collections::*;
3use std::fmt;
4use std::hash::Hash;
5use std::marker::PhantomData;
6
7use serde::de::{DeserializeSeed, Deserializer, SeqAccess, Visitor};
8
9use super::{Context, Presto, PrestoTy};
10
11macro_rules! gen_seq {
12    ($ty:ident,  $insert:ident, $seed:ident) => {
13        gen_seq! { $ty<>, $insert, $seed }
14    };
15    ($ty:ident < $($bound:ident ),* >,  $insert:ident, $seed:ident) => {
16        impl<T: Presto + $($bound+)*> Presto for $ty<T> {
17            // TODO: use impl trait after https://github.com/rust-lang/rust/issues/63063 stablized.
18            // type ValueType<'a> = impl Serialize + 'a where T: 'a;
19            type ValueType<'a> = Vec<T::ValueType<'a>> where T: 'a;
20            type Seed<'a, 'de> = $seed<'a, T>;
21
22            // fn value(&self) -> Self::ValueType<'_> {
23            //     let iter = self.iter().map(|t| t.value());
24            //
25            //     SerializeIterator {
26            //         iter,
27            //         size: Some(self.len()),
28            //     }
29            // }
30            fn value(&self) -> Self::ValueType<'_> {
31                self.iter().map(|t| t.value()).collect()
32            }
33
34            fn ty() -> PrestoTy {
35                PrestoTy::Array(Box::new(T::ty()))
36            }
37
38            fn seed<'a, 'de>(ctx: &'a Context) -> Self::Seed<'a, 'de> {
39                $seed::new(ctx)
40            }
41
42            fn empty() -> Self {
43                Default::default()
44            }
45        }
46
47        pub struct $seed<'a, T> {
48            ctx: &'a Context<'a>,
49            ty: &'a PrestoTy,
50            _marker: PhantomData<T>,
51        }
52
53        impl<'a, T> $seed<'a, T> {
54            // caller must provide a valid `Context`
55            pub(super) fn new(ctx: &'a Context) -> Self {
56                if let PrestoTy::Array(ty) = ctx.ty {
57                    $seed {
58                        ctx,
59                        ty: &*ty,
60                        _marker: PhantomData,
61                    }
62                } else {
63                    panic!("invalid context")
64                }
65            }
66        }
67
68        impl<'a, 'de, T: Presto + $($bound+)*> Visitor<'de> for $seed<'a, T> {
69            type Value = $ty<T>;
70            fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result {
71                formatter.write_str("sequence of same presto type")
72            }
73            fn visit_seq<A>(self, mut seq: A) -> Result<Self::Value, A::Error>
74            where
75                A: SeqAccess<'de>,
76            {
77                let mut ret: $ty<T> = Default::default();
78                let ctx = self.ctx.with_ty(self.ty);
79                while let Some(d) = seq.next_element_seed(T::seed(&ctx))? {
80                    ret.$insert(d);
81                }
82                Ok(ret)
83            }
84        }
85
86        impl<'a, 'de, T: Presto + $($bound+)*> DeserializeSeed<'de> for $seed<'a, T> {
87            type Value = $ty<T>;
88            fn deserialize<D>(self, deserializer: D) -> Result<Self::Value, D::Error>
89            where
90                D: Deserializer<'de>,
91            {
92                deserializer.deserialize_seq(self)
93            }
94        }
95    };
96}
97
98gen_seq!(Vec, push, VecSeed);
99gen_seq!(LinkedList, push_back, LinkedListSeed);
100gen_seq!(VecDeque, push_back, VecDequeSeed);
101gen_seq!(HashSet<Ord,Hash>, insert, HashSetSeed);
102gen_seq!(BTreeSet<Ord>, insert, BTreeSetSeed);
103gen_seq!(BinaryHeap<Ord>, push, BinaryHeapSeed);
prusto_rs/types/seq.rs

prusto_rs/types/
seq.rs
