verdict_parser/common/
vec_deep.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// A wrapper for Vec with its View implemented
7/// one layer deeper than the original Vec
8///
9/// Otherwise inherits all methods from Vec
10#[derive(Debug, Eq, PartialEq)]
11pub struct VecDeep<T>(pub Vec<T>);
12
13impl<T: View> View for VecDeep<T> {
14    type V = Seq<T::V>;
15
16    open spec fn view(&self) -> Self::V {
17        Seq::new(self.0.len() as nat, |i: int| self.0@[i]@)
18    }
19}
20
21/// Cloning VecDeep clones each element
22impl<T: PolyfillClone> PolyfillClone for VecDeep<T> where
23{
24    /// Same as clone of Vec, but this is a "deep" copy
25    fn clone(&self) -> Self {
26        let mut cloned: Vec<T> = Vec::with_capacity(self.len());
27
28        for i in 0..self.0.len()
29            invariant
30                cloned.len() == i,
31                forall |j| 0 <= j < i ==> cloned[j]@ == #[trigger] self.0[j]@,
32        {
33            cloned.push(self.0[i].clone());
34        }
35
36        assert(VecDeep(cloned)@ =~= self@);
37
38        VecDeep(cloned)
39    }
40}
41
42impl<T: View> VecDeep<T> {
43    #[inline(always)]
44    pub fn new() -> (res: Self)
45        ensures
46            res@ =~= Seq::<T::V>::empty(),
47    {
48        VecDeep(Vec::new())
49    }
50
51    #[inline(always)]
52    pub fn with_capacity(cap: usize) -> (res: Self)
53        ensures
54            res@ =~= Seq::<T::V>::empty(),
55    {
56        VecDeep(Vec::with_capacity(cap))
57    }
58
59    #[inline(always)]
60    pub fn push(&mut self, value: T)
61        ensures
62            self@ =~= old(self)@.push(value@)
63    {
64        self.0.push(value);
65    }
66
67    #[inline(always)]
68    pub fn len(&self) -> (res: usize)
69        ensures
70            res == self@.len()
71    {
72        self.0.len()
73    }
74
75    #[inline(always)]
76    pub fn get(&self, i: usize) -> (res: &T)
77        requires
78            i < self@.len(),
79        ensures
80            res@ == self@[i as int],
81    {
82        &self.0[i]
83    }
84
85    #[inline(always)]
86    pub fn remove(&mut self, i: usize) -> (res: T)
87        requires
88            i < old(self)@.len(),
89        ensures
90            res@ =~= old(self)@[i as int],
91            self@ =~= old(self)@.remove(i as int),
92    {
93        self.0.remove(i)
94    }
95
96    #[inline(always)]
97    pub fn append(&mut self, other: &mut VecDeep<T>)
98        ensures
99            self@ =~= old(self)@ + old(other)@,
100            other@ =~= Seq::<T::V>::empty(),
101    {
102        self.0.append(&mut other.0);
103    }
104
105    #[inline(always)]
106    pub fn append_owned(&mut self, mut other: VecDeep<T>)
107        ensures
108            self@ =~= old(self)@ + other@,
109    {
110        self.0.append(&mut other.0);
111    }
112
113    // #[verifier::external_body]
114    // #[inline(always)]
115    // pub fn flatten(v: VecDeep<VecDeep<T>>) -> (res: VecDeep<T>)
116    //     ensures res@ == v@.flatten()
117    // {
118    //     Self::from_vec(v.0.into_iter().map(|u| u.0).flatten().collect())
119    // }
120
121    #[inline(always)]
122    pub fn split_off(&mut self, at: usize) -> (res: VecDeep<T>)
123        requires
124            at <= old(self)@.len(),
125        ensures
126            self@ =~= old(self)@.subrange(0, at as int),
127            res@ =~= old(self)@.subrange(at as int, old(self)@.len() as int),
128    {
129        VecDeep(self.0.split_off(at))
130    }
131
132    #[inline(always)]
133    pub fn from_vec(v: Vec<T>) -> (res: Self)
134        ensures
135            res@ =~= VecDeep(v)@,
136    {
137        VecDeep(v)
138    }
139
140    #[verifier::external_body]
141    #[inline(always)]
142    pub fn from_slice(slice: &[T]) -> (res: Self)
143        where T: Copy
144        ensures
145            res@ =~= slice@.map_values(|x: T| x@),
146    {
147        VecDeep(slice.to_vec())
148    }
149
150    #[inline(always)]
151    pub fn to_vec_owned(self) -> (res: Vec<T>)
152        ensures
153            self@ =~= VecDeep(res)@,
154    {
155        self.0
156    }
157
158    #[inline(always)]
159    pub fn to_vec(&self) -> (res: &Vec<T>)
160        ensures
161            self@ =~= VecDeep(*res)@,
162    {
163        &self.0
164    }
165}
166
167#[allow(unused_macros)]
168#[macro_export]
169macro_rules! vec_deep {
170    ($($x:tt)*) => {
171        VecDeep::from_vec(vec![$($x)*])
172    };
173}
174pub use vec_deep;
175
176}
verdict_parser/common/vec_deep.rs

verdict_parser/common/
vec_deep.rs
